User:Michael Shulman/draft Homotopy Type Theory and Univalent Foundations

Cover of Homotopy Type Theory: Univalent Foundations of Mathematics.

In mathematical logic and computer science, Homotopy Type Theory (HoTT) refers to various lines of development of intensional type theory, based on the interpretation of types as objects to which the ideas of (abstract) homotopy theory apply. It includes, among other lines of work, the construction of homotopical and higher-categorical models for such type theories; the use of type theory as a logic (or internal language) for abstract homotopy theory and higher category theory; the development of mathematics within a type-theoretic foundation (including both previously existing mathematics and new mathematics that homotopical types make possible); and the formalization of each of these in computer proof assistants.

Univalent Foundations (UF) is a project that uses such systems as a foundation for mathematics whose basic objects behave like homotopy types (or, equivalently, ∞-groupoids). This is inspired both by the old Platonic ideas of Hermann Grassmann and Georg Cantor and by the "categorical" mathematics in the style of Alexander Grothendieck, and is compatible with mathematical structuralism in the categorical sense. Univalent foundations also emphasizes the practicality of this system for computer formalization of mathematics using proof assistants such as Coq and Agda.

There is a large overlap between the work referred to as "homotopy type theory" and "univalent foundations". Although neither term is precisely delineated, and they are sometimes used interchangeably, the choice of usage also sometimes corresponds to differences in viewpoint and emphasis. As such, this article may not represent the views of all researchers in the fields equally.

History

Prehistory: the groupoid model

At one time the idea that types in intensional type theory with their identity types could be regarded as groupoids was mathematical folklore. It was first made precise semantically in the 1998 paper of Hofmann and Streicher called "The groupoid interpretation of type theory", in which they showed that intensional type theory had a model in the category of groupoids. This was the first truly "homotopical" model of type theory, albeit only "1-dimensional" (the traditional models in the category of sets being homotopically 0-dimensional).

Their paper also foreshadowed several later developments in homotopy type theory. 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 would propose 10 years later. (The axiom for 1-types is notably simpler to formulate, however, since a coherent notion of "equivalence" is not required.) They also defined "categories with isomorphism as equality" and conjectured that in a model using higher-dimensional groupoids, for such categories one would have "equivalence is equality"; this was later proven by Ahrens, Kapulkin, and Shulman.

Model categories and higher groupoids

The first higher-dimensional models of intensional type theory were probably constructed by Michael Warren in 2005 using Quillen model categories. These results were presented at the conference FMCS 2006 at which Warren gave a talk entitled "Homotopy models of intensional type theory" and published in his thesis prospectus.

The idea of a relation between homotopy theory and type theory was also being investigated from other directions by many other researchers at the time, such as Richard Garner, Benno van den Berg, Thomas Streicher, and Peter Lumsdaine. It was discussed at several meetings, such as workshop about identity types at Uppsala University in 2006. For example, van den Berg conjectured in 2006 that the tower of identity types of a type in intensional type theory should have the structure of a ∞-groupoid in the "globular, algebraic" sense of Michael Batanin. This was later proven independently by van den Berg and Garner and by Peter Lumsdaine

