proposition: Lemma MorphismsIntoPullbackEqual {a b c d : C} {f : b --> a} {g : c --> a} {p1 : d --> b} {p2 : d --> c} {H : p1 · f = p2 · g} (P : isPullback f g p1 p2 H) {e} (w w': e --> d) (H1 : w · p1 = w' · p1) (H2 : w · p2 = w' · p2) : w = w'.
proof: Proof. assert (Hw : w · p1 · f = w · p2 · g). { rewrite <- assoc , H, assoc; apply idpath. } assert (Hw' : w' · p1 · f = w' · p2 · g). { rewrite <- assoc , H, assoc; apply idpath. } set (Pb := make_Pullback _ _ _ _ _ _ P). set (Xw := PullbackArrow Pb e (w·p1) (w·p2) Hw). intermediate_path Xw; [ apply PullbackArrowUnique; apply idpath |]. apply pathsinv0. apply PullbackArrowUnique. apply pathsinv0. apply H1. apply pathsinv0. apply H2. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.TransportMorphisms UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Monics