proposition: Lemma epi_to_pushout : isEpi f -> isPushout f f (identity _) (identity _) (idpath _).
proof: Proof. intro h. red. intros x p1 p2 eqx. assert (hp : p1 = p2). { now apply h. } induction hp. apply (unique_exists p1). - split; apply id_left. - intros y. apply isapropdirprod; apply homset_property. - intros y [h1 _]. now rewrite id_left in h1. 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