# 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.

Cardinality for a type T is expressed |T|. For example for the type

```
data Boolean = True | False
```

Then |Boolean| = 2 should be read as `the cardinality of Boolean is equal to 2`

## References¶

## Backlinks¶

- Void Type
- In type theory, the void type is a type with a cardinality of 0. It is therefore impossible to construct. It's dual is the unit type. It corresponds to the empty set from set theory.

- Type Theory
- Types have a cardinality, which is the number of possible values within that type.

- Cardinality can be used to express maths concepts
- Each type has a cardinality. This allows us to express equations and ideas from maths using only types because of the Curry-Howard isomorphism.

- Function types are like exponentiation for cardinality
- The cardinality of a
`function`

type is the second argument to the power of the first.

- The cardinality of a
- Product Type
- A product type is the result of the product operation on algebraic types. The cardinality of a product type is the product of it's fields. For example

- Sum Type
- The cardinality of a sum type is the sum of all the cardinailities of it's constructors. |Boolean| = 2