proposition: Lemma presentable_lp_colimK_mor_colimArrowCommutes {d : chain (arrow C)} {cl : arrow C} {cc : cocone d cl} (isclCC : isColimCocone d cl cc) (S : morcls_lp J cl) (HS : presentable (pr1 (morcls_lp_map S))) : presentable_lp_colimK_mor isclCC S HS · colimArrow (arrow_colims CC _ (mapdiagram K d)) _ (mapcocone K d cc) = morcls_lp_coprod_in S.
proof: Proof. unfold presentable_lp_colimK_mor. set (g := (morcls_lp_map S)). transparent assert (pred : (predicate_type d cl (pr1 g))). { intro S'. use make_hProp. - exact ( presentable_lp_colimK_mor isclCC (g,, S') HS · colimArrow (arrow_colims CC _ (mapdiagram K d)) _ (mapcocone K d cc) = morcls_lp_coprod_in (g,, S') ). - apply homset_property. } use (presentable_lp_colimK_mor_univ isclCC S HS pred). intros u Su. set (Su' := (pr1 S,, Su) : morcls_lp J (dob d u)). unfold pred. simpl. etrans. apply maponpaths_2. exact (presentable_lp_colimK_mor_coconeInCommutes isclCC Su' HS). use subtypePath; [intro; apply homset_property|]. apply pathsdirprod. - etrans. apply assoc'. etrans. apply cancel_precomposition. apply (colimArrowCommutes (CC _ (project_diagram00 (mapdiagram K d)))). etrans. apply (CoproductOfArrowsInclusionIn _ (morcls_lp_dom_coprod CC J (dob d u)) _ _ Su'). apply id_left. - etrans. apply assoc'. etrans. apply cancel_precomposition. apply (colimArrowCommutes (CC _ (project_diagram11 (mapdiagram K d)))). etrans. apply (CoproductOfArrowsInclusionIn _ (morcls_lp_cod_coprod CC J (dob d u)) _ _ Su'). apply id_left. 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