The PA_K trick is mine. (Still hope to find a version of it that works -- I have an idea, but need some time to try whether it can fix the proof...) A polymorphic variant of simple type theory is used in Isabelle/HOL; if you know Hindley-Milner polymorphism as used in Haskell, it's a variant of that. Probably the most useful thing to read more about is models of the untyped lambda calculus: I'd recommend Chantal Berline's From computation to foundations via functions and application: The λ-calculus and its webbed models (I think there's a non-paywall copy on her homepage, which is down currently); you don't need to read about all the models in that paper, the basic one in Section 4.6 exemplifies the basic idea. The von Neumann hierarchy stuff is basic model-theory-in-ZFC-extensions stuff.

Besides what I wrote about in the post, Coq's universe hierarchy is definitely an example; Chapter 12 of Adam Chipala's draft Certified Programming with Dependent Types seemed the most helpful thing among what Google turned up (HTML version here). Finally, Reynold's and Girard's parametricity is the best example I know of that gives a formal meaning to "the same words being interpreted in different ways on different levels" [ETA: and then does something relatively deep with it]. Wadler's Theorems for Free! is the best thing I can think of as an entry point.

The above list doesn't really make me happy. Polymorphic type theory is very simple, but it also isn't very deep. Other than that, Berline's and Wadler's papers are the only things that seem to give a reasonable return on time invested if you don't know the field in question already, and even they aren't really casual reading and all they'll give you in the present context is examples of where I'm coming from in this post (not that both subjects aren't worth studying for their own sake).