Abstract
Geometric morphisms between realizability toposes are studied in terms
of morphisms between partial combinatory algebras (pcas). The morphisms inducing
geometric morphisms (the computationally dense ones) are seen to be the ones whose
`lifts' to a kind of completion have right adjoints. We characterize topos inclusions
corresponding to a general form of relative computability. We characterize pcas whose
realizability topos admits a geometric morphism to the eective topos.
of morphisms between partial combinatory algebras (pcas). The morphisms inducing
geometric morphisms (the computationally dense ones) are seen to be the ones whose
`lifts' to a kind of completion have right adjoints. We characterize topos inclusions
corresponding to a general form of relative computability. We characterize pcas whose
realizability topos admits a geometric morphism to the eective topos.
| Original language | English |
|---|---|
| Pages (from-to) | 874-895 |
| Number of pages | 22 |
| Journal | Theory and Applications of Categories |
| Volume | 29 |
| Issue number | 30 |
| Publication status | Published - 2014 |