natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
(2,1)-quasitopos?
structures in a cohesive (∞,1)-topos
basic constructions:
strong axioms
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.
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.
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 $(\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
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.
Indeed:
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.
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.
sets cover, and more generally n-types cover.
Several variants of the axiom of choice.
representation theory and equivariant cohomology in terms of (∞,1)-topos theory/homotopy type theory:
homotopy type theory | representation theory |
---|---|
pointed connected context $\mathbf{B}G$ | ∞-group $G$ |
dependent type | ∞-action/∞-representation |
dependent sum along $\mathbf{B}G \to \ast$ | coinvariants/homotopy quotient |
context extension along $\mathbf{B}G \to \ast$ | trivial representation |
dependent product along $\mathbf{B}G \to \ast$ | homotopy invariants/∞-group cohomology |
dependent product of internal hom along $\mathbf{B}G \to \ast$ | equivariant cohomology |
dependent sum along $\mathbf{B}G \to \mathbf{B}H$ | induced representation |
context extension along $\mathbf{B}G \to \mathbf{B}H$ | |
dependent product along $\mathbf{B}G \to \mathbf{B}H$ | coinduced representation |
spectrum object in context $\mathbf{B}G$ | spectrum with G-action (naive G-spectrum) |
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.
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
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 $(\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
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
which in a presentation by a category of fibrant objects is given (see factorization lemma) by the ordinary pullback
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 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 | mere proposition, 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 $\infty$ | untruncated | homotopy type | ∞-groupoid | (∞,1)-sheaf/∞-stack | h-$\infty$-groupoid |
A survey page maintained by Steve Awodey is Homotopy Type Theory and the Univalent Foundations of Mathematics
The standard textbook is
Early sketches and introductions to the idea of homotopy type theory include
Steve Awodey, Type theory and homotopy, Epistemology versus Ontology. Springer Netherlands, 2012. 183-201. (2010) arXiv:1010.1810
Thorsten Altenkirch, Thierry Coquand, Towards higher dimensional type theory, Nottingham (2011) (pdf)
Mike Shulman, Minicourse on homotopy type theory, Swansea, April (2012) (web)
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
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)
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
A blog serving as a base for the HoTT community is at
Reports from the original Oberwolfach workshop on homotopy type theory are in
Material concerning the
is in the wiki
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
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)
Mike Shulman, section 2 of Univalence for inverse diagrams and homotopy canonicity (arXiv:1203.3253)
with lecture notes in
Mike Shulman, Categorical models of homotopy type theory, April 13, 2012 (pdf)
André Joyal, Categorical homotopy type theory, March 17, 2014 (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
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
Discussion of univalence in various other model category presentations for ∞Grpd (cubical sets, cellular sets) is 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.
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.
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)
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
More is in the repositories of various authors:
Mike Shulman and others, Higher inductive types (GitHub)
Mike Shulman, Reflective subcategories and cohesive toposes (GitHub)
Vladimir Voevodsky, Foundations (GitHub)