×

zbMATH — the first resource for mathematics

Characterizing partitioned assemblies and realizability toposes. (English) Zbl 1422.18004
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 E. Robinson and G. Rosolini [J. Symb. Log. 55, No. 2, 678–699 (1990; Zbl 0713.18003)] in the paper, and adapting the techniques in [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.

MSC:
18B25 Topoi
03G30 Categorical logic, topoi
PDF BibTeX XML Cite
Full Text: DOI arXiv
References:
[1] Birkedal, L., A general notion of realizability, (15th Annual IEEE Symposium on Logic in Computer Science, 2000. Proceedings, (2000), IEEE), 7-17
[2] Carboni, A.; Magno, R. Celia, The free exact category on a left exact one, J. Aust. Math. Soc. (Ser. A), 33, 03, 295-301, (1982) · Zbl 0504.18005
[3] Carboni, A.; Freyd, P.; Scedrov, A., A categorical approach to realizability and polymorphic types, (Mathematical Foundations of Programming Language Semantics, (1988)), 23-42
[4] Cassidy, C.; Hébert, M.; Kelly, G. M., Reflective subcategories, localizations and factorization systems, J. Aust. Math. Soc. Ser. A, 38, 3, 287-329, (1985), MR 779198 (86j:18001) · Zbl 0573.18002
[5] Carboni, A.; Rosolini, G., Locally cartesian closed exact completions, J. Pure Appl. Algebra, 154, 1, 103-116, (2000) · Zbl 0962.18001
[6] De Marchi, F.; Robinson, E.; Rosolini, G., An abstract look at realizability, Draft, available at · Zbl 0999.03059
[7] Freyd, P. J., Abelian categories, Represent. Theory Appl. Categ., 3, 23-164, (2003), Reprint of the 1964 original · Zbl 1041.18001
[8] Frey, J., A Fibrational Study of Realizability Toposes, (2013), Paris 7 University, Ph.D. thesis
[9] Faber, E.; van Oosten, J., More on geometric morphisms between realizability toposes, Theory Appl. Categ., 29, 30, 874-895, (2014) · Zbl 1316.18006
[10] Faber, E.; van Oosten, J., Effective operations of type 2 in PCAs, Computability, 5, 2, 127-146, (2016) · Zbl 1437.03136
[11] Hyland, J. M.E.; Johnstone, P. T.; Pitts, A. M., Tripos Theory, Math. Proc. Camb. Philos. Soc., 88, 2, 205-231, (1980) · Zbl 0451.03027
[12] Hofstra, P. J.W., All realizability is relative, Math. Proc. Camb. Philos. Soc., 141, 02, 239-264, (2006) · Zbl 1115.03093
[13] Hofstra, P. J.W.; van Oosten, J., Ordered partial combinatory algebras, Math. Proc. Camb. Philos. Soc., 134, 3, 445-463, (2003) · Zbl 1046.03038
[14] Hyland, J. M.E., The effective topos, (The L.E.J. Brouwer Centenary Symposium. The L.E.J. Brouwer Centenary Symposium, Noordwijkerhout, 1981. The L.E.J. Brouwer Centenary Symposium. The L.E.J. Brouwer Centenary Symposium, Noordwijkerhout, 1981, Stud. Logic Foundations Math., vol. 110, (1982), North-Holland: North-Holland Amsterdam), 165-216, MR 717245 (84m:03101)
[15] Johnstone, P. T., The Gleason cover of a realizability topos, Theory Appl. Categ., 28, 32, 1139-1152, (2013), MR 3148489 · Zbl 1307.18001
[16] Lietz, P.; Streicher, T., Impredicativity entails untypedness, Math. Struct. Comput. Sci., 12, 03, 335-347, (2002) · Zbl 1001.03013
[17] Menni, M., More exact completions that are toposes, Ann. Pure Appl. Logic, 116, 1-3, 187-203, (2002), MR 1900904 (2003d:18004) · Zbl 0994.18002
[18] Menni, M., A characterization of the left exact categories whose exact completions are toposes, J. Pure Appl. Algebra, 177, 3, 287-301, (2003) · Zbl 1050.18002
[19] Mac Lane, S., Categories for the Working Mathematician, Graduate Texts in Mathematics, vol. 5, (1998), Springer-Verlag: Springer-Verlag New York, MR 1712872 (2001j:18001) · Zbl 0906.18001
[20] Robinson, E.; Rosolini, G., Colimit completions and the effective topos, J. Symb. Log., 55, 2, 678-699, (1990) · Zbl 0713.18003
[21] Robinson, E.; Rosolini, G., An abstract look at realizability, (Computer Science Logic, (2001), Springer), 173-187 · Zbl 0999.03059
[22] Stekelenburg, W. P., Realizability Categories, (2013), Utrecht University, Ph.D. thesis
[23] Streicher, T., Fibred categories à la Jean Bénabou, (2018), arXiv preprint
[24] van Oosten, J., Realizability: An Introduction to its Categorical Side, (2008), Elsevier Science Ltd · Zbl 1225.03002
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.