Lemma inv_z_iso_unique {C : category} (a b : ob C) (f : z_iso a b) (g : z_iso b a) : is_inverse_in_precat f g -> g = z_iso_inv_from_z_iso f. Proof. intro H. apply z_iso_eq. apply (inverse_unique_precat _ _ f). - assumption. - split. + apply z_iso_inv_after_z_iso. + set (h := z_iso_after_z_iso_inv f). apply 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.