The Gleason cover of a realizability topos

Peter Johnstone

Recently Benno~van~den~Berg introduced a new class of realizability toposes which he christened Herbrand toposes. These toposes have strikingly different properties from ordinary realizability toposes, notably the (related) properties that the `constant object' functor from the topos of sets preserves finite coproducts, and that De Morgan's law is satisfied. In this paper we show that these properties are no accident: for any Schonfinkel algebra $\Lambda$, the Herbrand realizability topos over $\Lambda$ may be obtained as the Gleason cover (in the sense of Johnstone (1980)) of the ordinary realizability topos over $\Lambda$. As a corollary, we obtain the functoriality of the Herbrand realizability construction on the category of Schonfinkel algebras and computationally dense applicative morphisms.

Keywords: realizability topos, De Morgan topos, Gleason cover

2010 MSC: Primary 18B25. Secondary 03G30

Theory and Applications of Categories, Vol. 28, 2013, No. 32, pp 1139-1152.

Published 2013-12-12.

TAC Home