A simple presentation of the effective topos
Logic in Computer Science
2013-07-16 v1
Abstract
We propose for the Effective Topos an alternative construction: a realisability framework composed of two levels of abstraction. This construction simplifies the proof that the Effective Topos is a topos (equipped with natural numbers), which is the main issue that this paper addresses. In this our work can be compared to Frey's monadic tripos-to-topos construction. However, no topos theory or even category theory is here required for the construction of the framework itself, which provides a semantics for higher-order type theories, supporting extensional equalities and the axiom of unique choice.
Keywords
Cite
@article{arxiv.1307.3832,
title = {A simple presentation of the effective topos},
author = {Alexis Bernadet and Stéphane Graham-Lengrand},
journal= {arXiv preprint arXiv:1307.3832},
year = {2013}
}