proposition: 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: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.Combinatorics.StandardFiniteSets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Colimits