2013/01/01 by Alexis Bernadet, Bernadet, Alexis, Stéphane Graham-Lengrand +1
Computer Science · Mathematics · #FOS: Computer and information sciences #Homotopy and Cohomology in Algebraic Topology #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #cs.LO
paper · pdf · doi:10.48550/arxiv.1307.3832
arxiv created 2013/07/15 · openalex publication_date 2013/07/15 · arxiv updated 2013/07/16 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.