Definition make_Pullback {a b c : C} (f : C⟦b, a⟧)(g : C⟦c, a⟧) (d : C) (p1 : C⟦d,b⟧) (p2 : C ⟦d,c⟧) (H : p1 · f = p2 · g) (ispb : isPullback f g p1 p2 H) : Pullback f g. Proof. use tpair. - use tpair. + apply d. + use PullbCone; assumption. - apply ispb. 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.