On Thu, Apr 2, 2015 at 12:44 PM, Keean Schupke <[email protected]> wrote: >> I think you're still using the term "universe" wrong. A universe is a >> type whose elements are types. (If you think of everything as a type, >> then everything is also a universe. How silly.) So _Type is a >> universe, for example. If _Type contains Int, then Int's universe is >> _Type. But you are referring to "universe 1" and "universe 0". Why? >> What is their role? > > I think I see where the confusion is coming from. What I am labelling > universes is the stratification of > universes in a tower of universes. > > _Type and _Bool are level 0 universes, so I have labelled all the types that > are in a level 0 universe accordingly. > _Type and _Bool themselves must be in some (unnamed) universe of level 1.
OK. Aside from _Bool being a universe, this makes sense. >> >> > I suppose that makes me a constructivist :-) >> >> >> >> Naw. Pretty sure that's not what it means. >> > >> > http://en.wikipedia.org/wiki/Constructivism_%28mathematics%29 >> >> Being a constructivist isn't about preferring constructions of >> concepts (e.g. starting from MLTT) to axiomatizations. It's about >> requiring a construction of something to prove that it exists, as the >> article says. We haven't talked about existence at all, so whether >> you're a constructivist or not would not be evident from anything >> you've said so far. > > I want to construct _Bool from type theory, rather than magic it up. You've made that clear. I'm saying that's not what constructivism is about. "Constructivism" is a misleading name I guess. > When constructing mathematics from type-theory > you start with just types, there are no numbers, no booleans, > they all have to be made out of types. This is not an accurate statement about math in Martin-Lof type theory, since MLTT comes with natural numbers and booleans, all "magicked up" for you. Newer derivatives of MLTT have general inductive types magicked up for you. In either case, you don't build these objects out of types. How would that even work? _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
