A simple presentation of the effective topos

TL;DR

This paper introduces a simplified, two-level realizability framework for the Effective Topos that avoids complex category theory, making the construction more accessible and providing semantics for higher-order type theories.

Contribution

It presents an alternative, simplified construction of the Effective Topos that does not require advanced category theory, facilitating easier understanding and application.

Findings

Simplifies the proof that the Effective Topos is a topos

Provides a semantics for higher-order type theories

Supports extensional equalities and the axiom of unique choice

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.