proposition: Lemma isPushout_mor_paths {a b c d : C} {f1 f2 : a --> b} {g1 g2 : a --> c} {in11 in21 : b --> d} {in12 in22 : c --> d} (e1 : f1 = f2) (e2 : g1 = g2) (e3 : in11 = in21) (e4 : in12 = in22) (H1 : f1 · in11 = g1 · in12) (H2 : f2 · in21 = g2 · in22) (iPo : isPushout f1 g1 in11 in12 H1) : isPushout f2 g2 in21 in22 H2.
proof: Proof. induction e1, e2, e3, e4. assert (e5 : H1 = H2) by apply C. induction e5. exact iPo. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.TransportMorphisms UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Core.Functors