nLab
homotopy type theory

Idea

Homotopy type theory is a flavor of type theory – specifically of intensional (Martin-Löf-)dependent type theory – which takes seriously the natural interpretation of identity types as formalizing path space objects in homotopy theory.

In the categorical semantics of homotopy type theory, types are interpreted not as set-like objects, but as homotopy type- or ∞-groupoid/∞-stack-like objects. Thus, whereas extensional type theory can serve as the internal language of 1-categories (such as pretoposes, locally cartesian closed categories, or elementary toposes), homotopy type theory can serve as an internal language for various kinds of (∞,1)-category (such as locally cartesian closed (∞,1)-categories and (∞,1)-toposes). At present, such models are usually constructed by way of 1-categorical presentations of (∞,1)-categories using type-theoretic model categories and related structures such as weak factorization systems.

In addition to a viewpoint on identity types and a general class of categorical models, homotopy type theory is characterized by new homotopically motivated axioms and type-theoretic structures. Notable among these are:

• Voevodsky’s univalence axiom, which represents object classifiers in (∞,1)-categorical semantics.

• Strong function extensionality, which is a consequence of univalence.

• Higher inductive types, which among other things enable the construction of finite (∞,1)-colimits, cell complexes, truncations, localizations, and other objects which in classical homotopy theory are constructed using the small object argument.

With all of these axioms included, homotopy type theory behaves like the internal language of an (∞,1)-topos, and conjecturally should admit actual models in any (∞,1)-topos. With fewer axioms and type constructors, it is known to admit models in more weakly structured (∞,1)-categories — see below.

Many details are still being worked out, but the impression is that homotopy type theory thus should serve as a foundation for mathematics that is natively about homotopy theory/(∞,1)-category theory — in other words, a foundation in which homotopy types, rather than sets, are basic objects.

Properties

Advantages

As a foundation for mathematics, homotopy type theory (also called univalent foundations) has the following advantages. Many of these advantages are shared with some other foundational systems, but no other known system shares all of these, and some are unique to HoTT.

• It treats homotopy theory and ∞-groupoids natively. This is an advantage for doing homotopical and higher-categorical mathematics, which is spreading slowly into other fields.

• It inherits the good computational properties of intensional Martin-Löf type theory. Some of its new axioms, such as univalence and function extensionality, are not fully understood yet from a computational perspective, but progress is being made.

• It is constructive by default, but can easily be made classical by adding axioms. This makes it potentially more expressive at essentially no cost. (In fact, it is not entirely clear how possible it is to do homotopy theory constructively in other foundations.)

• It can (conjecturally) be internalized in many categories and higher categories, providing an internal logic which enables a single proof to be reinterpreted in many places with many different meanings.

• It is naturally isomorphism- and equivalence-invariant (non-evil). This is a consequence of the univalence axiom: any property or structure (even one which speaks only about sets and makes no reference to homotopy theory) which is expressible in the theory must be invariant under isomorphism/equivalence.

• Notions such as propositions and sets are defined objects, which inherit good computational properties from the underlying type theory.

• It treats sets, groupoids, and higher groupoids on an equal footing. One can easily remain entirely in the fragment of the theory which talks about sets, not worrying about groupoids or homotopy theory, but as soon as one starts to say something which naturally needs structures of higher homotopy level (such as talking about some collection of structured sets), the groupoidal and homotopical structure is already there.

Models

It is well known that extensional dependent type theory is an internal logic for locally cartesian closed categories. The step from extensional to intensional type theory and the identity types that this brings with it makes intensional dependent type theory have models in certain (∞,1)-categories. This connection is usually shown by means of a presentation of the $(\mathrm{\infty },1)$-category using a weak factorization system, a category of fibrant objects, a model category, or other similar structure.

It is conjectured (see for instance Joyal, 2011) that

• intensional dependent type theory with dependent sums and products and function extensionality (a form of homotopy type theory) is an internal language for locally cartesian closed (∞,1)-categories; and

• with the univalence axiom added, it becomes an internal language for (∞,1)-toposes.

For a short introduction to a simplicial model of homotopy type theory see T. Streicher - a model of type theory in simplicial sets - a brief introduction to Voevodsky' s homotopy type theory.

Machine implementation

An important aspect of HoTT is the fact that the intensional Martin-Löf type theory on which it is built has a computational implementation in proof assistants like Coq and Agda.

