  if \(T(A) : U [A:U]\). Notice the circularity, indeed of the same kind as the one that is rejected by the ramified hierarchy: we define an element of type \(U\) by quantifying over all elements of \(U\). For instance the type