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.
| Original language | English |
|---|---|
| Pages (from-to) | 571-593 |
| Number of pages | 23 |
| Journal | Theory and Applications of Categories |
| Volume | 31 |
| Issue number | 22 |
| Publication status | Published - 22 Jun 2016 |
Keywords
- realizability toposes
- partial combinatory algebras
- geometric morphisms
- local operators
- abstract Krivine structures
- non-localic Boolean toposes