proposition: Lemma isaprop_Pushouts: isaprop (Pushouts C).
proof: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.TransportMorphisms UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Core.Functors