Having read the parts of the hott book that introduce intuitionistic type theory (+univalence), I want to continue by studying some meta theory. I'm particularly interested in strategies for proving consistency of (not necessarily univalent) type theories but I couldn't find any introductory text book covering the subject.
As far as I can tell, the usual approach seems to be to find some set theoretic model using category theory, interpret the formulae/contexts of the type theory in the model category and prove that all deduction rules are satisifed in the model category (i.e. if there is an object $X$ in the model category $C$ whose existence is interpreted as validity of a formula $\phi$ of the type theory and there is rule that lets us conclude $\psi$ from $\phi$, there is an object $Y \in C$ that is interpreted as truth of $\psi$).
Is there a paper or a sequence of papers that introduce the technique rigorously without requiring much prior knowledge of the subject? I am familiar with some basic notions of category theory (adjunctions, limits, sheaves, sites, etc.).
I found these slides by Shulman and this paper by Clairambault and Dybjer that seem to be relevant. Is there other material I may be interested in?
I'm also happy to learn about other approaches. For example, in this paper, Chapman works towards 'dogfooding' type theory, i.e. interpreting (probably some weaker form of) it in itself (thus, proving consistency). Is there any news on this front?