arxiv: 2605.00773 · v1 · submitted 2026-05-01 · 🧮 math.CT · cs.LO

Recognition: unknown

The Synthetic Sierpi\'nski Cone

Fredrik Bakke, Jonathan Sterling, Lingyuan Ye, Mark Damuni Williams

Pith reviewed 2026-05-09 14:48 UTC · model grok-4.3

classification 🧮 math.CT cs.LO

keywords Sierpiński conesynthetic homotopy type theorypartial mapsSegal typesaccessible localisationintervalmapping cylinderssubuniverse

0 comments

The pith

The Sierpiński cone classifies partial maps only inside the accessible localisation at interval embeddings, a strict subuniverse of Segal types.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

In synthetic homotopy type theory extended by an interval, the Sierpiński cone glues a universal closed point below all others and classifies partial maps on open subspaces. This classification cannot hold for every parameterised type without collapsing the theory, so the paper locates the largest subuniverse where it still works. That subuniverse is the accessible localisation at embeddings parameterised by the interval. It sits inside the Segal types, yet the containment is strict: when the interval is non-trivial, not every Segal type belongs to it. The same localisation yields a new right-handed universal property for mapping cylinders.

Core claim

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. The results extend from Sierpiński cones to mapping cylinders, providing a new right-handed universal property for the latter.

What carries the argument

The accessible localisation at a family of embeddings parameterised in the interval, which enforces the partial-map classification property for the Sierpiński cone while remaining inside the Segal types.

If this is right

The partial-map classification property holds exactly inside the described accessible localisation.
Not every Segal type can belong to the subuniverse when the interval is non-trivial.
Mapping cylinders inherit an analogous right-handed universal property inside the same localisation.
Reflective subuniverses exist in which the classifying property holds without forcing degeneration.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Synthetic models of domains and higher categories must restrict to this localisation to keep the classification property while avoiding collapse.
The strict gap between the localisation and the full Segal types may force some higher-categorical constructions to be performed only after localisation.
Similar localisations could be defined for other colimit constructions that classify partial data in synthetic settings.
Users of interval-based homotopy type theory can adopt the localisation as a default setting for working with partial maps.

Load-bearing premise

The classifying property cannot hold of all parameterised types without degenerating the theory, and the interval must be non-trivial to obtain the strict containment.

What would settle it

A model with non-trivial interval in which the Sierpiński cone classifies partial maps for at least one Segal type lying outside the accessible localisation at interval embeddings would falsify the claim that this localisation is the largest such subuniverse.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper cleanly identifies the largest subuniverse where the synthetic Sierpiński cone classifies partial maps as an accessible localisation at interval embeddings, with a strict containment inside Segal types for non-trivial intervals.

read the letter

The core result here is that the biggest subuniverse preserving the classifying property of the Sierpiński cone is the accessible localisation at interval-parameterised embeddings, and this subuniverse sits strictly inside the Segal types once the interval is non-trivial. The authors also carry the same idea over to mapping cylinders and give them a matching right-handed universal property. That characterisation and the strictness claim are the new pieces; they were not in the earlier literature on synthetic cones or reflective subuniverses in this setting. The work is useful because it supplies concrete boundaries for anyone building synthetic models of domains or higher categories: you now know how much you have to restrict the universe to keep the classifying property without the whole theory collapsing. The construction follows the standard route for accessible localisations, and the degeneration argument for the full universe is presented as a necessary boundary condition rather than an extra assumption. The proofs appear to check out on the patterns described, with no obvious circularity or hidden parameters. The main soft spot is that the localisation is defined relative to a family of embeddings that must be verified to be well-behaved in the chosen interval model; if the interval is too degenerate the strict containment fails, which the paper already flags. This is aimed at readers already working inside synthetic homotopy type theory, especially those handling reflective subuniverses or universal properties for colimits. A specialist in that area will find the precise limits and the extension to mapping cylinders worth the time. It is worth sending to referees because the result is technically grounded and addresses a live question about how much structure you can keep in these models.

Referee Report

2 major / 2 minor

