Lemma iso_two_of_three_left {C : precategory} {x y z : C} {f : x --> y} {g : y --> z} (gf_is_iso : is_iso (f · g)) (g_is_iso : is_iso g) : is_iso f. Proof. assert (f_right_inv : f · (g · (inv_from_iso (make_iso _ gf_is_iso))) = identity _). rewrite assoc. apply (iso_inv_after_iso (make_iso _ gf_is_iso)). assert (f_left_inv : (g · (inv_from_iso (make_iso _ gf_is_iso))) · f = identity _). pose (iso_after_iso_inv (make_iso _ gf_is_iso)). apply (maponpaths (fun k => g · k · (inv_from_iso (make_iso _ g_is_iso)))) in p. simpl in p. rewrite <- assoc in p. rewrite <- assoc in p. rewrite <- assoc in p. rewrite id_right in p. pose (iso_inv_after_iso (make_iso _ g_is_iso)). simpl in p0. rewrite p0 in p. clear p0. rewrite id_right in p. rewrite assoc in p. apply p. eapply (is_iso_qinv _ _). exists f_right_inv. apply f_left_inv. 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.