Substituição hereditária por uma hierarquia de universo

Eu li sobre a substituição hereditária do Cálculo Lambda Simples e do The Logical Framework com termos e tipos distintos.

Gostaria de saber, existem exemplos de substituição hereditária em um sistema tipicamente dependente com uma hierarquia de universo? ou seja, onde etc.$True : Set_0 : Set_1:Set_2$

Eu estou querendo saber em particular como estabelecer uma medida de indução em tal sistema. A versão simplesmente digitada está diminuindo estruturalmente no tipo da variável que está sendo substituída. Isso não funciona com tipos dependentes, pois para LF o papel que vinculei usa o apagamento simples dos termos, realizando indução na forma do tipo.

No entanto, apagar para tipos simples não funciona com uma hierarquia de universo, pois se você tiver algo parecido com isto:

• $f : (x : Set_1)\to x \to True$ implica que
• $f\ ((y : True) \to True \to True ): True \to True \to True$

isto é, aplicar uma função resultou em um tipo estruturalmente maior.

Suponho que a solução tenha algo a ver com os índices do universo, mas se houver uma técnica existente para estabelecer que a indução seja bem fundamentada, prefiro citá-la do que inventar algo por conta própria.

Aqui está uma referência para o sistema predicativo F. A medida de fato inclui o conjunto múltiplo de níveis do universo em um tipo. Não posso dizer muito sobre se essa abordagem se generaliza à teoria do tipo dependente predicativo.

Em novembro de 2018, como fazer isso para teorias de tipos dependentes com grandes eliminações é uma questão em aberto.

Estabelecer que a recursão seja bem fundamentada não é tão ruim; você pode usar o teorema de Pataraia para provar que o ponto fixo que você deseja existe. Consulte * Construindo sistemas de tipos sobre uma semântica operacional de Robert Harper para obter instruções. (Você também pode fazer isso por meio de uma definição indutivo-recursiva.)

A parte difícil é realmente formular a substituição hereditária de uma maneira agradável - a direção natural leva você a substituir não um termo, mas toda uma substituição por um contexto, e isso levanta muitas questões sobre quando e como estabelecer propriedades das coisas composições semelhantes de substituições (hereditárias).

Se isso fosse impossível, eu ficaria totalmente chocado. No entanto, atualmente ninguém fez isso. Se você quiser trabalhar nisso, sugiro entrar em contato com Andreas Abel, Dan Licata e Mike Shulman. (Ou eu, nesse caso.)