proposition: Lemma commuting_cube_construction {f f' : arrow C} {aa : CoproductObject (morcls_lp_dom_coprod CC J _) --> CoproductObject (morcls_lp_dom_coprod CC J _)} {bb : CoproductObject (morcls_lp_cod_coprod CC J f) --> CoproductObject (morcls_lp_cod_coprod CC J f')} {cc : arrow_dom f --> arrow_dom f'} (leftface : (morcls_coprod_functor f) · bb = aa · (morcls_coprod_functor f')) (topface : arrow_mor00 (morcls_lp_coprod_diagram CC J f) · cc = aa · arrow_mor00 (morcls_lp_coprod_diagram CC J f')) : E1 CC J f --> E1 CC J f'.
proof: Proof. set (CE1f' := cc · (λ1 CC J f')). set (BE1f' := bb · (PushoutIn1 (morcls_lp_coprod_diagram_pushout CC J f'))). use (PushoutArrow (morcls_lp_coprod_diagram_pushout CC J f) _ BE1f' CE1f'). abstract ( etrans; [apply assoc|]; etrans; [apply cancel_postcomposition; exact leftface|]; etrans; [apply assoc'|]; apply pathsinv0; etrans; [apply assoc|]; etrans; [apply cancel_postcomposition; exact topface|]; etrans; [apply assoc'|]; apply cancel_precomposition; apply pathsinv0; exact (PushoutSqrCommutes (morcls_lp_coprod_diagram_pushout CC J f')) ). Defined.
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