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
2010 MSC: 03B40, 03E99, 03B40,18B25
Theory and Applications of Categories, Vol. 31, 2016, No. 22, pp 571-593.
Published 2016-06-22.
TAC Home