nLab
homotopy type theory

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

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
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
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive 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, (idemponent) 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

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

(∞,1)-topos theory

Background

Definitions

Characterization

Morphisms

Extra stuff, structure and property

Models

Constructions

structures in a cohesive (∞,1)-topos

Foundations

Contents

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:

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 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 (see for instance Awodey, 2010, Joyal, 2011) 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 infinity-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.

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.

Relation to representation theory

representation theory and equivariant cohomology in terms of (∞,1)-topos theory/homotopy type theory:

homotopy type theoryrepresentation theory
pointed connected context BG\mathbf{B}G∞-group GG
dependent type∞-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}H
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 code page at the HoTT site 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)-truncated(-1)-groupoid/truth valuemere proposition, h-proposition
h-level 20-truncateddiscrete space0-groupoid/setsheafh-set
h-level 31-truncatedhomotopy 1-type1-groupoid/groupoid(2,1)-sheaf/stackh-groupoid
h-level 42-truncatedhomotopy 2-type2-groupoidh-2-groupoid
h-level 53-truncatedhomotopy 3-type3-groupoidh-3-groupoid
h-level n+2n+2nn-truncatedhomotopy n-typen-groupoidh-nn-groupoid
h-level \inftyuntruncatedhomotopy type∞-groupoid(∞,1)-sheaf/∞-stackh-\infty-groupoid

References

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

Introductions

The standard textbook is

Early sketches and introductions to the idea of homotopy type theory include

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.

Writeups on the topic include

An introduction to the notion of equivalence in HoTT is in

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

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

Models and categorical semantics

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 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 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:

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

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

The 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

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

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

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:

Revised on November 6, 2014 17:20:31 by Urs Schreiber (81.194.35.225)