Lemma is_z_iso_from_is_iso' (C : precategory) {b c : C} (f : b --> c) : is_iso' f -> is_z_isomorphism f. Proof. intros i. assert (Q := i c (identity c)). induction Q as [[g E] _]. unfold postcomp_with in E. exists g. split. 2 : { exact E. } assert (X := id_left _ : postcomp_with f (identity _) = f). assert (Y := ! assoc _ _ _ @ maponpaths (precomp_with f) E @ id_right _ : postcomp_with f (f · g) = f). clear E. set (x := (_,,X) : hfiber (postcomp_with f) f). set (y := (_,,Y) : hfiber (postcomp_with f) f). exact (maponpaths pr1 (proofirrelevancecontr (i b f) y x)). Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories.