В Агде естьSet n, Насколько я понимаю,Set n расширяет иерархию типов значений в стиле Haskell до бесконечных уровней. То есть,Set 0 это вселенная нормальных типов,Set 1 это вселенная нормальных видов,Set 2 вселенная нормальных сортов и т. д.

Напротив, у Идриса есть так называемая «совокупная иерархия вселенных». Кажется, что дляa < b, Type a: Type bи уровни вселенной выведены. Но что это значит в реальных программах? Разве мы не можем определить то, что действует только в какой-то более высокой, но не нижней вселенной?

Кстати, я знаю, что это логически противоречиво, но что* : * по сравнению с вышеуказанными последовательными решениями?