[Agda] Size of propositional equality?

[Nils Anders Danielsson]

On 2010-12-16 19:23, Alan Jeffrey wrote:
> I'm sure there's a good reason for this change, any hints what it
> might be?

The small variant of _≡_ is accepted by Agda, but perhaps it shouldn't
be—several persons are sceptical about this. Propositional equality is a
rather important type, so I decided to switch to a more conservative
definition.

-- 
/NAD