Homotopy Type Theory
References (Rev #60)

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!

Surveys

  • Type theory and homotopy. Steve Awodey, 2010. (To appear.) PDF
  • 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. 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. 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. Dan Grayson, arxiv
  • 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. Steve Awodey. arxiv, 2017

See also Philosophy, below.

Synthetic homotopy theory

Higher category theory

Homotopical ideas and truncations in type theory

General models

Univalence

Inductive and higher-inductive types

  • Inductive Types in Homotopy Type Theory. S. Awodey, N. Gambino, K. Sojakova. To appear in LICS 2012. arXiv
  • W-types in homotopy type theory. Benno van den Berg and Ieke Moerdijk, arXiv
  • Homotopy-initial algebras in type theory Steve Awodey, Nicola Gambino, Kristina Sojakova. arXiv, Coq code
  • The General Universal Property of the Propositional Truncation. Nicolai Kraus, arXiv
  • Non-wellfounded trees in Homotopy Type Theory. Benedikt Ahrens, Paolo Capriotti, Régis Spadotti. TLCA 2015, doi:10.4230/LIPIcs.TLCA.2015.17, arXiv
  • Constructing the Propositional Truncation using Non-recursive HITs. Floris van Doorn, arXiV
  • Constructions with non-recursive higher inductive types. Nicolai Kraus, LiCS 2016, pdf
  • The join construction. Egbert Rijke, arXiv
  • Semantics of higher inductive types. Michael Shulman and Peter LeFanu Lumsdaine, arXiv
  • A Descent Property for the Univalent Foundations, Egbert Rijke, doi
  • Impredicative Encodings of (Higher) Inductive Types. Steve Awodey, Jonas Frey, and Sam Speight. arxiv, 2018
  • W-Types with Reductions and the Small Object Argument, Andrew Swan, arxiv

Formalizations

  • An experimental library of formalized Mathematics based on the univalent foundations, Vladimir Voevodsky, Math. Structures Comput. Sci. 25 (2015), no. 5, pp 1278-1294, 2015. arXiv journal

  • A preliminary univalent formalization of the p-adic numbers. Álvaro Pelayo, Vladimir Voevodsky, Michael A. Warren, 2012. arXiv

  • Univalent categories and the Rezk completion. Benedikt Ahrens, Chris Kapulkin, Michael Shulman, Math. Structures Comput. Sci. 25 (2015), no. 5, 1010?1039. arXiv:1303.0584 (on internal categories in HoTT)

  • The HoTT Library: A formalization of homotopy type theory in Coq, Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Mike Shulman, Matthieu Sozeau, Bas Spitters, 2016 arxiv

Applications to computing

  • Homotopical patch theory. Carlo Angiuli, Ed Morehouse, Dan Licata, Robert Harper, PDF
  • Guarded Cubical Type Theory: Path Equality for Guarded Recursion, Lars Birkedal, Ale? Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi, arXiv

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. 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
  • 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. Dimitris Tsementzis. Forthcoming in Synthese; Pitt-PhilSci
  • Homotopy type theory: the logic of space. Michael Shulman. To appear in New Spaces in Mathematics and Physics: arxiv

Other:

  • 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, Type-Theoretically (Extended Abstract). Nicolai Kraus and Christian Sattler. arXiv

category: references

Revision on October 10, 2018 at 13:41:29 by Ali Caglayan. See the history of this page for a list of all contributions to it.