This rule is more general than the rule for constructing small cartesian products of families of small types in intuitionistic type theory, since we can now quantify over arbitrary types \(A\), including \(\U\), and not just small types. We say that \(\U\) is impredicative since we can construct a new element of it by quantifying over all elements, even the element which is constructed.