Why can't I define a more explicit version of heterogenous equality like this:
data Eq : (A : Set) -> A -> A -> Set where
Refl : (T : Set) -> (x : T) -> Eq T x x
When I do so, I get the following error:
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
I know that this error has something to do with the universe heirarchy, but I don't know what exactly. Does it think that Eq T x x should be Set_1, or that it is but it shouldn't be? Why is anything here Set_1?
If the type you are defining has an index whose type is in Set n, then the type itself must be in at least Set n. In your case, one of your indices, A, has type Set, so its type is in Set 1 (since Set : Set 1). And so, Eq itself needs to be in at least Set 1.
Note that if A : Set was a parameter instead of an index, the above wouldn't apply, which is why homogenous equality can be in Set.