Lemma inv_z_iso_unique' (C : precategory) (a b : C) (f : z_iso a b) (g : b --> a) : precomp_with f g = identity _ -> g = inv_from_z_iso f. Proof. intro H. apply (cancel_z_iso' f). unfold precomp_with in H. rewrite H. apply pathsinv0. apply z_iso_inv_after_z_iso. 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.