Proposition is_epi_regular_epi {C : category} {x y : C} (f : x --> y) : is_regular_epi f → isEpi f. Proof. use factor_through_squash. { apply isapropisEpi. apply homset_property. } intros ( w & g₁ & g₂ & p & H ). pose (Coeq := make_Coequalizer _ _ _ _ H). intros z h₁ h₂ q. assert (g₁ · (f · h₁) = g₂ · (f · h₁)) as r. { rewrite !assoc. rewrite p. apply idpath. } assert (h₁ = CoequalizerOut Coeq z (f · h₁) r) as s₁. { use (CoequalizerOutsEq Coeq). rewrite CoequalizerCommutes. apply idpath. } refine (s₁ @ _). use (CoequalizerOutsEq Coeq). rewrite CoequalizerCommutes. exact q. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Epis.