constructive mathematics,realizability,computability
propositions as types,proofs as programs,computational trinitarianism
A realizability topos is atopos which embodies therealizability interpretation ofintuitionisticnumber theory (due to Kleene) as part of itsinternal logic. Realizability toposes form an important class ofelementary toposes that are notGrothendieck toposes, and don’t even have ageometric morphism toSet.
The input datum for forming a realizability topos is apartial combinatory algebra, or PCA.
When the PCA isKleene's first algebra, the resulting topos is called theeffective topos.
When the PCA isKleene's second algebra then is thefunction realizability topos.
There are a number of approaches toward constructing realizability toposes. One is throughtripos theory, and another is through assemblies (actually the latter is a family of related approaches).
Let be aPCA — inSet, for simplicity, but similar constructions usually work over other base toposes.
There is atripos whose base category is and for which the preorder of-indexed predicates is the set of functions from to thepowerset of. The order relation sets if there exists such that implies for all; note that must be chosen uniformly across all.
Applying the tripos-to-topos construction to this tripos produces the realizability topos over. Seetripos for details.
Let be the category ofassemblies on apartial combinatory algebra, and let be the category ofpartitioned assemblies on.
Therealizability topos is theex/reg completion of.
In the presence of theaxiom of choice, the realizability topos is theex/lex completion of, since with choice is thereg/lex completion of.
A general result about the ex/lex completion of a left exact category is that it has enough regularprojectives, meaning objects such that preserves regular epis. In fact, the regular projective objects coincide with the objects of (as a subcategory of). Of course, when is a topos, where every epi is regular, this means has enough projectives, or satisfies (external)COSHEP. It also satisfies internalCOSHEP, since binary products of projectives, i.e., products of objects of, are again objects of (seethis result).
The fact that a realizability topos is an ex/lex completion depends on theaxiom of choice forSet, since it requires the partitioned assemblies to be projective objects therein. In the absence of the axiom of choice, the projective objects in a realizability topos are the (isomorphs of) partitioned assemblies whose underlying set isprojective inSet. Thus, ifCOSHEP holds inSet, then a realizability topos is the ex/wlex completion of the category of such “projective partitioned assemblies” (wlex because this category may not have finite limits, only weak finite limits). Without some choice principle, the realizability topos may not be an ex/wlex completion at all; but it is still an ex/reg completion of.
The following is a statement characterizing realizability toposes which is analogous to theGiraud axioms characterizingGrothendieck toposes.
Alocally small category is (equivalent to) a realizability topos precisely if
hasenough projectives and thefull subcategory has allfinite limits;
has aright adjoint (which is necessarily areflective inclusion making a finite-limit preservingidempotent monad/closure operator);
factors through;
there exists an object such that
is-separated (in that its-unit is amonomorphism);
all-closedregular epimorphisms have theleft lifting property against;
for everyprojective object there is a-closed morphism.
This is due to (Frey 2014)
Stijn Vermeeren,Realizability Toposes, 2009 (pdf)
Matías Menni, Exact completions and toposes. Ph.D. Thesis, University of Edinburgh (2000). (web)
Ondomain theory in realizability toposes:
A characterization of realizability toposes analogous to theGiraud axioms forGrothendieck toposes is given in
Last revised on June 22, 2025 at 14:14:18. See thehistory of this page for a list of all contributions to it.