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