Fibred sets within a predicative and constructive effective topos

Cipriano Junior Cioffo, Maria Emilia Maietti, Samuele Maschio

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 predicat…