Proposition z_iso_is_regular_epi {C : category} {x y : C} (f : z_iso x y) : is_regular_epi f. Proof. use hinhpr. refine (y ,, inv_from_z_iso f ,, inv_from_z_iso f ,, idpath _ ,, _). intros z h q. use iscontraprop1. - use invproofirrelevance. intros φ₁ φ₂. use subtypePath. { intro. apply homset_property. } use (cancel_z_iso' f). exact (pr2 φ₁ @ !(pr2 φ₂)). - simple refine (_ ,, _). + exact (inv_from_z_iso f · h). + cbn. rewrite !assoc. rewrite z_iso_inv_after_z_iso. apply id_left. 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.