Typically, mathematics is viewed as an endeavour outside time and mathematical truth as a fixed, universal concept. In contrast, 20th century mathematician and philosopher Brouwer viewed mathematics as being about mental constructions, and and believed that a statement was true if it had an appropriate construction which one could experience in the mind fully. As a result, Brouwer thought of time as a crucial part of mathematics, which eventually resulted in the concept of choice sequences: that is, infinite sequences of numbers whose entries are generated one at a time, such that only a finite prefix of the sequence is available at any given time. By accepting choice sequences and Brouwer's intuitionism, we are able to reject classically true statements such as the law of excluded middle or even Markov's principle. These ideas can be applied to show that such statements are not provable in type theory by giving models featuring choice sequences as primitives.