Lemma is_z_iso_from_is_z_iso_in_subcategory (C:category) (C':sub_precategories C) (a b : C') (f : C'⟦ a , b ⟧) (H: is_z_isomorphism f) : is_z_isomorphism (precategory_morphism_from_sub_precategory_morphism _ _ _ _ f). Proof. induction H as (g,(gl,gr)). induction g as (g_und,?). use make_is_z_isomorphism. + exact g_und. + split. - exact (maponpaths pr1 gl). - exact (maponpaths pr1 gr). Defined.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos.