“A type is defined as the range of significance of a propositional function, i.e., as the collection of arguments for which the said function has values.” – Bertrand Russell, 1908
A type theory is a formal system in which every term has a ‘type’, and operations in the system are restricted to acting on specific types.
A number of type theories have been used or proposed for doing homotopy type theory.
Here we will describe the types present in “Book HoTT”, the type theory given in the HoTT Book.
With Russell-style universes, all types are seen as elements of a type called . This is the universe type. Due to Russel-like paradoxes, we cannot have , therefore we have an infinite hierarchy of universes
for every . For most cases it will not matter what universe we are in.
With Tarski-style universes, all types are seen as dependent types of a universal type family given a type called the universe type and a term , i.e. . The existence of Russell-like paradoxes means that we similarly cannot have a type such that .
Thus, we likewise have an infinite hierarchy of universes
for every . For most cases it will not matter what universe we are in.
Given a type and , there is a type called the function type representing the type of functions from to . A function can be defined explicitly using lambda notation . There is a computation rule saying there is a reduction for some . The notation means to replace all occurances of with in , giving us a term of .
Universes are closed under function types, i.e.
and
(…)
Given a type and , there is a type called the pair type? or product type? representing the type of pairs for and .
Universes are closed under pair types, i.e.
and
(…)
(…)
(…)
(…)
Given types , , and , and functions and , there is a type called the homotopy pushout type? representing the homotopy pushout of and .
Special cases of homotopy pushout types include the type of booleans, which is defined as
the coproduct type, which is defined as
and the circle type, which is defined as