[Agda] [newbie] universe levels and BUILTIN EQUALITY

[Andreas Abel]

Previously, this was the official definition, but in the meantime, we 
came to think of it as hazardous.  For instance, it has no predicative 
justification.

On 04.01.2017 21:58, Martin Stone Davis wrote:
> It's possible to define a kind of EQUALITY sorted in any universe we
> want. For example, Set₀:
>
> data _≡_ {a} {A : Set a} (x : A) : A → Set₀
>  where refl : x ≡ x
>
> However, to be declarable as BUILTIN, the sort needs to be Set a. Why is
> it that way? It seems, to my naive eye, that it would be somehow simpler
> or more conservative to have it at the lowest level possible. What bad
> things would happen if it were required to be Set₀?
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


-- 
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/