[Agda] dependent extensionality

James Chapman james at cs.ioc.ee
Tue Sep 28 21:48:10 CEST 2010


On Tue, Sep 28, 2010 at 9:52 AM, Thorsten Altenkirch <txa at cs.nott.ac.uk> wrote:
> I think dependent extensionality and non-dependent extensionality are equivalent anyway and I don't see how the levels should cause any harm.

Equivalent in what sense?

James


More information about the Agda mailing list