proposition: Lemma colim_K_L1_mor_commutes {g : graph} (d : diagram g (arrow C)) {u v : vertex g} (e : edge u v) : dmor (mapdiagram K d) e · colim_K_L1_mor_pointwise d v = colim_K_L1_mor_pointwise d u · dmor (mapdiagram (fact_L F1) d) e.
proof: Proof. use arrow_mor_eq. - etrans. apply (precompWithCoproductArrowInclusion). use CoproductArrow_eq. intro S. etrans. apply (CoproductInCommutes (morcls_lp_dom_coprod CC J (dob d u))). etrans. apply id_left. apply pathsinv0. etrans. apply assoc. etrans. apply cancel_postcomposition. apply (CoproductInCommutes (morcls_lp_dom_coprod CC J (dob d u))). reflexivity. - use CoproductArrow_eq. intro S. etrans. apply assoc. etrans. apply cancel_postcomposition. apply (CoproductOfArrowsInclusionIn _ (morcls_lp_cod_coprod CC J (dob d u))). apply pathsinv0. etrans. apply cancel_precomposition. apply (PushoutArrow_PushoutIn1). etrans. apply assoc. etrans. apply cancel_postcomposition. apply (CoproductOfArrowsInclusionIn _ (morcls_lp_cod_coprod CC J (dob d u))). 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