nLab homotopy type theory

Contents

Context

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

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
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

semantics

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

Introductions

Definitions

Paths and cylinders

Homotopy groups

Basic facts

Theorems

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

(∞,1)-topos theory

structures in a cohesive (∞,1)-topos

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Contents

Idea

Homotopy type theory is a flavor of type theory – specifically of intensional dependent type theory – which takes seriously the natural interpretation of identity types or path types as formalizing path space objects in homotopy theory. Examples of homotopy type theory include variants of Martin-Löf type theory and cubical type theory which have univalent universes and higher inductive types, as well as higher observational type 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:

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. [This paragraph should be updated in view of the computational interpretation of univalence by the cubical model.]

  • 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 (respecting the principle of equivalence). 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 in (,1)(\infty,1)-categories and (,1)(\infty,1)-toposes

It is well known that extensional dependent type theory is an internal logic for locally cartesian closed categories. See at relation between type theory and category theory.

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 (,1)(\infty,1)-category using a weak factorization system, a category of fibrant objects, a model category, or other similar structure.

It is conjectured (due to Awodey 09, Awodey, 2010, Joyal, 2011, see Awodey's conjecture) that

Indeed:

Proposition

Every presentable and locally cartesian closed (∞,1)-category has a presentation by a type-theoretic model category. This provides the categorical semantics for homotopy type theory (without, possibly, the univalence axiom).

For more on this see at locally cartesian closed (∞,1)-category in the section on internal logic.

With the univalence axiom included (for a type of types “weakly a la Tarski”) then homotopy type theory has categorical semantics in (∞,1)-toposes, with the type of types interpreted as the object classifier.

See also at relation between type theory and category theory — univalent homotopy type theory and elementary ( , 1 ) (\infty,1) -toposes.

For a short introduction to a simplicial model of homotopy type theory see Streicher 2014.

New Axioms

As a foundation for mathematics whose basic objects are higher groupoids, homotopy type theory makes visible new foundational axioms. Most of these axioms are true as statements about classical \infty-groupoids, but may be false in “nonclassical” models of homotopy type theory such as (∞,1)-toposes.

Additionally, since homotopy type theory as the internal language of (,1)(\infty, 1)-toposes is not classical, it is possible to add classically inconsistent axioms, just as, say, the Kock-Lawvere axiom may be added to ordinary topos theory.

Relation to representation theory

representation theory and equivariant cohomology in terms of (∞,1)-topos theory/homotopy type theory (FSS 12 I, exmp. 4.4):

homotopy type theoryrepresentation theory
pointed connected context BG\mathbf{B}G∞-group GG
dependent type on BG\mathbf{B}GGG-∞-action/∞-representation
dependent sum along BG*\mathbf{B}G \to \astcoinvariants/homotopy quotient
context extension along BG*\mathbf{B}G \to \asttrivial representation
dependent product along BG*\mathbf{B}G \to \asthomotopy invariants/∞-group cohomology
dependent product of internal hom along BG*\mathbf{B}G \to \astequivariant cohomology
dependent sum along BGBH\mathbf{B}G \to \mathbf{B}Hinduced representation
context extension along BGBH\mathbf{B}G \to \mathbf{B}Hrestricted representation
dependent product along BGBH\mathbf{B}G \to \mathbf{B}Hcoinduced representation
spectrum object in context BG\mathbf{B}Gspectrum with G-action (naive G-spectrum)

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 page formalized libraries of homotopy type theory for more.

Dictionary HoTT-Coq / (,1)(\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 CC be a given ambient (∞,1)-category which

For instance CC 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 CC, 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 CC.

We then have the following dictionary.

The type of types Type

Type

denotes an object classifier in CC 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 (,1)(\infty,1)-category CC. In a presentation of CC by a model category or weak factorization system, it denotes a fibrant object.

The unit type

unit : Type

is the terminal object.

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

X -> Y : Type

denotes the internal hom [X,Y]C[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 PXP \to X (regarded as a fibration or bundle) in CC. In a presentation of CC by a category of fibrant objects, it literally denotes a fibration PXP \to X. In this case,

P : X -> Type

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

The total space object PP 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 PXP\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

P f X = X. \array{ && P \\ & {}^{\mathllap{f}}\nearrow& \downarrow \\ X &= & X } \,.

Given a type XX, its identity type, denoted

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

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

The fact that there is a weak equivalence XX IX \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 1X1\to X, the application of the identity type xx and yy (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

x× Xy * x * y X \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

P x,yX * x X Δ[1] X * y X. \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)


homotopy leveln-truncationhomotopy theoryhigher category theoryhigher topos theoryhomotopy type theory
h-level 0(-2)-truncatedcontractible space(-2)-groupoidtrue/​unit type/​contractible type
h-level 1(-1)-truncatedcontractible-if-inhabited(-1)-groupoid/​truth value(0,1)-sheaf/​idealmere proposition/​h-proposition
h-level 20-truncatedhomotopy 0-type0-groupoid/​setsheafh-set
h-level 31-truncatedhomotopy 1-type1-groupoid/​groupoid(2,1)-sheaf/​stackh-groupoid
h-level 42-truncatedhomotopy 2-type2-groupoid(3,1)-sheaf/​2-stackh-2-groupoid
h-level 53-truncatedhomotopy 3-type3-groupoid(4,1)-sheaf/​3-stackh-3-groupoid
h-level n+2n+2nn-truncatedhomotopy n-typen-groupoid(n+1,1)-sheaf/​n-stackh-nn-groupoid
h-level \inftyuntruncatedhomotopy type∞-groupoid(∞,1)-sheaf/​∞-stackh-\infty-groupoid


proof assistants:

based on plain type theory/set theory:

based on dependent type theory/homotopy type theory:

based on cubical type theory:

based on modal type theory:

based on simplicial type theory:

For monoidal category theory:

For higher category theory:

projects for formalization of mathematics with proof assistants:

Other proof assistants

Historical projects that died out:

References

The standard textbook on homotopy type thoery:

For further resources see also:

Early development

Precursor discussion that led to the formulation of homotopy type theory in UFP13:

For more on the early history see also:

Introductions

A survey of homotopy type theory aimed at logicians and philosophers of mathematics:

and one with an emphasis on synthetic geometry:

More technical introductions:

On synthetic homotopy theory in homotopy type theory:

Motivation via practical problems in homotopy theory and higher category theory is given in

(specifically highlighting the technical delicacies involved in the Simpson conjecture).

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

Introduction and review:

An introduction to the notion of equivalence in HoTT:

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

An computer science oriented introduction to HoTT:

An introduction to HoTT through Agda:

An introduction to homotopy theory through type theory:

Gentle invitation to some basics:

From the point of view of cubical type theory:

  • Anders Mörtberg, Loïc Pujet, Cubical synthetic homotopy theory, CPP 2020: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs January 2020, pp. 158–171, doi:10.1145/3372885.3373825, (pdf)

General

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

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

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

Material concerning the

is in the wiki

A FAQ of sorts, with tips for those getting started in the field, is being maintained at

Forums dedicated to homotopy type theory

The HoTT research group at Carnegie Mellon University:

The HoTT electronic seminar talks:

Models and categorical semantics

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

Generalization of this to strict ∞-groupoids were discussed in

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

and with more details in

with lecture notes in

The full model in the classical model structure on simplicial sets is due to

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 (see also at universal Kan fibration). Some expositions are:

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

Proof that all ∞-stack (∞,1)-topos have presentations by model categories which interpret (provide categorical semantics) for homotopy type theory with univalent type universes:

Discussion of univalence in various other model category presentations for ∞Grpd (cubical sets, cellular sets) is in

Models in terms of cubical sets inside constructive set theory/type theory are discussed in

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

See also the references at relation between type theory and category theory.

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

  • Vladimir Voevodsky, Experimental library of univalent formalization of mathematics (arXiv:1401.0053) github

  • The HoTT Library: A formalization of homotopy type theory in Coq, Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Mike Shulman, Matthieu Sozeau, Bas Spitters, 2016 arxiv and on github

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

Homotopy theory formalized in homotopy type theory

The following is a list of topics and results of homotopy theory that have been formalized in homotopy type theory.


On homotopy groups of spheres:

On Whitehead's theorem:

On Eilenberg-MacLane spaces:

On ordinary cohomology:

On the Freudenthal suspension theorem:

  • Implies π k(S n)=π k+1(S n+1)\pi_k(S^n) = \pi_{k+1}(S^{n+1}) whenever k2n2k \leq 2n - 2

  • Peter’s encode/decode-style proof, formalized by Dan, using a clever lemma about maps out of 2 n-connected types. This is the “95%” version, which shows that the relevant map is an equivalence on truncations.

  • The full “100%” version, formalized by Dan, which shows that the relevant map is 2n2n-connected.

On homotopy limits:

  • Jeremy Avigad, Chris Kapulkin and Peter Lumsdaine arXiv Coq code

On the van Kampen theorem:

On covering spaces:

  • Favonia’s proofs (link in flux due to library rewrite).

On Blakers-Massey theorem:

  • Favonia/Peter/Guillaume/Dan’s formalization of Peter/Eric/Dan’s proof (link in flux due to library rewrite).

Last revised on March 7, 2024 at 01:09:02. See the history of this page for a list of all contributions to it.