> > 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. > You would not infer True or False from any values, and if the user did > > explicitly use them: > > > > type X = True > > > > The are just creating an alias. > > Because True and False cannot be the domain of a function, (from the > kind of (->)) why should we treat them as types in this way? I don't > mind you privately thinking of everything as a type, but please don't > let that be a reason to recommend useless quirks like this. > I agree with your point, I think I am happy to restrict type definitions to being _Type types. > >> > 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. 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. Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
