Characterizing partitioned assemblies and realizability toposes (Q1713020)

The article describes a characterisation of realizability toposes over a partial combinatory algebra (PCA) \(A\) as the exact completion of the category of partitioned assemblies over \(A\) (Theorem 4.2). Furthermore, from this result an extensional characterisation is derived (Theorem 4.6). The paper, starting from a result of \textit{E. Robinson} and \textit{G. Rosolini} [J. Symb. Log. 55, No. 2, 678--699 (1990; Zbl 0713.18003)] in the paper, and adapting the techniques in [\textit{P. J. W. Hofstra}, Math. Proc. Camb. Philos. Soc. 141, No. 2, 239--264 (2006; Zbl 1115.03093)], first defines the notion of discrete combinatory object (DCO), which is shown to be a generalisation of PCA (Corollary 2.15), thus, via Proposition 2.4, PCAs can be identified with a class of indexed preorders. Then, the category of partitioned assemblies over a DCO is defined as the total category over its family fibration. When a category of partitioned assemblies arise from a PCA, it is shown to have many nice properties, summarised in Corollary 3.9. From here, the sought characterisation (Theorem 4.2) is just one step away. Despite the rather technical exposition, which is necessary, the final result provides a deep insight on how realizability toposes arise from PCAs, a significant achievement that may lead to further developments, and thus the paper is of interest to anyone interested in realizability toposes.