The motivation for this theory was that inductively defined types and families of types become definable in terms of impredicative quantification. For example, the type of natural numbers can be defined as the type of Church numerals: