[Agda] A type for positive type functors?

Nils Anders Danielsson nad at Cs.Nott.AC.UK
Tue Nov 23 14:08:10 CET 2010


On 2010-11-23 12:15, Sam Staton wrote:
> (unless Agda is made less intensional, which would be welcome)

I don't think we should let intensionality guide our design choices too
much. Hopefully Agda will steal some good ideas from Epigram/OTT so that
we get rid of this wart.

-- 
/NAD


More information about the Agda mailing list