  expressing that there are arbitrarily large primes. Under the Curry-Howard interpretation this becomes the type \(\Pi m {:} \N.\, \Sigma n {:} \N.\, m \lt n \times \mathrm{Prime}(n)\) of functions which map a number \(m\) to a triple \((n,(p,q))\), where \(n\) is a number, \(p\) is a proof that \(m \lt n\) and \(q\) is a proof that \(n\) is prime. This is the proofs as programs principle: a constructive proof that there are arbitrarily large primes becomes a program which given any number produces a larger prime together with proofs that it indeed is larger and indeed is prime.