Hereditary substitution with a universe hierarchy I've read about hereditary substitution for the Simple Lambda Calculus and for The Logical Framework with distinct terms and types.

I'm wondering, are there any examples of hereditary substitution in a dependently typed system with a universe hierarchy? i.e. where $ True : Set_0 : Set_1:Set_2$ etc.

I'm wondering in particular how to establish an induction measure in such a system. The simply typed version is structurally decreasing in the type of the variable being replaced. This doesn't work work with dependent types, to for LF the paper I linked uses the simply-typed erasure of the terms, performing induction on the shape of the type.

However, erasing to simple types doesn't work with a universe hierarchy, since if you have something like this:


$ f : (x : Set_1)\to x \to True$ implies that
$ f\ ((y : True) \to True \to True ): True \to True \to True$


i.e. applying a function resulted in a structurally larger type.

I'm assuming the solution has something to do with the universe indexes, but if there's an existing technique for establishing that the induction is well founded, I'd prefer to cite it rather than coming up with something up on my own.
As of November 2018, how to do this for dependent type theories with large eliminations is an open question. 

Establishing that the recursion is well-founded is not too bad; you can use Pataraia's theorem to prove the fixed point you want exists. See Robert Harper's *Constructing Type Systems Over an Operational Semantics for a how-to. (You can also do this via an inductive-recursive definition.)

The hard part is actually formulating the hereditary substitution in a nice way -- the natural direction leads you towards substituting not one term, but an entire substitution for a context, and this raises a lot of questions about when and how to establish properties of things like compositions of (hereditary) substitutions. 

If it turned out to be impossible, I would be utterly shocked. However, at present no one has done it. If you want to work on this, I would suggest getting in touch with Andreas Abel, Dan Licata and Mike Shulman. (Or me, for that matter.)