Na Agda, háSet n. Como eu entendo,Set n estende a hierarquia de tipo de valor no estilo Haskell para níveis infinitos. Isso é,Set 0 é o universo dos tipos normais,Set 1 é o universo de tipos normais,Set 2 é o universo de tipos normais, etc.

Por outro lado, Idris tem a chamada "hierarquia cumulativa de universos". Parece que paraa < b, Type a: Type b, e os níveis do universo são inferidos. Mas o que isso significa nos programas do mundo real? Não podemos definir algo que só opera em algum universo superior, mas não inferior?

A propósito, eu sei que é logicamente inconsistente, mas o que é* : * em comparação com as soluções consistentes acima?