Definition z_iso_from_z_iso_in_Subobjectcategory {c : C} {S S' : Subobjectscategory c} (h : z_iso S S') : (z_iso (Subobject_dom S) (Subobject_dom S')). Proof. use make_z_iso. + exact (Subobjectmor_Cmor h). + exact (Subobjectmor_Cmor (inv_from_z_iso h)). + induction h as (h, (g,(hg,gh))). use make_is_inverse_in_precat. - exact (maponpaths Subobjectmor_Cmor hg). - exact (maponpaths Subobjectmor_Cmor gh). 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.