At the PSSL86 in 2007, Steve Awodey (Warren's advisor) gave a talk entitled "Homotopy type theory" (this may have been the first public usage of that term, which was coined by Awodey). 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 and published in 2009; a more detailed version appeared in Warren's thesis "Homotopy theoretic aspects of constructive type theory" in 2008.

Univalent foundations

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. He originally attempted to create foundations of mathematics based on higher category theory, using ideas related to those that Michael Makkai expressed in his visionary paper known as FOLDS. Eventually, however, Voevodsky came to the conclusion that the "higher dimensional analogs of sets" should be ∞-groupoids, with categories being considered instead as higher-dimensional analogs of partially ordered sets. The philosophical connections between univalent foundations and earlier ideas are discussed in Voevodsky's 2014 Bernays lectures.

In September 2006, Voevodsky posted to the Types mailing list "A very short note on homotopy lambda calculus", which outlined a possible model of type theory in Kan simplicial sets. This included a syntactic definition of "equality types" that were claimed to be interpreted by path-spaces, but did not consider Per Martin-Löf's rules for identity types. It also stratified the universes by homotopy dimension in addition to size, an idea that later would be mostly discarded, and introduced the concept of a univalent fibration, whose associated fibration of pairwise homotopy equivalences between the fibers is equivalent to the path-space fibration of the base.

In 2009, Voevodsky recognized that univalence could be expressed using Martin-Lof's identity types, and proved, using an idea of A. K. Bousfield, that the universal Kan fibration was univalent. He also observed that it could also be used to resolve the coherence problems for a model of type theory in Kan complexes. Finally, he found a way to formulate univalence by adding an axiom to the existing Martin-Löf type theory by defining "equivalences" syntactically, thereby generalizing Hofmann and Streicher's "universe extensionality" to higher dimensions. This put all the main pieces in place for a foundational system of mathematics based on type theory, which Voevodsky called "univalent foundations".

He then began developing mathematics in univalent foundations, using the proof assistant Coq. This led to the library later called "Foundations" and eventually "UniMath". Originally, Voevodsky's goal was to enable classical pure mathematicians to use computers to verify their theorems and constructions, but while writing the Foundations library he discovered that the new foundations were inherently constructive (see below).

Further developments

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 and his Coq code to a group including Awodey, Warren, Lumsdaine, and Robert Harper, Dan Licata, Michael Shulman, and others. This meeting produced the outlines of a proof (by Warren, Lumsdaine, Licata, and Shulman) that every homotopy equivalence is an equivalence in Voevodsky's sense. Soon afterwards, Voevodsky proved that the univalence axiom implies function extensionality.

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, entitled "The homotopy interpretation of constructive type theory". As part of a Coq tutorial for this workshop, Andrej Bauer wrote a small Coq library based on Voevodsky's ideas; this would eventually become the kernel of the first version of the "HoTT" Coq library.

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. The participants also formulated a list of important open questions, such as whether the univalence axiom satisfies canonicity (still open, although some special cases have been resolved positively), whether the univalence axiom has nonstandard models (since answered positively by Shulman), and how to define (semi)simplicial types (still open in MLTT, although it can be done in Voevodsky's Homotopy Type System (HTS), a type theory with two equality types).

Soon after the Oberwolfach workshop, the Homotopy Type Theory website and blog was established, and the subject began to be popularized under that name. An idea of some of the important progress during this period can be obtained from the blog history.

Special Year on Univalent Foundations of Mathematics

An animation showing development of the HoTT Book on the GitHub repository by the participants in the Univalent Foundations Special Year project.

In 2012-13 researchers at the Institute for Advanced Study held A Special Year on Univalent Foundations of Mathematics. The special year brought together researchers in topology, computer science, category theory, and mathematical logic. The program was organized by Steve Awodey, Vladimir Voevodsky and Thierry Coquand.

During the program Peter Aczel, who was one of the participants, initiated a working group which investigated how to do type theory informally but rigorously, in a style that is analogous to ordinary mathematicians doing set theory. After initial experiments, it became clear that this was not only possible but highly beneficial. These experiments eventually coalesced into a book which grew into an exposition of the foundational aspects of the subject, including much of the progress made during the special year. Many other participants of the project 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.

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. In particular, Licata's isolation of the "encode-decode method" from Shulman's proof that the fundamental group of the circle is the integers kickstarted an explosion of theorems in "synthetic homotopy theory".

As can be seen from the titles of the special year and the book, the phrase "univalent foundations" has sometimes been used interchangeably with "homotopy type theory",. At other times, this phrase was used to refer only to its use as a foundational system (excluding, for example, the study of model-categorical semantics or computational metatheory). More recently, Voevodsky has tried to reserve the term "univalent foundations" for work that follows more closely the line of his original vision, such as the UniMath library of formalized mathematics. Currently there does not seem to be consensus among researchers as to the exact meaning and relationship of the phrases "homotopy type theory" and "univalent foundations".

Official participants in the special year

• Peter Aczel
• Benedikt Ahrens
• Thorsten Altenkirch
• Steve Awodey
• Bruno Barras
• Andrej Bauer
• Yves Bertot
• Marc Bezem
• Thierry Coquand
• Eric Finster
• Daniel Grayson
• Hugo Herbelin
• André Joyal
• Dan Licata
• Peter Lumsdaine
• Assia Mahboubi
• Per Martin-Löf
• Sergey Melikhov
• Alvaro Pelayo
• Andrew Polonsky
• Michael Shulman
• Matthieu Sozeau
• Bas Spitters
• Benno van den Berg
• Vladimir Voevodsky
• Michael Warren
• Noam Zeilberger

ACM Computing Reviews listed the book as a notable 2013 publication in the category "mathematics of computing".

Key concepts

Intensional type theory	Homotopy theory
types $A$	spaces $A$
terms $a$	points $a$
$a:A$	$a\in A$
dependent type $x:A\ \vdash \ B(x)\$	fibration $B\to A$
identity type $\mathrm {Id} _{A}(a,b)$	path space
$p:\mathrm {Id} _{A}(a,b)$	path $p:a\rightsquigarrow b$
$\alpha :\mathrm {Id} _{\mathrm {Id} _{A}(a,b)}(p,q)$	homotopy $\alpha :p\Rightarrow q$

Paths

The fundamental concept of homotopy type theory is Martin-Lof's identity type $a=b$. In line with the Propositions as types principle, Martin-Lof regarded this as the type of "proofs" (or "witnesses") that $a$equals $b$. In HoTT, however, this type is often called a path type, since it is thought of as the type of all paths from the point $a$ to the point $b$. (Therefore, a proof that a point $a$ equals a point $b$ is the same thing as a path from the point $a$ to the point $b$.) For any point $a$, there exists a path of type $a=a$, corresponding to the reflexive property of equality. A path of type $a=b$ can be inverted, forming a path of type $b=a$, corresponding to the symmetric property of equality. Two paths $a=b$ and $b=c$ can be concatenated, forming a path of type $a=c$; this corresponds to the transitive property of equality.

Most importantly, given a path $a=b$, and a proof of some property $P(a)$, the proof can be "transported" along the path $a=b$, forming a proof of the property $P(b)$. (Equivalently stated, an object of type $P(a)$ can be turned into an object of type $P(b)$.) This corresponds to the substitution property of equality. Here, an important difference between HoTT and classical mathematics comes in. In classical mathematics, once the equality of two values $a$ and $b$ has been established, $a$ and $b$ may be used interchangeably thereafter, with no regard to any distinction between them. In homotopy type theory, however, there may be multiple different paths $a=b$, and transporting an object along two different paths will yield two different results. Therefore, in homotopy type theory, when applying the substitution property, it is necessary to state which path is being used.

h-levels (n-types)

One of Voevodsky's 2009 insights, which enabled the syntactic formulation of univalence and the development of the Foundations library, was a way to define the notion of homotopy $n$-type internally, thereby stratifying the universe of types by "homotopy dimension". Voevodsky called these "h-levels" and started numbering them from 0, but many other researchers in the field use the more traditional terminology "homotopy $n$-type", which begins numbering from -2.

The bottom rung of the ladder is h-level 0 (the homotopy (-2)-types). These types are equal to the one point type, and are also called "contractible types".

The next rung is h-level 1, a.k.a. homotopy (-1)-types. These are the types in which any two elements are equal. (If one assumes the Law of excluded middle, then every (-1)-type is either contractible or empty.) These types are also called "propositions" or "mere propositions" or "h-propositions", and they play roughly the same role as propositions in classical predicate logic, being "proof-irrelevant". The idea that only a subclass of types should represent propositions had appeared earlier. Currently there is no consensus among researchers in the field on whether or not all types should be allowed to be "used as propositions" in HoTT.

Types of h-level 2 (a.k.a. homotopy 0-types) are called "sets" or "h-sets". For example, the type of natural numbers is a set, as is the type of real numbers, and any type with decidable equality ("Hedberg's theorem"). Practically all of "traditional" mathematics can be formalized inside these sets; in particular, they satisfy the axioms of Lawvere's "Elementary Theory of the Category of Sets". Voevodsky has claimed that this univalent formalization of sets is the best available environment today for formal reasoning about all aspects of set-theoretical mathematics, both constructive and classical.

Types of higher h-level behave like higher homotopy types or higher groupoids, and can be used to develop mathematics in new "synthetic" ways. For example, "categories" are defined in univalent foundations to have a type of objects that is of h-level 3 (i.e. a homotopy 1-type), so that paths therein can be identified with categorical isomorphisms; the structure making a 1-type into a category is closely analogous to that making a set into a poset. The resulting theory of categories is different from the set-theoretic theory of categories in certain ways, including a new distinction between pre-categories and categories.

Higher types can also be used to do "synthetic homotopy theory". For example, with higher inductive types one can define types that act like the spheres in classical homotopy theory, and calculate homotopy groups of spheres internally in type theory.

The univalence axiom

The univalence axiom states that for types $A$ and $B$, the canonical map

$(A=B)\to (A\simeq B)$

is an equivalence. Here $A\simeq B$ is the type of equivalences from $A$ to $B$. "In other words, identity is equivalent to equivalence. In particular, one may say that 'equivalent types are identical'."

Higher inductive types

Higher inductive types (HITs) are an enhancement to inductive types which allow constructors taking values in the path-types and iterated path-types of the type being defined, rather than the type itself. This corresponds roughly to "cell complexes" in classical homotopy theory. Applications of HITs include the truncation into $n$-types (in particular, the truncation to propositions, a.k.a. "squash" or "bracket"), colimits of types (e.g. pushouts and coequalizers), the construction of particular higher homotopy types (such as spheres and tori), and localizations. HITs are central to synthetic homotopy theory, but are not used in univalent foundations as Voevodsky envisions it (e.g. the UniMath library).

Semantics

The central problem to deal with in the construction of higher-dimensional models of type theory is coherence, notably the substitution property for the eliminator of the intensional identity type. Without this, only a weaker "type theory" lacking substitution can actually be modeled. The original models of Awodey and Warren in general model categories were not coherent; Warren's only fully coherent higher-dimensional models used strict higher groupoids. For the classical homotopy theory (presented by topological spaces or simplicial sets), the problem was first resolved by Voevodsky in 2009 using the universal Kan fibration (and then again in 2010, differently, by van den Berg and Garner). A reasonably general solution, building on Voevodsky's construction, was eventually given by Lumsdaine and Warren in 2014.

A detailed account of the univalent model of the Martin-Löf type theory with values in Kan simplicial sets can be found in a paper by Chris Kapulkin, Peter LeFanu Lumsdaine and Vladimir Voevodsky. Univalent models with values in the categories of inverse diagrams of simplicial sets (and, later, elegant Reedy presheaves) were constructed by Michael Shulman. In particular, these models show that the univalence axiom is independent of the Law of excluded middle for h-propositions.

More recently, a univalent model of Martin-Löf type theory in cubical sets was constructed by Marc Bezem, Thierry Coquand and Simon Huber. Unlike the original model in simplicial sets that relies on the axiom of choice, the cubical model is constructed in a constructive meta-theory. The ideas of this paper are now being developed in several directions including the development of the cubical type theory.

An open problem in HoTT is to construct a fully coherent model of type theory with the univalence axiom in (a model category presentation of) an arbitrary ∞-topos. (The coherence theorem of Lumsdaine and Warren shows how to do this for type theory without universes.)

Constructivity

Like the Martin-Löf type theory on which it is based, homotopy type theory and univalent foundations is naturally constructive, in the "agnostic" sense that it does not assert classical axioms such as the Law of excluded middle or the Axiom of choice. It is, however, fully compatible with these axioms (at least when they are stated for h-propositions, which most researchers in the field consider to be the "correct" way to do it). Thus, although HoTT and UF are constructive by default, classical mathematics can easily be formalized in them as well.

There is also a "positive" sort of constructivity meaning that there is an algorithm to compute the value of terms. This is an open problem for HoTT, but progress is being made (e.g. the constructive cubical model mentioned above).

See also

• Calculus of constructions
• Curry–Howard correspondence
• Intuitionistic type theory
• Homotopy hypothesis

Bibliography

• Homotopy Type Theory: Univalent Foundations of Mathematics. The Univalent Foundations Program. Institute for Advanced Study.
• S. Awodey and M. A. Warren (2009), Homotopy theoretic models of identity types, Mathematical Proceedings of the Cambridge Philosophical Society.
• Awodey, Steve (2012). "Type theory and homotopy". In Dybjer, P.; Lindström, Sten; Palmgren, Erik; Sundholm, G. (eds.). Epistemology versus Ontology (PDF). Logic, Epistemology, and the Unity of Science. Springer Netherlands. pp. 183–201. doi:10.1007/978-94-007-4435-6_9. ISBN 978-94-007-4434-9.
• Martin Hofmann and Thomas Streicher (1996), 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.
• Egbert Rijke (2012) Homotopy Type Theory, Masters Thesis, Utrecht University.
• Voevodsky, Vladimir (2006), A very short note on homotopy lambda calculus (PDF)
• Voevodsky, Vladimir (2010), The equivalence axiom and univalent models of type theory
• Michael A. Warren (2008), Homotopy theoretic aspects of constructive type theory, Ph.D. thesis, Carnegie Mellon University.

Libraries of formalized mathematics

• Foundations library (2010-current)
• HoTT Coq library (2011-current)
• HoTT-Agda library (2011-current)
• P-adics library (2011-2012)
• RezkCompletion library
• Ktheory library
• UniMath library (2014-current)

External links

• Homotopy Type Theory
• Homotopy type theory at the nLab
• Homotopy type theory wiki
• Vladimir Voevodsky's webpage on the Univalent Foundations
• Homotopy Type Theory and the Univalent Foundations of Mathematics by Steve Awodey
• "Constructive Type Theory and Homotopy" – Video lecture by Steve Awodey at the Institute for Advanced Study
• #hott ^connect Homotopy Type Theory IRC channel

Category:Foundations of mathematics Category:Type theory Category:Homotopy theory Category:Formal methods Category:Articles containing video clips