There are several kinds of universes that one can consider in type theory. ## Universes a la Russell A **universe a la Russell** is a [[type]] whose terms *are* types. In the presence of a separate [[judgment]] "$A type$", this can be formulated as a rule $$\frac{A:U}{A type}$$ Thus, the type formers have rules saying which universe they belong to, such as: $$\frac{A:U\quad B:A\to U}{\Pi\, A\, B : U}$$ With universes a la Russell, we can also omit the judgment "$A type$" and replace it everywhere by a judgment that A is a term of some universe. This is the approach taken by the [[book]] and by [[Coq]]. ## Universes a la Tarski A **universe a la Tarski** is a type together with an "interpretation" operation allowing us to regard its terms as types (or "codes for types"). Thus we have a rule such as $$\frac{A:U}{El(A) type}$$ We usually also have operations on the universe corresponding to (but not identical to) type formers, such as $$\frac{A:U\quad B:A\to U}{pi(A, B) : U}$$ with an equality $El(pi(A,B))=\Pi \, El(A)\, El(B)$. Usually this latter equality (and those for other type formers) is a [[judgmental equality]]. If it is only a [[propositional equality]],we may speak of a **weakly a la Tarski universe**. Universes defined internally via [[induction-recursion]] are (strongly) a la Tarski. Weakly a la Tarski universes are easier to obtain in [[semantics]]: they are somewhat more annoying to use, but probably suffice for most purposes.