[Agda] Why is propositional equality "Set a" instead of just Set?

[Nils Anders Danielsson]

On 2013-08-22 14:32, Conor McBride wrote:
> I'm troubled by the "suc".

[...]

> I accept that _<->_ is defined with a large index, which is perhaps a
> dangerous thing, in general. However, when you define _<->_ instead by
> recursion on the structure of types (e.g., for an IR-encoded universe),
> you find it is indeed as small as claimed.

I proposed the large definition because the small one might not be
accepted in the future. One might believe that one could work around
this issue by using --type-in-type, but --type-in-type is (currently)
incompatible with universe polymorphism. However, I guess that we could
add another flag: --ignore-size-of-indices.

-- 
/NAD