Chuangjie Xu, 2013 This is an Agda formalization of the paper A constructive manifestation of the Kleene-Kreisel continuous functionals by Martin Escardo and Chuangjie Xu http://www.cs.bham.ac.uk/~mhe/papers/kleene-kreisel.pdf The agda files are at http://www.cs.bham.ac.uk/~mhe/papers/kleene-kreisel/kleene-kreisel.zip \begin{code} module index where \end{code} As discussed in Section 5 of the paper, we need function extensionality, but we can actually get away with its double negation, which has the advantage of not breaking canonicity (every closed term of type ℕ will still normalize to a numeral). \begin{code} import not-not-funext \end{code} The following corresponds to Section 2 of the paper, sheaves and C-spaces, but here we only formalize C-spaces: \begin{code} import Space import Space-exponential import Space-product import Space-coproduct import Space-discrete import Space-cantor import Space-LCC \end{code} The following module is used above to prove the coverage axiom and sheaf condition for exponentials and discrete spaces, and also later to implement and prove the fan functional: \begin{code} import UniformContinuity \end{code} Next we show that the Kleene-Kreisel and full type hierarchies agree if UC holds for types (Section 3). For this part of the development (only), the double negation of function extensionality doesn't seem to be sufficient, as mentioned in Section 5 of the paper, and hence use full function extensionality as a hypothesis. \begin{code} import Hierarchy \end{code} Section 4.1 (the fan functional): \begin{code} open import Fan \end{code} Section 4.2 (modelling system T with C-spaces): \begin{code} import T import C-interpretation-of-T import Validation-of-fan \end{code} The above file C-interpretation-of-T has some examples of computations of moduli of uniform continuity. Section 4.2 (Validating UC in the model of dependent types): \begin{code} import Validation-of-UC-in-LCCC \end{code} The following was included in the TLCA paper http://www.cs.bham.ac.uk/~mhe/papers/xu-escardo.pdf and just mentioned in Section 5 of the journal paper formalized here: \begin{code} import HAomega \end{code} The following contain auxiliary definitions and proofs: \begin{code} import MiniLibrary import Inequality import Sequence import not-not \end{code}