proposition: Lemma presentable_lp_homSet_colim_arrow_of_factored_arrow {d : chain (arrow C)} {cl : arrow C} {cc : cocone d cl} (isclCC : isColimCocone d cl cc) {v : vertex nat_graph} (S : morcls_lp J (dob d v)) (HS : presentable (pr1 (morcls_lp_map S))) : let Sin := (pr1 S,, pr2 S · coconeIn cc v) : morcls_lp J cl in presentable_lp_homSet_colim_arrow isclCC Sin HS = setquotpr (Colimits.eqr _ (homSet_diagram (pr1 (morcls_lp_map Sin)) d)) (v,, pr2 S).
proof: Proof. intro Sin. set (homset_ccbase_isCC := HS _ _ _ (pr2 (arrow_colims CC _ d))). set (homset_ccbase_CC := make_ColimCocone _ _ _ homset_ccbase_isCC). set (homset_iso := isColim_is_z_iso _ (ColimsHSET _ (homSet_diagram (pr1 (morcls_lp_map S)) d)) _ _ homset_ccbase_isCC). set (carrcomm := colimArrowCommutes (homset_ccbase_CC) _ (colimCocone (ColimsHSET _ (homSet_diagram (pr1 (morcls_lp_map S)) d))) v). use (pathscomp1 (funeq carrcomm (pr2 S))); [|reflexivity]. etrans. use (funeq _ (pr2 S)). 2: { use (colimArrowCommutes (homset_ccbase_CC)). } unfold presentable_lp_homSet_colim_arrow. set (iso := isColim_is_z_iso _ (ColimsHSET nat_graph (homSet_diagram (pr1 (morcls_lp_map Sin)) d)) _ _ (HS d (pr11 (arrow_colims CC nat_graph d)) (pr21 (arrow_colims CC nat_graph d)) (pr2 (arrow_colims CC nat_graph d)))). set (ziso := (_,, iso) : z_iso _ _). set (iso_rel := pr122 ziso). assert (X : pr2 (morcls_lp_colim_lp_to_morcls_base_colim_lp isclCC Sin) = pr1 ziso (coconeIn (colimCocone (ColimsHSET nat_graph (homSet_diagram (pr1 (morcls_lp_map S)) d))) v (pr2 S))). { etrans. apply assoc'. etrans. apply cancel_precomposition. apply (colimArrowCommutes (make_ColimCocone _ _ _ isclCC)). apply pathsinv0. etrans. apply assoc'. use arrow_mor_eq; apply id_left. } rewrite X. apply pathsinv0. etrans. use (funeq iso_rel). reflexivity. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.Graphs.Coequalizers UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Chains.Chains UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Colimits UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.Monads.Comonads UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Examples.Arrow UniMath.CategoryTheory.DisplayedCats.Examples.Three UniMath.ModelCategories.MorphismClass UniMath.ModelCategories.NWFS UniMath.ModelCategories.Generated.LiftingWithClass UniMath.ModelCategories.Generated.OneStepMonad UniMath.ModelCategories.Helpers