This is the Agda implementation of the thesis

  A CONTINUOUS COMPUTATIONAL INTERPRETATION OF TYPE THEORIES

by

  Chuangjie XU

It type checks and runs with Agda 2.4.2 and is available for
downloading at

  http://cj-xu.github.io/ContinuityType/xu-thesis-agda.zip

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

\begin{code}

module index where

\end{code}

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.

\begin{code}

-- § 2.3  The Curry-Howard interpretation of (UC)
import Continuity.EquivalentFormulationsOfUC

\end{code}

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 ₂ℕ → ℕ.

\begin{code}

-- § 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
import UsingFunext.Space.Coproduct
import UsingFunext.Space.LocalCartesianClosedness

-- § 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

\end{code}

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.

\begin{code}

-- § 4.3  The Kleene-Kreisel and full-type hierarchies
import UsingFunext.Space.IndiscreteSpace
import UsingFunext.ModellingUC.Hierarchy

\end{code}

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.

\begin{code}

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

-- § 5.2  A continuous realizability semantics of HAω
import UsingFunext.ModellingUC.UCinHAo

\end{code}

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).

\begin{code}

-- § 6.2  Modelling UC via the LCCC of C-spaces
import UsingFunext.ModellingUC.ValidatingUCviaLCCC

-- § 6.3  Categories with families
import CwF.Sets.Base
import CwF.Sets.TypesAndTerms
import CwF.Sets.ContextComprehension
import CwF.Sets.SigmaType
import CwF.Sets.PiType
import CwF.Sets.IdentityType

-- § 6.4  A continuous model of dependent types
import CwF.Space.Base
import CwF.Space.TypesAndTerms
import CwF.Space.ContextComprehension

-- § 6.5  A sheaf model of dependent types
import CwF.Sheaf.Base
import CwF.Sheaf.TypesAndTerms
import CwF.Sheaf.ContextComprehension

\end{code}

Other versions of implementation, in which the computational content
of the development is not destroyed.

\begin{code}

-- § 7.2.2  Construction by using setoids
import UsingSetoid.Space.Space
import UsingSetoid.ModellingUC.UCinT
import UsingSetoid.ModellingUC.ComputationExperiments

-- § 7.2.3  Construction by adding a probe axiom
import AddingProbeAxiom.Space.Space
import AddingProbeAxiom.ModellingUC.UCinT
import AddingProbeAxiom.ModellingUC.ComputationExperiments

-- § 7.2.4  Construction by postulating ¬¬(funext)
-- Construction by postulating (funext) in an irrelevant field
import UsingIrrelevantFunext.Space.Space
import UsingIrrelevantFunext.ModellingUC.UCinT
import UsingIrrelevantFunext.ModellingUC.ComputationExperiments
-- Construction by postulating the double negation of (funext)
import UsingNotNotFunext.Space.Space
import UsingNotNotFunext.ModellingUC.UCinT
import UsingNotNotFunext.ModellingUC.ComputationExperiments

\end{code}