proposition: Lemma is_symmetric_isPushout : isPushout _ _ _ _ H -> isPushout _ _ _ _ (!H).
proof: Proof. intro isPo. set (Po := make_Pushout _ _ _ _ _ _ isPo). use make_isPushout. intros e x y Hxy. use unique_exists. - use (PushoutArrow Po). + exact y. + exact x. + exact (! Hxy). - cbn. split. + apply (PushoutArrow_PushoutIn2 Po). + apply (PushoutArrow_PushoutIn1 Po). - intros y0. apply isapropdirprod. + apply C. + apply C. - intros y0. intros X. cbn in X. use PushoutArrowUnique. + exact (dirprod_pr2 X). + exact (dirprod_pr1 X). Defined.
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