# nLab Kleene-Vesley topos

Contents

### Context

#### Constructivism, Realizability, Computability

intuitionistic mathematics

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.