proposition: Lemma is_z_iso_from_is_iso' (C : precategory) {b c : C} (f : b --> c) : is_iso' f -> is_z_isomorphism f.
proof: 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.
imports: UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories