Lemma isaprop_Pullbacks: isaprop Pullbacks. Proof. apply impred; intro a; apply impred; intro b; apply impred; intro c; apply impred; intro f; apply impred; intro g; apply invproofirrelevance. intros Pb Pb'. apply subtypePath. - intro; apply isofhleveltotal2. + apply hs. + intros; apply isaprop_isPullback. - apply (total2_paths_f (isotoid _ H (iso_from_Pullback_to_Pullback Pb Pb' ))). rewrite transportf_dirprod, transportf_isotoid. rewrite inv_from_iso_iso_from_Pullback. rewrite transportf_isotoid. rewrite inv_from_iso_iso_from_Pullback. destruct Pb as [Cone bla]; destruct Pb' as [Cone' bla']; simpl in *. destruct Cone as [p [h k]]; destruct Cone' as [p' [h' k']]; simpl in *. unfold from_Pullback_to_Pullback; rewrite PullbackArrow_PullbackPr2, PullbackArrow_PullbackPr1. apply idpath. 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.