Homotopy Type Theory
References (Rev #60, changes)

Showing changes from revision #59 to #60: 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!

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

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 13:41:29 by Ali Caglayan. See the history of this page for a list of all contributions to it.