Weeknotes 2025-W15 › Two papers to appear in LICS ’25 › With Leoni Pugh: When is the partial map classifier a Sierpiński cone? [01A6]

Leoni Pugh is my old Part III student from 2023–2024, and this work builds on her Part III dissertation. The goal of our paper was to better understand the relationship between two approaches to partial functions in denotational semantics:

1. “Geometrical” partiality / “the Sierpiński cone”: freely add a lowest element to the space representing a given data type. This is useful for defining functions whose inputs are partially defined, because you can do a case-analysis on the definedness of the input.
2. “Logical” partiality / “the partial map classifier”: representing partially defined elements of a space $X$ by pairs $(p,x)$ where $p$ is a proposition and $x$ is a function from $\mathrm{isTrue}\left(p\right)$ to $X$. This is useful for defining functions whose outputs are partially defined.

In traditional domain theory as developed by Scott, the two kinds of partiality coincide—even constructively. I am, however, interested in synthetic domain theory which abstracts away from continuity and limits and lets you just use sets and functions rather than cpos and continuous functions—provided that you avoid non-constructive principles like the Axiom of Choice or the Law of Excluded Middle. The starting point of our work is my observation that the two notions cannot coincide absolutely in synthetic domain theory, but that there may be restricted subuniverses in which they do coincide. The main result of our paper is to define such a subuniverse, made possible by my discovery of the based Segal condition—a strengthening of the usual Segal condition for higher categories.

A broader motivation of this work is to develop synthetic domain theory and synthetic higher category theory within the same framework. Whereas synthetic domain theory traditionally concerned itself with spaces that behaved like ω-complete partial orders (but where all functions are automatically monotone and continuous), the same ideas (if applied within homotopy type theory) allow you to consider spaces that behave like ∞-categories with colimits of ω-chains (but where all functions are automatically ∞-functorial and ω-continuous). I believe that unifying domain theory and higher category theory will prove useful for studying things like the denotational semantics of concurrency, which is inherently higher-dimensional.