2 Feb
2009
2 Feb
'09
12:01 p.m.
On Mon, Feb 2, 2009 at 8:09 AM, Gregg Reynolds
Yes, that's my hypothesis: type constructors take us outside of set theory (ZF set theory, at least). I just can't prove it.
It's "too big" for Set Theory if you insist on representing functions in type theory as functions in set theory - ie. set(A -> B) = set(B)^set(A). But if you don't insist on such a constraint there's no problem with sets. -- Dan