homotopy type theory FAQ


under construction


Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
logical conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type/path type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels


Constructivism, Realizability, Computability

Homotopy theory

homotopy theory, (∞,1)-category theory, homotopy type theory

flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed

models: topological, simplicial, localic, …

see also algebraic topology



Paths and cylinders

Homotopy groups

Basic facts


(,1)(\infty,1)-Topos Theory

(∞,1)-topos theory





Extra stuff, structure and property



structures in a cohesive (∞,1)-topos


This page is to provide non-technical or maybe semi-technical discussion of the nature and role of the foundational system for mathematics known as homotopy type theory. For more technical details and further pointers see at homotopy type theory.



What is homotopy type theory?

For the person on the street


For set theorists

Homotopy type theory is a refinement of constructive set theory that takes fully seriously the constructive nature also of identity. (As with all constructive mathematics, with the relevant axioms added, this subsumes, rather than excludes, classical mathematics, see below at Is HoTT limited to constructive mathematics?.)

It is this insistence on constructive witnesses for identity and on witnesses for identity of such witnesses, and so ever on, that makes what in traditional set theory are just sets (whose elements are either equal or not) in homotopy type theory instead be groupoids (whose elements may have non-trivial isomorphism between them) and indeed 2-groupoids (with isomorphisms between these isomorphisms) and so ever on; hence what makes what used to be just sets be what is kown as ∞-groupoids or homotopy types.

More technically, restriction to the 0-truncated types in HoTT (the “h-sets”) gives a predicative topos “of sets”, and a topos if one allows the resizing axiom (details are here). When adding the axiom of choice to HoTT, one obtains a model of ETCS. The iterative notion of set can also be captured. Aczel’s sets-as-trees interpretation gives a model of constructive set theory CZF. Again by adding choice to HoTT, one obtains a model of ZFC; see Ch10 of the HoTT book.

Conversely HoTT has models in ZFC (+a number of Grothendieck universes to model the type theoretic universes), namely in structures called (∞,1)-toposes which are presented by presheaves of simplicial sets. (See also at Does HoTT have models in infinity-toposes?)

The nature and role of these higher toposes in HoTT may be understood by analogy with the familar forcing models: When one proves something in ZF, it is automatically also true in all forcing extensions. The same is true for constructive set theory, except that there are more forcing extensions since we don’t have to force the law of excluded middle; those constructive notions of forcing (which also subsume permutation models) are called “sites” and their models are called “1-toposes”. Now in HoTT we have an even more general sort of forcing appropriate for homotopy theory, called (∞,1)-sites, whose models are called (∞,1)-toposes.

For type theorists


For homotopy theorists


Why should I care?

For the person on the street

For set theorists

Traditional set theory is formulated in first-order logic. Under the propositions as types interpretation, first order logic maps soundly and completely into type theory (Martin-Löf 74, section 3.1, Barendregt 91, section 4). But now the homotopy 0-types in homotopy type theory already give a constructive set theory, natively, without further axiomatization. See at h-set for more.

For type theorists

For homotopy theorists

Most homotopy-theoretic theorems that are proven in the HoTT textbook are, in their traditional informal version, material of a first-year course on homotopy theory. Experts who do not care about formal proof might not be impressed yet.

But the point is that there is significant prospect. By the discussion at Does HoTT have models in infinity-toposes, it is a fact that homotopy type theory is the internal language of (∞,1)-toposes, hence of the most powerful modern incarnation of homotopy theory. Whether or not anyone has already made impressive use of this fact (but see below), this is of genuine interest in homotopy theory irrespective of the issue of formal proof.

Historically, making use of the internal logic-perspective of elementary toposes led to substantial insight into all theory that uses Grothendieck toposes, such as notably algebraic geometry. While Lurie‘s book Higher Topos Theory based on Charles Rezk’s note Homotopy Topos Theory is an astounding piece of work, it falls short of saying anything about this crucial internal aspect of (higher) topos theory. Homotopy type theory is precisely what fills this gap. For more on how this works see at HoTT methods for homotopy theorists.

An illustration of the use of this is the proof of the Blakers-Massey theorem. This basic fact of homotopy theory has a classical proof in the classical homotopy category ∞Grpd \simeq L wheL_{whe} Top, a proof that is however rather roundabout. From this follows a proof in all (∞,1)-toposes with an (∞,1)-site of definition by, essentially, reducing stalkwise to the classical theorem (details are here). But now the theorem was also proven in homotopy type theory (details are here). Translating this formal proof back to ordinary language produces first of all a new and more elegant proof of Blakers-Massey in ∞Grpd \simeq L wheL_{whe} Top, second a new and elegant proof of the statement for (∞,1)-toposes with (∞,1)-site of definition. This is something that some homotopy theorists tried to find by classical means and failed (details are here). And moreover, the HoTT proof of Blakers-Massey is actually a new result when applied to elementary (∞,1)-toposes, where the classical methods of proving it completely break down.

It seems rather plausible that this is just a simple first example of a future where HoTT methods allow to enter new territory in classical homotopy theory. Of course it will require some expert homotopy theorists to seriously look into the internal-language-of-\infty-toposes way of doing homotopy theory. This is now an open problem for homotopy theorists just as it is for type theorists.

What role does the univalence axiom play?

For the person on the street

The axiom of univalence may be thought of as a formalization of what might be called the principle of equivalence of mathematics, which is the basic but important idea that mathematical structures which are equivalent should behave the same, satisfy the same theorems and so forth.

