Fibred sets within a predicative and constructive effective topos

TL;DR

This paper analyzes the fibrational structure of sets within a predicative variant of Hyland's Effective Topos, showing it forms a fibred predicative topos validating Church's thesis in a constructive setting.

Contribution

It provides a structural analysis of fibred sets in a predicative effective topos, extending the understanding of its fibrational and logical properties within constructive set theories.

Findings

The subcategory of discrete objects forms a fibred predicative topos.

The structure validates the formal Church's thesis.

Analysis is carried out within constructive and predicative set theories.

Abstract

We describe the fibrational structure of sets within the predicative variant $\mathbf{pEff}$ of Hyland's Effective Topos $\mathbf{Eff}$ previously introduced in Feferman's predicative theory of non-iterative fixpoints $\widehat{ID_1}$. Our structural analysis can be carried out in constructive and predicative variants of $\mathbf{Eff}$ within extensions of Aczel's Constructive Zermelo-Fraenkel Set Theory. All this shows that the full subcategory of discrete objects of Hyland's Effective topos $\mathbf{Eff}$ contains already a fibred predicative topos validating the formal Church's thesis, even when both are formalized in a constructive metatheory.