With propositions as types, predicates become dependent types. For example, the predicate \(\mathrm{Prime}(x)\) becomes the type of proofs that \(x\) is prime. This type depends on \(x\). Similarly, \(x &lt; y\) is the type of proofs that \(x\) is less than \(y\).