Classical and relative realizability
Publication date
2016-06-22
Authors
van Oosten, Jakobus
Zou, Tingxiang
Editors
Advisors
Supervisors
DOI
Document Type
Article
Metadata
Show full item recordCollections
License
Abstract
We show that every abstract Krivine structure in the sense of Streicher can be obtained, up to equivalence of the resulting tripos, from a filtered opca (A,A') and a subobject of 1 in the relative realizability topos RT(A',A); the topos is always a Boolean subtopos of RT(A',A). We exhibit a range of non-localic Boolean subtriposes of the Kleene-Vesley tripos.
Keywords
realizability toposes, partial combinatory algebras, geometric morphisms, local operators, abstract Krivine structures, non-localic Boolean toposes
Citation
van Oosten, J & Zou, T 2016, 'Classical and relative realizability', Theory and Applications of Categories, vol. 31, no. 22, pp. 571-593. < http://www.tac.mta.ca/tac/volumes/31/22/31-22abs.html >