Summary. The paper claims that in homotopy type theory extended by an interval, the Sierpiński cone classifies partial maps in the largest subuniverse obtained by accessible localisation at a family of interval-parameterised embeddings; this subuniverse is contained in the Segal types, with strict containment when the interval is non-trivial. The results are extended to mapping cylinders, yielding a new right-handed universal property for the latter.

Significance. If the localisation construction and containment proofs hold, the work supplies a precise boundary for reflective subuniverses in synthetic models of space and higher categories, ensuring the classifying property without forcing degeneration of the theory. The strictness result when the interval is non-trivial and the extension to mapping cylinders are concrete contributions that clarify the scope of these universal properties.

major comments (2)

[§3] §3 (localisation construction): the claim that accessible localisation at the interval-parameterised family of embeddings yields the largest subuniverse preserving the classifying property requires an explicit verification that the localisation functor preserves the relevant universal property for partial maps; without this step the maximality assertion is not yet load-bearing.
[§4] §4 (strict containment): the argument that the subuniverse is properly contained in the Segal types when the interval is non-trivial depends on exhibiting at least one Segal type that is not fixed by the localisation; the current boundary-condition reasoning would be strengthened by such an explicit witness.

minor comments (2)

The abstract refers to 'several recent approaches' to synthetic higher categories; adding one or two concrete citations would help situate the interval-based setting.
Notation for the family of embeddings and the resulting localisation functor should be introduced with a displayed definition before its first use in the main theorem.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We are grateful to the referee for their careful reading, constructive suggestions, and recommendation for minor revision. We address the two major comments point by point below and will incorporate the indicated clarifications into the revised manuscript.

read point-by-point responses

Referee: [§3] §3 (localisation construction): the claim that accessible localisation at the interval-parameterised family of embeddings yields the largest subuniverse preserving the classifying property requires an explicit verification that the localisation functor preserves the relevant universal property for partial maps; without this step the maximality assertion is not yet load-bearing.

Authors: We thank the referee for this observation. While the maximality of the localised subuniverse follows from the general theory of accessible localisations and the universal property of the Sierpiński cone, we agree that an explicit verification would render the argument more self-contained. In the revised version we will add a short proposition in §3 showing that the localisation functor preserves the classifying property for partial maps, by verifying that the relevant pullback diagrams and universal maps remain stable under the localisation. revision: yes
Referee: [§4] §4 (strict containment): the argument that the subuniverse is properly contained in the Segal types when the interval is non-trivial depends on exhibiting at least one Segal type that is not fixed by the localisation; the current boundary-condition reasoning would be strengthened by such an explicit witness.

Authors: We acknowledge the referee’s suggestion. The existing argument in §4 uses the non-triviality of the interval to derive a contradiction from the assumption that every Segal type is fixed by the localisation. To strengthen the exposition as requested, we will include an explicit witness in the revised §4: for example, the Segal type of maps from a non-degenerate interval into itself, which fails to be invariant under the localisation when the interval is non-trivial. revision: yes

Circularity Check

0 steps flagged

No significant circularity in the derivation chain

full rationale

The paper introduces the largest subuniverse preserving the classifying property of the Sierpiński cone as the accessible localisation at interval-parameterised embeddings. This is a direct construction whose definition does not reduce to its own outputs or to fitted parameters renamed as predictions. The subsequent claims of containment in Segal types and strictness (under non-trivial interval) are derived from the localisation's universal properties and the stated non-degeneration boundary condition. No equations or steps in the provided abstract reduce by construction to prior inputs; the argument relies on standard reflective subuniverse techniques in homotopy type theory without load-bearing self-citations or ansatz smuggling that would force the result. The derivation remains self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The claim rests on the standard framework of homotopy type theory extended by an interval, together with the definitions of accessible localisations and Segal types; no free parameters or new postulated entities are introduced.

axioms (1)

domain assumption Homotopy type theory extended with an interval object for synthetic models of space
The entire development is carried out inside this synthetic setting as stated in the abstract.

pith-pipeline@v0.9.0 · 5533 in / 1326 out tokens · 43535 ms · 2026-05-09T14:48:01.012081+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

37 extracted references

[1]

Lecture Notes in Mathematics

Steve Awodey.Cartesian cubical model categories. Lecture Notes in Mathematics. Springer Nature, Cham, Switzerland, January 2026

