Proposition is_z_isomorphism_is_regular_epi {C : category} {x y : C} (f : x --> y) (Hf : is_z_isomorphism f) : is_regular_epi f. Proof. exact (z_iso_is_regular_epi (f ,, Hf)). 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.