To overcome this pathological impredicativity, but still retain some of its expressivity, Martin-Löf introduced in 1972 a universe \(\U\) of small types closed under all type formers of the theory, except that it does not contain itself (Martin-Löf 1998 [1972]). The rules are: