proposition: Lemma commuting_cube_construction_eq {f f' : arrow C} {aa : CoproductObject (morcls_lp_dom_coprod CC J f) --> CoproductObject (morcls_lp_dom_coprod CC J f')} {bb : CoproductObject (morcls_lp_cod_coprod CC J f) --> CoproductObject (morcls_lp_cod_coprod CC J f')} {cc : arrow_dom f --> arrow_dom f'} {aa' : CoproductObject (morcls_lp_dom_coprod CC J f) --> CoproductObject (morcls_lp_dom_coprod CC J f')} {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')) (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')) : bb = bb' -> cc = cc' -> commuting_cube_construction leftface topface = commuting_cube_construction leftface' topface'.
proof: Proof. intros Hb Hc. use PushoutArrowUnique. - etrans. apply PushoutArrow_PushoutIn1. apply cancel_postcomposition. exact Hb. - etrans. apply PushoutArrow_PushoutIn2. apply cancel_postcomposition. exact Hc. 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