Proposition regular_epi_mono_factorization_is_regular_is_monic_eq : PullbackPr1 K · CoequalizerArrow im · m = PullbackPr2 K · CoequalizerArrow im · m. Proof. rewrite !assoc'. unfold m, regular_epi_mono_factorization_mono. rewrite !CoequalizerCommutes. exact (PullbackSqrCommutes K). 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.