The Synthetic Sierpinski Cone

1. Problem Statement

The paper addresses a fundamental tension in synthetic mathematics (specifically within Homotopy Type Theory, or HoTT) regarding the relationship between geometric constructions and logical classification of partial maps.

• The Classical Coincidence: In classical category theory and domain theory, the Sierpi´nski cone ($X_\perp$), constructed by gluing a universal closed point below a space $X$, is equivalent to the partial map classifier ($L^\circ(X)$). The latter classifies partial maps defined on open subspaces. This equivalence is a cornerstone of the duality between logic and geometry in these fields.
• The Synthetic Obstacle: In synthetic settings based on HoTT with a generic interval $I$, asserting that $X_\perp \simeq L^\circ(X)$ for all types $X$ leads to a degeneration of the theory. Specifically, if this equivalence holds universally, it forces the interval $I$ to be "codiscrete" (trivial), collapsing the distinction between open and closed subspaces and rendering all synthetic spaces trivial.
• The Core Question: Can one identify a non-trivial subuniverse of types where the Sierpi´nski cone does classify partial maps, and how does this relate to existing notions of completeness in synthetic higher category theory (specifically Segal completeness)?

2. Methodology

The authors work within Univalent Foundations (HoTT) without assuming strong axioms about the interval $I$ (such as it being a strict linear order) or using modalities globally, except where necessary for specific arguments. They utilize:

• Distributive Lattices: They parameterize their theory over a bounded distributive lattice $\Sigma$ (representing the "interval" $I$) rather than fixing a specific model.
• Localization Theory: They employ the theory of accessible reflective localizations (following Rijke et al.) to define subuniverses of "complete" types.
• Orthogonality: They define completeness via orthogonality to specific classes of maps (inclusions of horns, cones, etc.).
• Mapping Cylinders: They generalize the Sierpi´nski cone to open mapping cylinders (or open display cylinders) to handle dependent families of types.
• Modalities (Limited): They briefly use a "global points" modality ($\flat$) to analyze exponentiability of global points without collapsing the internal logic.

3. Key Contributions and Definitions

A. Hierarchy of Completeness

The paper establishes a strict hierarchy of completeness conditions for types, refining the work of Pugh and Sterling:

1. Segal Complete: Orthogonal to the inner horn inclusion $\Lambda^2_1 \hookrightarrow \Delta^2$. This is the standard condition for synthetic $\infty$-categories.
2. Based Segal Complete: Orthogonal to the family of inclusions $\{(i=1)_\perp \hookrightarrow I/i \mid i:I\}$. This is a stronger condition.
3. Little Sierpi´nski Complete: Orthogonal to the "little" comparison maps $\sigma_{(i=1)}: (i=1)_\perp \to L^\circ(i=1)$.
4. Sierpi´nski Complete: Orthogonal to the full family of comparison maps $\sigma_X: X_\perp \to L^\circ(X)$ for all $X$.

B. The Main Equivalence

The authors prove that Little Sierpi´nski Completeness is equivalent to Sierpi´nski Completeness.

• Significance: Pugh and Sterling had previously shown this equivalence only for 0-truncated types (sets). This paper extends it to untruncated types (higher groupoids/$\infty$-categories), proving that checking orthogonality against the small "little" maps is sufficient to guarantee orthogonality against all maps.

C. Separation of Segal and Based Segal Completeness

The paper resolves a conjecture by Ulrik Buchholtz, proving that Segal completeness does not imply Based Segal completeness in non-trivial contexts.

• They show that if every Segal complete type were also Based Segal complete, the interval $I$ would become quotient-initial (collapsing to a two-element set), which contradicts the properties of standard models like simplicial spaces.
• This establishes that the "Based Segal" condition is strictly stronger and necessary for the Sierpi´nski cone to function as a partial map classifier.

D. Mapping Cylinders and Partial Map Classifiers

The authors extend the Sierpi´nski cone results to open mapping cylinders ($M^\circ_Y(f)$).

• They demonstrate that for Sierpi´nski complete types, the open mapping cylinder of a function $f: X \to Y$ is equivalent to the relative partial map classifier $L^\circ_Y(f)$.
• This provides a new "right-handed" universal property for mapping cylinders within the subuniverse of Sierpi´nski complete types.

4. Key Results

1. Theorem 64 & Corollary 66: A type is Sierpi´nski complete if and only if it is Little Sierpi´nski complete. Consequently, the Sierpi´nski complete types form an accessible reflective subuniverse.
2. Corollary 48/49/50: In standard models (simplicial spaces, Dedekind cubical spaces), Based Segal completeness is strictly stronger than Segal completeness.
3. Theorem 75 & Corollary 77: The subuniverse of Sierpi´nski complete types is closed under the formation of relative open-partial map classifiers. Within this subuniverse, the open mapping cylinder $M^\circ_Y(f)$ classifies points $y:Y$ equipped with open partial elements of the fiber $\text{fib}_f(y)$.
4. Exponentiability: The paper analyzes the exponentiability of global points. It shows that while global point inclusions are exponentiable in the classical sense, they are not $L_{Segal}$-exponentiable internally unless the interval is trivial. This highlights the distinction between internal and external properties in synthetic mathematics.

5. Significance and Applications

• Denotational Semantics: In synthetic domain theory, partiality is often modeled via the partial map classifier monad $L^\circ$. The results clarify that to define lazy functions (which depend on whether an input is defined) by cases, the codomain must be Sierpi´nski complete. This implies that any synthetic domain supporting such lazy functions must satisfy the Segal condition (path transitivity) and, more strongly, the Based Segal condition.
• Synthetic Higher Category Theory: The work clarifies the structure of free cocompletion by an initial object. In synthetic $\infty$-categories, the Sierpi´nski cone $C_\perp$ is not automatically an $\infty$-category. However, within the reflective subuniverse of Sierpi´nski complete $\infty$-categories, the reflection $R(C_\perp)$ is equivalent to the partial map classifier $L^\circ(C)$. This provides a computationally tractable description of free cocompletion in these specific contexts.
• Unification of Fields: The paper successfully unifies concepts from synthetic topology, domain theory, and higher category theory. It demonstrates that the "coincidence" between the geometric Sierpi´nski cone and the logical partial map classifier is not a universal law but a property of a specific, well-behaved subuniverse of types.
• Mechanization: The authors note that their main results have been mechanized in the Agda proof assistant, ensuring the rigorous correctness of the type-theoretic arguments.

In summary, the paper resolves a critical ambiguity in synthetic mathematics by identifying the precise conditions (Sierpi´nski completeness) under which geometric constructions (cones/cylinders) align with logical classification (partial maps), while simultaneously proving that these conditions are strictly stronger than the standard requirements for synthetic $\infty$-categories.