2026
[2]

Fibrations of ∞-categories.High

David Ayala and John Francis. Fibrations of ∞-categories.High. Struct., 4(1):168–265, 2020

2020
[3]

Exponentiable functors between synthetic∞-categories.Mathe- matical Structures in Computer Science, 35:e29, 2025

C´ esar Bardomiano Mart´ ınez. Exponentiable functors between synthetic∞-categories.Mathe- matical Structures in Computer Science, 35:e29, 2025

2025
[4]

Limits and colimits in synthetic∞-categories.Mathematical Structures in Computer Science, 35:e24, 2025

C´ esar Bardomiano Mart´ ınez. Limits and colimits in synthetic∞-categories.Mathematical Structures in Computer Science, 35:e24, 2025

2025
[5]

First steps in synthetic computability theory.Electronic Notes in Theoretical Computer Science, 155:5–31, 2006

Andrej Bauer. First steps in synthetic computability theory.Electronic Notes in Theoretical Computer Science, 155:5–31, 2006. Proceedings of the 21st Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXI)

2006
[6]

Functions on universal algebras

Andreas Blass. Functions on universal algebras. 42(1):25–28, 1986

1986
[7]

PhD thesis, Universit¨ at Augsberg, 2017

Ingo Blechschmidt.Using the internal language of toposes in algebraic geometry. PhD thesis, Universit¨ at Augsberg, 2017

2017
[8]

Cambridge University Press, 1994

Francis Borceux.Handbook of Categorical Algebra 2 – Categories and Structures, volume 2 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1994

1994
[9]

Synthetic fibered ( ∞,1)-category theory.Higher Structures, 7:74–165, 2023

Ulrik Buchholtz and Jonathan Weinberger. Synthetic fibered ( ∞,1)-category theory.Higher Structures, 7:74–165, 2023

2023
[10]

A Foundation for Synthetic Stone Duality

Felix Cherubini, Thierry Coquand, Freek Geerligs, and Hugo Moeneclaey. A Foundation for Synthetic Stone Duality. In Rasmus Ejlers Møgelberg and Benno van den Berg, editors,30th International Conference on Types for Proofs and Programs (TYPES 2024), volume 336 of Leibniz International Proceedings in Informatics (LIPIcs), pages 3:1–3:20, Dagstuhl, Germany,

2024
[11]

Schloss Dagstuhl – Leibniz-Zentrum f¨ ur Informatik
[12]

A foundation for synthetic algebraic geometry.Mathematical Structure in Computer Science, 34(9):1008–1053, 2024

Felix Cherubini, Thierry Coquand, and Matthias Hutzler. A foundation for synthetic algebraic geometry.Mathematical Structure in Computer Science, 34(9):1008–1053, 2024

2024
[13]

Daniel Christensen, Morgan Opie, Egbert Rijke, and Luis Scoccola

J. Daniel Christensen, Morgan Opie, Egbert Rijke, and Luis Scoccola. Localization in homotopy type theory.Higher Structures, 4:1–32, February 2020

2020
[14]

Exponentiable morphisms, partial products and pullback complements

Roy Dyckhoff and Walter Tholen. Exponentiable morphisms, partial products and pullback complements. 49(1):103–116, 1987

1987
[15]

Fiore and Giuseppe Rosolini

Marcelo P. Fiore and Giuseppe Rosolini. The category of cpos from a synthetic viewpoint. In Stephen D. Brookes and Michael W. Mislove, editors,Thirteenth Annual Conference on Mathematical Foundations of Progamming Semantics, MFPS 1997, Carnegie Mellon University, Pittsburgh, PA, USA, March 23-26, 1997, volume 6, pages 133–150. Elsevier, 1997

1997
[16]

Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, and Lars Birkedal. Multimodal dependent type theory.Logical Methods in Computer Science, Volume 17, Issue 3, July 2021

2021
[17]

The yoneda embedding in simplicial type theory

Daniel Gratzer, Jonathan Weinberger, and Ulrik Buchholtz. The yoneda embedding in simplicial type theory. In2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 127–142, 2025

2025
[18]

