Homotopy Type Theory
References (Rev #65)

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


See also Philosophy, below.

Synthetic homotopy theory

Higher category theory

Homotopical ideas and truncations in type theory

General models


Inductive, coinductive, and higher-inductive types


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


  • 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


category: reference, navigation

Revision on February 14, 2019 at 10:24:12 by Ali Caglayan. See the history of this page for a list of all contributions to it.