Homotopy Type Theory References (Rev #65, changes)

Showing changes from revision #64 to #65: Added | Removed | Changed

A roughly taxonomised listing of some of the papers on Homotopy Type Theory. Titles link to more details, bibdata, etc. Currently very incomplete; please add!

A good place to start

Surveys

• Type theory and homotopy.? Steve Awodey, 2010. (To appear.) PDF
• Homotopy type theory and Voevodsky's univalent foundations.?Homotopy type theory and Voevodsky’s univalent foundations. Álvaro Pelayo and Michael A. Warren, 2012. (Bulletin of the AMS, forthcoming) arXiv
• Voevodsky's Univalence Axiom in homotopy type theory.?Voevodsky’s Univalence Axiom in homotopy type theory. Steve Awodey, Álvaro Pelayo, and Michael A. Warren, October 2013, Notices of the American Mathematical Society 60(08), pp.1164-1167. arXiv
• Homotopy Type Theory: A synthetic approach to higher equalities. Michael Shulman. To appear in Categories for the working philosopher; arXiv
• Univalent Foundations and the UniMath library.?Univalent Foundations and the UniMath library. Anthony Bordg, 2017. PDF
• Homotopy type theory: the logic of space. Michael Shulman. To appear in New Spaces in Mathematics and Physics: arxiv
• An introduction to univalent foundations for mathematicians?An introduction to univalent foundations for mathematicians. Dan Grayson, arxiv
• A self-contained, brief and complete formulation of Voevodsky's Univalence Axiom?A self-contained, brief and complete formulation of Voevodsky’s Univalence Axiom. Martín Escardó, web, arxiv
• A proposition is the (homotopy) type of its proofs?A proposition is the (homotopy) type of its proofs. Steve Awodey. arxiv, 2017
• Homotopy Type Theory: Univalent Foundations of Mathematics, The Univalent Foundations Program, Institute for Advanced Study, 2013. homotopytypetheory.org/book

Philosophy

• Structuralism, Invariance, and Univalence?Structuralism, Invariance, and Univalence. Steve Awodey. Philosophia Mathematica (2014) 22 (1): 1-11. online
• Identity in Homotopy Type Theory, Part I: The Justification of Path Induction. James Ladyman and Stuart Presnell. Philosophia Mathematica (2015), online
• A synthetic approach to higher equalities?Homotopy Type Theory: A synthetic approach to higher equalities. Michael Shulman. To appear in Categories for the working philosopher; arXiv
• Univalent Foundations as Structuralist Foundations?Univalent Foundations as Structuralist Foundations. Dimitris Tsementzis. Forthcoming in Synthese; Pitt-PhilSci
• the logic of space?Homotopy type theory: the logic of space. Michael Shulman. To appear in New Spaces in Mathematics and Physics: arxiv

Other

• Martin-Löf Complexes?Martin-Löf Complexes.. S. Awodey, P. Hofstra and M.A. Warren, 2013, Annals of Pure and Applied Logic, 164(10), pp. 928-956. PDF, arXiv
• Space-Valued Diagrams?Space-Valued Diagrams, Type-Theoretically (Extended Abstract), Type-Theoretically (Extended Abstract). Nicolai Kraus and Christian Sattler?. arXiv