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? Sam Moelius