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.