proposition: Lemma inv_iso_unique (C : precategory) (a b : C) (f : iso a b) (g : iso b a) : precomp_with f g = identity _ -> g = iso_inv_from_iso f.
proof: Proof. intro H. apply eq_iso. simpl. 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.
imports: UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories