Lemma coslice_precat_z_iso_to_z_iso (af bg : x / C) (h : af --> bg) (p : is_z_isomorphism h) : is_z_isomorphism (pr1 h). Proof. induction p as [hinv [h1 h2]]. exists (pr1 hinv); split. - apply (maponpaths pr1 h1). - apply (maponpaths pr1 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.