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.
There are a number of approaches toward constructing realizability toposes. One is through tripos theory, and another is through assemblies.
Let be a PCA. An (-)partitioned assembly consists of a set and a function . A morphism between partitioned assemblies is a function for which there exists such that is defined for all and . The category of partitioned assemblies is denoted .
A general result about the ex/lex completion of a left exact category is that it has enough regular projectives, 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 internal COSHEP, since binary products of projectives, i.e., products of objects of , are again objects of (see this result).