Homotopy Type Theory
References (Rev #59)

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.

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

Synthetic homotopy theory

Higher category theory

  • 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)
  • A type theory for synthetic \infty-categories. Emily Riehl, Michael Shulman. arxiv, 2017
  • Univalent Higher Categories via Complete Semi-Segal Types. Paolo Capriotti, Nicolai Kraus, arxiv, 2017

Homotopical ideas and truncations in type theory

  • Generalizations of Hedberg?s Theorem. Nicolai Kraus, Martín Escardó, Thierry Coquand, and Thorsten Altenkirch.TLCA 2013, pdf
  • Notions of anonymous existence in Martin-Lof type theory. Nicolai Kraus, Martín Escardó, Thierry Coquand, and Thorsten Altenkirch. pdf
  • Idempotents in intensional type theory. Michael Shulman, arXiv
  • Functions out of Higher Truncations. Paolo Capriotti, Nicolai Kraus, and Andrea Vezzosi. CSL 2015 arxiv
  • Truncation levels in homotopy type theory. Nicolai Kraus, PhD Thesis: University of Nottingham, 2015. pdf
  • Parametricity, automorphisms of the universe, and excluded middle. Auke Bart Booij, Martín Hötzel Escardó, Peter LeFanu Lumsdaine, Michael Shulman. 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 12:34:20 by Ali Caglayan. See the history of this page for a list of all contributions to it.