The Synthetic Sierpiński Cone

2026-05-01Logic in Computer Science

Logic in Computer Science
AI summary

The authors study a construct called the Sierpiński cone, which in classical settings adds a special point to a space that helps describe partial maps. They find that in newer, more abstract models of space based on advanced type theory, this neat property of classifying partial maps does not hold universally. Instead, it only works within certain smaller collections of types, identified by the authors using a process called accessible localization. They also show that these collections fit inside a broader class called Segal types but do not cover all of them. Finally, the authors extend their findings from Sierpiński cones to a related construction called mapping cylinders, showing new universal properties there as well.

Sierpiński conepartial mapshomotopy type theorysynthetic higher categoriesaccessible localizationSegal typesreflective subuniversesmapping cylindersinterval objectuniversal property
Authors
Fredrik Bakke, Jonathan Sterling, Mark Damuni Williams, Lingyuan Ye
Abstract
In domains, categories, and toposes, the Sierpiński 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ński 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ński 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ński 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ński cones to mapping cylinders, providing a new right-handed universal property for the latter.