{-# OPTIONS --cubical #-}

module index where


This is the cubical Agda implementation of the PhD thesis


defended 1st May 2015, School of Computer Science, University of
Birmingham, UK, by

  Chuangjie XU

supervised by Martín Escardó.

The original version was developed in Agda and is available
for downloading at


This version, 9th November 2017, is ported to cubical Agda, and only
includes one of the five original branches, the one postulating
function extensionality. 

In the original, non-cubical, version of this branch, we had a closed
term of type ℕ (a modulus of uniform continuity of a simple function)
whose normal form was not a numeral but instead a 367-lines long
term. The term is (modu F₂) and its original normal form is named
(old-modu-F₂-normal-form) in the following file.


import UsingFunext.ModellingUC.ComputationExperiments


This was because function extensionality was postulated as a term
funext. However, in this cubical version, funext is proved, and hence
the original term normalizes to zero (modu-F₂-normal-form).

Porting this to cubical Agda involved:

  1. Using Andrea Vezzosi's cubical library with a new definition of
  the identity type Id, which we rename to ≡ to conform with our
  original development. (Because our original development didn't use
  the standard library, but Vezzozi's one does, we had to slighly
  adapt his development for our needs.)


open import Id
open import PathPrelude
open import Primitives
open import Sub


  2. Removing all uses of pattern matching on refl, and instead using
  the J induction principle for Id. 

  3. Giving up using built-in NATURALS.

In this version of the development, we only include the chapters of
the thesis that are needed to compute moduli of uniform continuity.

To navigate this set of files, click at module names, keywords or symbols.

Chapter 2 investigates the Curry-Howard formulations of the two
fundamental continuity principles, (Cont) and (UC).  The latter, which
is the one that we are working with in this thesis, is logically
equivalent to the logical formulation.  For this, we need to extend
the type theory with propositional truncation and the axiom of
function extensionality. This is removed from this branch of the

Chapter 3 develops a variation of the topological topos, consisting of sheaves
on a certain uniform-continuity site.  In particular, C-spaces, corresponding to
concrete sheaves, form a (locally) cartesian closed category with a natural
numbers object.  Moreover, there is a fan functional, in the category of
C-spaces, that continuously calculates least moduli of uniform continuity of
maps ₂ℕ → ℕ. Not all of this is included in this version of the development.


-- § 3.2.1  The uniform-continuity site
import UsingFunext.Space.Coverage

-- § 3.3.1  Concrete sheaves as a variation of quasi-topological spaces
import UsingFunext.Space.Space

-- § 3.3.2  The (local) cartesian closed structure of C-Space
import UsingFunext.Space.CartesianClosedness

-- § 3.3.3  Discrete C-spaces and natural numbers object
import UsingFunext.Space.DiscreteSpace

-- § 3.4  The representable sheaf is the Cantor space
import UsingFunext.Space.YonedaLemma

-- § 3.5  The fan functional in the category of C-spaces
import UsingFunext.Space.Fan


Chapter 4 shows how the Kleene-Kreisel continuous functionals can be
calculated within C-spaces.  When assuming the Brouwerian axiom that
all set-theoretic functions ₂ℕ → ℕ are uniformly continuous, the full
type hierarchy is equivalent to the Kleene--Kreisel continuous
hierarchy within C-spaces. This is not included in this version of the

Chapter 5 employs C-spaces to model Gödel's system T with a
skolemization of (UC), and to realizes (UC) in the intuitionistic
arithmetic HAω of finite types, with the aid of the fan
functional. Not all of this is included in this version of the


-- § 5.1  A continuous model of Gödel's System T
import UsingFunext.ModellingUC.UCinT


Chapter 6 validates the Curry-Howard interpretation of (UC) in the
locally cartesian closed category of C-spaces using the fan
functional, and demonstrates how C-spaces and sheaves form models of
dependent types, without the coherence problem, via the notion of
category with families (CwF). This is not included in this version of
the development.

Chapter 7 discusses other versions of implementation, in which the
computational content of the development is not destroyed (using
setoids, using computationally irrelevant fields, and other
methods). This is not included in this version of the development.