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.
http://www.tac.mta.ca/tac/volumes/28/32/28-32.dvi
http://www.tac.mta.ca/tac/volumes/28/32/28-32.ps
http://www.tac.mta.ca/tac/volumes/28/32/28-32.pdf
ftp://ftp.tac.mta.ca/pub/tac/html/volumes/28/32/28-32.dvi
ftp://ftp.tac.mta.ca/pub/tac/html/volumes/28/32/28-32.ps