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