Lemma equiv_isPullback_2 {a b c d : C} (f : C ⟦b, a⟧) (g : C ⟦c, a⟧) (p1 : C⟦d,b⟧) (p2 : C⟦d,c⟧) (H : p1 · f = p2· g) : Limits.Pullbacks.isPullback H <- isPullback f g p1 p2 H. Proof. intro X. set (XR := make_Pullback _ _ _ _ _ _ X). intros R k h HH. use tpair. - use tpair. use (PullbackArrow XR); try assumption. split. + apply (PullbackArrow_PullbackPr1 XR). + apply (PullbackArrow_PullbackPr2 XR). - abstract ( intro t; apply subtypePath; [ intro; apply isapropdirprod; apply C |] ; induction t as [x Hx]; simpl in * ; use (PullbackArrowUnique _ _ XR); [apply R | apply (pr1 Hx) | apply (pr2 Hx) ] ). Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.