Lemma is_symmetric_isPushout : isPushout _ _ _ _ H -> isPushout _ _ _ _ (!H). 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.
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.