Variations on realizability: realizing the propositional axiom of choice
J. M. E. Hyland · Mathematical Structures in Computer Science · 2002
Realizability and related functional interpretations provide models for constructive mathematics. Generally, these models do not validate the axiom of choice for propositions taken over hierarchies of extensional functionals. We describe simple classes of models where the axiom is validated.