proposition: 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: 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.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos