A dependently typed system
Inductively defined datatypes
Implicit arguments, Metavariables, and Unification
Universe hierarchy
Universe Polymorphism
Cumulative Universes(?)