Proposition regular_epi_mono_factorization_is_regular_epi : is_regular_epi e. Proof. use hinhpr. simple refine (_ ,, PullbackPr1 K ,, PullbackPr2 K ,, _ ,, _). - exact (CoequalizerEqAr im). - exact (isCoequalizer_Coequalizer im). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.EpiFacts. Require Import UniMath.CategoryTheory.RegularAndExact.RegularEpi.