Definition Pullback {a b c : C} (f : b --> a)(g : c --> a) := total2 (fun pfg : total2 (λ p : C, (p --> b) × (p --> c)) => total2 (fun H : pr1 (pr2 pfg) · f = pr2 (pr2 pfg) · g => isPullback f g (pr1 (pr2 pfg)) (pr2 (pr2 pfg)) H)).
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.