On Thu, Apr 2, 2015 at 11:11 PM, Matt Oliveri <[email protected]> wrote: > On Thu, Apr 2, 2015 at 2:28 PM, Keean Schupke <[email protected]> wrote: >> Now I realise that is says z is an object, but there is no reason we have to >> be operating at the bottom. z can just as easily be one level higher, and be >> an empty universe at the U0 level, and 'nat' is now at the U1 level. Now we >> don't need values at all, we can build everything from empty universes, like >> everything is set theory is built from empty sets. > > It sounds like you're trying to turn type theory into set theory. > Maybe you should be talking to Geoffrey. > > Many type theorists consider set theory's trick of encoding everything > as a set to be a misfeature. The particular encoding of mathematical > objects as sets is arbitrary, and allows for stupid questions, like > "Is the zeta function an element of pi?". You'd like to consider that > question nonsensical, but you can't because the zeta function and pi > have been constructed from sets in one way or another, and so you're > asking a perfectly valid question about those arbitrarily-chosen sets.
By the way, if you really turn type theory into set theory, do not expect any parametricity results! _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
