proposition: Lemma one_step_comonad_ρ1_compat {f f' : arrow C} (γ : f --> f') : arrow_mor11 (#(one_step_comonad_functor) γ)%cat · ρ1 CC J f' = ρ1 CC J f · arrow_mor11 γ.
proof: Proof. use (MorphismsOutofPushoutEqual (isPushout_Pushout (morcls_lp_coprod_diagram_pushout CC J f))). - etrans. apply assoc. etrans. apply cancel_postcomposition. use PushoutArrow_PushoutIn1. etrans. apply assoc'. etrans. apply cancel_precomposition. use PushoutArrow_PushoutIn1. etrans. apply precompWithCoproductArrowInclusion. apply pathsinv0. etrans. apply assoc. etrans. apply cancel_postcomposition. apply PushoutArrow_PushoutIn1. etrans. apply postcompWithCoproductArrow. apply maponpaths. apply funextsec. intro. apply pathsinv0. apply id_left. - etrans. apply assoc. etrans. apply cancel_postcomposition. use PushoutArrow_PushoutIn2. etrans. apply assoc'. etrans. apply cancel_precomposition. use PushoutArrow_PushoutIn2. apply pathsinv0. etrans. apply assoc. etrans. apply cancel_postcomposition. apply PushoutArrow_PushoutIn2. apply pathsinv0. exact (arrow_mor_comm γ). Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.Monads.MonadAlgebras UniMath.CategoryTheory.Monads.Comonads UniMath.CategoryTheory.Monads.ComonadCoalgebras UniMath.CategoryTheory.catiso UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.SIP UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.NaturalTransformations UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Examples.Opposite UniMath.CategoryTheory.DisplayedCats.Examples.Arrow UniMath.CategoryTheory.DisplayedCats.Examples.Three UniMath.ModelCategories.MorphismClass UniMath.ModelCategories.Retract UniMath.ModelCategories.Lifting UniMath.ModelCategories.NWFS UniMath.ModelCategories.NWFSisWFS UniMath.ModelCategories.Generated.LiftingWithClass UniMath.CategoryTheory.DisplayedCats.Examples.MonadAlgebras