Lemma inv_iso_unique' (C : precategory) (a b : C) (f : iso a b) (g : b --> a) : precomp_with f g = identity _ -> g = inv_from_iso f. Proof. intro H. set (T := invmaponpathsweq (make_weq (precomp_with f) (pr2 f a ))). apply T; simpl. intermediate_path (identity a). + assumption. + apply pathsinv0. apply iso_inv_after_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.