Definition make_z_iso_in_Subobjectscategory {c : C} {S S' : Subobjectscategory c} (h : C ⟦Subobject_dom S ,Subobject_dom S'⟧) (is_z_iso : is_z_isomorphism h) (tri : Subobject_mor S = h · Subobject_mor S') : z_iso S S'. Proof. use make_z_iso'. + use tpair. - use precategory_morphisms_in_subcat. * exact h. * use is_iso_isMonic. exact is_z_iso. - use eq_in_sub_precategory. exact tri. + use z_iso_to_slice_precat_z_iso. use is_z_iso_in_subcategory_of_monics_weq. exact is_z_iso. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.slicecat. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Subcategory.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.opp_precat.