This forms the basis of the Univalent Foundations program (Voevodsky), which uses Coq to generate and verify proofs with homotopical content.

See the code page at the HoTT site for more.

Dictionary HoTT-Coq / $(\mathrm{\infty },1)$-Category theory

The following list displays some keywords defined in the Coq-implementation of homotopy type theory together with their meaning in the homotopy theory/(∞,1)-category theory that they describe. (See also at categorical semantics and categorical semantics of homotopy type theory.)

Let $C$ be a given ambient (∞,1)-category which

• is locally cartesian closed;

• in addition has (∞,1)-colimits.

For instance $C$ could be an (∞,1)-topos (in which case the homotopy type theory would be the internal language of an (∞,1)-topos).

Note that while Coq-HoTT is supposed to be the internal language for such $C$, the strict models for it are actually homotopical 1-categories equipped with extra structure (such as model categories or categories of fibrant objects) that make them serve as presentations for $C$.

We then have the following dictionary.

The type of types Type

Type

denotes an object classifier in $C$ for a certain size of universe. Both Coq and Agda have systems to manage universe sizes and universe enlargement automatically; Agda’s is more advanced (universe polymorphism), whereas Coq’s is good enough for many purposes but tends to produce “universe inconsistencies” when working with univalence. As a stopgap measure until this is improved, some HoTT code must be compiled with a patch to Coq that turns off all universe consistency checks.

A term of type Type (in the empty context)

X : Type

denotes an object in the $(\mathrm{\infty },1)$-category $C$. In a presentation of $C$ by a model category or weak factorization system, it denotes a fibrant object.

The unit type

unit : Type

is the terminal object.

For $X,Y\in C$ two objects, the function type

X -> Y : Type

denotes the internal hom $[X,Y]\in C$ (a formal proof of that fact is here).

A dependent type (that is, a type in context)

x : X  |-  P x : Type

denotes a morphism $P\to X$ (regarded as a fibration or bundle) in $C$. In a presentation of $C$ by a category of fibrant objects, it literally denotes a fibration $P\to X$. In this case,

P : X -> Type

denotes the corresponding classifying map, via an internal (∞,1)-Grothendieck construction.

The total space object $P$ of this bundle – the dependent sum type – is the type equivalently coded as any of the following.

{ x : X  &  P x } : Type
sigT (fun (x : X) => P x) : Type.
sigT P : Type

The first one is syntactic sugar for the second. The third is related to the second by eta expansion, which (assuming function extensionality) is an equivalence in Coq, but not the identity. In the next version of Coq, all three types above will be identical.

One might expect to also call the dependent sum type

exists x : X, P x

(see existential quantifier) but in the current Coq implementation that keyword is reserved for the corresponding operation on Coq’s built-in universe Prop, which is not used by homotopy type theory. In particular, it should not be confused with what HoTT calls propositions, which are the (-1)-truncated types. In fact, arguably in HoTT exists should refer not to the dependent sum itself, but to the (-1)-truncation thereof (its bracket type).

The type

forall x : X, P x

denotes the object of homotopy sections of this bundle $P\to X$ — that is, the dependent product of the bundle. (See the section relation to spaces of sections there). It also denotes the universal quantifier when acting on (-1)-truncated objects propositions. A term of this type :

f : forall x : X, P x

denotes therefore a particular section of this bundle

$$\begin{array}{ccc}& & P\\ & {}^f\nearrow & \downarrow \\ X& =& X\end{array}.$$\array{ && P \\ & {}^{\mathllap{f}}\nearrow& \downarrow \\ X &= & X } \,.

Given a type $X$, its identity type, denoted

paths X : X -> X -> Type
Id X : X -> X -> Type

corresponds to the diagonal morphism $X\to X\times X$ in $C$, regarded as a bundle over $X\times X$. In a presentation of $C$ by a category of fibrant objects, this means the path space object $X^I$, since dependent types must always be fibrations.

The fact that there is a weak equivalence $X\stackrel{\simeq }{\to }{X}^I$ given by the inclusion of identity morphisms is reflected in the inductive type-definition of paths, which says that any proposition about terms in the path type is already determined by its value on all identity paths.

Then for x y : X two terms regarded as morphisms $1\to X$, the application of the identity type $x$ and $y$ (also called the identity type) denoted variously

