Homotopy Type Theory
type theory (Rev #7, changes)

Showing changes from revision #6 to #7: Added | Removed | Changed

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

All types are seen as elements of a type called 𝒰\mathcal{U}. This is the universe type. Due to Russel-like paradoxes, we cannot have 𝒰:𝒰\mathcal{U} : \mathcal{U}, therefore we have an infinite hierarchy of universes

𝒰 1:𝒰 2:𝒰 3:\mathcal{U}_1 : \mathcal{U}_2 : \mathcal{U}_3 : \dots

for every nn. For most cases it will not matter what universe we are in.

Function types

Given a type AA and BB, there is a type ABA \to B called the function type representing the type of functions from AA to BB. A function can be defined explicitly using lambda notation λx.y\lambda x . y. There is a computation rule saying there is a reduction (λx.y)ay[a/x](\lambda x . y ) a \equiv y[a / x] for some a:Aa : A. The notation y[a/x]y[a / x] means to replace all occurances of xx with aa in yy, giving us a term of BB.

Pi types


Pair types


Sigma types



List of types in HoTT

Typically types come with four sets of inference rules. Rules allow one to conclude one set of judgements from others. A collection of judgements is typically called a context.

  • function type ABA \to B
  • pi type? a:AB\prod_{a:A}B
  • universe 𝒰\mathcal{U}
  • product type? A×BA \times B
  • sigma type? a:AB\sum_{a:A}B
  • zero type?
  • unit type?

List of axioms in HoTT

See axioms

Old page

List of examples

This page lists some of the type theories and variations that have been used or proposed for doing homotopy type theory.

  • The system presented in the HoTT book, chapter 1 and appendix A.
  • Martin-Löf Intensional Type Theory: the original.
  • The Calculus Of Constructions?: the basis of the Coq proof assistant.
  • Agda: based on Martin-Löf type theory, extended by a flexible scheme for specifying inductive definitions.
  • Homotopy Type System: a proposal by Vladimir Voevodsky.
  • Two-level type theory?
  • cubical type theory? (which has various forms)

See also

Type theory’ on the nLab wiki.

category: type theory

Revision on January 19, 2019 at 10:26:12 by Ali Caglayan. See the history of this page for a list of all contributions to it.