Homotopy Type Theory References > history (Rev #76)

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

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

  • 2-Dimensional Directed Dependent Type Theory.? Dan Licata and Robert Harper. MFPS 2011. See also Chapters 7 and 8 of Dan?s thesis. PDF
  • A type theory for synthetic $\infty$-categories?. Emily Riehl, Michael Shulman. arxiv
  • Synthetic fibered (∞,1)-category theory. Ulrik Buchholtz, Jonathan Weinberger. arxiv, 2021.
  • Limits and colimits of synthetic ∞-categories. César Bardomiano Martínez. arxiv, 2022.

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

category: reference, navigation

Revision on February 28, 2022 at 19:07:27 by Mike Shulman. See the history of this page for a list of all contributions to it.