Homotopy Type Theory
References (Rev #61, changes)

Showing changes from revision #60 to #61: 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.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 mathematiciansAn introduction to univalent foundations for mathematicians?. Dan Grayson, arxiv
  • A self-contained, brief and complete formulation of Voevodsky’s Univalence AxiomA self-contained, brief and complete formulation of Voevodsky's Univalence Axiom?. Martín Escardó, web, arxiv
  • A proposition is the (homotopy) type of its proofsA 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 and higher-inductive types

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

Formalizations

Applications to computing

Cubical models and cubical type theory

Syntax of type theory: theory

Strict equality types

Directed type theory

Cohesion and modalities

Theories and models

Computational interpretation: interpretation

Philosophy: Philosophy

  • Structuralism, Invariance, and UnivalenceStructuralism, 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 A synthetic approach to higher equalities?. Michael Shulman. To appear in Categories for the working philosopher; arXiv
  • Univalent Foundations as Structuralist FoundationsUnivalent Foundations as Structuralist Foundations?. Dimitris Tsementzis. Forthcoming in Synthese; Pitt-PhilSci
  • Homotopy type theory: the logic of space the logic of space?. Michael Shulman. To appear in New Spaces in Mathematics and Physics: arxiv

Other: 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.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)Space-Valued Diagrams?, Type-Theoretically (Extended Abstract) . Nicolai Kraus and Christian Sattler.Nicolai Kraus and Christian Sattler?. arXiv

category: references

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