Definition  Let X, Y be sets, φ:X ↔ Y be a bijection, x ∈ X, y ∈ Y. We define:
xφy  :⇔  φ(x) = y

The definitions in this section are somewhat technical. Their purpose is to implement a generic notion of "isomorphism" that can be checked purely syntactically. If it can be determined that the equality definition of a constructor does not identify any non-isomorphic objects, definitions based on the decomposition of that constructor are automatically well-defined.