Definition. Type Universes [002p]

In an abstract sense type universes can be regarded similarly in motivation to Grothendieck universes in that they represent a collection (type in this case) of types which are closed under certain type constructions. There are typically two presentations of type universes either a la Russell or Tarksi, starting with the former we have:


\[ \pi (X, B) : \prod _{(X\ :\ \mathcal {U}_i)} (\texttt {El}_i(X) \to \mathcal {U}_i) \to \mathcal {U}_i \]