6 Aug
2003
6 Aug
'03
12:07 p.m.
Samuel E Moelius, wrote (on Wed, 06 Aug 2003 at 15:35):
> On Wednesday, August 6, 2003, at 06:15 AM, C T McBride wrote: >> This is why most sensible dependent type theories have a hierarchy of >> universes behind the scenes. You can think of * in Haskell as the lowest >> universe, inhabited by types. > Why wouldn't terms be the lowest universe? A universe is a type of types/set-like-things, modulo a pile of subtleties. (The first of which is that it is actually a type of codes for types.) I think the term "universe", which afaik was introduced into type theory by Martin-Lof, was chosen for its use in the foundations of category theory in dealing with questions of "size" (smallness/largeness). Peter Hancock