We use techniques from denotational semantics to prove the well-known fact that the Gödel's System T definable functions on the Baire type (ℕ → ℕ) with values on the natural numbers are continuous, and their retriction to the Cantor type (ℕ → 𝟚) are uniformly continuous.

This repository has both the source of the paper and associated Agda files.

• How to cite this paper

• The directory latex has the literate Agda file that generates the latex file and the pdf file of the paper.

• The directory source has various Agda files:

  1. laconic-dialogue is the above literate Agda file with the comments removed. This works with the combinatory combinatory version of system T.

  2. dialogue-lambda works with the lambda-calculus version of system T instead. Additionally, we now let Rec be the primitive recursion combinator rather than the iteration combinator.

  3. dialogue-lambda-internal internalizes this to system T using Church encoding of dialogue trees in system T rather than external inductive definition of such trees.

  4. church-dialogue variation of the above.

  5. church-dialogue-internal variation of the above.

  6. dialogue-without-oracle is a file by Vincent Rahli (2015) that shows how to get rid of the use of oracles.

  7. dialogue-to-brouwer, by Paulo Oliva and me (2017) converts from dialogue trees to Brouwer trees.

• Renderings in html at my institutional web page.