proposition: Lemma presentable_lp_colimK_mor_coconeInCommutes {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))) : presentable_lp_colimK_mor isclCC (pr1 S,, pr2 S · coconeIn cc v) HS = morcls_lp_coprod_in S · colimIn (arrow_colims CC _ (mapdiagram K d)) v.
proof: Proof. set (Sin := (pr1 S,, pr2 S · coconeIn cc v) : morcls_lp J cl). unfold presentable_lp_colimK_mor. set (Sinarr := presentable_lp_homSet_colim_arrow isclCC Sin HS). set (rel := (Colimits.eqr _ (homSet_diagram (pr1 (morcls_lp_map Sin)) d))). set (X := presentable_lp_homSet_colim_arrow_of_factored_arrow isclCC S HS : Sinarr = setquotpr rel (v,, pr2 S)). rewrite X. etrans. exact ( setquotunivcomm rel _ (presentable_lp_homSet_colim_colimK_fun d Sin) (presentable_lp_homSet_colim_colimK_fun_iscomprel d Sin HS) (v,, pr2 S) ). unfold presentable_lp_homSet_colim_colimK_fun. use arrow_mor_eq; 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