[Agda] Size of propositional equality?

Nils Anders Danielsson nad at Cs.Nott.AC.UK
Fri Dec 17 09:33:34 CET 2010


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



More information about the Agda mailing list