Effective topos

In mathematics, the effective topos ${\displaystyle {\mathsf {Eff}}}$ introduced by Martin Hyland (1982) captures the mathematical idea of effectivity within the category theoretical framework.

The topos is based on the partial combinatory algebra given by Kleene's first algebra ${\displaystyle {\mathcal {K}}_{1}}$. In Kleene's notion of recursive realizability, any predicate is assigned realizing numbers, i.e. a subset of ${\displaystyle {\mathbb {N} }}$. The extremal propositions are ${\displaystyle \top }$ and ${\displaystyle \bot }$, realized by ${\displaystyle {\mathbb {N} }}$ and ${\displaystyle \{\}}$. However in general, this process assigns more data to a proposition than just a binary truth value.

A formula with ${\displaystyle k}$ free variables will give rise to a map in ${\displaystyle ({\mathcal {P}}{\mathbb {N} })^{{\mathbb {N} }^{k}}}$ the values of which are the subsets of corresponding realizing numbers.

${\displaystyle {\mathsf {Eff}}}$ is a prime example of a realizability topos. These are a class of elementary topoi with an intuitionistic internal logic and fulfilling a form of dependent choice. They are generally not Grothendieck topoi.

In particular, the effective topos is ${\displaystyle {\mathsf {RT}}({\mathcal {K}}_{1})}$. Other realizability topos constructions can be said to abstract away some aspects played by ${\displaystyle {\mathbb {N} }}$ here.

There are several ways to construct the effective topos, for example, via the notion of tripos, or as the ex/reg completion of the category of assemblies. The following is a fully unfolded explicit definition.^1: 115

An object of the effective topos is a set ${\displaystyle X}$ equipped with a function ${\displaystyle E:X^{2}\to {\mathcal {P}}(\mathbb {N} )}$ satisfying certain conditions. We denote ${\displaystyle n\in E(x,y)}$ by ${\displaystyle n\Vdash x=y}$. (The notation is not standardized; the usage of the ${\displaystyle =}$ symbol overloads its normal meaning, similarly to the notation ${\displaystyle P(X=Y)}$ in probability theory.) Informally, this means that ${\displaystyle n}$ is a computational witness, or realizer of the equality ${\displaystyle x=y}$. The conditions to be satisfied are the following:

• There must exist a program ${\displaystyle e}$ such that for all ${\displaystyle n\in \mathbb {N} }$ and ${\displaystyle x,y\in X}$, if ${\displaystyle n\Vdash x=y}$ then the output of ${\displaystyle e}$ on ${\displaystyle n}$, i.e., ${\displaystyle \phi _{e}(n)}$ (where ${\displaystyle \phi _{e}}$ is the ${\displaystyle e}$-th partial computable function), is defined, and ${\displaystyle \phi _{e}(n)\Vdash y=x}$. In short, ${\displaystyle e}$ takes a realizer of ${\displaystyle x=y}$ and outputs a realizer of ${\displaystyle y=x}$ (for all ${\displaystyle x,y}$). (Note that ${\displaystyle e}$ cannot depend on ${\displaystyle x,y}$, and it only receives the realizer of ${\displaystyle x=y}$ as input, without further information on ${\displaystyle x}$ and ${\displaystyle y}$.)
• Similarly, there must exist a program which takes a realizer of ${\displaystyle x=y}$ and a realizer of ${\displaystyle y=z}$, and outputs a realizer of ${\displaystyle x=z}$ (for all ${\displaystyle x,y,z}$).

A realizer of ${\displaystyle x=x}$ will be called more simply a realizer of ${\displaystyle x}$.

A functional relation from an object ${\displaystyle X}$ to an object ${\displaystyle Y}$ is a function ${\displaystyle f:X\times Y\to {\mathcal {P}}(\mathbb {N} )}$, again satisfying certain conditions. We suggestively denote ${\displaystyle n\in f(x,y)}$ by ${\displaystyle n\Vdash f(x)=y}$ (again, this is a special notation; ${\displaystyle f(x)}$ has no meaning by itself). This informally means that ${\displaystyle n}$ realizes the fact that ${\displaystyle f}$ sends ${\displaystyle x}$ to ${\displaystyle y}$, or “realizes ${\displaystyle f(x)=y}$”. The conditions are the following:

• There exists a program which takes a realizer of ${\displaystyle f(x)=y}$ and outputs a realizer of ${\displaystyle x}$ and a realizer of ${\displaystyle y}$ (for all ${\displaystyle x\in X,y\in Y}$).
• There exists a program which takes a realizer of ${\displaystyle f(x)=y}$ and realizers of ${\displaystyle x=x'}$ and ${\displaystyle y=y'}$, and outputs a realizer of ${\displaystyle f(x')=y'}$ (for all ${\displaystyle x,x',y,y'}$).
• There exists a program which takes realizers of ${\displaystyle f(x)=y}$ and ${\displaystyle f(x)=y'}$, and outputs a realizer of ${\displaystyle y=y'}$ (for all ${\displaystyle x,y,y'}$).
• There exists a program ${\displaystyle e}$ such that for all ${\displaystyle x\in X}$ and for all realizer ${\displaystyle n}$ of ${\displaystyle x}$, there exists some ${\displaystyle y\in Y}$ such that the output ${\displaystyle \phi _{e}(n)}$ realizes ${\displaystyle f(x)=y}$.

Suppose ${\displaystyle f}$ is a functional relation from ${\displaystyle X}$ to ${\displaystyle Y}$ and ${\displaystyle g}$ is a functional relation from ${\displaystyle Y}$ to ${\displaystyle Z}$. The composition ${\displaystyle g\circ f}$ is the functional relation from ${\displaystyle X}$ to ${\displaystyle Z}$ defined by letting the realizers of ${\displaystyle (g\circ f)(x)=z}$ be the codes of pairs ${\displaystyle (r,s)}$ such that, for some ${\displaystyle y\in Y}$, we have ${\displaystyle r\Vdash f(x)=y}$ and ${\displaystyle s\Vdash g(y)=z}$. The identity functional relation ${\displaystyle \operatorname {id} }$ on an object ${\displaystyle X}$ is defined by letting the realizers of ${\displaystyle \operatorname {id} (x)=y}$ be just the realizers of ${\displaystyle x=y}$.

The morphisms from ${\displaystyle X}$ to ${\displaystyle Y}$ in the effective topos are the functional relations from ${\displaystyle X}$ to ${\displaystyle Y}$, quotiented to identify ${\displaystyle f}$ and ${\displaystyle g}$ when there exists a program which maps realizers of ${\displaystyle f(x)=y}$ to realizers of ${\displaystyle g(x)=y}$ (for all ${\displaystyle x,y}$), and another program which maps realizers of ${\displaystyle g(x)=y}$ to realizers of ${\displaystyle f(x)=y}$. Composition of morphisms is induced on the quotients by composition on the level of functional relations, and likewise for identity morphisms.

The effective topos arises as a completion of the simpler category of assemblies.

An assembly is a set ${\displaystyle X}$ equipped with a function ${\displaystyle R:X\to {\mathcal {P}}(\mathbb {N} )}$. We denote ${\displaystyle n\in R(x)}$ by ${\displaystyle n\Vdash x}$, read “${\displaystyle n}$ realizes ${\displaystyle x}$”. Every assembly ${\displaystyle X}$ can be construed as an object of the effective topos, by declaring that ${\displaystyle n}$ realizes ${\displaystyle x=y}$ when ${\displaystyle x}$ and ${\displaystyle y}$ are actually equal and ${\displaystyle n}$ realizes them in the assembly ${\displaystyle X}$. (Thus, the realizers of ${\displaystyle x}$ in ${\displaystyle X}$ as an object of the effective topos, i.e., the realizers of ${\displaystyle x=x}$, are exactly the realizers of ${\displaystyle x}$ in ${\displaystyle X}$ as an assembly.)

A morphism of assemblies ${\displaystyle f:X\to Y}$ is a function ${\displaystyle f:X\to Y}$ between the underlying sets such that there exists a program, independent of ${\displaystyle x\in X}$, which maps realizers of ${\displaystyle x}$ to realizers of ${\displaystyle f(x)}$. Such a morphism gives rise to a morphism in the effective topos, represented by the functional relation (still denoted ${\displaystyle f}$) where ${\displaystyle f(x)=y}$ is realized if and only if ${\displaystyle f(x)}$ is actually equal to ${\displaystyle y}$, and then the realizers of ${\displaystyle f(x)=y}$ are the pairs of a realizer of ${\displaystyle x}$ and a realizer of ${\displaystyle y}$.

This correspondence makes the category of assemblies a full subcategory of the effective topos.

The category of sets is a full subcategory of the category of assemblies, via the functor ${\displaystyle \nabla }$ that maps a set ${\displaystyle X}$ to the assembly with underlying set ${\displaystyle X}$ where every element is realized by every natural number. In particular, the category of sets is also a full subcategory of the effective topos.^1: 117

The effective topos is an elementary topos with natural numbers object. This means that it supports a number of standard categorical constructions, which are explicitly performed as follows.

• The initial object is the empty assembly.
• The terminal object is the unit assembly, a singleton where the unique element is realized by every natural number.
• The natural numbers object is ${\displaystyle \mathbb {N} }$ where each natural number is realized only by itself.
• The product of two objects ${\displaystyle X}$ and ${\displaystyle Y}$ is the Cartesian product of sets ${\displaystyle X\times Y}$ where a realizer of ${\displaystyle (x,y)}$ in ${\displaystyle X\times Y}$ is the code of a pair of a realizer of ${\displaystyle x}$ and a realizer of ${\displaystyle y}$.
• The coproduct of ${\displaystyle X}$ and ${\displaystyle Y}$ is the coproduct of sets ${\displaystyle X+Y}$ where a realizer of ${\displaystyle x\in X}$ in ${\displaystyle X+Y}$ is the code of a pair of 0 and a realizer of ${\displaystyle x}$ in ${\displaystyle X}$, and a realizer of ${\displaystyle y\in Y}$ in ${\displaystyle X+Y}$ is the code of a pair of 1 and a realizer of ${\displaystyle y}$ in ${\displaystyle Y}$.
• The subobject classifier ${\displaystyle \Omega }$ is ${\displaystyle {\mathcal {P}}(\mathbb {N} )}$ where a realizer of ${\displaystyle P=Q}$ is a pair of a program which returns an element of ${\displaystyle Q}$ given an element of ${\displaystyle P}$, and a program which returns an element of ${\displaystyle P}$ given an element of ${\displaystyle Q}$. It is not (isomorphic to) an assembly.

Some objects exhibit a rather trivial existence predicate depending only on the validity of the equality relation "${\displaystyle =}$" of sets, so that valid equality maps to the top set ${\displaystyle \mathbb {N} }$ and rejected equality maps to ${\displaystyle \{\}}$. This gives rise to a full and faithful functor ${\displaystyle \nabla \colon {\mathsf {Sets}}\to {\mathsf {Eff}}}$ out of the category of sets, which has the finite-limit preserving global sections functor ${\displaystyle \Gamma }$ as its left-adjoint. This factors through a finite-limit preserving, full and faithful embedding ${\displaystyle \omega }$-${\displaystyle {\mathsf {Sets}}\to {\mathsf {Eff}}}$.

The topos has a natural numbers object ${\displaystyle N=\langle {\mathbb {N} },E_{\mathbb {N} }\rangle }$ with simply ${\displaystyle E_{\mathbb {N} }(n)=\{n\}}$. Sentences true about ${\displaystyle N}$ are exactly the recursively realized sentences of Heyting arithmetic ${\displaystyle {\mathsf {HA}}}$.

Now arrows ${\displaystyle N\to N}$ may be understood as the total recursive functions and this also holds internally for ${\displaystyle N^{N}}$. The latter is the pair given by total recursive functions ${\displaystyle \mathrm {TR} }$ and a relation such that ${\displaystyle E_{\mathrm {TR} }(f)}$ is the set of codes ${\displaystyle e\in {\mathbb {N} }}$ for ${\displaystyle f}$. The latter is a subset of the naturals but not just a singleton, since there are several indices computing the same recursive function. So here the second entry of the objects represent the realizing data.

With ${\displaystyle N}$ and functions from and to it, as well as with simple rules for the equality relations when forming finite products ${\displaystyle \times }$, one may now more broadly define the hereditarily effective operations. Again one may think of functions in ${\displaystyle N^{N}}$ as given by indices and their equality is determined by the objects that compute the same function. This equality clearly puts a constraint on ${\displaystyle N^{(N^{N})}}$, as these functions come out to be only those computable functions that also properly respect the mentioned equality in their domain. Et cetera. The situation for general ${\displaystyle \langle X,E_{X}\rangle \to \langle Y,E_{Y}\rangle }$, equality (in the sense of the ${\displaystyle E}$'s) in domain and image must be respected.

With this, one may validate Markov's principle ${\displaystyle {\mathrm {MP} }}$ and the extended Church's principle ${\displaystyle {\mathrm {ECT} }_{0}}$ (and a second-order variant thereof), which come down to simple statement about object such as ${\displaystyle N^{N}}$ or ${\displaystyle (1+1)^{N}}$. These imply ${\displaystyle {\mathrm {CT} }_{0}}$ and independence of premise ${\displaystyle {\mathrm {IP} }_{0}}$.

A choice principle ${\displaystyle N^{N}}$ related to Brouwerian weak continuity fails. From any object, there are only countably many arrows to ${\displaystyle N}$. ${\displaystyle \Omega ^{N}}$ fulfills a uniformity principle. ${\displaystyle N}$ is not the countable coproduct of copies of ${\displaystyle 1}$. This topos is not a category of sheaves.

The object ${\displaystyle \langle {\mathbb {Q} }^{\mathbb {N} },E_{{\mathbb {Q} }^{\mathbb {N} }}\rangle }$ is effective in a formal sense and from it one may define computable Cauchy sequences. Through a quotient, the topos has a real numbers object which has no non-trivial decidable subobject. With choice, the notion of Dedekind reals coincides with the Cauchy one.

Analysis here corresponds to the recursive school of constructivism. It rejects the claim that ${\displaystyle x\leq 0\lor 0\leq x}$ would hold for all reals ${\displaystyle x}$. Formulations of the intermediate value theorem fail and all functions from the reals to the reals are provenly continuous. A Specker sequence exists and then Bolzano–Weierstrass fails.