Lemma z_iso_to_coslice_precat_z_iso (af bg : x / C) (h : af --> bg) (isoh : is_z_isomorphism (pr1 h)) : is_z_isomorphism h. Proof. induction isoh as [hinv [h1 h2]]. use ((hinv ,, _) ,, _ ,, _); simpl. - now rewrite <- id_right, <- h1, assoc, (pr2 h). - apply subtypePath. { intro. apply homset_property. } apply h1. - apply subtypePath. { intro. apply homset_property. } apply h2. Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total.