proposition: Lemma ColimFf_unique {v0 : vertex g} (F : Ff C) (cc : cocone d F) : ∃! x : ColimFf v0 --> F, ∏ v, colim_nat_trans_in_data · x = coconeIn cc v.
proof: Proof. use unique_exists. - exact (ColimFf_unique_mor v0 F cc). - abstract ( intro v; functorial_factorization_mor_eq a; etrans; [use pr1_transportf_const|]; etrans; [apply (colimArrowCommutes (CCFf_pt_ob1 a))|]; reflexivity ). - abstract ( intro; apply impred; intro; apply homset_property ). - abstract ( intros f t; functorial_factorization_mor_eq a; apply colimArrowUnique; intro u; set (tax := eq_section_nat_trans_disp_on_morphism (t u) a); apply pathsinv0; etrans; [exact (pathsinv0 (base_paths _ _ tax))|]; etrans; [use pr1_transportf_const|]; reflexivity ). Defined.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.Monads.MonadAlgebras UniMath.CategoryTheory.Monads.Comonads UniMath.CategoryTheory.Monads.ComonadCoalgebras UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.Combinatorics.StandardFiniteSets UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Coequalizers UniMath.CategoryTheory.Chains.Chains UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.DisplayedCats.Examples.Arrow UniMath.CategoryTheory.DisplayedCats.Examples.Three UniMath.ModelCategories.NWFS UniMath.ModelCategories.Helpers UniMath.ModelCategories.Generated.LNWFSHelpers UniMath.ModelCategories.Generated.FFMonoidalStructure