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}