A pair of types with the same cardinality will always be isomorphic

There will always be a way of exhaustively mapping each value of type $a$ to type $b$, injectively and surjectively when viewing the domain and the codomain as a set.

This is known as a bijection. Bijectivity is a more specific version of isomorphism, specific to Set - the category of all sets.

References

• Book: Thinking with types

Backlinks

• CT: Isomorphism
  • In software, A pair of types with the same cardinality will always be isomorphic
• Types have a cardinality
  • In type theory a type has a cardinality. The cardinality for a given type is the number of possible values. A cardinality can be finite or infinite. A pair of types with the same cardinality will always be isomorphic.