Definition subprecategory_of_monics_mor {c' c : C} (f : c' --> c) (isM : isMonic f) : subcategory_of_monics⟦subprecategory_of_monics_ob c', subprecategory_of_monics_ob c⟧ := tpair _ f isM. Local Lemma is_z_iso_in_subcategory_of_monics_from_is_z_iso (a b : subcategory_of_monics) (f : C⟦ pr1 a , pr1 b ⟧) (p : isMonic f) (H : is_z_isomorphism f) : is_z_isomorphism (precategory_morphisms_in_subcat f p). Proof. use make_is_z_isomorphism. + use precategory_morphisms_in_subcat. - exact (is_z_isomorphism_mor H). - use is_iso_isMonic. use is_z_isomorphism_inv. + induction (is_z_isomorphism_is_inverse_in_precat H) as (H1,H2). split. - use eq_in_sub_precategory. exact H1. - use eq_in_sub_precategory. exact H2. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.covyoneda. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Subcategory.Core.