proposition: 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: 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.
imports: UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories