proposition: Lemma ccμ_cod_preservation_mor (a : arrow C) : arrow_cod (colim (ccμ a)) --> three_ob1 (fact_functor (colim Finf) (fact_L (colim Finf) a)).
proof: Proof. use colimOfArrows. - intro v. set (vinFinf := colimIn Finf v). set (LvinFinf := three_mor_mor01 (section_nat_trans vinFinf a)). set (dobvLvinFinf := #(fact_functor (pr1 (dob d v))) LvinFinf). exact (three_mor11 dobvLvinFinf). - abstract ( intros u v e; etrans; [apply assoc'|]; set (morcolim := three_mor_mor01 (section_nat_trans (colim_nat_trans_in_data CC dbase H (v0 := v0) (v := v)) a)); set (dmorenat := (section_nt_disp_axioms_from_section_nt_disp (dmor dbase e)) _ _ morcolim); etrans; [apply cancel_precomposition; exact (pathsinv0 (base_paths _ _ dmorenat))|]; etrans; [apply cancel_precomposition; apply pr1_transportf_const|]; etrans; [apply assoc|]; apply cancel_postcomposition; etrans; [apply pr1_section_disp_on_morphisms_comp|]; use section_disp_on_eq_morphisms; [apply id_left|]; apply (colimInCommutes (CCFf_pt_ob1 CC dbase a)) ). 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