Homotopy type theory

There is a large overlap between the work referred to as homotopy type theory, and that called the univalent foundations project.

Although neither is precisely delineated, and the terms are sometimes used interchangeably, the choice of usage also sometimes corresponds to differences in viewpoint and emphasis.

It was first made precise semantically in the 1994 paper of Martin Hofmann and Thomas Streicher called "The groupoid model refutes uniqueness of identity proofs",[2] in which they showed that intensional type theory had a model in the category of groupoids.

For instance, they noted that the groupoid model satisfies a rule they called "universe extensionality", which is none other than the restriction to 1-types of the univalence axiom that Vladimir Voevodsky proposed ten years later.

These results were first presented in public at the conference FMCS 2006[5] at which Warren gave a talk titled "Homotopy models of intensional type theory", which also served as his thesis prospectus (the dissertation committee present were Awodey, Nicola Gambino and Alex Simpson).

At the same conference Benno van den Berg gave a talk titled "Types as weak omega-categories" where he outlined the ideas that later became the subject of a joint paper with Richard Garner.

Awodey and Warren summarized their results in the paper "Homotopy theoretic models of identity types", which was posted on the ArXiv preprint server in 2007[13] and published in 2009; a more detailed version appeared in Warren's thesis "Homotopy theoretic aspects of constructive type theory" in 2008.

At about the same time, Vladimir Voevodsky was independently investigating type theory in the context of the search of a language for practical formalization of mathematics.

Even the definition of the model of TS in the homotopy category is non-trivial" referring to the complex coherence issues that were not resolved until 2009.

In particular, the idea that univalence can be introduced simply by adding an axiom to the existing Martin-Löf type theory appeared only in 2009.

This enabled him to give a syntactic statement of univalence, generalizing Hofmann and Streicher's "universe extensionality" to higher dimensions.

He was also able to use these definitions of equivalences and contractibility to start developing significant amounts of "synthetic homotopy theory" in the proof assistant Coq; this formed the basis of the library later called "Foundations" and eventually "UniMath".

[19] Unification of the various threads began in February 2010 with an informal meeting at Carnegie Mellon University, where Voevodsky presented his model in Kan complexes to a group including Awodey, Warren, Lumsdaine, Robert Harper, Dan Licata, Michael Shulman, and others.

The next pivotal event was a mini-workshop at the Mathematical Research Institute of Oberwolfach in March 2011 organized by Steve Awodey, Richard Garner, Per Martin-Löf, and Vladimir Voevodsky, titled "The homotopy interpretation of constructive type theory".

One of the most important things to come out of the Oberwolfach meeting was the basic idea of higher inductive types, due to Lumsdaine, Shulman, Bauer, and Warren.

Soon after the Oberwolfach workshop, the Homotopy Type Theory website and blog[26] was established, and the subject began to be popularized under that name.

[27] The phrase "univalent foundations" is agreed by all to be closely related to homotopy type theory, but not everyone uses it in the same way.

[28] As Voevodsky's work became integrated with the community of other researchers working on homotopy type theory, "univalent foundations" was sometimes used interchangeably with "homotopy type theory",[29] and other times to refer only to its use as a foundational system (excluding, for example, the study of model-categorical semantics or computational metatheory).

[29] In 2012–13 researchers at the Institute for Advanced Study held "A Special Year on Univalent Foundations of Mathematics".

[31] The special year brought together researchers in topology, computer science, category theory, and mathematical logic.

Many other participants of the project then joined the effort with technical support, writing, proof reading, and offering ideas.

Unusually for a mathematics text, it was developed collaboratively and in the open on GitHub, is released under a Creative Commons license that allows people to fork their own version of the book, and is both purchasable in print and downloadable free of charge.

[33][34][35] More generally, the special year was a catalyst for the development of the entire subject; the HoTT Book was only one, albeit the most visible, result.

A "mere proposition" is any type which either is empty, or contains only one point with a trivial path space.

"[29]: 4 Martín Hötzel Escardó has shown that the property of univalence is independent of Martin-Löf Type Theory (MLTT).

HoTT adopts the univalence axiom, which relates the equality of logical-mathematical propositions to homotopy theory.

In homotopy type theory, this is taken to mean that the two shapes which represent the values of the symbols are topologically equivalent.

In set theory, this information would have to be defined additionally, which, advocates argue, makes the translation of mathematical propositions into programming languages more difficult.

[38] As of 2015, intense research work was underway to model and formally analyse the computational behavior of the univalence axiom in homotopy type theory.

[40] However, it is believed that certain objects, such as semi-simplicial types, cannot be constructed without reference to some notion of exact equality.