6 Aug
2003
6 Aug
'03
10:35 a.m.
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