[Agda] Records and irrelevant fields

[Dan Doel]

On Saturday 18 September 2010 1:42:28 am wren ng thornton wrote:
> But I'm not terribly familiar with EPTSes yet. I've had some thoughts on
> how to do irrelevance better than Coq (e.g., removing the Set/Prop
> distinction). I'd thought my ideas were along the same lines as EPTSes,
> though maybe not...

They may well be along the same lines, in that irrelevance is expressed by a 
modality. It may just not be the same modality.

If you don't have it already, you might want to also look at Frank Pfenning's 
Intensionality, Extensionality and Proof Irrelevance in Modal Type Theory. * 
He has a theory with three different modalities (and equality types). I 
haven't studied hard enough to know if/how his proof irrelevant modality is 
different from the one in EPTSes, but I suspect it is.

(I was going to send this off list, but it might be relevant to the larger 
conversation. Andreas mentioned LiCS earlier, and that's by Pfenning. Was it 
an implementation of something like the stuff in the above paper?)

-- Dan

[*] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.28.5884