Intuitionistic type theory is not intended to model Brouwer’s notion of free choice sequence, although lawlike choice sequences can be modelled as functions from \(\N\). However, there are extensions of the theory which incorporate such choice sequences: namely partial type theory and non-standard type theory (Martin-Löf 1990). The types in partial type theory can be interpreted as Scott domains (Martin-Löf 1986, Palmgren and Stoltenberg-Hansen 1990, Palmgren 1991). In this way a type \(\N\) which contains an infinite number \(\infty\) can be interpreted. However, in partial type theory all types are inhabited by a least element \(\bot\), and thus the propositions as types principle is not maintained. Non-standard type theory incorporates non-standard elements, such as an infinite number \(\infty {:} \N\) without inhabiting all types.