Fibred Sets Within a Predicative and Constructive Effective Topos

We describe the fibrational structure of sets within the predicative variant pEff pEff bold pEff of Hyland’s Effective Topos Eff Eff bold upper E f f , previously introduced in Feferman’s classical predicative theory of non-iterative fixpoints I D 1 ^ ID₁ ModifyingAbove upper I upper D 1 With caret . Our structural analysis can be carried out also in constructive and predicative variants of Eff 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 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.