为什么我不能在Agda中只使用索引定义`Eq`？

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。