Another typing question

[Peter G. Hancock]

>>>>> 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