proposition: Lemma L1_colim_L1_map_ispushoutOut_subproof {g : graph} {d : diagram g (arrow C)} {f : arrow C} {ccf : cocone d f} (HK : preserves_colimit K _ _ ccf) (isclCC : isColimCocone d f ccf) : arrow_mor00 (K_L1_colim_mor f) · (L1_colim_L1_map00 isclCC) = arrow_mor00 (Kcolim_colimL1_mor HK isclCC).
proof: Proof. use CoproductArrow_eq. intro S. etrans. apply assoc. etrans. apply cancel_postcomposition. apply (CoproductInCommutes (morcls_lp_dom_coprod CC J f)). etrans. apply cancel_precomposition. apply id_left. apply (post_comp_with_z_iso_is_inj (z_iso_inv (colim_dom_L1_dom_iso isclCC))). etrans. apply assoc'. etrans. apply cancel_precomposition. exact (pr122 (colim_dom_L1_dom_iso isclCC)). etrans. apply id_right. apply pathsinv0. etrans. apply assoc'. etrans. apply cancel_precomposition. exact (L1_colim_L1_map_ispushoutOut_subproof0 HK isclCC). etrans. apply (CoproductInCommutes (morcls_lp_dom_coprod CC J f)). 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