paperbot · PL 论文追踪

RSS

The Sierpinski Object in the Scott Realizability Topos

LMCS vol.Volume 16, Issue 32020引用 0
Tom de Jong, Jaap van Oosten

尚未生成 AI 速览(可能缺少 API key 或等待下次运行补跑)。

原文摘要(Abstract)

We study the Sierpinski object $\Sigma$ in the realizability topos based on Scott's graph model of the $\lambda$-calculus. Our starting observation is that the object of realizers in this topos is the exponential $\Sigma ^N$, where $N$ is the natural numbers object. We define order-discrete objects by orthogonality to $\Sigma$. We show that the order-discrete objects form a reflective subcategory of the topos, and that many fundamental objects in higher-type arithmetic are order-discrete. Building on work by Lietz, we give some new results regarding the internal logic of the topos. Then we consider $\Sigma$ as a dominance; we explicitly construct the lift functor and characterize $\Sigma$-subobjects. Contrary to our expectations the dominance $\Sigma$ is not closed under unions. In the last section we build a model for homotopy theory, where the order-discrete objects are exactly those objects which only have constant paths.

链接与引用

DOI 原文 · arXiv · PDF(开放获取) · DBLP

BibTeX
@article{abs-1904-13354,
  title = {The Sierpinski Object in the Scott Realizability Topos},
  author = {Tom de Jong and Jaap van Oosten},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 16, Issue 3},
  year = {2020},
  doi = {10.23638/lmcs-16(3:12)2020}
}