All of the type theory based proof assistants that I have seen have an infinite hierarchy of type universes to avoid the type of types being a term of itself. Are there alternative systems which could be implemented in a proof assistant, to solve the same problem, which don't involve universe levels?

  • 5
    $\begingroup$ You can restrict yourself to just one level, and that technically gets rid of the levels. $\endgroup$
    – Trebor
    Commented Jul 22, 2022 at 4:29
  • 3
    $\begingroup$ I believe type-in-type with only linear uses of variables is consistent. Very restrictive though. $\endgroup$ Commented Jul 22, 2022 at 6:35
  • 1
    $\begingroup$ Universe levels are often explained in terms of natural numbers. You have universe 0, universe 1 and so on. But really you don't need all that. All you need is universe a is less than universe b is less universe c. It's a little like New Foundations and stratification and it's kind of like some sorts of universe polymorphism. $\endgroup$ Commented Jul 22, 2022 at 18:29
  • 2
    $\begingroup$ Higher order logic, used in HOL Light, HOL4, and Isabelle/HOL, is a simple type theory with no universes. Types and objects are different sorts, so you can quantify over objects in a type, but not over types themselves. However, HOL implementations usually come with type polymorphism and types can also depend on other types (just not on elements of a type). $\endgroup$
    – Jason Rute
    Commented Jul 26, 2022 at 2:55
  • $\begingroup$ Yes, but not the common kind of type theory. See this post. $\endgroup$
    – user21820
    Commented Sep 1, 2022 at 19:51


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.