A paradox in type theory wherein a function like N -> Type is also type Type. Fixed by Type Hierarchy