proposition: Lemma MorphismsOutofPushoutEqual {a b c d : C} {f : a --> b} {g : a --> c} {in1 : b --> d} {in2 : c --> d} {H : f · in1 = g · in2} (P : isPushout f g in1 in2 H) {e} (w w': d --> e) (H1 : in1 · w = in1 · w') (H2 : in2 · w = in2 · w') : w = w'.
proof: Proof. assert (Hw : f · in1 · w = g · in2 · w). { rewrite H. apply idpath. } assert (Hw' : f · in1 · w' = g · in2 · w'). { rewrite H. apply idpath. } set (Pb := make_Pushout _ _ _ _ _ _ P). rewrite <- assoc in Hw. rewrite <- assoc in Hw. set (Xw := PushoutArrow Pb e (in1 · w) (in2 · w) Hw). intermediate_path Xw; [ apply PushoutArrowUnique; apply idpath |]. apply pathsinv0. apply PushoutArrowUnique. apply pathsinv0. apply H1. apply pathsinv0. apply H2. 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