Contents

topos theory

Contents

Idea

The effective part of the function realizability topos $RT(\mathcal{K}_2)$.

References

This construction in realizability goes back to

• Stephen Kleene, R. E. Vesley, The foundations of intuitionistic mathematics,North-Holland (1965)

The Kleene-Vesley topos as such is discussed for instance in

• Jaap van Oosten, page 279 of Realizability: an introduction to its categorical side, Studies in Logic and the Foundations of Mathematics, vol. 152, Elsevier, 2008 (preface pdf)

Last revised on March 8, 2014 at 07:42:34. See the history of this page for a list of all contributions to it.