paths X x y : Type
x ~~> y : Type
x == y : Type

(the latter two make use of Coq’s ability to define new notations), denotes the homotopy pullback of the form

$$\begin{array}{ccc}x{\times }_{X}y& \to & *\\ \downarrow & & {\downarrow }^x\\ *& \stackrel{y}{\to }& X\end{array}$$\array{ x \times_X y &\to& {*} \\ \downarrow && \downarrow^{\mathrlap{x}} \\ {*} &\stackrel{y}{\to}& X }

which in a presentation by a category of fibrant objects is given (see factorization lemma) by the ordinary pullback

$$\begin{array}{ccccc}{P}_{x,y}X& \to & & \to & *\\ \downarrow & & & & {\downarrow }^x\\ \downarrow & & X^{\Delta [1]}& \to & X\\ \downarrow & & \downarrow \\ *& \stackrel{y}{\to }& X\end{array}.$$\array{ P_{x,y} X &\to& &\to& {*} \\ \downarrow && && \downarrow^{\mathrlap{x}} \\ \downarrow && X^{\Delta[1]} &\to& X \\ \downarrow && \downarrow \\ {*} &\stackrel{y}{\to}& X } \,.

Beware that the path induction rule applies to paths X not to paths X x y. Where for the former a proposition is fixed by what it does on identity paths, for the latter this is not the case anymore.

More generally, we can define arbitrary pullbacks. If f : A -> C and g : B -> C, the homotopy pullback of f and g is defined by

{a : A & {b : B & f a ~~> g b}}

together with the obvious projections to A and B and the homotopy between the composites. (a proof can be found here)

Using higher inductive types, we can also define homotopy pushouts. if g : C -> A and f : C -> B, the homotopy pushout of f and g is defined by

Inductive hopushout :=
  | inl : A -> hopushout
  | inr : B -> hopushout
  | glue : forall x : C, inl (g x) ~~> inr (f x).

together with the map inl, inr and the homotopy glue. (see here for the proof)

Related entries

• intensional type theory, observational type theory, extensional type theory

• HoTT methods for homotopy theorists

• cohesive homotopy type theory

• directed homotopy type theory

homotopy level	n-truncation	homotopy theory	higher category theory	higher topos theory	homotopy type theory
h-level 0	(-2)-truncated	contractible space	(-2)-groupoid		true/unit type/contractible type
h-level 1	(-1)-truncated		(-1)-groupoid/truth value		h-proposition
h-level 2	0-truncated	discrete space	0-groupoid/set	sheaf	h-set
h-level 3	1-truncated	homotopy 1-type	1-groupoid/groupoid	(2,1)-sheaf/stack	h-groupoid
h-level 4	2-truncated	homotopy 2-type	2-groupoid		h-2-groupoid
h-level 5	3-truncated	homotopy 3-type	3-groupoid		h-3-groupoid
h-level $n+2$	$n$-truncated	homotopy n-type	n-groupoid		h-$n$-groupoid
h-level $\mathrm{\infty }$	untruncated	homotopy type	∞-groupoid	(∞,1)-sheaf/∞-stack	h-$\mathrm{\infty }$-groupoid

References

A survey page maintained by Steve Awodey is Homotopy Type Theory and the Univalent Foundations of Mathematics

Introductions

Introductions to the idea of homotopy type theory include

• Steve Awodey, Type theory and homotopy (pdf)

• Michael Shulman, Homotopy type theory I, II, III, IV, V, VI

• Mike Shulman, Minicourse on homotopy type theory, Swansea, April (2012) (web)

• Vladimir Voevodsky, Univalent foundations

Writeups on the topic include

• Nicolai Kraus, Homotopy type theory – An overview (pdf)

• Egbert Rijke, Homotopy type theory (2012) (pdf)

• Álvaro Pelayo, Michael Warren, Homotopy type theory and Voevodsky’s univalent foundations (arXiv:1210.5658)

Introductory talks include also

• Thorsten Altenkirch, Thierry Coquand, Towards higher dimensional type theory, Nottingham (2011) (pdf)

A list of video-recorded talks by Voevodsky on this topic is here.

An introduction to the notion of equivalence in HoTT is in

• Andrej Bauer, A seminar on HoTT equivalences (blog post)

A guided walk through the basics of HoTT and then the formal proof in Coq that the univalence axiom implies functional extensionality is at

