The Sierpinski Object in the Scott Realizability Topos

MaRDI QIDQ6318012arXivFDO

Authors Tom J. de Jong, Jaap van Oosten

Publication date 30 April 2019

Published in arXiv

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Categorical logic, topoi (03G30) Topoi (18B25)

arXiv classification

cs.LOmath.LO

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 $Sigm{a}^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.

This page was built for publication: The Sierpinski Object in the Scott Realizability Topos

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6318012)