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
    Jul 22 at 4:29
  • 3
    $\begingroup$ I believe type-in-type with only linear uses of variables is consistent. Very restrictive though. $\endgroup$ Jul 22 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$ Jul 22 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
    Jul 26 at 2:55
  • $\begingroup$ Yes, but not the common kind of type theory. See this post. $\endgroup$
    – user21820
    Sep 1 at 19:51


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.