Definition make_isPullback {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) : (∏ e (h : C ⟦e, b⟧) (k : C⟦e,c⟧)(Hk : h · f = k · g ), iscontr (total2 (fun hk : C⟦e,d⟧ => dirprod (hk · p1 = h)(hk · p2 = k)))) → isPullback f g p1 p2 H. Proof. intros H' x cx; simpl in *. set (H1 := H' x (coneOut cx One) (coneOut cx Three) ). use (let p : coneOut cx One · f = coneOut cx Three · g := _ in _ ). { eapply pathscomp0; [apply (coneOutCommutes cx One Two tt)|]. apply pathsinv0, (coneOutCommutes cx Three Two tt). } set (H2 := H1 p). use tpair. + exists (pr1 (pr1 H2)). use three_rec_dep. * apply (pr1 (pr2 (pr1 H2))). * simpl. change (three_rec_dep (λ n, C⟦d,_⟧) _ _ _ _) with (p1 · f). rewrite assoc. eapply pathscomp0. eapply cancel_postcomposition, (pr2 (pr1 H2)). apply (coneOutCommutes cx One Two tt). * apply (pr2 (pr2 (pr1 H2))). + abstract (intro t; apply subtypePath; [ intro; apply impred; intro; apply C | destruct t as [t p0]; apply path_to_ctr; split; [ apply (p0 One) | apply (p0 Three) ]]). Defined.
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.