Fibred sets within a predicative and constructive effective topos
Cipriano Junior Cioffo, Maria Emilia Maietti, Samuele Maschio

TL;DR
This paper analyzes the fibrational structure of sets within a predicative variant of Hyland's Effective Topos, showing it forms a fibred predicative topos validating Church's thesis in a constructive setting.
Contribution
It provides a structural analysis of fibred sets in a predicative effective topos, extending the understanding of its fibrational and logical properties within constructive set theories.
Findings
The subcategory of discrete objects forms a fibred predicative topos.
The structure validates the formal Church's thesis.
Analysis is carried out within constructive and predicative set theories.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFuzzy and Soft Set Theory
