nLab homotopy type theory - references


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

  • 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.
  • A Synthetic Perspective on (∞,1)-Category Theory: Fibrational and Semantic Aspects. Jonathan Weinberger. PhD Thesis; arxiv, 2022.
  • Two-sided cartesian fibrations of synthetic (∞,1)-categories. Jonathan Weinberger, arxiv.

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


Last revised on June 9, 2022 at 14:03:50. See the history of this page for a list of all contributions to it.