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, in: Types for Proofs and Programs, Lecture Notes in Computer Science 1158 (1996) 120-134 [doi:10.1007/3-540-61780-9_66, 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 January 1, 2023 at 17:06:36. See the history of this page for a list of all contributions to it.