• Andrej Bauer, Peter LeFanu Lumsdaine, Oberwolfach HoTT-Coq tutorial

General

A blog serving as a base for the HoTT community is at

• Homotopy Type Theory website

Reports from the original Oberwolfach workshop on homotopy type theory are in

• Homotopy type theory , Oberwolfach Reports 11-2011, (pdf).

Material concerning the

• Univalent foundations program 2012/2013, Institute of Advanced Study, Princeton

is in the wiki

• UF-IAS-2012 .

Models

The first model for intensional Martin-Löf type theory on groupoids (instead of sets = 0-groupoids) was

• Martin Hofmann, Thomas Streicher The groupoid interpretation of type theory. in Sambin, Giovanni (ed.) et al., Twenty-five years of constructive type theory . Proceedings of a congress, Venice, Italy, October 19—21, 1995. Oxford: Clarendon Press. Oxf. Logic Guides. 36, 83-111 (1998). (ps)

Generalization of this to strict ω-groupoids:

• Michael Warren, The strict $\omega$-groupoid interpretation of type theory (pdf)

The fact that every simplicial model category in which the cofibrations are monomorphisms provides a sound model for intensional Martin-Löf type theory is discussed in

• Steve Awodey, Michael Warren, Homotopy theoretic models of identity type, Mathematical Proceedings of the Cambridge Philosophical Society vol 146, no. 1 (2009) (arXiv:0709.0248)

and with more details in

• Michael Warren, Homotopy theoretic aspects of constructive type theory, PhD thesis (2008) (pdf)

• Richard Garner, Benno van den Berg, Topological and simplicial models of identity types. , ACM Transactions on Computational Logic (pdf)

The trickiest question in finding models of homotopy type theory is to validate the univalence axiom. The first model satisfying this axiom was constructed by Voevodsky using the standard model structure on simplicial sets, hence for the archetypical (∞,1)-topos ∞Grpd of discrete ∞-groupoids. Some expositions are:

• Chris Kapulkin, Peter LeFanu Lumsdaine, Vladimir Voevodsky, Univalence in simplicial sets, arXiv

• T. Streicher - a model of type theory in simplicial sets - a brief introduction to Voevodsky' s homotopy type theory

• Ieke Moerdijk (notes by Chris Kapulkin): Fiber bundles and univalence, link

A discussion of univalence for categories of presheaves over an inverse category, with values in a category for which univalence is already established (such as simplicial sets) is discussed in

• Michael Shulman, The univalence axiom for inverse diagrams (arXiv:1203.3253).

the conjecture that the models of HoTT with function extensionality are locally cartesian closed (∞,1)-categories is explicitly stated in

• André Joyal, Remarks on homotopical logic Oberwolfach (2011) (pdf)

Syntax

• Nicola Gambino, Richard Garner, The identity type weak factorisation system , Theoretical Computer Science 409 (2008), no. 3, pages 94–109.

• Richard Garner, Benno van den Berg, Types are weak ω-groupoids ,

• Peter LeFanu Lumsdaine, Weak ω-Categories from Intensional Type Theory , TLCA 2009, Brasília, Logical Methods in Computer Science, Vol. 6, issue 23, paper 24.

• Peter LeFanu Lumsdaine, Higher Categories from Type Theories , PhD Thesis: Carnegie Mellon University, 2010. PDF

• Michael Hedberg, A coherence theorem for Martin-Löf’s type theory , Journal of Functional Programming 8 (4): 413–436, July 1998.

Code

The basic Coq-code libraries that set up identity types and the resulting homotopy type theory are at

• https://github.com/HoTT/HoTT/tree/master/theories

A slightly more human readable version is collected as a single pdf in

• HoTT-Coq code (HoTT-Coq-code.pdf) .

A collection of all this code equipped with html-functionality that does display also the proofs (which otherwise only display when the code is loaded into a Coq-system) is at

• Proviola/HoTT .

A further translation of these proofs into ordinary text is in

• Carlo Angiuli, Univalence implies function extensionality (pdf)

More is in the repositories of various authors:

• Andrej Bauer, (GitHub)

• Peter LeFanu Lumsdaine, (GitHub)

• Mike Shulman and others, Higher inductive types (GitHub)

• Mike Shulman, Reflective subcategories and cohesive toposes (GitHub)

• Vladimir Voevodsky, Foundations (GitHub)