Proposition is_strong_epi_regular_epi {C : category} {x y : C} {e : x --> y} : is_regular_epi e → is_strong_epi e. Proof. use factor_through_squash. { apply isaprop_is_strong_epi. } intros (w & p₁ & p₂ & p & H) a b m f g q Hm. pose (Coeq := make_Coequalizer _ _ _ _ H). use iscontraprop1. - use invproofirrelevance. intros l₁ l₂. use subtypePath. { intro. apply isapropdirprod ; apply homset_property. } use Hm. exact (pr12 l₁ @ !(pr12 l₂)). - simple refine (_ ,, _ ,, _). + use (CoequalizerOut Coeq). * exact f. * use Hm. rewrite !assoc'. rewrite <- !q. rewrite !assoc. rewrite p. apply idpath. + use (CoequalizerOutsEq Coeq). refine (assoc _ _ _ @ _). rewrite CoequalizerCommutes ; cbn. exact (!q). + cbn. use Hm. refine (_ @ q). refine (assoc' _ _ _ @ _). apply maponpaths. use (CoequalizerOutsEq Coeq). refine (assoc _ _ _ @ _). rewrite CoequalizerCommutes ; cbn. 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. Require Import UniMath.CategoryTheory.EpiFacts. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.RegularAndExact.RegularEpi. Require Import UniMath.CategoryTheory.RegularAndExact.RegularCategory.