[Agda] [newbie] universe levels and BUILTIN EQUALITY

[Stefan Monnier]

>> Not sure what you mean by "a non-universe-polymorphic one".
> Of type
>   {A : Set} (x y : A) -> Set
> See also issue #2386: https://github.com/agda/agda/issues/2386

Isn't this just the case where you instantiate the level `a` to 0 ?
What'd be the benefit of having this special case when you have the more
general case already?


        Stefan