proposition: Lemma ColimFf_axioms (v0 : vertex g) : section_disp_axioms (ColimFf_data v0).
proof: Proof. split. - intro a. use subtypePath; [intro; apply isapropdirprod; apply homset_property|]. apply pathsinv0, colim_endo_is_identity; intro u. etrans. use (colimOfArrowsIn _ _ (CCFf_pt_ob1 a)). etrans. apply cancel_postcomposition. apply maponpaths. exact (section_disp_id (dob d u) _). apply id_left. - intros a b c fab fbc. use subtypePath; [intro; apply isapropdirprod; apply homset_property|]. apply pathsinv0. etrans. apply precompWithColimOfArrows. apply pathsinv0, colimArrowUnique. intro u. etrans. apply colimOfArrowsIn. apply pathsinv0. etrans. apply assoc. apply cancel_postcomposition. etrans. apply pr1_section_disp_on_morphisms_comp. reflexivity. 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