Lemma z_iso_two_of_three_left {C : category} {x y z : C} {f : x --> y} {g : y --> z} (gf_is_iso : is_z_isomorphism (f · g)) (g_is_iso : is_z_isomorphism g) : is_z_isomorphism f. Proof. apply is_z_iso_from_is_iso. eapply iso_two_of_three_left. exact (is_iso_from_is_z_iso _ gf_is_iso). exact (is_iso_from_is_z_iso _ g_is_iso). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos.