Definition 1.5.28.  Let X, Y be sets. We define:
(X ↔ Y) := {f:X → Y : f is bijective}
We write “let f:X ↔ Y be a bijection” for “let f ∈ (X ↔ Y).”
Remarks.

Bijections are important enough to warrant their own notation. A bidirectional arrow seems appropriate, even though it does not appear to be standard.

References.