Classical and Relative Realizability
Category Theory
2016-03-14 v1 Logic
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 Booleanization of a closed subtopos of RT(A',A). We exhibit a range of non-localic Boolean subtoposes of the Kleene-Vesley topos.
Cite
@article{arxiv.1603.03621,
title = {Classical and Relative Realizability},
author = {Jaap van Oosten and Tingxiang Zou},
journal= {arXiv preprint arXiv:1603.03621},
year = {2016}
}
Comments
22 pages