proposition: Lemma ColimLNWFS_disp_cc_mor {L: total_category (LNWFS C)} (cc : cocone d L) : ColimLNWFS_disp -->[ColimFf_unique_mor CC dbase v0 (pr1 L) (project_cocone _ cc)] (pr2 L).
proof: Proof. split; intro f. - apply subtypePath; [intro; apply homset_property|]. apply pathsdirprod. * etrans. apply id_left. apply pathsinv0. etrans. apply assoc'. etrans. apply assoc'. etrans. apply id_left. etrans. apply id_left. etrans. apply id_left. apply pathsinv0. apply (lnwfs_Σ_top_map_id (pr2 L)). * use colimArrowUnique'. intro v. etrans. apply assoc. etrans. apply cancel_postcomposition. apply (colimArrowCommutes). apply pathsinv0. etrans. apply assoc. etrans. apply cancel_postcomposition. apply assoc. etrans. do 2 apply cancel_postcomposition. etrans. apply assoc. apply cancel_postcomposition. apply colimOfArrowsIn. etrans. apply assoc'. etrans. apply assoc4. etrans. apply cancel_postcomposition, cancel_precomposition. apply colimArrowCommutes. etrans. apply cancel_postcomposition, assoc. etrans. apply assoc'. etrans. apply cancel_precomposition. { etrans. apply assoc. etrans. apply cancel_postcomposition. apply colimOfArrowsIn. etrans. apply assoc'. apply cancel_precomposition. apply colimArrowCommutes. } apply pathsinv0. etrans. exact (pr2 (pathsdirprodweq (base_paths _ _ (pr12 (coconeIn cc v) f)))). etrans. apply assoc'. apply pathsinv0. etrans. apply assoc'. apply cancel_precomposition. etrans. apply assoc. apply cancel_postcomposition. etrans. apply (pr1_section_disp_on_morphisms_comp). apply section_disp_on_eq_morphisms. + apply id_left. + apply (colimArrowCommutes (CCFf_pt_ob1 CC dbase f)). - apply subtypePath; [intro; apply homset_property|]. apply pathsdirprod; [apply id_left|]. use colimArrowUnique. intro v. etrans. apply assoc. etrans. apply cancel_postcomposition. apply colimArrowCommutes. exact (pr2 (pathsdirprodweq (base_paths _ _ (pr22 (coconeIn cc v) f)))). Qed.
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