Homotopy Type Theory References > history (Rev #72, changes)

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

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

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 November 20, 2020 at 15:55:26 by Mike Shulman. See the history of this page for a list of all contributions to it.