On 3 Apr 2015 04:23, "Matt Oliveri" <[email protected]> wrote: > > 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!
A LF can prove things about mathematics, and you have to build up all the mathematical rules to formalise the proof. If we can make natural numbers out of types, what do we need the natural numbers for? It becomes a redundant definition. Surely there is no difference between Nat1 (the type of nats) and Nat2 the kind of type level nats, they can be the same definition, one is just lifted a level. Isn't this what HoTT is talking about with the univalent foundation of mathematics, and being an alternative to set theory? What I have is a subset of HoTT as I haven't got to the point of needing type identities, the J operator, or paths yet. Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
