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.

Question

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.

References

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