Fibred sets within a predicative and constructive effective topos
Logic
2024-12-05 v2
Abstract
We describe the fibrational structure of sets within the predicative variant of Hyland's Effective Topos previously introduced in Feferman's predicative theory of non-iterative fixpoints . Our structural analysis can be carried out in constructive and predicative variants of within extensions of Aczel's Constructive Zermelo-Fraenkel Set Theory. All this shows that the full subcategory of discrete objects of Hyland's Effective topos contains already a fibred predicative topos validating the formal Church's thesis, even when both are formalized in a constructive metatheory.
Keywords
Cite
@article{arxiv.2411.19239,
title = {Fibred sets within a predicative and constructive effective topos},
author = {Cipriano Junior Cioffo and Maria Emilia Maietti and Samuele Maschio},
journal= {arXiv preprint arXiv:2411.19239},
year = {2024}
}