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. 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.
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.