En Agda, haySet n. Según entiendo,Set n extiende la jerarquía de tipo de valor de tipo estilo Haskell a niveles infinitos. Es decir,Set 0 es el universo de los tipos normales,Set 1 es el universo de los tipos normales,Set 2 es el universo de los tipos normales, etc.

En contraste, Idris tiene la llamada "jerarquía acumulativa de universos". Parece que paraa < b, Type a: Type b, y se infieren los niveles del universo. Pero, ¿qué significa en los programas del mundo real? ¿No podemos definir algo que solo opera en un universo superior pero no inferior?

Por cierto, sé que es lógicamente inconsistente, pero lo que es* : * en comparación con las soluciones consistentes anteriores?