Definition regular_category_epi_mono_factorization {C : category} (HC : is_regular_category C) {x y : C} (f : x --> y) : ∑ (im : C) (e : x --> im) (m : im --> y), is_regular_epi e × isMonic m × f = e · m. Proof. use regular_epi_mono_factorization. - exact (is_regular_category_pullbacks HC). - exact (is_regular_category_coeqs_of_kernel_pair HC). - exact (is_regular_category_regular_epi_pb_stable HC). Defined.
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.