Obvious as this may seem, this principle may be violated in other foundations of mathematics such as ZFC. On the other hand, while these models allow such violation, in practice one essentially never wants to use such violation. The univalence axiom hence serves to make formal mathematical foundation be closer to the actual “nature of mathematics”, at least to the practice of mathematics.

For set theorists

For type theorists

The axiom of univalence added to Martin-Löf type theory implies all of the following:

  1. functional extensionality

  2. quotient types

  3. higher inductive types with nontrivial homotopies,

    Which in turn imply a wealth of further structure such as (but not limited to)

    1. bracket types

    2. etc.

For homotopy theorists

In view of the answer at Does HoTT have interpretation in infinity-toposes? the axiom of univalence axiomatizes the presence of an object classifier in an (∞,1)-topos H\mathbf{H} (details are here).

In the default choice H=\mathbf{H} = ∞Grpd \simeq L wheL_{whe}Top of traditonal homotopy theory this is the universal fibration over the disjoint union of classifying spaces [F]BAut(F)\coprod_{[F]} B Aut(F) of the automorphism ∞-groups of all (small) homotopy types [F][F].

Therefore from the axiom of univalence follows for instance the theory of ∞-actions, associated ∞-bundles and of twisted cohomology (details are here).

What advantages does homotopy type theory have over set theory?

As explained at What is HoTT for set theorists?, HoTT subsumes set theory. It has all the advantages that structural set theory (Algebraic set theory, ETCS) has over material set theory (ZFC), but moreover it allows us to natively capture higher categorical (more precisely, higher groupoidal) and homotopical reasoning. Moreover, as a practical foundation, set theory may be compared to the Turing machine model, or perhaps more generously, say, ALGOL. Whereas, homotopy type theory is closely related to modern programming languages like Haskell and ML, or more accurately Coq and Agda.

Is homotopy type theory limited to constructive mathematics?

No. On the 0-types (the h-sets) the axioms of classical logic may be imposed, such as the law of excluded middle (details are here) and the axiom of choice (details are here).

One model that interprets the resulting axioms is the standard model in simplicial sets (here) inside ZFC+inaccessible cardinals. The 0-types in this model are precisely the ordinary sets in ZFC. See also the discussion at What is HoTT? For set theorists.

For more exposition see also

Does HoTT have interpretation/semantics/models in \infty-toposes?

The short answer is: Yes. Homotopy type theory has higher categorical semantics in every (∞,1)-topos, in refinement of how plain dependent type theory has categorical semantics in toposes.

The more detailed answer depends on which axiomatics precisely one subsumes under “homotopy type theory”. A hierarchy of three main variants (“fragments”) of homotopy type theory should be distinguished here:

  1. HoTT without univalent type universes;

  2. HoTT with univalent weak type universes à la Tarski;

  3. HoTT with univalent strict type universes à la Russell or à la Tarski;

In all three cases the \infty-categorical semantics is induced by ordinary categorical semantics in a type-theoretic model category which in turn presents an (∞,1)-category. The way this works is reviewed also at HoTT methods for homotopy theorists. This relies on standard techniques for interpreting any dependent type theory in a locally cartesian closed category (see here for details).

With that understood, the higher categorical semantics for the above three cases is as follows:

  1. HoTT without univalent universes has semantics in every locally presentable locally cartesian closed (∞,1)-category (details are here).

  2. HoTT with strict univalent universes has semantics at least in (∞,1)-presheaf (∞,1)-toposes over elegant Reedy categories. This includes in particular the standard base (∞,1)-topos ∞Grpd as well as for instance the Sierpinski (∞,1)-topos (details are here).

  3. HoTT with weak univalent universes has semantics in every (∞,1)-sheaf (∞,1)-topos (details are here).

Since we are assuming local presentability here, all these models have enough (∞,1)-colimits to interpret higher inductive types. (One might also ask for models of HoTT without univalence and without higher inductive types and would expect that this then also includes locally cartesian closed (∞,1)-categories which are not necessarily locally presentable.)

One may also ask about models in elementary (∞,1)-toposes. Their theory or even definition is however much in the making. On the other hand, existing proposals essentially turn the question around and define elementary (∞,1)-toposes as (∞,1)-categories with the minimum of properties such that HoTT may be modeled in them. This reflects the idea that what is “elementary” about elementary (,1)(\infty,1)-toposes is precisely the fact that there is an internal type theory language for them.

In conclusion, every proposition proven in homtopy type theory yields (subject to the above qualification) a statement that holds true in every (∞,1)-topos (in every presentable locally cartesian closed (∞,1)-category), i.e. homotopy type theory is the internal language of \infty-toposes.

If one wishes to prove statements that hold only in some class of \infty-toposes, then one needs to add further axioms to HoTT that characterize these classes. For instance adding higher modalities that define cohesive homotopy type theory make it a language that proves theorems which hold in all cohesive (∞,1)-toposes.

What is meant by a “computational interpretation of univalence”?

What are higher inductive types?

What do we gain by a proof in homotopy type theory of π 1(S 1)=\pi_1(S^1) = \mathbb{Z} over ordinary proofs?

Is it possible to define higher coinductive types?

In what sense does homotopy type theory already contain logic?

Can category theory be carried out in homotopy type theory?

Can (,1)(\infty,1)-categories be defined in homotopy type theory?

Last revised on April 27, 2020 at 05:16:30. See the history of this page for a list of all contributions to it.