Martin-Löf’s first version of type theory (Martin-Löf 1971a) had an axiom stating that there is a type of all types. This was proved inconsistent by Girard who found that the Burali-Forti paradox could be encoded in this theory.