# Unit Type¶

In type theory, the unit type can always be constructed. It has a single value, `unit`

.

It is related to the singleton set from set theory and dual to the void type

In Haskell, unit is represented with the empty list `()`

.

It's possible to construct the function `f :: a -> ()`

easily, as unit can always be constructed.

Similarly, `f :: () -> Int`

or to any other concrete type in a pure language acts as a constant for a specific value. When corresponding this idea into category theory it's possible to use this to define all objects within the category - this is the initial object. Not every category has an initial object.

## Backlinks¶

- The singleton set and the unit type
- The singleton set from set theory corresponds to the Unit type from type theory. Also to
`true`

in logic, and to a 1-category in category theory.

- The singleton set from set theory corresponds to the Unit type from type theory. Also to
- 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.

- Dual
- It's dual is the unit type. It corresponds to the empty set from set theory.

- Void and Unit form the basis for all types
- Product Type
- Product types have a monoidal identity of Unit. |Unit| = 1.