一句话：把有效 topos 与装配拟 topos 都看作基于分划装配的 Lawvere doctrine 的初等商完成，以解释两种 Church 论题差异。
Hyland 的有效 topos 是构造数学的重要可实现性模型，其内部逻辑使 Church 论题成立；它包含一个由装配组成的布尔满子拟 topos，其中只有受限形式的 Church 论题成立。本文比较有效 topos 与装配拟 topos，将二者分别构造为基于分划装配的 Lawvere doctrine 的初等商完成。通过分析该 doctrine 的特定性质如何被初等商完成继承，作者解释了这两个范畴各自满足的 Church 论题为何不同。论文属于范畴论与可实现性语义的基础研究，为理解不同商完成构造对内部逻辑的影响提供了统一框架。
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.
@article{paperbot785,
title = {Elementary Quotient Completions, Church's Thesis, and Partioned Assemblies},
author = {Maria Emilia Maietti and Fabio Pasquali and Giuseppe Rosolini},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 2},
year = {2019},
doi = {10.23638/lmcs-15(2:21)2019}
}