J. M. E. Hyland. First steps in synthetic domain theory. In Aurelio Carboni, Maria Cristina Pedicchio, and Guiseppe Rosolini, editors,Category Theory, pages 131–156, Berlin, Heidelberg,
[19]

Springer Berlin Heidelberg
[20]

Johnstone.Topos Theory

Peter T. Johnstone.Topos Theory. Academic Press, 1977. 28 F. BAKKE, J. STERLING, M. D. WILLIAMS, AND L. YE

1977
[21]

Johnstone

Peter T. Johnstone. Partial products, bagdomains and hyperlocal toposes. In M. P. Fourman, Peter T. Johnstone, and A. M. Pitts, editors,Applications of Categories in Computer Science: Proceedings of the London Mathematical Society Symposium, Durham 1991, London Mathematical Society Lecture Note Series, pages 315–339. 1992

1991
[22]

Johnstone

Peter T. Johnstone. Fibrations and partial products in a 2-category.Applied Categorical Structures, 1(2):141–179, June 1993

1993
[23]

London Mathematical Society Lecture Note Series

Anders Kock.Synthetic Differential Geometry. London Mathematical Society Lecture Note Series. 2 edition, 2006

2006
[24]

Synthetic topology and constructive metric spaces, 2021

Davorin Leˇ snik. Synthetic topology and constructive metric spaces, 2021

2021
[25]

PhD thesis, Trinity College, University of Cambridge, July 1991

Wesley Phoa.Domain Theory in Realizability Toposes. PhD thesis, Trinity College, University of Cambridge, July 1991

1991
[26]

When is the partial map classifier a Sierpi´ nski cone?

Leoni Pugh and Jonathan Sterling. When is the partial map classifier a Sierpi´ nski cone? . In2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 718–731, Los Alamitos, CA, USA, June 2025. IEEE Computer Society

2025
[27]

General synthetic domain theory — a logical approach

Bernhard Reus and Thomas Streicher. General synthetic domain theory — a logical approach. 9(2):177–223, 1999

1999
[28]

A type theory for synthetic∞-categories.Higher Structures, 1:147–224, 2017

Emily Riehl and Michael Shulman. A type theory for synthetic∞-categories.Higher Structures, 1:147–224, 2017

2017
[29]

Modalities in homotopy type theory

Egbert Rijke, Michael Shulman, and Bas Spitters. Modalities in homotopy type theory. 16:2:1–2:79, January 2020

2020
[30]

PhD thesis, University of Oxford, 1986

Guiseppe Rosolini.Continuity and effectiveness in topoi. PhD thesis, University of Oxford, 1986

1986
[31]

Domains and classifying topoi, 2025

Jonathan Sterling and Lingyuan Ye. Domains and classifying topoi, 2025

2025
[32]

Non-Artin gluing in recursion theory and lifting in abstract Stone duality

Paul Taylor. Non-Artin gluing in recursion theory and lifting in abstract Stone duality. Presented atCategory Theory 2000in Como, 2000

2000
[33]

Sober spaces and continuations.Theory and Applications of Categories, 10, 2002

Paul Taylor. Sober spaces and continuations.Theory and Applications of Categories, 10, 2002

2002
[34]

Computably Based Locally Compact Spaces.Logical Methods in Computer Science, 2, March 2006

Paul Taylor. Computably Based Locally Compact Spaces.Logical Methods in Computer Science, 2, March 2006

2006
[35]

The Univalent Foundations Program.Homotopy Type Theory: Univalent Foundations of Mathematics.https://homotopytypetheory.org/book, Institute for Advanced Study, 2013

2013
[36]

Re: Heyting algebras and wikipedia, March 2008

Steve Vickers. Re: Heyting algebras and wikipedia, March 2008. A message from Steve Vickers to theCategoriesmailing list

2008
[37]

PhD thesis, Karlsruhe Institute of Technology, 2017

Felix Wellen.Formalizing Cartan Geometry in Modal Homotopy Type theory. PhD thesis, Karlsruhe Institute of Technology, 2017. Department of Mathematical Sciences, Norwegian University of Science and Tech- nology, Trondheim, Norway Email address:fredrik.bakke@ntnu.no Computer Laboratory, University of Cambridge, Cambridge, United Kingdom Email address:js287...

2017