Elementary Quotient Completions, Church's Thesis, and Partioned Assemblies
Maria Emilia Maietti, Fabio Pasquali, Giuseppe Rosolini

TL;DR
This paper compares the effective topos and assemblies as elementary quotient completions of a Lawvere doctrine, explaining differences in Church's Thesis validity based on categorical properties.
Contribution
It introduces a categorical framework linking effective topos and assemblies through elementary quotient completions of Lawvere doctrines.
Findings
Effective topos validates Church's Thesis internally.
Assemblies support a restricted form of Church's Thesis.
Categorical properties explain the differing Church's Thesis validity.
Abstract
Hyland's effective topos offers an important realizability model for constructive mathematics in the form of a category whose internal logic validates Church's Thesis. It also contains a boolean full sub-quasitopos of "assemblies" where only a restricted form of Church's Thesis survives. In the present paper we compare the effective topos and the quasitopos of assemblies each as the elementary quotient completions of a Lawvere doctrine based on the partitioned assemblies. In that way we can explain why the two forms of Church's Thesis each category satisfies differ by the way each is inherited from specific properties of the doctrine which determines the elementary quotient completion.
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.
