“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 a typical models of homotopy type theory.
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 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 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