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. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Monics. Definition UnivProductFromPullback (c d a : C) (f : a --> c) (g : a --> d): exists (UnivProductFromPullback c d a f g). Definition BinProductsFromPullbacks : BinProducts C := BinProduct_Pullback.