Почему я не могу определить `Eq`, используя только индексы в Agda?

Question

Почему я не могу определить более явный вариант гетерогенного равенства, как это:

data Eq : (A : Set) -> A -> A -> Set where 
    Refl : (T : Set) -> (x : T) -> Eq T x x 

Когда я так, я получаю следующее сообщение об ошибке:

The type of the constructor does not fit in the sort of the 
datatype, since Set₁ is not less or equal than Set 
when checking the constructor Refl in the declaration of Eq 

Я знаю, что эта ошибка есть что-то делать с вселенской иерархией, но я не знаю, что именно. Думает ли это, что Eq T x x должен быть Set_1, или что это такое, но этого не должно быть? Почему что-то здесь Set_1?

Answer 1

Если тип, который вы определяете, имеет индекс, тип которого находится в Set n, тогда сам тип должен быть не менее Set n. В вашем случае один из ваших индексов, A, имеет тип Set, поэтому его тип составляет вSet 1 (с Set : Set 1). И так, Eq сам должен быть как минимум Set 1.

Обратите внимание, что если A : Set был параметром вместо индекса, выше не будет применяться, поэтому гомогенное равенство может быть в Set.