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.
Elementary quotient completions, church’s thesis, and partitioned assemblies
Pasquali, F;Rosolini, G
2019-01-01
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.File | Dimensione | Formato | |
---|---|---|---|
MaiettiME_etal_eleqcc.pdf
accesso aperto
Tipologia:
Documento in versione editoriale
Dimensione
491.5 kB
Formato
Adobe PDF
|
491.5 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.