The Synthetic Sierpi\'nski Cone

TL;DR

This paper investigates the universal properties of the Sierpiński cone in synthetic higher category models, identifying the largest subuniverse where it classifies partial maps and extending results to mapping cylinders.

Contribution

It characterizes the maximal subuniverse where the Sierpiński cone classifies partial maps and extends the universal property to mapping cylinders in synthetic models.

Findings

Largest subuniverse for classification is the accessible localisation at a family of embeddings.

The subuniverse is contained within Segal types, but not all Segal types are included when the interval is non-trivial.

Extends the universal property from Sierpiński cones to mapping cylinders.

Abstract

In domains, categories, and toposes, the Sierpi\'nski cone construction glues onto a space a universal closed point lying below all the other points. Although this is a lax colimit, it also enjoys a well-known right-handed universal property: the Sierpi\'nski cone classifies partial maps defined on an open subspace. The situation proves more subtle in synthetic models of space based on extending homotopy type theory with an interval, as in several recent approaches to synthetic higher categories and domains: although globally it may well be the case that the Sierpi\'nski cone classifies partial maps, this property cannot hold of all parameterised types without degenerating the theory. On the other hand, there are reflective subuniverses within which the classifying property nonetheless holds. We show that the largest subuniverse in which the Sierpi\'nski cone classifies partial maps is the accessible localisation at a family of embeddings parameterised in the interval, and this subuniverse is contained within the Segal types; this containment is moreover strict in the sense that when the interval is non-trivial, it is not possible for all Segal types to lie in the subuniverse. We finally extend these results from Sierpi\'nski cones to mapping cylinders, providing a new right-handed universal property for the latter.