[Agda] ANNOUNCE: Agda 2.2.10

[Jean-Philippe Bernardy]

>> > data Eq (A : Set) (a : A) : .A ->  Set where
>> >
>> >    refl : Eq A a a

> This definition should simply not be allowed, I'd say. If we think about:
>
>  Eq A a : .A -> Set
>
> then this means that the second A should be irrelevant for the purpose of
> determining what _set_ is returned. Which implies that Eq A a b and Eq A a c
> should be in some sense the same set even if b and c are different. But this
> is clearly not what Eq is trying to accomplish.

Maybe, this is in fact what Eq is trying to accomplish (in some sense). :)

Cheers,
-- JP