Andrew Swan: Oracle modalities
Abstract: Hyland's original paper on the effective topos already introduced an interesting link between computability theory and categorical logic: the Turing degrees embed into the lattice of subtoposes of the effective topos. I bring this result up to date with a new version replacing the extensional type theory of the effective topos with homotopy type theory. We replace the effective topos with cubical assemblies (cubical sets constructed internally in the lcc of assemblies) and subtoposes with topological modalities.
We first use the modality of double negation sheafification $\nabla$ to access classical logic from within cubical assemblies. In particular, in cubical assemblies, where all functions $\mathbb{N} \to \mathbb{N}$ are computable, we can define non computable functions, such as the halting set, as functions $ \mathbb{N} \to \nabla \mathbb{N}$. Given such a function $\chi : \mathbb{N} \to \nabla \mathbb{N}$, we can naturally define a topological modality $\bigcirc[\chi]$ as the least modality forcing $\chi$ to extend to a function $\mathbb{N} \to \mathbb{N}$ (the "oracle modality" on $\chi$). More of the construction can be carried out internally than in Hyland's proof for the effective topos by identifying two useful axioms for working with these modalities that hold in cubical assemblies: computable choice and Markov induction.
By working with cubical assemblies we can easily combine this construction with higher types. I give two examples of this:
- We can use ideas from HoTT to give simpler, potentially easier to formalise, proofs of results in computability. In particular we can use the HoTT formulation of groups as pointed, connected, 1-truncated types to prove that two Turing degrees are equal as soon as they induce isomorphic permutation groups on the natural numbers.
- We can define new modalities combining computability with higher types that would be trivial in the effective topos. E.g. by taking the suspension of oracle modalities, we can define modalities making some homotopy groups non computable, while leaving others computable.
