Definition 1.5.29.  Let X, Y be sets, f : X ↔ Y be a bijection. For g : Y ↔ X, we define:
f-1 = g  :⇔  g ∘ f = idX  ⇔  f ∘ g = idY
Equivalence.  No proof.
Well-definedness.  No proof.
References.