A predicative variant of Hyland's Effective Topos

TL;DR

This paper introduces pEff, a predicative subcategory of Hyland's Effective Topos, designed to model constructive mathematics within a predicative framework, validating the Formal Church's thesis.

Contribution

It constructs pEff as a predicative variant of Eff, formalizable in Feferman's ID1, and embeds it into Eff while preserving key categorical structures.

Findings

pEff is a list-arithmetic locally cartesian closed pretopos.

pEff coincides with the exact completion of a predicative subcategory of Eff.

It validates the Formal Church's thesis within a predicative setting.

Abstract

Here, we present a subcategory pEff of Hyland's Effective Topos Eff which can be considered a predicative variant of Eff itself. The construction of pEff is motivated by the desire of providing a "predicative" categorical universe of realizers to model the Minimalist Foundation for constructive mathematics which was ideated by the first author with G. Sambin in 2005 and completed into a two-level formal system by the first author in 2009. pEff is a "predicative" categorical universe because its objects and morphisms can be formalized in Feferman's predicative weak theory of inductive definitions ID1^. Moreover, it is a predicative variant of the Effective Topos for the following reasons. First, pEff is a list-arithmetic locally cartesian closed pretopos of definable objects in dID1 with a fibred category of small objects over pEff and a (non-small) classifier of small subobjects. Second, it happens to coincide with the exact completion on the lex category defined as a predicative rendering in ID1^ of the subcategory of Eff of recursive definitions. As a consequence it validates the Formal Church's thesis and it embeds in Eff by preserving the list-arithmetic locally cartesian closed pretopos structure.