jonmsterling.com
+312
lics.tex
+312
lics.tex
···+In a 2-category of spaces, the \emph{mapping cone} of a continuous function $f\colon A\to B$ glues a copy of $A$ onto its image in $B$ by means of a system of directed 2-cells $\gamma_a\colon fa\Rightarrow a$; this is the lax colimit of the diagram $\{ f\colon A\to B\}$. In the case of the punctual map $!_A\colon A\to\mathbf{1}$, this gives the \emph{Sierpi\'nski cone} which adjoins an initial point to the space $A$. In certain 2-categories, this lax colimit also enjoys a \emph{right-handed} universal property, which is well-known in the case of the Sierpi\'nski cone: for example, in $\mathbf{Cat}$ and in $\mathbf{Topos}$, the Sierpi\'nski cone classifies partial maps defined on an open subspace of their domain.+The situation becomes more subtle in synthetic models of space based on extending homotopy type theory with a generic interval, as in several recent approaches to synthetic higher categories and domains. In these cases, although \emph{globally} it may well be the case that the Sierpi\'nski cone classifies partial maps, this property cannot descend unconditionally to \emph{parameterised} types without degenerating the theory.+Pugh and Sterling previously identified a slight strengthening of the Segal condition that generates an accessible reflective subuniverse of $0$-truncated types in which the Sierpi\'nski cone can be computed as a partial map classifier. We generalise the results of \emph{op.~cit.}\ by dealing with general mapping cones in both lax and oplax orientation, and by removing the restriction to $0$-truncated types so that the theory becomes applicable to totally untruncated synthetic $(\infty,1)$-categories.+In both category theory and domain theory, there is a remarkable coincidence involving the Sierpi\'nski object $\II\equiv \{ 0\hookrightarrow 1 \}$. A figure $\II\xrightarrow{\alpha}\mathbb{C}$ represents an arrow $\alpha \colon \alpha(0)\to \alpha(1)$ in $\mathbb{C}$; on the other hand, an arrow $\mathbb{C}\xrightarrow{\chi}\II$ classifies an ``open'' subspace of $\mathbb{C}$ given by the pre-image of $1\in \II$.+The two-handedness of $\II$ extends to an identification between the \emph{Sierpi\'nski cone} and the \emph{partial map classifier} of any space $\XX$, which we illuminate below. The Sierpi\'nski cone $\XX_\bot$ of a space $\XX$ is the following co-comma square, which we may compute by means of a pushout:+\One\arrow[r,swap,closed immersion,"\bot_\XX"]\ar[ur,phantom,"{\Uparrow}\gamma_\XX"] & \XX\mathrlap{_\bot}+\XX\ar[r,closed immersion,"{(0,\XX)}"]\ar[d] & \II\times\XX \ar[d,"\gamma_\XX"description] & \XX\ar[l,open immersion,swap,"{(1,\XX)}"]\ar[dl,sloped,swap,open immersion,"\iota_\XX"] \\+\One\ar[r,swap,closed immersion,"\bot_\XX"] & \XX\mathrlap{_\bot}\ar[ul,phantom,very near start,"\ulcorner"]+The (open) partial map classifier $\eta_\XX\colon \XX\hookrightarrow L(\XX)$ is, on the other hand, the partial product of $\XX$ with the open embedding $\{1\}\hookrightarrow \II$ and classifies spans+where $U$ is an \emph{open} subspace of $\mathbb{Y}$, \emph{i.e.}\ a pullback of $\{1\}\hookrightarrow \II$ in the sense that every such span arises in the context of a unique pullback square:+U\ar[r]\ar[d,open immersion]\ar[dr,phantom,very near start,"\lrcorner"] & \XX\ar[d,open immersion,"\eta_\XX"]\\+Now, it so happens that we may define a universal comparison map $\sigma_\XX\colon \XX_\bot\to L(\XX)$ using \emph{either} the universal property of the Sierpi\'nski cone or the universal property of the partial map classifier. In the former case, we construct a lax square (left) and in the latter case we observe that $\iota_\XX\colon \XX\hookrightarrow \XX_\bot$ is an open embedding and construct a partial map (right):+|[gray]|\varnothing \ar[u,gray,open immersion]\ar[ur,gray,phantom,very near start,"\urcorner"] \ar[r,gray,-{Triangle[fill=gray]}, hook] & |[gray]|\XX \ar[u,swap,gray,open immersion,"\eta_\XX"]+\XX\ar[r,equals]\ar[d,open immersion,swap,"\iota_\XX"]\ar[dr,phantom,very near start,"\lrcorner"] & \XX\ar[d,open immersion,"\eta_\XX"]\\+The promised coincidence is that the induced comparison map $\XX_\bot\to L(\XX)$ is invertible. This property also extends to models of higher categories such as simplicial sets: when \[ L(X) \equiv \textstyle\sum_{(i:\Spx{\One})}X^{(i=1)}\] is the open partial map classifier of a simplicial set,\footnote{We mean, $L(X)$ classifies partial maps whose support is classified by the open embedding $\{1\}\hookrightarrow \Spx{\One}$.} it actually happens that $L(X)$ is the directed join of simplicial sets $\Spx{\Zero}\star X \cong X_\bot$. It may therefore be reasonable to say that the correspondence between these two views on partiality is part of the core logic--geometry duality that underpins (higher) category theory, domain theory, topology, \emph{etc.}+Surprisingly, the situation changes considerably when passing to synthetic notions of space---as in synthetic domain theory, synthetic topology, and synthetic (higher) category theory---when expressed in the language of Martin-L\"of type theory or, indeed, homotopy type theory, extended by a generic interval $\II$. The problem is that in dependent type theory, it is unexpectedly strong to assert an axiom like+because statements in type theory are automatically invariant under change-of-context.\footnote{Indeed, context invariance is in some sense the entire reason for dependent type theory to exist at all.} Indeed, \citet{pugh-sterling-2025} noted that under this assumption, we could deduce+from which it follows that the boundary inclusion $\{0\}+\{1\}\hookrightarrow \mathbb{I}$ is an equivalence and hence that all synthetic spaces are codiscrete.+When a dependent type theorist working in a topos $\mathcal{S}$ says \emph{``Let $X$ be a type\ldots''}, what follows is in some sense taking place not in $\mathcal{S}$ but in the classifying topos $\mathcal{S}[X]$ of an object over $\mathcal{S}$. So an assumed type is, in the dependent type theoretic interpretation, a \emph{generic} type rather than an \emph{arbitrary} type. In contrast, a practitioner of the Mitchell--B\'enabou language of toposes would explain the same turn of phrase as a conservative use of \emph{prenex polymorphism} over simple type theory; a schema of this kind can only be instantiated with a global type, and so the bad deduction \eqref{bad-deduction} would not obtain.+Those who do not wish to sacrifice all the advantages of dependent type theory may instead introduce \emph{modalities} that can be used to safely state assumptions that are meant to hold only globally. These modalities do come at a cost, but they have proved indispensible to prior work in the general development of synthetic higher category theory inside dependent type theory~\citep{11186122}.+Although either suggestion above may be used to faithfully express the partial map classification property of the Sierpi\'nski cone, we recall Steve Vickers' parable concerning the use of violence in mathematics~\citep{vickers-categories-2008-elephant}:+As a parable, I think of toposes as gorillas (rather tha[n] elephants). At first they look very fierce and hostile, and the locker-room boasting is all tales of how you overpower the creature and take it back to a zoo to live in a cage---if it’s lucky enough not to have been shot first. When it dies you stuff it, mount it in a threatening pose with its teeth bared and display it in a museum to frighten the children. But get to know them in the wild, and gain their trust, then you begin to appreciate their gentleness and can play with them.+It was in Vickers' immanent spirit that \citeauthor{pugh-sterling-2025} sought an internally viable analysis of the comparison map $\sigma_X\colon X_\bot\to L(X)$ for \emph{generic} $X$ in the dependent type theoretic sense.+Notwithstanding the fact that we cannot expect the comparison map $\sigma_X \colon X_\bot\to L(X)$ to be an equivalence for generic $X$, there are many types $C$ that are nonetheless \emph{internally orthogonal} to all $\sigma_X$, in the sense that the restriction map+is an equivalence. \citeauthor{pugh-sterling-2025} referred to these ``local'' types as \emph{Sierpi\'nski complete}, and sought to show that they formed an accessible reflective subuniverse in the sense of \citet{rijke-shulman-spitters:2020} that is moreover closed under the formation of partial map classifiers $L(X)$. In such a subuniverse, one could compute the Sierpi\'nski cone \emph{as} the partial map classifier without resorting to higher inductive types.+Given the overwhelming size of the localising class \[ \mathcal{L}_{\mathit{Sierp}} \equiv \{\sigma_X\colon X_\bot \to L(X)\mid X\ \mathit{type}\}\text{,}\] reflectivity was a tall order, however.+The key geometrical observation of \citeauthor{pugh-sterling-2025} was that under reasonable assumptions, the generic inner horn inclusion $\Horn \hookrightarrow \Spx{\Two}$ is actually the \emph{sum} of all ``little'' comparison maps \[ i:\II \vdash \sigma_{(i=1)}\colon (i=1)_\bot \hookrightarrow L(i=1)\] in the sense that we have the following for generic $i:\II$+(i=1)_\bot\ar[r,hookrightarrow]\ar[d,hookrightarrow,swap,"\sigma_{(i=1)}"]\ar[dr,phantom,very near start,"\lrcorner"] & \Horn \ar[d,hookrightarrow]\ar[r,"\cong"description]\ar[dr,phantom,very near start,"\lrcorner"] & \sum_{i:\II}(i=1)_\bot\ar[d,"\sum_{(i:\II)}\sigma_{(i=1)}"]+L(i=1)\ar[r,hookrightarrow]\ar[d]\ar[dr,phantom,very near start,"\lrcorner"] & \Spx{\Two}\ar[dr,phantom,very near start,"\lrcorner"] \ar[d,"\max"description]\ar[r,"\cong"description] & \sum_{(i:\II)} L(i=1)\ar[d,"\pi_1"]+Types internally orthogonal to the inner horn inclusion $\Horn\hookrightarrow\Spx{\Two}$ are well-studied already; in synthetic higher category theory~\citep{riehl-shulman:2017}, this is called \emph{Segal completeness}, and in the context of synthetic domain theory, has been referred to as \emph{path transitivity} by \citet{fiore-rosolini:1997:cpos}. In either case, the intuition for this condition is that an extension+Therefore a \emph{Segal complete} type is one that has a coherent composition operation for arrows. \citet{riehl-shulman:2017} point out that the internal orthogonality condition ensures not only the existence of composites, but also associators, pentagonators, \emph{etc.}\footnote{This is in contrast to the usual external formulation, in which one must consider inner horns of arbitrary dimension.}+\citeauthor{pugh-sterling-2025} referred to the types that are internally orthogonal to \[ \sigma_{(i=1)}\colon (i=1)_{\bot}\hookrightarrow L(i=1) \] for generic $i:\II$ as \emph{based Segal complete}. It follows immediately from the description of $\Horn\hookrightarrow \Spx{\Two}$ as $\sum_{(i:\II)}\sigma_{(i=1)}$ that any based Segal complete type is Segal complete. Therefore, the based Segal completeness condition gives rise to a natural strengthening of the notion of a synthetic $(\infty,1)$-category.+\citeauthor{pugh-sterling-2025} conjectured that a generic type would be based Segal complete if and only if it is Sierpi\'nski complete, but they only achieved the following more restricted result:+\emph{A $0$-truncated type (\emph{i.e.}\ a set) is based Segal complete if and only if it is Sierpi\'nski complete.}~\citep[Lemma~6.1, Theorem 6.6]{pugh-sterling-2025}+The above restriction to $0$-truncated types was deeply disappointing, because the only synthetic $(\infty,1)$-categories that are $0$-truncated are the synthetic posets. Therefore, the results of \emph{loc.~cit.}\ are applicable to traditional synthetic domain theory, but fail to shed light on higher-dimensional notions of space (including synthetic higher categories and, putatively, synthetic higher domains).+The Sierpi\'nski cone is a special case of a more general co-comma construction that yields the \emph{Artin glueing} or \emph{closed mapping cone} of a function $f\colon X\to Y$:+Our first observation is that in the synthetic setting, the above is evidently a \emph{family} of Sierpi\'nski cones. Indeed, any $f\colon X\to Y$ may be identified with its ``fibrant replacement''+and under this identification, the Artin glueing of $f$ becomes the sum of all the Sierpi\'nski cones of the fibres of $f\colon X\to Y$,+\sum_{(y:Y)}\mathsf{fib}_f(y)\ar[r,equals]\ar[d,swap,"\sum_{(y:Y)}\star"] & \sum_{(y:Y)}\mathsf{fib}_f(y) \ar[d,open immersion,"\iota_f"]\\+\sum_{(y:Y)}\mathbf{1}\arrow[r,swap,closed immersion,"\bot_f"]\ar[ur,phantom,"{\Uparrow}\sum_{(y:Y)}\gamma_{\mathsf{fib}_f(y)}"] & \sum_{(y:Y)} (\mathsf{fib}_f(y))_\bot+keeping in mind that the summing functor \[ \textstyle\sum_{Y}\colon \mathbf{Type}/Y\to \mathbf{Type} \]+preserves colimits by virtue of being left adjoint to pullback. Thus any insight of Sierpi\'nski cones can be straightforwardly transformed into an insight about general Artin glueings; this allows us, in particular, to characterise the right-handed universal property of Artin glueings within certain reflective subuniverses in terms of partial map classifiers, adapting the results of \citeauthor{pugh-sterling-2025} concerning the latter.+The Sierpi\'nski cone of a space $X$ is contains $X$ as an \emph{open} subspace above a minimal closed point as depicted below:+\One\arrow[r,swap,closed immersion,"\bot_X"]\ar[ur,phantom,"{\Uparrow}\gamma_X"] & X\mathrlap{_\bot}+There is a dual construction $X^\top$ in which we change the orientation of the cylinder so as to obtain $X$ as a \emph{closed} subspace under a maximal open point, \citet{taylor:2000} refers to as \emph{inverted Sierpi\'nski cone}:+\One\arrow[r,swap,open immersion,"\top_X"]\ar[ur,phantom,"{\Downarrow}\bar\gamma_X"] & X\mathrlap{^\top}+We may compare the above with the notion of \emph{co-partial map} studied by \citet{hyland:1991} and its \emph{co-partial map classifier} \[ T(X) :\equiv \textstyle\sum_{(i:\II)} X^{(i=0)}\]+(i=0)^\top\ar[r,hookrightarrow]\ar[d,hookrightarrow,swap,"\bar\sigma_{(i=0)}"]\ar[dr,phantom,very near start,"\lrcorner"] & \Horn \ar[d,hookrightarrow]\ar[r,"\cong"description]\ar[dr,phantom,very near start,"\lrcorner"] & \sum_{i:\II}(i=0)^\bot\ar[d,"\sum_{(i:\II)}\bar\sigma_{(i=0)}"]+T(i=0)\ar[r,hookrightarrow]\ar[d]\ar[dr,phantom,very near start,"\lrcorner"] & \Spx{\Two}\ar[dr,phantom,very near start,"\lrcorner"] \ar[d,"\min"description]\ar[r,"\cong"description] & \sum_{(i:\II)} T(i=0)\ar[d,"\pi_1"]+This suggests that the ``Sierpi\'nski completness'' and ``based Segal completeness'' of \citeauthor{pugh-sterling-2025} amount to but one side of a pair of topologically dual conditions corresponding to different orientations the glueing. For this reason, it seems appropriate to use the following terminology for generic $C$:+\item $C$ is called \emph{Sierpi\'nski complete} when it is orthogonal to $\sigma_X\colon X_\bot\to L(X)$ for generic $X$, and \emph{upper Segal complete} when it is orthogonal to $\sigma_{i=1}\colon (i=1)_\bot\hookrightarrow L(i=1)$ for generic $i:\II$.+\item $C$ is called \emph{inverted Sierpi\'nski complete} when it is orthogonal to $\bar\sigma_X\colon X^\top\to T(X)$ for generic $X$, and \emph{lower Segal complete} when it is orthogonal to $\bar\sigma_{i=0}\colon (i=0)^\top\hookrightarrow T(i=0)$ for generic $i:\II$.+Our first result is to resolve the conjecture of \citeauthor{pugh-sterling-2025} in the positive: a generic type is upper Segal complete if and only if it is Sierpi\'nski complete, without any truncation condition whatsoever. From this, we obtain a range of reflective subuniverses of synthetic $(\infty,1)$-categories of all truncation levels in which the Sierpi\'nski cone (a lax colimit) may be computed as the partial map classifier.+Dualising, we obtain the same result for \emph{inverted} Sierpi\'nski completeness and \emph{lower} Segal completeness, yielding reflective subuniverses of synthetic $(\infty,1)$-categories in which the inverted Sierpi\'nski cone (an oplax colimit) may be computed as Hyland's co-partial map classifier.+Finally, we observe that the results above imply similar right-handed universal properties for both \emph{closed} and \emph{open} mapping cones in appropriate subcategories. This provides a particularly simple description of the Artin glueing (closed mapping cone) of a map $f\colon A\to B$ within any subuniverse of upper Segal complete types as a classifying space for elements of $B$ equipped with a partial element of the corresponding \emph{fibre} of $f$. Dually, we find that the open mapping cone of $f$ within any subuniverse of lower Segal complete types is the classifying space for elements of $B$ equipped with a co-partial element of the corresponding fibre of $f$.
+10
-10
main.tex
+10
-10
main.tex
···-In both category theory and domain theory, there is a remarkable coincidence involving the Sierpi\'nski object $\II\equiv \{ 0\hookrightarrow 1 \}$. A figure $\II\xrightarrow{\alpha}\mathbb{C}$ represents an arrow $\alpha \colon \alpha(0)\to \alpha(1)$ in $\mathbb{C}$; on the other hand, an arrow $\mathbb{C}\xrightarrow{\chi}\II$ represents an ``open'' subspace of $\mathbb{C}$ given by the preimage of $1\in \II$.+In both category theory and domain theory, there is a remarkable coincidence involving the Sierpi\'nski object $\II\equiv \{ 0\hookrightarrow 1 \}$. A figure $\II\xrightarrow{\alpha}\mathbb{C}$ represents an arrow $\alpha \colon \alpha(0)\to \alpha(1)$ in $\mathbb{C}$; on the other hand, an arrow $\mathbb{C}\xrightarrow{\chi}\II$ represents an ``open'' subspace of $\mathbb{C}$ given by the preimage of $1\in \II$.The two-handedness of $\II$ extends to an identification between the \emph{Sierpi\'nski cone} and the \emph{partial map classifier} of any space $\XX$, which we illuminate below. The Sierpi\'nski cone $\XX_\bot$ of a space $\XX$ is the following co-comma square, which we may compute by means of a pushout:\One\arrow[r,swap,closed immersion,"\bot_\XX"]\ar[ur,phantom,"{\Uparrow}\gamma_\XX"] & \XX\mathrlap{_\bot}-\XX\ar[r,closed immersion,"{(0,\XX)}"]\ar[d] & \II\times\XX \ar[d,"\gamma_\XX"description] & \XX\ar[l,open immersion,swap,"{(1,\XX)}"]\ar[dl,sloped,swap,open immersion,"\iota_\XX"] \\+\XX\ar[r,closed immersion,"{(0,\XX)}"]\ar[d] & \II\times\XX \ar[d,"\gamma_\XX"description] & \XX\ar[l,open immersion,swap,"{(1,\XX)}"]\ar[dl,sloped,swap,open immersion,"\iota_\XX"] \\\One\ar[r,swap,closed immersion,"\bot_\XX"] & \XX\mathrlap{_\bot}\ar[ul,phantom,very near start,"\ulcorner"]-The (open) partial map classifier $\eta\colon \XX\hookrightarrow L(\XX)$ is, on the other hand, the partial product of the open embedding $\{1\}\hookrightarrow \XX$ and classifies spans+The (open) partial map classifier $\eta\colon \XX\hookrightarrow L(\XX)$ is, on the other hand, the partial product of the open embedding $\{1\}\hookrightarrow \XX$ and classifies spanswhere $U$ is an \emph{open} subspace of $\mathbb{Y}$, \emph{i.e.}\ a pullback of $\{1\}\hookrightarrow \II$ in the such that every such span arises in the context of a unique pullback square:U\ar[r]\ar[d,open immersion]\ar[dr,phantom,very near start,"\lrcorner"] & \XX\ar[d,open immersion,"\eta_\XX"]\\···
+121
refs.bib
+121
refs.bib
···+abstract = { We study the relationship between partial map classifiers, Sierpiński 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ński cone (a lax colimit) can be computed as a partial map classifier by strengthening the Segal condition. },+@inproceedings{10.1145/3373718.3394736, author = {Gratzer, Daniel and Kavvos, G. A. and Nuyts, Andreas and Birkedal, Lars}, title = {Multimodal Dependent Type Theory}, year = {2020}, isbn = {9781450371049}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, url = {https://doi.org/10.1145/3373718.3394736}, doi = {10.1145/3373718.3394736}, abstract = {We introduce MTT, a dependent type theory which supports multiple modalities. MTT is parametrized by a mode theory which specifies a collection of modes, modalities, and transformations between them. We show that different choices of mode theory allow us to use the same type theory to compute and reason in many modal situations, including guarded recursion, axiomatic cohesion, and parametric quantification. We reproduce examples from prior work in guarded recursion and axiomatic cohesion --- demonstrating that MTT constitutes a simple and usable syntax whose instantiations intuitively correspond to previous handcrafted modal type theories. In some cases, instantiating MTT to a particular situation unearths a previously unknown type theory that improves upon prior systems. Finally, we investigate the metatheory of MTT. We prove the consistency of MTT and establish canonicity through an extension of recent type-theoretic gluing techniques. These results hold irrespective of the choice of mode theory, and thus apply to a wide variety of modal situations.}, booktitle = {Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science}, pages = {492–506}, numpages = {15}, keywords = {Modal types K@dependent types, categorical semantics, gluing, guarded recursion}, location = {Saarbr\"{u}cken, Germany}, series = {LICS '20} }+@inproceedings{10.1145/3531130.3532398, author = {Gratzer, Daniel}, title = {Normalization for Multimodal Type Theory}, year = {2022}, isbn = {9781450393515}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, url = {https://doi.org/10.1145/3531130.3532398}, doi = {10.1145/3531130.3532398}, abstract = {We prove normalization for MTT, a general multimodal dependent type theory capable of expressing modal type theories for guarded recursion, internalized parametricity, and various other prototypical modal situations. We prove that deciding type checking and conversion in MTT can be reduced to deciding the equality of modalities in the underlying modal situation, immediately yielding a type checking algorithm for all instantiations of MTT in the literature. This proof follows from a generalization of synthetic Tait computability—an abstract approach to gluing proofs—to account for modalities. This extension is based on MTT itself, so that this proof also constitutes a significant case study of MTT.}, booktitle = {Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science}, articleno = {2}, numpages = {13}, keywords = {type theory, normalization, modalities, modal type theory, categorical semantics, Artin gluing}, location = {Haifa, Israel}, series = {LICS '22} }+keywords={Computer science;Complexity theory;Logic;type theory;category theory;modal dependent type theory;infinity category theory;homotopy type theory},+booktitle = {Thirteenth Annual Conference on Mathematical Foundations of Progamming Semantics, {MFPS} 1997, Carnegie Mellon University, Pittsburgh, PA, USA, March 23-26, 1997},