proposition: Lemma z_iso_eq_inv {C : category} {a b : C} (i i' : z_iso a b) (e2 : inv_from_z_iso i = inv_from_z_iso i') : i = i'.
proof: Proof. use z_iso_eq. assert (H : is_inverse_in_precat (inv_from_z_iso i) i'). { use make_is_inverse_in_precat. - rewrite e2. exact (is_inverse_in_precat2 i'). - rewrite e2. exact (is_inverse_in_precat1 i'). } exact (inverse_unique_precat _ _ _ _ _ (z_iso_inv i) H). Qed.
imports: UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories