Lemma isaprop_Pushouts: isaprop (Pushouts C). Proof. apply impred; intro a; apply impred; intro b; apply impred; intro c; apply impred; intro p1; apply impred; intro p2; apply invproofirrelevance. intros Pb Pb'. apply subtypePath. - intro; apply isofhleveltotal2. + apply C. + intros; apply isaprop_isPushout. - apply (total2_paths_f (isotoid _ H (z_iso_from_Pushout_to_Pushout Pb Pb' ))). rewrite transportf_dirprod, transportf_isotoid', transportf_isotoid'. fold (PushoutIn1 Pb). fold (PushoutIn2 Pb). use (dirprodeq); simpl. 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_Pushout_to_Pushout. rewrite PushoutArrow_PushoutIn1. apply idpath. unfold from_Pushout_to_Pushout. rewrite PushoutArrow_PushoutIn2. 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.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.Core.Functors.