[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