jonmsterling.com
+881
-59
lics.tex
+881
-59
lics.tex
······+\draw[scale=0.7, line width=0.5pt] ($(\tikzlastnode) + (.3cm,-.6cm)$) -- ++(0.3cm,0) -- ++(0,0.3cm);+\draw[scale=0.7, line width=0.5pt] ($(\tikzlastnode) + (-.3cm,-.6cm)$) -- ++(-0.3cm,0) -- ++(0,0.3cm);+\draw[scale=0.7, line width=0.5pt] ($(\tikzlastnode) + (.3cm,.6cm)$) -- ++(0.3cm,0) -- ++(0,-0.3cm);+\draw[gray, scale=0.7, line width=0.5pt] ($(\tikzlastnode) + (.3cm,.6cm)$) -- ++(0.3cm,0) -- ++(0,-0.3cm);+\draw[scale=0.7, line width=0.5pt] [densely dotted] ($(\tikzlastnode) + (.3cm,-.6cm)$) -- ++(0.3cm,0) -- ++(0,0.3cm);+\draw[gray,scale=0.7, line width=0.5pt] ($(\tikzlastnode) + (.3cm,-.6cm)$) -- ++(0.3cm,0) -- ++(0,0.3cm);+\draw[scale=0.7, line width=0.5pt] ($(\tikzlastnode) + (-.3cm,.6cm)$) -- ++(-0.3cm,0) -- ++(0,-0.3cm);+\draw[scale=0.7, line width=0.5pt] ($(\tikzlastnode) + (.3cm,.6cm)$) -- ++(0.3cm,0) -- ++(0,-0.3cm);+\draw[scale=0.7, line width=0.5pt,densely dotted] ($(\tikzlastnode) + (-.3cm,.6cm)$) -- ++(-0.3cm,0) -- ++(0,-0.3cm);·········-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.+In a 2-category of spaces, the \emph{mapping cylinder} 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.+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 cylinders 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.···\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+The (open) partial map classifier $\eta_\XX\colon \XX\hookrightarrow \Lift(\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):+Now, it so happens that we may define a universal comparison map $\sigma_\XX\colon \XX_\bot\to \Lift(\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 under reasonable assumptions 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"]+|[gray, sw muted pullback]|\varnothing \ar[u,gray,open immersion]\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"]\\+|[pullback]|\XX\ar[r,equals]\ar[d,open immersion,swap,"\iota_\XX"] & \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.}+The promised coincidence is that the induced comparison map $\XX_\bot\to \Lift(\XX)$ is invertible. This property also extends to models of higher categories such as simplicial sets: when \[ \Lift(X) \equiv \textstyle\sum_{(i:\Spx{\One})}X^{(i=1)}\] is the open partial map classifier of a simplicial set,\footnote{We mean, $\Lift(X)$ classifies partial maps whose support is classified by the open embedding $\{1\}\hookrightarrow \Spx{\One}$.} it actually happens that $\Lift(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 likebecause 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.···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}:+Although either suggestion above may be used to faithfully express the partial map classification property of global Sierpi\'nski cones, 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.+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 \Lift(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+Notwithstanding the fact that we cannot expect the comparison map $\sigma_X \colon X_\bot\to \Lift(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.+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 $\Lift(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$+Given the overwhelming size of the localising class \[ \mathcal{L}_{\mathit{Sierp}} \equiv \{\sigma_X\colon X_\bot \to \Lift(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 \Lift(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)}"]+|[pullback]|(i=1)_\bot\ar[r,hookrightarrow]\ar[d,hookrightarrow,swap,"\sigma_{(i=1)}"] & |[pullback]|\Horn \ar[d,hookrightarrow]\ar[r,"\cong"description] & \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"]+|[pullback]|\Lift(i=1)\ar[r,hookrightarrow]\ar[d] & |[pullback]|\Spx{\Two} \ar[d,"\max"description]\ar[r,"\cong"description] & \sum_{(i:\II)} \Lift(i=1)\ar[d,"\pi_1"]···-\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} referred to the types that are internally orthogonal to \[ \sigma_{(i=1)}\colon (i=1)_{\bot}\hookrightarrow \Lift(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:···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). One of our main contributions is to lift this restriction and give a full characterisation of the Sierpi\'nski complete types at all truncation levels.-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$:+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 cylinder} of a function $f\colon X\to Y$:Y\arrow[r,swap,closed immersion,"\bot_f"]\ar[ur,phantom,"{\Uparrow}\gamma_f"] & f \uparrow X-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''+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,"\sum_{(y:Y)}\iota_{\mathsf{fib}_f(y)}"]\\\sum_{(y:Y)}\mathbf{1}\arrow[r,swap,closed immersion,"\sum_{(y:Y)}\bot_{\mathsf{fib}_f(y)}"]\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} \]+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}+\One\arrow[r,swap,open immersion,"\top_X"]\ar[ur,phantom,"{\Downarrow}\Flip{\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)}\]+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} \[ \CoLift(X) :\equiv \textstyle\sum_{(i:\II)} X^{(i=0)}\]culminating in a decomposition of the generic inner horn inclusion into dual comparison maps:-(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)}"]+|[pullback]|(i=0)^\top\ar[r,hookrightarrow]\ar[d,hookrightarrow,swap,"\Flip{\sigma}_{(i=0)}"] & |[pullback]|\Horn \ar[d,hookrightarrow]\ar[r,"\cong"description]& \sum_{i:\II}(i=0)^\bot\ar[d,"\sum_{(i:\II)}\Flip{\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"]+|[pullback]|\CoLift(i=0)\ar[r,hookrightarrow]\ar[d] & |[pullback]|\Spx{\Two} \ar[d,"\min"description]\ar[r,"\cong"description] & \sum_{(i:\II)} \CoLift(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$.+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 rename ``based Segal completeness' to \emph{upper Segal completeness}, and then a corresponding notion of \emph{lower Segal completeness} that we shall compare with a corresponding \emph{inverted Sierpi\'nski completeness} condition.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{open} and \emph{closed} mapping cylinders in appropriate subcategories. This provides a particularly simple description of the Artin glueing (open mapping cylinder) 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 closed mapping cylinder 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$.+There are several different metalanguages in use for working synthetically with higher categories. For simplicity's sake, we work informally in univalent foundations~\citep{hottbook}. Rather than globally assuming an interval object satisfying various axioms, we instead state definitions and theorems parameterised in a bounded distributive lattice so that they can be instantiated at will.-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$.+In contrast to the original work of \citet{riehl-shulman:2017}, we therefore do not make use of any special types satisfying strong laws of definitional equality, such as extension types. In contrast to the work of \citet{11186122}, we do not extend Martin-L\"of type theory with any modalities, nor do we assume any simplicially-inspired axioms on the interval (\emph{e.g.}\ that it is a total order, \emph{etc.}). As a result, our work can be readily mechanised in any stock proof assistant that supports intensional type theory---and, indeed, several key results have been mechanised already.+We shall write $\BDL$ for the category of bounded distributive lattices; for a given bounded distributive lattice $\J$, we will write $\ALG{\J} :\equiv \J/\BDL$ for the category of bounded distributive lattices equipped with a homomorphism from $\J$, which we shall refer to as $\J$-algebras. Of course, we can view $\J$ itself as a generic $\J$-algebra via its identity map. We will write $\mathsf{U}\colon\BDL\to\SET$ and $\mathsf{U}_\J\colon \ALG{\J}\to\SET$ for evident forgetful functors projecting out carrier sets. We may regard any bounded distributive lattice as a partial order, taking $i\leq j$ to be either $i\land j = i$ or equivalently $i\lor j = j$.+We will write $\IsT{-},\IsF{-}\colon \mathsf{U}\J\to\Prop$ for the indicator functions of the subsets $\{1\}, \{0\}\subseteq \J$ respectively. These functions are monotone, and so extend to functors of partial orders $\J\to \Prop$; when $\J$ is \emph{local} in a sense that we shall define in \S~\ref{sec:duality} these functions shall in fact become homomorphisms of bounded distributive lattices.+A bounded distributive lattice $\J$ is called \emph{non-trivial} when $\IsT{-}\colon \J\to\Prop$ preserves the empty join $0$, and \emph{local} when $\IsT{-}\colon \J\to\Prop$ preserves all finite joins. We call $\J$ \emph{conservative} when the indicator function $\IsT{-}\colon \mathsf{U}\J\to\Prop$ is an embedding, or (equivalently) when $\IsT{-}\colon \J\to\Prop$ is an \emph{order-embedding}.+The \emph{spectrum} of an $\J$-algebra $A$ is defined to be the set of $\J$-algebra homomorphisms from $A$ to $\J$:+The \emph{observational $\J$-algebra} of a type $X$ is defined to be the following $X$-fold product of $\J$+The spectrum construction is right adjoint to the observational algebra construction for any $\J\in\BDL$:+Recent work in synthetic (topology, geometry, category theory) has emphasised various \emph{synthetic quasi-coherence} axioms that are closely related to the Kock--Lawvere axiom from synthetic differential geometry and the Phoa principle of synthetic domain theory; in each case, certain classes of algebras are asserted to lie within the fixed points of the adjunction $\Opens{\J}\dashv \Spec{\J}$. We follow \citet{sterling2025domainsclassifyingtopoi} by instead studying a general notion of quasi-coherence in terms of the adjunction above.\footnote{This is similar to the approach of \emph{abstract Stone duality}~\citep{taylor:2002}, although the adjunction that we are considering is not monadic.}+We shall refer to the fixed points of the adjunction $\Opens{\J}\dashv \Spec{\J}$ as \emph{quasi-coherent $\J$-algebras} and \emph{affine $\J$-spaces} respectively, making the following restricted adjunction an adjoint equivalence by definition:+A $\J$-algebra $A$ is called \emph{stably quasi-coherent} when the quotient $\J/(a_i=b_i)_{i\leq n}$ of $\J$ by any finite set of identifications is quasi-coherent.+Each bounded distributive lattice $\J$ generates a ``geometry'' of cubes, simplices, horns, \emph{etc.}\ that are all obtained by glueing together various $\J$-spectrums.+We will write $\II$ to denote the ``interval'', which we may define to be the underlying set of $\J$ itself. The ``observational topology'' $\Opens{\J}X \equiv \J^X$ of a space $X$ therefore has $\II^X$ as its underlying set/space. The role of the interval in representing the intrinsic topology of a given space leads to a simple description of \emph{open} and \emph{closed} subspaces.+An embedding $X\hookrightarrow Y$ is called an \emph{open immersion} when it arises as the pullback of the inclusion $\{1\}\hookrightarrow \II$, and a \emph{closed immersion} when it arises as a pullback of the inclusion $\{0\}\hookrightarrow \II$.+induce \emph{polynomial} or \emph{partial product} constructions~\citep{dyckhoff-tholen:1987, johnstone:1992, johnstone:1993}+It is instructive to view all the cubes $\II^n$ as the spaces dual to the \emph{free finitely generated} $\J$-algebras:+The simplices $\Spx{n} = \{ \alpha \colon n \to \II \mid i_1 \geq \cdots \geq i_n \}$ are the spaces dual to the \emph{finitely presented} $\J$-algebras that freely add to $\J$ a finite descending chain:+\Spx{n} = \Spec{\J} \J[\mathsf{x}_1, \ldots,\mathsf{x}_n] / \mathsf{x}_1\geq \cdots \geq \mathsf{x}_n+In type theoretic terms, we may compute the generic inner horn following \citet{riehl-shulman:2017} as the following subspace of the triangle $\Spx{\Two}$:+From a geometrical point of view, the above amounts to glueing the interval onto itself end-to-end with the images of each copy of the interval forming open and closed subspaces respectively of the horn as follows:+Let $X$ be a type. The \emph{Sierpi\'nski cone} $X_\bot$ of $X$ is computed by \citet{pugh-sterling-2025} in the style of dependent type theory to be the sum+where $P*X$ is the \emph{closed modality} associated to a proposition $P$ as explained by \citet{rijke-shulman-spitters:2020}, which is obtained as the following pushout of product projections:+Because the summing functor $\sum_{\II}\colon \mathbf{Type}/\II\to \mathbf{Type}$ preserves colimits, being a left adjoint, the following is a pushout:+Eliminating singletons, we therefore obtain the familiar categorical description of the Sierpi\'nski cone:+X\ar[r,closed immersion,"{(0,X)}"]\ar[d] & \II\times X \ar[d,"\gamma_X"description] & X\ar[l,open immersion,swap,"{(1,X)}"]\ar[dl,sloped,swap,hookrightarrow,"\iota_X"] \\+Note that unless $\J$ is consistent, the inclusion $\iota_X\colon X\hookrightarrow X_\bot$ may not be an open immersion.+Dually, we define the \emph{inverted} Sierpi\'nski cone $X^\top$ of $X$ to be the Sierpi\'nski cone in the geometric context of the distributed lattice $\J\Op$. In particular, we have+We define a new notion that is analogous to mapping cylinders, but from the point of view of dependent type theory.+Let $x:B\vdash E[x]$ be a family of types; the \emph{open fibre cylinder} of $E$ over $B$ is defined to be the sum+of all the Sierpi\'nski cones of the fibres of $E$. Dually, the \emph{closed fibre cylinder} of $E$ over $B$ is defined to be the open fibre cylinder in the dual geometric context $\J\Op$, or more explicitly,+The \emph{(open, closed) mapping cylinder} of a function $f\colon E\to B$ is defined to be (closed, open) fibre cylinder of the family $x:B\vdash \mathsf{fib}_f(x)$:+Restricting attention to the open mapping cylinder, we recall that the summing functor $\sum_B\colon\mathbf{Type}/B\to\mathbf{Type}$ preserves colimits and so the following is a pushout square:+Adjusting by the canonical equivalence $E\cong \sum_{(x:B)}\mathsf{fib}_f(x)$ and a few others, we obtain the familiar categorical description of the open and closed mapping cylinders:+From this it is clear that the open mapping cylinder $\OpenMCyl_B(f)$ is precisely the Artin glueing of $f\colon E\to B$.+Several results depend on the generic open immersion $\{1\}\hookrightarrow \II$ forming a dominance in the sense of \citet{rosolini:1986}, which is to say that $\J$ is conservative and open immersions are closed under composition.+We will say that $\J$ is \emph{dominant} when the open immersion $\{1\}\hookrightarrow\II$ forms a dominance.+As an example, the dual lattice $\J\Op$ is dominant if and only if the closed immersion $\{0\}\hookrightarrow\II$ for $\J$ forms a dominance.+If $\J$ itself is stably quasi-coherent, then both $\J$ and $\J\Op$ are conservative and dominant.+Rosolini's dominances gives rise to an evident theory of partial maps and partial map classifier. In particular, we define a $\J$-partial map from $X$ to $Y$ to be a function $Z\to Y$ defined on an open subspace $Z$ of $X$. Dually, a $\J\Op$-partial map from $X$ to $Y$ would be a function $Z\to Y$ defined on a closed subspace $Z$ of $X$. When $\J$ is conservative, the partial products $\Lift(Y)$ and $\CoLift(Y)$ classify $\J$-partial and $\J\Op$-partial maps \emph{qua} spans+When $\J$ is dominant, the $\J$-partial maps are closed under composition and thus $\Lift$ forms a monad; likewise, when $\J\Op$ is dominant, $\J\Op$-partial maps are closed under composition and so $\CoLift$ forms a monad. Returning to \citet{hyland:1991}, these are the \emph{partial} and \emph{co-partial} map classifiers respectively within the domain theoretic context of $\J$. We might refer to these more symmetrically as the \emph{open partial} and \emph{closed partial} map classifiers of $\J$.+We will generalise the operation that sends a type $X$ to its partial product with $\{0\}\hookrightarrow \II$ or $\{1\}\hookrightarrow \II$ to families of types, by analogy with the relationship between Sierpi\'nski cones and fibre cylinders. Letting $x:B\vdash E[x]$ be a family of types, we consider the following sums of partial products:+We refer to the above as the (open, closed) \emph{logical} fibre cylinders of $E$ over $B$ respectively. When $\J$ is conservative, these classify the following kinds of squares respectively:+U \ar[d, open immersion] \ar[r] & \sum_{(x:B)}E[x]\ar[d, "\pi_1"description] & K\ar[d,closed immersion]\ar[l]\\+By this token, we might refer to the actual fibre cylinder $\OpenMCyl_{(x:B)}E[x]$ as the \emph{geometrical} fibre cylinder.+For a function $f\colon E\to B$, we may likewise define \emph{logical} versions of the open and closed mapping cylinder respectively in terms of the logical fibre cylinder:+We shall refer to these as the logical open/closed mapping cylinders respectively. At times, we may refer to the ordinary mapping cylinders $\OpenMCyl_B(f),\ClosedMCyl_B(f)$ as \emph{geometrical} mapping cylinders.+We will now describe the comparison maps $\sigma_X\colon X_\bot\to \Lift(X)$ and, dually, $\Flip{\sigma}_X\colon X^\top\to\CoLift(X)$. These comparison maps always exist as soon as $\J$ is consistent, but it will actually streamline subsequent matters slightly if we relax this assumption and instead consider $X$ drawn from the reflective subuniverse of \emph{$\IsF{1}$-connected} types, specified below.+Let $P$ be a proposition. Then a type $X$ is $P$-connected if and only if either of the following equivalent conditions hold:+is cartesian, where $\pi\colon X_\bot \to \II$ is the map obtained universally from the following square:+of the Sierpi\'nski cone, the described map $\pi\colon X_\bot \to \II$ is precisely the first projection function, whose fibre over generic $i:\II$ is $\IsF{i}*X$. We are asked to check that the fibre of $\pi$ at $1:\II$ is precisely $X$, \emph{i.e.}\ that the canonical map $X \to \IsF{1}*X$ is an equivalence. But this is one of the equivalent formulations of $X$ being $\IsF{1}$-connected.+Dually, the embedding $\Flip{\iota}_X\colon X\hookrightarrow X^\top$ is a closed immersion for $\IsT{0}$-connected $X$. Furthermore, the embeddings $\iota_f\colon E\hookrightarrow \OpenMCyl_B(f)$ and $\Flip{\iota}_f\colon E\hookrightarrow \ClosedMCyl_B(f)$ are open and closed respectively when $f\colon E\to B$ is a $\IsF{1}$-connected map. Of course, $\IsT{0}\cong \IsF{1}$ so $\IsF{1}$-connectedness and $\IsT{0}$-connectedness coincide, but they are \emph{definitionally} distinct properties.+When $X$ is $\IsF{1}$-connected, we may construct the \emph{undefined} partial element $\mathsf{undef}_X : \Lift(X)$ using the universal property of the partial product $\Lift(X)$:+We can always construct the \emph{interpolation} $\mathsf{glue}_X\colon \II\times X \to \Lift(X)$ between the undefined element the fully defined element as follows:+The comparison map $\sigma_X\colon X_\bot\to\Lift(X)$ for $\IsF{1}$-connected $X$ can be equivalently constructed using either the universal property of $X_\bot$ or the universal property of $\Lift(X)$. In the former case, we consider the square below:+The Sierpi\'nski comparison maps (\S~\ref{sec:sierpinski-comparison-map}) also allow a comparison between the ``geometrical'' and ``logical'' fibre cylinders. In particular, when $x:B\vdash E[x]$ is a family of $\IsF{1}$-connected types, we have the sum of comparison maps+and, dually, when $x:B\vdash E[x]$ is a family of $\IsT{0}$-connected types, we have the sum of dual comparison maps+Therefore, when $f\colon E\to B$ is a $\IsF{1}$-connected map, the above gives rise to comparison maps from the geometrical to the logical open mapping cylinder+\OpenMCyl_B(f) \ar[r,equals] \ar[d,densely dashed] & \OpenMCyl_{(x:B)}\mathsf{fib}_f(x)\ar[d, "\sum_{(x:B)}\sigma_{E[x]}"]+and dually for $\IsT{0}$-connected $f\colon E\to B$ a dual comparison map $\ClosedMCyl_B(f)\to \CoLift_B(f)$ for the closed mapping cylinders.+From \citet{riehl-shulman:2017} we recall that a type $C$ is called \emph{Segal complete} when it is internally right orthogonal to the comparison map $\Horn\hookrightarrow\Spx{\Two}$. To be precise, this means that the restriction map+is an equivalence. The Segal complete types form an \emph{accessible} reflective subuniverse---because the localising class $\mathcal{L}_{\textit{Segal}} \equiv \{\Horn\hookrightarrow\Spx{\Two}\}$ is very small indeed.+We also have evident inclusions $\II/i \hookrightarrow \Lift\IsT{i}$ and $i/\II\hookrightarrow \CoLift\IsF{i}$ as in the following classification squares:+\IsT{i}\ar[d,open immersion, "\eta_{\IsT{i}}"'] & |[pullback,ne pullback]|\IsT{i} \ar[r]\ar[l, equals] \ar[d,open immersion]& \{1\}\ar[d,open immersion]+\Lift\IsT{i} & \ar[l,hookrightarrow,densely dashed, "\exists!"] \II/i\ar[r,hookrightarrow] & \II+\IsF{i}\ar[d,closed immersion, "\Flip{\eta}_{\IsF{i}}"'] & |[pullback,ne pullback]|\IsF{i} \ar[r]\ar[l,equals] \ar[d,closed immersion]& \{0\}\ar[d,closed immersion]+\CoLift\IsF{i} & \ar[l,hookrightarrow,densely dashed, "\exists!"] i/\II\ar[r,hookrightarrow] & \II+When $\J$ is conservative, the inclusion $\II/i\hookrightarrow \Lift\IsT{i}$ is an equivalence.+Dually when $\J\Op$ is conservative, the comparison map $i/\II\to\CoLift\IsF{i}$ is an equivalence. Hence, when $\J$ is stably quasi-coherent, both comparison maps are equivalences.+\IsT{i}_\bot \ar[r,hookrightarrow]\ar[dr,hookrightarrow,sloped,"\sigma_{\IsT{i}}"'] & \II/i\ar[d,hookrightarrow]\\+\IsF{i}^\top \ar[r,hookrightarrow]\ar[dr,hookrightarrow,sloped,"\Flip{\sigma}_{\IsF{i}}"'] & i/\II\ar[d,hookrightarrow]\\+A type $C$ is said to be \emph{upper Segal complete} when it is orthogonal to the inclusion $\IsT{i}_\bot \hookrightarrow \II/i$ for generic $i:\II$. Dually, $C$ is said to be \emph{lower Segal complete} when it is orthogonal to the inclusion+(Evidently, a type is upper Segal complete with respect to $\J$ if and only if it is lower Segal complete with respect to the dual lattice $\J\Op$.)+When $\J$ is conservative, a type $C$ is upper Segal complete if and only if it is orthogonal to the little comparison map $\sigma_{\IsT{i}}\colon \IsT{i}_\bot\hookrightarrow \Lift\IsT{i}$ for generic $i:\II$.+Dually, when $\J\Op$ is conservative, $C$ is lower Segal complete if and only if it is orthogonal to the dual comparison map $\Flip{\sigma}_{\IsF{i}}\colon \IsF{i}^\top\hookrightarrow \CoLift\IsF{i}$ for generic $i:\II$. Therefore, when $\Sigma$ is stably quasi-coherent, the upper and lower Segal conditions are precisely equivalent to being orthogonal to each $\sigma_{\IsT{i}}$ and $\Flip{\sigma}_{\IsF{i}}$ respectively.+We shall slightly adapt the definition of \emph{Sierpi\'nski completeness} from \citet{pugh-sterling-2025} to avoid relying on global assumptions.+A type $C$ is called \emph{Sierpi\'nski complete} when it is internally right orthogonal to the comparison map+for generic $\IsF{1}$-connected $X$.\footnote{Compare with \citet{pugh-sterling-2025}, who gave the definition of Sierpi\'nski completeness only under the global assumption that the $\J$ is non-trivial, so that \emph{every} $X$ is $\IsF{1}$-connected.}+Dually, we may define a type to be \emph{inverted Sierpi\'nski complete} when it is internally right orthogonal to+for generic $\IsT{0}$-connected $X$. Evidently a type is Sierpi\'nski complete with respect to $\J$ if and only if it is inverted Sierpi\'nski complete with respect to $\J\Op$.+If $\J$ is conservative, then any Sierpi\'nski complete type with respect to $\J$ is upper Segal complete.+\cref{prop:lift-as-slice} identifies the inclusion $\IsT{i}_\bot\hookrightarrow \II/i$ with the comparison map $\sigma_{\IsT{i}}\colon \IsT{i}_\bot\to \Lift\IsT{i}$.+When $\J\Op$ is conservative, dually, any inverted Sierpi\'nski complete type with respect to $\J$ is \emph{lower} Segal complete. Therefore, when $\J$ is stably quasi-coherent, Sierpi\'nski completeness (\emph{resp.}\ inverted Sierpi\'nski completeness) implies upper (\emph{resp.}\ lower) Segal completeness.+\[ \OpenMCyl_{(x:B)}E[x]\to \Lift_{(x:B)}E[x]\] from the geometrical to the logical for each family of $\IsF{1}$-connected types $x:B\vdash E[x]$.+\item The type $C$ is internally right orthogonal to the comparison map \[ \OpenMCyl_B(f)\to \Lift_B(f)\] for each $\IsF{1}$-connected function $f\colon E\to B$.+The latter two conditions are obviously equivalent. The (2) implies (1) follows by viewing a $\IsF{1}$-connected type $X$ as a family $\_:\One\vdash X$. That (1) implies (2) can be seen by consider the following (definitionally) commuting square+in which we must verify that the left-hand map is an equivalence. The upper and lower maps are the dependent currying/uncurrying equivalences, and the eastern map is the functorial action of the \emph{product} functor on the family of equivalences given by the Sierpi\'nski completeness of $C$. By the three-for-two property of equivalences, it follows that the left-hand map is an equivalence.+The thrust of \cref{thm:sierpinski-completeness-mapping-cylinders} is to say that in any subuniverse in which partial map classifiers exist and satisfy the universal property of the Sierpi\'nski cone, it \emph{also} follows that logical mapping cylinders (if they exist) must satisfy the universal property of (geometrical) mapping cylinders.
+1
-1
main.tex
+1
-1
main.tex
···-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: when $L(X)$ is the open partial map classifier of a simplicial set,\footnote{We mean, $L(X)$ classifies partial maps whose support is classified by the nerve of the open embedding $\{1\}\hookrightarrow \{0\to 1\}$.} we actually do have $L(X) \cong \Spx{\Zero}\star X \equiv X_\bot$. It is therefore reasonable to say that the correspondence between classifying partial maps and representing mapping cones is part of the core logic--geometry duality shared by (higher) category theory, domain theory, topology, \emph{etc.}+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: when $L(X)$ is the open partial map classifier of a simplicial set,\footnote{We mean, $L(X)$ classifies partial maps whose support is classified by the nerve of the open embedding $\{1\}\hookrightarrow \{0\to 1\}$.} we actually do have $L(X) \cong \Spx{\Zero}\star X \equiv X_\bot$. It is therefore reasonable to say that the correspondence between classifying partial maps and representing mapping cylinders is part of the core logic--geometry duality shared by (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.
+66
refs.bib
+66
refs.bib
···+booktitle = {Applications of Categories in Computer Science: Proceedings of the London Mathematical Society Symposium, Durham 1991},