http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.UniversePolymorphism
В Agda, Level - это явное значение, которое можно указать, поэтому вам нужно убедиться, что вы количественно оценили все n, если вы хотите, чтобы тип работал на всех уровнях.
Бумага Кока для полиморфизма вселенной , кажется, указывает на то, что n может быть выведено, так что можно написать Set : Set и при этом иметь согласованный язык (где он автоматически превращается во что-то в форме {n m} Set n : Set m, и к контексту добавляется ограничение n < m.
Есть ли предположение, что Агда делает невозможным вывод уровней? (Или делает невозможным вычисление по какой-то причине?)