Lemma merely_split_monic_is_epi_to_is_z_iso {C : category} {A B : ob C} (m : A --> B) : is_merely_split_monic m -> isEpi m -> is_z_isomorphism m. Proof. intros is_monic is_epi. apply is_z_iso_from_is_iso. intro c. apply isweqinclandsurj. - apply precomp_with_epi_isincl; assumption. - apply is_merely_split_monic_weq_precomp_is_surjection. assumption. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.Retracts.