Mark Damuni Williams | Searcharxiv

arXiv2026

The Synthetic Sierpiński Cone

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.

math.CT↗

arXiv2025

Projective Presentations of Lex Modalities

Modalities in homotopy type theory are used to create and access subuniverses of a given type universe. These have significant applications throughout mathematics and computer science, and in particular can be used to create universes in which certain logical principles are true. We define presentations of topological modalities, which act as an internalisation of the notion of a Grothendieck topology. A specific presentation of a modality gives access to a surprising amount of computational information, such as explicit methods of determining membership of the subuniverse via internal sheaf conditions. Furthermore, assuming all terms of the presentation satisfy the axiom of choice, we are able to describe generic and powerful computational tools for modalities. This assumption is validated for presentations given by representables in presheaf categories. We deduce a local choice principle, and an internal reconstruction of Kripke-Joyal style reasoning. We use the local choice principle to show how to relate cohomology between universes, showing that a certain class of abelian groups has cohomolgoy stable between universes. We apply the methods to a prominent example, a type theory axiomatising the classifying topos of an algebraic theory, which specialises to give type theories for synthetic algebraic geometry and synthetic higher category theory. We apply the sheaf conditions to show that several presentations of interest are subcanonical, and apply the cohomology methods to show that quasi-coherent modules have cohomology stable between the Zariski, étale and fppf toposes.

cs.LO↗