  That \(M\) is of this type means that \(M A:T(A)\) whenever \(A:U\). We get in this way extensions of type theory whose strength is similar to the one of Zermelo’s set theory (Miquel 2001). More powerful form of universes are considered in (Palmgren 1998). Miquel (2003) presents a version of type theory of strength equivalent to the one of Zermelo-Fraenkel.