Maria Emilia Maietti

FIBRED SETS WITHIN A PREDICATIVE AND CONSTRUCTIVE EFFECTIVE TOPOS

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...