The inconsistent version of intuitionistic type theory of Martin-Löf (1971a) was based on the strongly impredicative axiom that there is a type of all types. However, (Coquand and Huet 1988) showed with their calculus of constructions, that there is a powerful impredicative but consistent version of type theory. In this theory the universe \(\U\) (usually called \({\bf Prop}\) in this theory) is closed under the following formation rule for cartesian product of families of types: