FIBRED SETS WITHIN A PREDICATIVE AND CONSTRUCTIVE EFFECTIVE TOPOS

Abstract

Abstract We describe the fibrational structure of sets within the predicative variant pEff $\textbf {pEff}$ bold pEff 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.