Lemma is_z_iso_from_is_iso {C : precategory} {a b : C} (f : a --> b): is_iso f -> is_z_isomorphism f. Proof. intro H. set (fiso := make_iso f H). exists (inv_from_iso fiso). split. - set (H2 := iso_inv_after_iso fiso). simpl in H2. apply H2. - set (H2 := iso_after_iso_inv fiso). simpl in H2. apply H2. 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.