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

See also Philosophy, below.

Synthetic homotopy theory

Higher category theory

Homotopical ideas and truncations in type theory

General models

Univalence

Inductive, coinductive, and higher-inductive types

Formalizations

Applications to computing

Cubical models and cubical type theory

Syntax of type theory

Strict equality types

Directed type theory

Cohesion and modalities

Theories and models

Computational interpretation

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

category: reference, navigation

Revision on February 14, 2019 at 10:24:12 by Ali Caglayan. See the history of this page for a list of all contributions to it.