FIBRED SETS WITHIN A PREDICATIVE AND CONSTRUCTIVE EFFECTIVE TOPOS

Abstract

We describe the fibrational structure of sets within the predicative variant

of Hyland’s Effective Topos

Eff ${\mathbf {Eff} }$ bold upper E f f

, previously introduced in Feferman’s classical predicative theory of non-iterative fixpoints

I D 1 ^ ${\widehat {ID_1}}$ ModifyingAbove upper I upper D 1 With caret

. Our structural analysis can be carried out also in constructive and predicative variants of

Eff ${\mathbf {Eff} }$ bold upper E f f

developed within extensions of Aczel’s constructive Zermelo–Fraenkel set theory. This shows that the full subcategory of discrete objects of Hyland’s Effective Topos

Eff ${\mathbf {Eff} }$ bold upper E f f

already contains a fibred predicative topos validating the Formal Church Thesis, even when both are formalized in a constructive and predicative foundational theory.