Definition 4.6.  Let u ∈ ℕ, C be a/an u-small category, X, Y ∈ C. We define:
Iso(X, Y) := {f : X → Y : ∃ g : Y → X : [g ∘ f = idX and f ∘ g = idY]} = {f : X → Y : ∃! g : Y → X : [g ∘ f = idX and f ∘ g = idY]}
We write “let F : X ↔ Y be an isomorphism” for “let F ∈ Iso(X, Y).”
Equality.  No proof.
References.