constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
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.
When the PCA is Kleene's first algebra $\mathcal{K}_1$, the resulting topos is called the effective topos $RT(\mathcal{K}_1)$.
When the PCA is Kleene's second algebra $\mathcal{K}_2$ then $RT(\mathcal{K}_2)$ is the function realizability topos.
There are a number of approaches toward constructing realizability toposes. One is through tripos theory, and another is through assemblies.
…
Let $A$ be a PCA. An ($A$-)partitioned assembly $X$ consists of a set ${|X|}$ and a function $[-]_X \colon {|X|} \to A$. A morphism $X \to Y$ between partitioned assemblies is a function $f \colon {|X|} \to {|Y|}$ for which there exists $a \in A$ such that $a[x]_X$ is defined for all $x \in X$ and $a[x]_X = [f(x)]_Y$. The category of partitioned assemblies is denoted $Pass_A$.
$Pass_A$ is lextensive.
The ex/lex completion of $Pass_A$ is a topos, called the realizability topos of $A$.
A general result about the ex/lex completion $C_{ex/lex}$ of a left exact category $C$ is that it has enough regular projectives, meaning objects $P$ such that $\hom(P, -) \colon C_{ex/lex} \to Set$ preserves regular epis. In fact, the regular projective objects coincide with the objects of $C$ (as a subcategory of $C_{ex/lex}$). Of course, when $C_{ex/lex}$ is a topos, where every epi is regular, this means $C_{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 $C$, are again objects of $C$ (see this result).
Stijn Vermeeren, Realizability Toposes, 2009 (pdf)
Matías Menni, Exact completions and toposes. Ph.D. Thesis, University of Edinburgh (2000). (web)