[Agda] A plea for Set:Set

Wouter Swierstra wss at cs.nott.ac.uk
Wed May 14 00:10:30 CEST 2008


>
> I'm at a bit of a loss as to how you would express this in Agda...

Writing it out in a type theory where Set : Set is better known as  
"Girard's Paradox". The simplest proof out there is, I think:

http://portal.acm.org/citation.cfm?id=671442&dl=&coll=

A variation of it has been written out in Coq:

http://coq.inria.fr/library/Coq.Logic.Hurkens.html

   Wouter



More information about the Agda mailing list