Lemma equiv_isPullback_1 {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. intros R cc. set (XR := Limits.Pullbacks.make_Pullback _ X). use tpair. - use tpair. + use (Limits.Pullbacks.PullbackArrow XR). * apply (coneOut cc One). * apply (coneOut cc Three). * abstract ( assert (XRT := coneOutCommutes cc Three Two tt); simpl in XRT; eapply pathscomp0; [| apply (!XRT)]; clear XRT; assert (XRT := coneOutCommutes cc One Two tt); simpl in XRT; eapply pathscomp0; [| apply (XRT)]; apply idpath ). + use three_rec_dep. * abstract (apply (Limits.Pullbacks.PullbackArrow_PullbackPr1 XR)). * abstract (simpl; change (three_rec_dep (λ n, C⟦d,_⟧) _ _ _ _) with (p1 · f); rewrite assoc; rewrite (Limits.Pullbacks.PullbackArrow_PullbackPr1 XR); assert (XRT := coneOutCommutes cc One Two tt); simpl in XRT; eapply pathscomp0; [| apply (XRT)]; apply idpath). * abstract (apply (Limits.Pullbacks.PullbackArrow_PullbackPr2 XR)). - abstract ( intro t; apply subtypePath; [intro; apply impred; intro; apply C |]; simpl; destruct t as [t HH]; simpl in *; apply Limits.Pullbacks.PullbackArrowUnique; [ apply (HH One) | apply (HH Three)] ). 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.