internal type theory

Internal Type Theory


In set theory, it is common to build non-standard models of set theory inside an existing model of set theory. The same can be done in topos theory. It is natural to consider a similar construction in type theory, or perhaps in homotopy type theory.


Mike Shulman, in his blog-post HoTT should eat itself gives a good overview of the state of the art. There is later work by Altenkirch and Kaposi which treats the set level case. This makes progress over earlier work in standard type theory.


  • Peter Dybjer, Internal type theory, Types for Proofs and Programs (1996): 120-134. PDF
  • Alexandre Buisse and Peter Dybjer, Towards Formalizing Categorical Models of Type Theory in Type Theory (2008). PDF
  • James Chapman, Type theory should eat itself, Electronic Notes in Theoretical Computer Science 228 (2009): 21-36, html.
  • Thorsten Altenkirch, Ambrus Kaposi, Type Theory in Type Theory using Quotient Inductive Types, POPL17, 2017 PDF

Last revised on July 9, 2017 at 05:51:33. See the history of this page for a list of all contributions to it.