Homotopy type theory#Higher inductive types

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 1994 paper of Martin Hofmann and Thomas Streicher called "The groupoid model refutes uniqueness of identity proofs",{{Cite book |last1=Hofmann |first1=M. |last2=Streicher |first2=T. |title=Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science |chapter=The groupoid model refutes uniqueness of identity proofs |date=1994 |chapter-url=https://ieeexplore.ieee.org/document/316071 |pages=208–212 |doi=10.1109/LICS.1994.316071|isbn=0-8186-6310-3 |s2cid=19496198 }} 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 follow-up paper{{cite book |last1=Hofmann |first1=Martin |title=Twenty Five Years of Constructive Type Theory |last2=Streicher |first2=Thomas |date=1998 |publisher=Clarendon Press |isbn=978-0-19-158903-4 |editor1-last=Sambin |editor1-first=Giovanni |series=Oxford Logic Guides |volume=36 |pages=83–111 |chapter=The groupoid interpretation of type theory |mr=1686862 |author2-link=Thomas Streicher |editor2-last=Smith |editor2-first=Jan M. |chapter-url=https://books.google.com/books?id=pLnKggT_In4C&pg=PA83}} 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 proposed ten 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 Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman.{{cite journal |first1=Benedikt |last1=Ahrens |first2=Krzysztof |last2=Kapulkin |first3=Michael |last3=Shulman |author3-link=Michael Shulman (mathematician)|title=Univalent categories and the Rezk completion |journal=Mathematical Structures in Computer Science |volume=25 |year=2015|issue= 5|pages= 1010–1039|arxiv=1303.0584 |doi=10.1017/S0960129514000486|mr=3340533|s2cid=1135785 }}

The first higher-dimensional models of intensional type theory were constructed by Steve Awodey and his student Michael Warren in 2005 using Quillen model categories. These results were first presented in public at the conference FMCS 2006{{cite web | url=http://pages.cpsc.ucalgary.ca/~robin/FMCS/FMCS_06/FMCS06.html | title=Foundational Methods in Computer Science 2006, University of Calgary, June 7th - 9th, 2006 | publisher=University of Calgary | accessdate=6 June 2021 }} 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). A summary is contained in Warren's thesis prospectus abstract.{{cite thesis |first=Michael A. |last=Warren |title=Homotopy Models of Intensional Type Theory |date=2006 |url=http://mawarren.net/papers/prospectus.pdf }}

At a subsequent workshop about identity types at Uppsala University in 2006{{cite web | url=http://www2.math.uu.se/~palmgren/itt/ | title=Identity Types - Topological and Categorical Structure, Workshop, Uppsala, November 13-14, 2006 | publisher=Uppsala University - Department of Mathematics | accessdate=6 June 2021 }} there were two talks about the relation between intensional type theory and factorization systems: one by Richard Garner, "Factorisation systems for type theory",[http://comp.mq.edu.au/~rgarner/Papers/Uppsala.pdf Richard Garner, Factorisation axioms for type theory] and one by Michael Warren, "Model categories and intensional identity types". Related ideas were discussed in the talks by Steve Awodey, "Type theory of higher-dimensional categories", and Thomas Streicher, "Identity types vs. weak omega-groupoids: some ideas, some problems". 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.

All early constructions of higher dimensional models had to deal with the problem of coherence typical of models of dependent type theory, and various solutions were developed. One such was given in 2009 by Voevodsky, another in 2010 by van den Berg and Garner.{{cite arXiv |first1=Benno van den |last1=Berg |first2=Richard |last2=Garner |title=Topological and simplicial models of identity types |date=27 July 2010 |eprint=1007.4638|class=math.LO }} A general solution, building on Voevodsky's construction, was eventually given by Lumsdaine and Warren in 2014.{{cite journal |first1=Peter LeFanu |last1=Lumsdaine |first2=Michael A. |last2=Warren |title=The local universes model: an overlooked coherence construction for dependent type theories |journal=ACM Transactions on Computational Logic |volume=16 |issue=3 |pages=1–31 |date=6 November 2014 |arxiv=1411.1736 |doi=10.1145/2754931|s2cid=14068103 }}

At the PSSL86 in 2007{{cite web | url=http://www.loria.fr/~lamarche/psslHomeEN.html | title=86th edition of the Peripatetic Seminar on Sheaves and Logic, Henri Poincaré University, September 8-9, 2007 | publisher=loria.fr | access-date=20 December 2014 | archive-date=17 December 2014 | archive-url=https://archive.today/20141217151510/http://www.loria.fr/~lamarche/psslHomeEN.html | url-status=dead }} Awodey gave a talk titled "Homotopy type theory" (this was the first public usage of that term, which was coined by Awodey[http://www.loria.fr/~lamarche/listPart.html Preliminary list of PSSL86 participants]). 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{{cite journal |first1=Steve |last1=Awodey |first2=Michael A. |last2=Warren |title=Homotopy theoretic models of identity types |date=3 September 2007 |arxiv=0709.0248 |doi=10.1017/S0305004108001783 |volume=146 |journal=Mathematical Proceedings of the Cambridge Philosophical Society |issue=1 |page=45|bibcode=2008MPCPS.146...45A |s2cid=7915709 }} 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. In September 2006 he posted to the Types mailing list "A very short note on homotopy lambda calculus",{{cite web | url=http://math.ucr.edu/home/baez/Voevodsky_note.ps | title=A very short note on homotopy λ-calculus | first=Vladimir | last=Voevodsky | date=27 September 2006 | publisher=ucr.edu | accessdate=6 June 2021}} which sketched the outlines of a type theory with dependent products, sums and universes and of a model of this type theory in Kan simplicial sets. It began by saying "The homotopy λ-calculus is a hypothetical (at the moment) type system" and ended with "At the moment much of what I said above is at the level of conjectures. 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. This note included a syntactic definition of "equality types" that were claimed to be interpreted in the model 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 was mostly discarded.

On the syntactic side, Benno van den Berg conjectured in 2006 that the tower of identity types of a type in intensional type theory should have the structure of an ω-category, and indeed a ω-groupoid, in the "globular, algebraic" sense of Michael Batanin. This was later proven independently by van den Berg and Garner in the paper "Types are weak omega-groupoids" (published 2008),{{cite journal |first1=Benno |last1=van den Berg |first2=Richard |last2=Garner |title=Types are weak omega-groupoids |journal=Proceedings of the London Mathematical Society |volume=102 |issue=2 |pages=370–394 |date=1 December 2007 |arxiv=0812.0298 |doi=10.1112/plms/pdq026|s2cid=5575780 }} and by Peter Lumsdaine in the paper "Weak ω-Categories from Intensional Type Theory" (published 2009) and as part of his 2010 Ph.D. thesis "Higher Categories from Type Theories".{{cite web |first=Peter |last=Lumsdaine |title=Higher Categories from Type Theories |date=2010 |type=Ph.D. |publisher=Carnegie Mellon University |url=http://lib.rett.org.uk/~peterlefanulumsdaine/research/Lumsdaine-2010-Thesis.pdf |access-date=21 December 2014 |archive-date=21 December 2014 |archive-url=https://web.archive.org/web/20141221160345/http://lib.rett.org.uk/~peterlefanulumsdaine/research/Lumsdaine-2010-Thesis.pdf |url-status=dead }}

The concept of a univalent fibration was introduced by Voevodsky in early 2006.[https://github.com/vladimirias/2006_Mar_Homotopy_lambda_calculus Notes on homotopy lambda calculus, March 2006]

However, because of the insistence of all presentations of the Martin-Löf type theory on the property that the identity types, in the empty context, may contain only reflexivity, Voevodsky did not recognize until 2009 that these identity types can be used in combination with the univalent universes. 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.{{efn|name= univalenceIsaType |1= Univalence is a type, a property of the identity type IdU of a universe U —Martín Hötzel Escardó (2018){{rp|p.1}}}}{{efn|name= 2018formulation|1= "Univalence is a type, and the univalence axiom says that this type has some inhabitant."{{rp|p.1}}}}

Also in 2009, Voevodsky worked out more of the details of a model of type theory in Kan complexes, and observed that the existence of a universal Kan fibration could be used to resolve the coherence problems for categorical models of type theory. He also proved, using an idea of A. K. Bousfield, that this universal fibration was univalent: the associated fibration of pairwise homotopy equivalences between the fibers is equivalent to the paths-space fibration of the base.

To formulate univalence as an axiom Voevodsky found a way to define "equivalences" syntactically that had the important property that the type representing the statement "f is an equivalence" was (under the assumption of function extensionality) (-1)-truncated (i.e. contractible if inhabited). 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 Rocq (previously known as Coq); this formed the basis of the library later called "Foundations" and eventually "UniMath".[https://github.com/UniMath/UniMath GitHub repository, Univalent Mathematics]

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 version of Rocq, to a group including Awodey, Warren, Lumsdaine, 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 good coherent sense), based on the idea from category theory of improving equivalences to adjoint equivalences. 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, titled "The homotopy interpretation of constructive type theory".{{cite journal | url=https://hottheory.files.wordpress.com/2011/06/report-11_2011.pdf | title=Mini-Workshop: The Homotopy Interpretation of Constructive Type Theory | publisher=Mathematical Research Institute of Oberwolfach | doi=10.4171/OWR/2011/11 | date=27 February – 5 March 2011 | accessdate=6 June 2021 | last1=Awodey | first1=Steve | last2=Garner | first2=Richard | last3=Martin-Löf | first3=Per | last4=Voevodsky | first4=Vladimir | journal=Oberwolfach Reports | volume=8 | pages=609–638 }} As part of a Coq tutorial for this workshop, Andrej Bauer wrote a small Coq library[https://github.com/andrejbauer/Homotopy GitHub repository, Andrej Bauer, Homotopy theory in Coq] based on Voevodsky's ideas (but not actually using any of his code); this eventually became the kernel of the first version of the "HoTT" Coq library{{cite web | url=https://github.com/HoTT/HoTT/commit/1fb4ed9e5cdc5494f26ae6d13c4ebc851b81e1ba | publisher=GitHub | title=Basic homotopy type theory | first1=Andrej | last1=Bauer | first2=Vladimir | last2=Voevodsky | date=29 April 2011 | accessdate=6 June 2021 }} (the first commit of the latter[https://github.com/HoTT/HoTT GitHub repository, Homotopy type theory] by Michael Shulman notes "Development based on Andrej Bauer's files, with many ideas taken from Vladimir Voevodsky's files"). 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{{cite journal |first=Michael |last=Shulman |title=Univalence for inverse diagrams and homotopy canonicity |journal=Mathematical Structures in Computer Science |volume=25 |issue=5 |pages=1203–1277 |year=2015 |arxiv=1203.3253 |doi=10.1017/S0960129514000565|s2cid=13595170 }}{{cite web | url=https://www.cs.cmu.edu/~drl/pubs/lh112tt/lh112tt.pdf | title=Canonicity for 2-Dimensional Type Theory | first1=Daniel R. | last1=Licata | first2=Robert | last2=Harper | publisher=Carnegie Mellon University | date=21 July 2011 | accessdate=6 June 2021 }}), 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[http://homotopytypetheory.org Homotopy Type Theory and Univalent Foundations 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.[http://homotopytypetheory.org/blog Homotopy Type Theory blog]

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. It was originally used by Vladimir Voevodsky to refer to his vision of a foundational system for mathematics in which the basic objects are homotopy types, based on a type theory satisfying § the univalence axiom, and formalized in a computer proof assistant.[http://homotopytypetheory.org/ Type Theory and Univalent Foundations]

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", 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).[http://ncatlab.org/homotopytypetheory/show/References Homotopy Type Theory: References] For instance, the subject of the IAS special year was officially given as "univalent foundations", although a lot of the work done there focused on semantics and metatheory in addition to foundations. The book produced by participants in the IAS program was titled "Homotopy type theory: Univalent foundations of mathematics"; although this could refer to either usage, since the book only discusses HoTT as a mathematical foundation.

File:The making of HoTT book.webm

In 2012–13 researchers at the Institute for Advanced Study held "A Special Year on Univalent Foundations of Mathematics".[https://www.math.ias.edu/sp/univalent IAS school of mathematics: Special Year on The 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, Thierry Coquand and Vladimir Voevodsky.

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, and that a book (the so-called HoTT Book){{cite book|author=Univalent Foundations Program|title=Homotopy Type Theory: Univalent Foundations of Mathematics|year=2013|publisher=Institute for Advanced Study|url=http://homotopytypetheory.org/book/}}[http://homotopytypetheory.org/2013/06/20/the-hott-book/ Official announcement of The HoTT Book, by Steve Awodey, 20 June 2013] could and should be written. 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.{{cite journal |first=D |last=Monroe |title=A New Type of Mathematics? |journal=Comm ACM |volume=57 |issue=2 |pages=13–15 |year=2014 |doi=10.1145/2557446 |s2cid=6120947 |url=http://cacm.acm.org/magazines/2014/2/171675-a-new-type-of-mathematics/abstract|url-access=subscription }}{{cite web | url=https://golem.ph.utexas.edu/category/2013/06/the_hott_book.html | title=The HoTT Book | first=Mike | last=Shulman | publisher=The n-Category Café | via=University of Texas | date=20 June 2013 | accessdate=6 June 2021 }}{{cite web | url=http://math.andrej.com/2013/06/20/the-hott-book/ | title=The HoTT Book | first=Andrej | last=Bauer | date=20 June 2013 | publisher=Mathematics and Computation | accessdate=6 June 2021 }}

{{clear}}

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.

Official participants in the special year

{{div col|colwidth=18em}}

• 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
• Khem al-Khem Kardasheva
• Noam Zeilberger

{{div col end}}

ACM Computing Reviews listed the book as a notable 2013 publication in the category "mathematics of computing".ACM Computing Reviews. [http://computingreviews.com/recommend/bestof/notableitems_2013.cfm "Best of 2013"].

HoTT uses a modified version of the "propositions as types" interpretation of type theory, according to which types can also represent propositions and terms can then represent proofs. In HoTT, however, unlike in standard "propositions as types", a special role is played by 'mere propositions' which, roughly speaking, are those types having at most one term, up to propositional equality. These are more like conventional logical propositions than are general types, in that they are proof-irrelevant.

The fundamental concept of homotopy type theory is the path. In HoTT, the type $a\; =\; b$ is 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 of type $a\; =\; b$ resp. $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 $p:a=b$, and a proof of some property $P(a)$, the proof can be "transported" along the path $p$ to yield 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.

In general, a "proposition" can have multiple different proofs. (For example, the type of all natural numbers, when considered as a proposition, has every natural number as a proof.) Even if a proposition has only one proof $a$, the space of paths $a\; =\; a$ may be non-trivial in some way. A "mere proposition" is any type which either is empty, or contains only one point with a trivial path space.

Note that people write $a\; =\; b$ for $Id\_A(a,b)$,

thereby leaving the type $A$ of $a,\; b$ implicit.

Do not confuse it with $id\_A\; :\; A\backslash to\; A$, denoting the identity function on $A$.{{efn|name= ttConvention|1= Here the type theory convention is used, that type names begin with a capitalized letter, but that function names begin with a lower-case letter.}}

Two functions $f,g:A\backslash rightarrow\; B$ are homotopies by pointwise identification:{{r|hott|at=2.4.1}}

:$f\; \backslash sim\; g\; :\backslash equiv\; \backslash prod\_\{x:A\}\; f(x)\; =\; g(x)$

Equivalences between two types $A$ and $B$ belonging to some universe $U$ are defined by the functions $f:A\backslash rightarrow\; B$ together with the proof of having retractions and sections with respect to homotopies:{{r|hott|at=2.4.11,2.4.10}}

:$A\; \backslash simeq\; B\; :\backslash equiv\; \backslash sum\_\{f:A\backslash rightarrow\; B\}\; isequiv(f)$, where

:$isequiv(f)\; :\backslash equiv\; (\; \backslash sum\_\{g:B\backslash rightarrow\; A\}\; (f\backslash circ\; g)\; \backslash sim\; id\_B\; )\; \backslash times\; (\; \backslash sum\_\{h:B\backslash rightarrow\; A\}\; (h\backslash circ\; f)\; \backslash sim\; id\_A\; )$

Together with the univalence axiom below, one receives a non-circular "$\backslash infty$-isomorphism" expanded to identity.[http://www.andrew.cmu.edu/user/awodey/preprints/uapl.pdf] Steve Awodey. Univalence as a principle of logic. Indagationes Mathematicae: Special Issue L.E.J. Brouwer, 50 years later, D. van Dalen, et al. (ed.s), 2018. Preprint.

:$A\; \backslash simeq\; B\; :\backslash equiv\; \backslash text\{there\; are\}\; f\; :\; A\; \backslash leftrightarrows\; B\; :\; g\backslash \; \backslash text\{with\}\backslash \; g\; \backslash circ\; f\; \backslash simeq\; id\_A\backslash \; \backslash text\{and\}\backslash \; f\; \backslash circ\; g\; \backslash simeq\; id\_B$

Having defined functions that are equivalences as above, one can show that there is a canonical way to turn paths to equivalences.

In other words, there is a function of the type

:$(A\; =\; B)\; \backslash to\; (A\; \backslash simeq\; B),$

which expresses that types $A,B$ that are equal are, in particular, also equivalent.

The univalence axiom states that this function is itself an equivalence.{{rp|115}}Martín Hötzel Escardó (October 18, 2018) [https://arxiv.org/pdf/1803.02294.pdf A self-contained, brief and complete formulation of Voevodsky’s Univalence Axiom]{{rp|4–6}} Therefore, we have

: $(A\; =\; B)\; \backslash simeq\; (A\; \backslash simeq\; B)$

"In other words, identity is equivalent to equivalence. In particular, one may say that 'equivalent types are identical'."{{rp|4}}

Martín Hötzel Escardó has shown that the property of univalence is independent of Martin-Löf Type Theory (MLTT).{{rp|6}}{{efn|name=HötzelEscardó2018|1= Martín Hötzel Escardó has shown that the property of univalence, "a property of the identity type IdU of a universe U",{{rp|4}} may or may not have an inhabitant. By the Univalence Axiom the type 'isUnivalent(U)' has an inhabitant; Hötzel Escardó notes that when reflection is the only way to construct elements of the identity type, other than univalence, one may construct a function J from the identity type, from reflection, and from J.{{rp|2.4 The identity type}} Hötzel Escardó proceeds to construct the univalence type, using repeated applications of J. When 'all types are sets' (denoted Axiom K),{{rp|2.4}} Axiom K implies the type 'isUnivalent(U)' does not have an inhabitant. Thus Hötzel Escardó finds the type 'isUnivalent(U)' is undecided in Martin-Löf Type Theory (MLTT).{{rp|3.2, p.6 The Univalence Axiom}} }}

This is because type equivalence is compatible with all constructions of the type theory{{r|hott|at=2.6-2.15}}.

Advocates claim that HoTT allows mathematical proofs to be translated into a computer programming language for computer proof assistants much more easily than before. They argue this approach increases the potential for computers to check difficult proofs.{{Cite web|url = https://www.rdworldonline.com/a-new-foundation-for-mathematics|title = A new foundation for mathematics|date = 3 September 2014|access-date = 29 July 2021|publisher = R&D Magazine|last = Meyer|first = Florian}} However, these claims aren't universally accepted and many research efforts and proof assistants don't make use of HoTT.

HoTT adopts the univalence axiom, which relates the equality of logical-mathematical propositions to homotopy theory. An equation such as $a=b$ is a mathematical proposition in which two different symbols have the same value. In homotopy type theory, this is taken to mean that the two shapes which represent the values of the symbols are topologically equivalent.

These equivalence relationships, ETH Zürich Institute for Theoretical Studies director Giovanni Felder argues, can be better formulated in homotopy theory because it is more comprehensive: Homotopy theory explains not only why "a equals b" but also how to derive this. 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.

As of 2015, intense research work was underway to model and formally analyse the computational behavior of the univalence axiom in homotopy type theory.{{Cite conference|url = http://dl.acm.org/citation.cfm?id=2676983|title = Higher Inductive Types as Homotopy-Initial Algebras|last = Sojakova|first = Kristina|date = 2015|conference = POPL 2015|doi = 10.1145/2676726.2676983|arxiv = 1402.0761}}

Cubical type theory is one attempt to give computational content to homotopy type theory.{{cite conference|title=Cubical Type Theory: a constructive interpretation of the univalence axiom|url=https://hal-iogs.archives-ouvertes.fr/INRIA/hal-01378906v2|last1=Cohen|first1=Cyril|last2=Coquand|first2=Thierry|last3=Huber|first3=Simon|last4=Mörtberg |first4=Anders|conference=TYPES 2015|year=2015}}

However, it is believed that certain objects, such as semi-simplicial types, cannot be constructed without reference to some notion of exact equality. Therefore, various two-level type theories have been developed which partition their types into fibrant types, which respect paths, and non-fibrant types, which do not. Cartesian cubical computational type theory is the first two-level type theory which gives a full computational interpretation to homotopy type theory.{{cite conference|title=Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities| last1=Anguili|first1=Carlo|last2=Favonia|last3=Harper|first3=Robert|conference=Computer Science Logic 2018|url=https://www.cs.cmu.edu/~rwh/papers/cartesian/paper.pdf|year=2018|access-date=26 Aug 2018}} (to appear)

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

{{Notelist}}

{{Reflist|30em}}

{{refbegin}}

• {{cite book | url=https://books.google.com/books?id=LkDUKMv3yp0C | title=Homotopy Type Theory: Univalent Foundations of Mathematics | author=The Univalent Foundations Program | publisher=Institute for Advanced Study | location=Princeton, NJ | year=2013 | mr=3204653}} ([https://web.archive.org/web/20170707022332/https://hott.github.io/book/nightly/hott-a4-1075-g3c53219.pdf GitHub version] cited in this article.)
• {{cite journal |first1=S. |last1=Awodey | author-link1=Steve Awodey |first2=M. A. |last2=Warren |title=Homotopy Theoretic Models of Identity Types |journal=Mathematical Proceedings of the Cambridge Philosophical Society |volume=146 |issue=1 |pages=45–55 |date=January 2009 |doi=10.1017/S0305004108001783 |arxiv=0709.0248 |bibcode=2008MPCPS.146...45A |s2cid=7915709 }} As [http://www.andrew.cmu.edu/user/awodey/preprints/homotopy.pdf PDF].
• {{Cite book |title = Epistemology versus Ontology |last = Awodey |first = Steve | author-link = Steve Awodey |publisher = Springer |year = 2012 |isbn = 978-94-007-4434-9 |pages = 183–201 |chapter = Type Theory and Homotopy |chapter-url = http://www.andrew.cmu.edu/user/awodey/preprints/TTH.pdf |editor-last = Dybjer |editor-first = P. |doi = 10.1007/978-94-007-4435-6_9 |editor2-last = Lindström |editor2-first = Sten |editor3-last = Palmgren |editor3-first = Erik |display-editors = 3 |editor4-last = Sundholm |editor4-first = G. |series = Logic, Epistemology, and the Unity of Science |citeseerx = 10.1.1.750.3626 |s2cid = 4499538 }}
• {{cite journal |last=Awodey |first=Steve | author-link=Steve Awodey |date=2014 |title=Structuralism, Invariance, and Univalence |journal=Philosophia Mathematica |volume=22 |issue=1 |pages=1–11 |doi=10.1093/philmat/nkt030 |citeseerx=10.1.1.691.8113 }}
• {{cite book |first1=Martin |last1=Hofmann |author-link2=Thomas Streicher |first2=Thomas |last2=Streicher |chapter=The groupoid interpretation of type theory |editor1-first=G. |editor1-last=Sambin |editor2-first=J.M. |editor2-last=Smith |title=Twenty Five Years of Constructive Type Theory |chapter-url=https://books.google.com/books?id=pLnKggT_In4C&pg=PA83 |date=1998 |publisher=Clarendon Press |isbn=978-0-19-158903-4 |pages=83–112 }} As [http://www.mathematik.tu-darmstadt.de/~streicher/venedig.ps.gz postscript].
• {{cite thesis |first=Egbert |last=Rijke |title=Homotopy Type Theory |date=2012 |type=Master's |publisher=Utrecht University |url=http://hottheory.files.wordpress.com/2012/08/hott2.pdf }}
• {{Citation | last1=Voevodsky | first1=Vladimir | author1-link=Vladimir Voevodsky | title = A Very Short Note on Homotopy Lambda Calculus | url = http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/Hlambda_short_current.pdf | year = 2006 }}
• {{Citation|last1=Voevodsky |first1=Vladimir |author1-link=Vladimir Voevodsky |title=The Equivalence Axiom and Univalent Models of Type Theory |arxiv=1402.5556 |year=2010 |bibcode=2014arXiv1402.5556V }}
• {{cite thesis |first=Michael A. |last=Warren |title=Homotopy Theoretic Aspects of Constructive Type Theory |date=2008 |type=Ph.D. |publisher=Carnegie Mellon University |url=http://www.andrew.cmu.edu/user/awodey/students/warren.pdf }}

{{refend}}

• David Corfield (2020), Modal Homotopy Type Theory: The Prospect of a New Logic for Philosophy, Oxford University Press.
• Egbert Rijke (2022), Introduction to Homotopy Type Theory, {{arxiv|2212.11082}}. Introductory textbook.

{{commons category}}

• {{official website|http://homotopytypetheory.org/|Homotopy Type Theory}}
• {{nlab|id=homotopy+type+theory|title=Homotopy type theory}}
• [http://ncatlab.org/homotopytypetheory/show/HomePage Homotopy type theory wiki]
• [http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html Vladimir Voevodsky's webpage on the Univalent Foundations]
• [http://www.andrew.cmu.edu/user/awodey/htt.html Homotopy Type Theory and the Univalent Foundations of Mathematics] by Steve Awodey
• [http://video.ias.edu/univalent/awodey "Constructive Type Theory and Homotopy"] – Video lecture by Steve Awodey at the Institute for Advanced Study

{{refbegin}}

• {{Citation|title =Foundations library (2010-current) |url=https://github.com/UniMath/UniMath/tree/master/UniMath/Foundations}}
• {{Citation|title =HoTT library (2011-current) |date=30 January 2022|url=https://github.com/HoTT/HoTT}}
• {{Citation|title=P-adics library (2011-2012)|url=https://github.com/UniMath/UniMath/tree/master/UniMath/PAdics}}
• {{Citation|title=RezkCompletion library |date=January 2022 |url=https://github.com/benediktahrens/rezk_completion }} (now integrated into UniMath, where further development takes place)
• {{Citation|title=Ktheory library|url=https://github.com/UniMath/UniMath/tree/master/UniMath/Ktheory}}
• {{Citation|title =UniMath library (2014-current) |date=25 January 2022|url=https://github.com/UniMath/UniMath}}

{{refend}}

{{Foundations-footer}}

Category:Foundations of mathematics

Category:Type theory

Category:Homotopy theory

Category:Formal methods

Category:Articles containing video clips