> > 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