Lemma inverse_unique_precat {C : precategory} (a b : ob C) (f : a --> b) (g g': b --> a) (H : is_inverse_in_precat f g) (H' : is_inverse_in_precat f g') : g = g'. Proof. destruct H as [eta eps]. destruct H' as [eta' eps']. assert (H : g = identity b · g). rewrite id_left; apply idpath. apply (pathscomp0 H). rewrite <- eps'. rewrite <- assoc. rewrite eta. apply id_right. 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.