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