Proposition regular_epi_mono_factorization_is_regular_is_monic : isMonic m. Proof. intros w g h p. pose (ζ := PullbackArrow K' _ g h p). refine (!(PullbackArrow_PullbackPr1 K' _ g h p) @ _). refine (_ @ PullbackArrow_PullbackPr2 K' _ g h p). apply maponpaths. apply monic_mor_eq. 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.