proposition: Lemma ColimLNWFS_unique {L: total_category (LNWFS C)} (cc : cocone d L) : ∃! x : ColimLNWFS --> L, ∏ v, ColimLNWFS_in v · x = coconeIn cc v.
proof: Proof. set (Ff_unique := ColimFf_unique (v0 := v0) CC _ H _ (project_cocone _ cc)). use unique_exists. - exists (pr1 (iscontrpr1 Ff_unique)). exact (ColimLNWFS_disp_cc_mor cc). - abstract ( intro v; apply subtypePath; [intro; apply isaprop_lnwfs_mor_axioms|]; apply (pr2 (iscontrpr1 Ff_unique)) ). - abstract ( intro y; apply impred; intro; apply homset_property ). - abstract ( intros y ccy; destruct y as [Fy Ly]; use total2_paths2_f; [|apply isaprop_lnwfs_mor_axioms]; set (Ff_uniqueness := λ t, base_paths _ _ (iscontr_uniqueness Ff_unique t)); use (Ff_uniqueness (Fy,, _)); intro v; exact (base_paths _ _ (ccy v)) ). 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