When is the partial map classifier a Sierpi\'nski cone?
Logic in Computer Science
2025-05-07 v2 Programming Languages
Category Theory
Abstract
We study the relationship between partial map classifiers, Sierpi\'nski cones, and axioms for synthetic higher categories and domains within univalent foundations. In particular, we show that synthetic -categories are closed under partial map classifiers assuming Phoa's principle, and we isolate a new reflective subuniverse of types within which the Sierpi\'nski cone (a lax colimit) can be computed as a partial map classifier by strengthening the Segal condition.
Cite
@article{arxiv.2504.06789,
title = {When is the partial map classifier a Sierpi\'nski cone?},
author = {Leoni Pugh and Jonathan Sterling},
journal= {arXiv preprint arXiv:2504.06789},
year = {2025}
}
Comments
To appear in to LICS 2025. Main result updated to omit unnecessary side condition (boundary separation)