[Agda] [newbie] universe levels and BUILTIN EQUALITY

[Andreas Abel]

On 07.01.2017 16:36, Stefan Monnier wrote:
>>> 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?

The point is only a didactic one.  If I write a paper with Agda that 
uses equality but no universes other than Set, I'd like to define 
propositional equality just for Sets.

Anyway, BUILTIN EQUALITY just means you can use the `rewrite` keyword 
with it.

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/