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
-
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$– Albert ten NapelCommented 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$– Ms. Molly Stewart-GallusCommented 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 RuteCommented Jul 26, 2022 at 2:55
-
$\begingroup$ Yes, but not the common kind of type theory. See this post. $\endgroup$– user21820Commented Sep 1, 2022 at 19:51
Add a comment
|