nLab homotopy type theory

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:

• 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. [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 $(\infty,1)$-categories and $(\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 $(\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

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

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.

• model of type theory in an (infinity,1)-topos

See also at relation between type theory and category theory — univalent homotopy type theory and elementary $(\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.

• Whitehead's principle.

• sets cover, and more generally n-types cover.

• Several variants of the axiom of choice.

Additionally, since homotopy type theory as the internal language of $(\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.

• Axiom R (Shulman 15)

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 theory	representation theory
pointed connected context $\mathbf{B}G$	∞-group $G$
dependent type on $\mathbf{B}G$	$G$-∞-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$	restricted representation
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)

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 / $(\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 $(\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

$$\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

$$\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

$$\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

• univalent foundations for mathematics

• homotopy type theory FAQ

• homotopy type theory events

• open problems in homotopy type theory

• higher structures

• intensional type theory, extensional type theory

• observational type theory, higher observational type theory

• book HoTT

• cubical type theory

• type-theoretic model category, fibrant type

• synthetic homotopy theory

• HoTT methods for homotopy theorists

• internal category in homotopy type theory

• Homotopy Type System

• modal homotopy type theory

• geometric homotopy type theory

• cohesive homotopy type theory

• directed homotopy type theory

  opetopic type theory

  simplicial 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	contractible-if-inhabited	(-1)-groupoid/​truth value	(0,1)-sheaf/​ideal	mere proposition/​h-proposition
h-level 2	0-truncated	homotopy 0-type	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	(3,1)-sheaf/​2-stack	h-2-groupoid
h-level 5	3-truncated	homotopy 3-type	3-groupoid	(4,1)-sheaf/​3-stack	h-3-groupoid
h-level $n+2$	$n$-truncated	homotopy n-type	n-groupoid	(n+1,1)-sheaf/​n-stack	h-$n$-groupoid
h-level $\infty$	untruncated	homotopy type	∞-groupoid	(∞,1)-sheaf/​∞-stack	h-$\infty$-groupoid

proof assistants:

based on plain type theory/set theory:

• Metamath

• Mizar, NuPRL, Isabelle, HOL

based on dependent type theory/homotopy type theory:

• Coq, Agda, Lean, Arend

based on cubical type theory:

• cubicaltt

• redtt

• yacctt

• RedPRL

• Cubical Agda

  • library and demos

  • 1lab (cross-linked reference resource)

based on modal type theory:

• Agda-flat: installation instructions

based on simplicial type theory:

• Rzk

For monoidal category theory:

• DisCoPy

For higher category theory:

• opetopic type theory

• Globular, homotopy.io

projects for formalization of mathematics with proof assistants:

• Archive of Formal Proofs (using Isabelle)

• ForMath project (using Coq)

• MathScheme

• UniMath project (using Coq and Agda)

• Xena project (using Lean)

Other proof assistants

• Andromeda

Historical projects that died out:

• The QED Project

References

The standard textbook on homotopy type thoery:

• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)

For further resources see also:

• Steve Awodey, Homotopy Type Theory and the Univalent Foundations of Mathematics [www.andrew.cmu.edu/user/awodey/htt.html]

Early development

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

• Martin Hofmann, Thomas Streicher, The groupoid model refutes uniqueness of identity proofs, Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science (1994) [doi:10.1109/LICS.1994.316071]

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

  see also:

  • Martin Hofmann, The groupoid interpretation of type theory, a personal retrospective, talk at HoTT at DMV2015 (2015) [slides]

  • Ethan Lewis, Max Bohnet, The groupoid model of type theory, seminar notes (2017) [pdf, pdf]

• Steve Awodey, Homotopy and Type Theory, grant proposal project description (2009) [pdf]

• Vladimir Voevodsky, Univalent Foundations Project (2010) [pdf, pdf]

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

• Steve Awodey, Type theory and homotopy, in: Epistemology versus Ontology Springer (2012) 183-201 [arXiv:1010.1810, doi:10.1007/978-94-007-4435-6_9]

For more on the early history see also:

• Thorsten Altenkirch, Martin Hofmann’s contributions to type theory: Groupoids and univalence, Mathematical Structures in Computer Science 31 9 (2021) 953-957 [doi:10.1017/S0960129520000316]

Introductions

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

• Michael Shulman, Homotopy Type Theory: A synthetic approach to higher equalities (arXiv:1601.05035)

and one with an emphasis on synthetic geometry:

• Michael Shulman, Homotopy type theory: the logic of space, in Gabriel Catren, Mathieu Anel (eds.) New Spaces for Mathematics and Physics (arXiv:1703.03007)

More technical introductions:

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

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

• Dan Licata, Programming in Homotopy Type Theory, Talk at IFIP Working Group 2.8 meeting, November, 2012 (pdf, pdf)

On synthetic homotopy theory in homotopy type theory:

• Guillaume Brunerie, Dan Licata, Peter LeFanu Lumsdaine: Homotopy theory in type theory, 2013 (pdf slides, pdf, blog entry 1, blog entry 2)

  (focus on synthetic homotopy theory)

• Vladimir Voevodsky, Univalent foundations

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

• Vladimir Voevodsky, Univalent foundations, talk IAS, March 2014 (pdf, video)

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

• 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)

• Cecilia Flori, Tobias Fritz, Homotopy Type Theory: Univalent Foundations of Mathematics, lecture notes (2014) [pdf, webpage]

• Daniel Grayson, An introduction to univalent foundations for mathematicians (2017) [arXiv:1711.01477]

• Egbert Rijke, Introduction to Homotopy Type Theory (2019) (web, pdf, GitHub)

• Egbert Rijke, Classifying Types (arXiv:1906.09435)

• David Jaz Myers, How do you identify one thing with another? – an intro to Homotopy Type Theory, talk in Prof. Sadok Kallel‘s seminar at American University of Sharjah (10 Apr 2023) [slides: pdf]

An introduction to the notion of equivalence in HoTT:

• Andrej Bauer, Introduction to homotopy type theory (2019) [YT]

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

An computer science oriented introduction to HoTT:

• Bob Harper, Homotopy Type Theory (web)

An introduction to HoTT through Agda:

• Martín Escardó, Introduction to Univalent Foundations of Mathematics with Agda [arXiv:1911.00580, webpage]

An introduction to homotopy theory through type theory:

• Andrej Bauer, Homotopy (type) theory (web)

• Egbert Rijke, Introduction to Homotopy Type Theory (web)

Gentle invitation to some basics:

• Andrej Bauer, What is an explicit bijection?, talk at FPSAC 2019 (slides pdf, video recording)

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

• 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 .

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

• What I wish I knew when learning HoTT.

Forums dedicated to homotopy type theory

• The Homotopy Type Theory Google Group

• The HoTT Cafe Google Group

• The HoTT Zulip Chat

The HoTT research group at Carnegie Mellon University:

• CMU website

The HoTT electronic seminar talks:

• HoTTEST

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: Giovanni Sambin et al. (ed.) , 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, pdf, doi:10.1093/oso/9780198501275.003.0008]

Generalization of this to strict ∞-groupoids were discussed in

• 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 types, Mathematical Proceedings of the Cambridge Philosophical Society 146 1 (2009) [arXiv:0709.0248, doi:10.1017/S0305004108001783]

and with more details in

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

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

• section 2 of (Shulman 12)

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 full model in the classical model structure on simplicial sets is due to

• Chris Kapulkin, Peter LeFanu Lumsdaine, The Simplicial Model of Univalent Foundations (after Voevodsky), Journal of the European Mathematical Society 23 (2021) 2071–2126 $[$arXiv:1211.2851, doi:10.4171/jems/1050$]$

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:

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

• Thomas Streicher, A model of type theory in simplicial sets: A brief introduction to Voevodsky’s homotopy type theory, Journal of Applied Logic 12 1 (2014) 45-49 [doi:10.1016/j.jal.2013.04.001]

• 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).

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

• Michael Shulman, All $(\infty,1)$-toposes have strict univalent universes (arXiv:1904.07004).

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

• Denis-Charles Cisinski, Univalent universes for elegant models of homotopy types (arXiv:1406.0058)

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

• Marc Bezem, Thierry Coquand, Simon Huber, A model of type theory in cubical sets, 2013 (web, pdf)

• Ambrus Kaposi, Thorsten Altenkirch, A syntax for cubical type theory (pdf)

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

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

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

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

• Voevodsky, Vladimir and Ahrens, Benedikt and Grayson, Daniel and others, UniMath, GitHub link.

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:

• homotopy groups of spheres in HoTT

On Whitehead's theorem:

• Dan’s proof for n-types.

On Eilenberg-MacLane spaces:

• Dan’s construction.

• $K(G,n)$ is a spectrum, formalized

On ordinary cohomology:

• Deriving cohomology theories from spectra

• Mayer-Vietoris sequence, with exposition

• Cohomology of the n-torus, which could be easily extended to any finite product of spheres.

• to do:

  • cohomology with finite coefficients, all we need is the boring work of defining $\mathbb{Z}/p\mathbb{Z}$ as an explicit group.

  • Calculate some more cohomology groups.

  • Compute the loop space of this construction and use it to define spectra.

On the Freudenthal suspension theorem:

• Implies $\pi_k(S^n) = \pi_{k+1}(S^{n+1})$ whenever $k \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 $2n$-connected.

On homotopy limits:

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

On the van Kampen theorem:

• Mike’s proofs are in the book and Favonia formalized it. {{deadlink}}

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).