Proposition is_regular_epi_strong_epi : is_regular_epi e. Proof. use (is_regular_epi_arrow_z_iso_f _ _ _ _ _ He'). - apply identity_z_iso. - use make_z_iso. + exact m. + exact l. + split. * use Hm. rewrite !assoc'. rewrite ql. rewrite id_left, id_right. apply idpath. * exact ql. - simpl. rewrite id_left. exact (!p). 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.