In contrast, how would the mathematical relation \(&gt;\) between natural numbers be handled in intuitionistic type theory? First of all we need a type of numbers \(\N\). We could in principle introduce an unspecified individual domain \(\N\), and then add axioms just as we do in first-order logic when we set up the axiom system for Peano arithmetic. However this would not give us the desirable computational interpretation. So as explained below we lay down introduction rules for constructing new natural numbers in \(\N\) and elimination and computation rules for defining functions on \(\N\) (by recursion). The standard order relation \(&gt;\) should satisfy