proposition: 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: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Retracts