realizability topos


Topos Theory

topos theory



Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory


Constructivism, Realizability, Computability



A realizability topos is a topos which embodies the realizability interpretation of intuitionistic number theory (due to Kleene) as part of its internal logic. Realizability toposes form an important class of toposes that are not Grothendieck toposes, and don’t even have a geometric morphism to Set.

The input datum for forming a realizability topos is a partial combinatory algebra, or PCA.


There are a number of approaches toward constructing realizability toposes. One is through tripos theory, and another is through assemblies.

Via tripos theory

Via assemblies


Let AA be a PCA. An (AA-)partitioned assembly XX consists of a set X{|X|} and a function [] X:XA[-]_X \colon {|X|} \to A. A morphism XYX \to Y between partitioned assemblies is a function f:XYf \colon {|X|} \to {|Y|} for which there exists aAa \in A such that a[x] Xa[x]_X is defined for all xXx \in X and a[x] X=[f(x)] Ya[x]_X = [f(x)]_Y. The category of partitioned assemblies is denoted Pass APass_A.


Pass APass_A is lextensive.


The ex/lex completion of Pass APass_A is a topos, called the realizability topos of AA.


A general result about the ex/lex completion C ex/lexC_{ex/lex} of a left exact category CC is that it has enough regular projectives, meaning objects PP such that hom(P,):C ex/lexSet\hom(P, -) \colon C_{ex/lex} \to Set preserves regular epis. In fact, the regular projective objects coincide with the objects of CC (as a subcategory of C ex/lexC_{ex/lex}). Of course, when C ex/lexC_{ex/lex} is a topos, where every epi is regular, this means C ex/lexC_{ex/lex} has enough projectives, or satisfies (external) COSHEP. It also satisfies internal COSHEP, since binary products of projectives, i.e., products of objects of CC, are again objects of CC (see this result).


  • Stijn Vermeeren, Realizability Toposes, 2009 (pdf)

  • Matías Menni, Exact completions and toposes. Ph.D. Thesis, University of Edinburgh (2000). (web)

Revised on March 2, 2014 09:20:19 by Urs Schreiber (