Homotopy type theory
In mathematical logic and computer science, homotopy type theory (HoTT) attempts to give an account of the semantics of intensional type theory using the framework of (abstract) homotopy theory, in particular Quillen model categories and weak factorization systems. Conversely, intensional type theory forms a logic (internal language) for homotopy theory.
|This section requires expansion. (September 2013)|
The Institute for Advanced Study held a special year for intensive work on developing homotopy type theory in the academic year 2012-2013, jointly organised by Steve Awodey, Thierry Coquand and Vladimir Voevodsky, which numerous mathematicians and computer scientists attended.
Out of this, a book, Homotopy Type Theory, was born. 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.
Also, unusually, key parts of the mathematics were implemented in the computer proof assistant Coq and Agda, where Agda is broadly equivalent to Coq but has a greater emphasis on functional programming than on constructing proofs through tactics. In both cases, type checking—or, viewed another way, computer proof verification—guarantees that the proofs were valid deductions, assuming that the proof assistant used was implemented correctly.
Open questions include a computational interpretation of homotopy type theory. Work is also underway to investigate new types of computer proof assistants with the goal of better supporting homotopy type theory.
|Intensional type theory||Homotopy theory|
|identity type||path space|
- weak ω-groupoid
- Homotopy hypothesis
- Univalence axiom
- Vladimir Voevodsky – Initiator of the Univalent Foundations of Mathematics research program.
- Calculus of constructions
- Intuitionistic type theory
- Curry–Howard isomorphism
References and further reading
- Homotopy Type Theory: Univalent Foundations of Mathematics. The Univalent Foundations Program. Institute for Advanced Study.
- Steve Awodey (2010). "Type theory and homotopy". To appear.
- 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.
- Michael A. Warren (2008), Homotopy theoretic aspects of constructive type theory, Ph.D. thesis, Carnegie Mellon University.
- S. Awodey and M. A. Warren (2009), Homotopy theoretic models of identity types, Mathematical Proceedings of the Cambridge Philosophical Society.
- Egbert Rijke (2012) Homotopy Type Theory, Masters Thesis, Utrecht University.
- Homotopy Type Theory
- Homotopy type theory in nLab
- 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
- Homotopy Type Theory Google Group
- Homotopy Type Theory IRC channel