Lemma isaprop_isPullback {a b c d : C} (f : b --> a) (g : c --> a) (p1 : d --> b) (p2 : d --> c) (H : p1 · f = p2 · g) : isaprop (isPullback f g p1 p2 H). Proof. repeat (apply impred; intro). apply isapropiscontr. 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.