this repo has no description
jonmsterling.com
1\documentclass[10pt, sigconf, nonacm]{acmart}
2% unset nonacm upon acceptance.
3
4\usepackage{mathtools}
5\usepackage{tikz-cd}
6\usepackage[capitalise]{cleveref}
7\usetikzlibrary{arrows.meta, calc}
8\settopmatter{printfolios=true}
9
10\NewDocumentCommand\OpenMCyl{}{\mathsf{M}^\circ}
11\NewDocumentCommand\ClosedMCyl{}{\mathsf{M}^\bullet}
12
13\makeatletter
14\NewDocumentCommand{\Flip}{m}{%
15 \text{\m@th\rotatebox[origin=c]{-180}{$#1$}}%
16}
17\makeatother
18
19\NewDocumentCommand\IsT{m}{[#1]}
20\NewDocumentCommand\IsF{m}{\langle #1\rangle}
21
22\NewDocumentCommand\Prop{}{\mathbf{Prop}}
23
24\tikzset{curve/.style={settings={#1},to path={(\tikztostart)
25.. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$)
26and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$)
27.. (\tikztotarget)\tikztonodes}},
28settings/.code={\tikzset{quiver/.cd,#1}
29 \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}},
30quiver/.cd,pos/.initial=0.35,height/.initial=0}
31
32\tikzset{
33pullback/.style = {
34 append after command={
35 \pgfextra{
36 \draw[scale=0.7, line width=0.5pt] ($(\tikzlastnode) + (.3cm,-.6cm)$) -- ++(0.3cm,0) -- ++(0,0.3cm);
37 }
38 }
39 },
40ne pullback/.style = {
41 append after command={
42 \pgfextra{
43 \draw[scale=0.7, line width=0.5pt] ($(\tikzlastnode) + (-.3cm,-.6cm)$) -- ++(-0.3cm,0) -- ++(0,0.3cm);
44 }
45 }
46 },
47sw pullback/.style = {
48 append after command={
49 \pgfextra{
50 \draw[scale=0.7, line width=0.5pt] ($(\tikzlastnode) + (.3cm,.6cm)$) -- ++(0.3cm,0) -- ++(0,-0.3cm);
51 }
52 }
53 },
54sw muted pullback/.style = {
55 append after command={
56 \pgfextra{
57 \draw[gray, scale=0.7, line width=0.5pt] ($(\tikzlastnode) + (.3cm,.6cm)$) -- ++(0.3cm,0) -- ++(0,-0.3cm);
58 }
59 }
60 },
61dotted pullback/.style = {
62 append after command={
63 \pgfextra{
64 \draw[scale=0.7, line width=0.5pt] [densely dotted] ($(\tikzlastnode) + (.3cm,-.6cm)$) -- ++(0.3cm,0) -- ++(0,0.3cm);
65 }
66 }
67 },
68muted pullback/.style = {
69 append after command={
70 \pgfextra{
71 \draw[gray,scale=0.7, line width=0.5pt] ($(\tikzlastnode) + (.3cm,-.6cm)$) -- ++(0.3cm,0) -- ++(0,0.3cm);
72 }
73 }
74 },
75pushout/.style = {
76 append after command={
77 \pgfextra{
78 \draw[scale=0.7, line width=0.5pt] ($(\tikzlastnode) + (-.3cm,.6cm)$) -- ++(-0.3cm,0) -- ++(0,-0.3cm);
79 }
80 }
81 },
82sw pushout/.style = {
83 append after command={
84 \pgfextra{
85 \draw[scale=0.7, line width=0.5pt] ($(\tikzlastnode) + (.3cm,.6cm)$) -- ++(0.3cm,0) -- ++(0,-0.3cm);
86 }
87 }
88 },
89dotted pushout/.style = {
90 append after command={
91 \pgfextra{
92 \draw[scale=0.7, line width=0.5pt,densely dotted] ($(\tikzlastnode) + (-.3cm,.6cm)$) -- ++(-0.3cm,0) -- ++(0,-0.3cm);
93 }
94 }
95 },
96}
97
98
99
100\NewDocumentCommand\Spx{m}{\Delta^{#1}}
101\NewDocumentCommand\Ord{m}{\mathbf{#1}}
102\NewDocumentCommand\One{}{\Ord{1}}
103\NewDocumentCommand\Two{}{\Ord{2}}
104\NewDocumentCommand\Zero{}{\Ord{0}}
105
106\NewDocumentCommand\II{}{\mathbb{I}}
107\NewDocumentCommand\XX{}{\mathbb{X}}
108\NewDocumentCommand\Horn{}{\Lambda^\Two_\One}
109
110\NewDocumentCommand\SET{}{\mathbf{Set}}
111\NewDocumentCommand\ALG{m}{#1\text{-}\mathbf{Alg}}
112\NewDocumentCommand\Spec{m}{\operatorname{Spec}_{#1}}
113\NewDocumentCommand\Opens{m}{\mathcal{O}_{#1}}
114\NewDocumentCommand\Op{}{^{\mathrm{op}}}
115\NewDocumentCommand\J{}{\Sigma}
116
117\NewDocumentCommand\Lift{}{\mathsf{L}^\circ}
118\NewDocumentCommand\CoLift{}{\mathsf{L}^\bullet}
119
120\tikzcdset{
121 open immersion/.style={
122 -{Triangle[open]}, hook
123 },
124 closed immersion/.style={
125 -{Triangle[fill=black]}, hook
126 }
127}
128
129\AtEndPreamble{%
130\theoremstyle{acmdefinition}
131\newtheorem{remark}[theorem]{Remark}}
132
133\AtEndPreamble{%
134\theoremstyle{acmdefinition}
135\newtheorem{construction}[theorem]{Construction}}
136
137\citestyle{acmauthoryear}
138
139\begin{document}
140
141\title{What do mapping cylinders classify?}
142\subtitle{An investigation of Artin glueing in synthetic higher category theory}
143
144\author{Jonathan Sterling}
145\email{js2878@cl.cam.ac.uk}
146\orcid{0000-0002-0585-5564}
147\affiliation{%
148 \department{Computer Laboratory}
149 \institution{University of Cambridge}
150 \city{Cambridge}
151 \country{United Kingdom}
152}
153
154\begin{abstract}
155 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.
156
157 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.
158%
159 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.
160\end{abstract}
161
162\keywords{Synthetic methods, higher category theory, domain theory, homotopy type theory}
163
164\maketitle
165
166\section{Introduction}
167
168\subsection{Two views on partiality}
169
170In 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$.
171
172The 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:
173\[
174 \begin{tikzcd}
175 \XX\ar[r,equals]\ar[d] & \XX \ar[d,open immersion,"\iota_\XX"]\\
176 \One\arrow[r,swap,closed immersion,"\bot_\XX"]\ar[ur,phantom,"{\Uparrow}\gamma_\XX"] & \XX\mathrlap{_\bot}
177 \end{tikzcd}
178 \qquad
179 \begin{tikzcd}
180 \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"] \\
181 \One\ar[r,swap,closed immersion,"\bot_\XX"] & |[pushout]|\XX\mathrlap{_\bot}
182 \end{tikzcd}
183\]
184
185
186The (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
187\[
188 \begin{tikzcd}
189 \XX & U\ar[l]\ar[r,open immersion]& \mathbb{Y}
190 \end{tikzcd}
191\]
192where $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:
193\[
194 \begin{tikzcd}
195 |[pullback]|U\ar[r]\ar[d,open immersion] & \XX\ar[d,open immersion,"\eta_\XX"]\\
196 \mathbb{Y}\ar[r,densely dashed,swap,"\exists!"] & \Lift(\XX)
197 \end{tikzcd}
198\]
199
200Now, 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):
201
202\[
203 \begin{tikzcd}
204 \XX\ar[r,equals]\ar[d] & \XX \ar[d,open immersion,"\eta_\XX"]\\
205 \One\arrow[r,swap,closed immersion,"\bot_\XX"]\ar[ur,phantom,"{\Uparrow}"] & \Lift(\XX)
206 \\
207 |[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"]
208 \end{tikzcd}
209 \qquad
210 \begin{tikzcd}
211 |[pullback]|\XX\ar[r,equals]\ar[d,open immersion,swap,"\iota_\XX"] & \XX\ar[d,open immersion,"\eta_\XX"]\\
212 \XX_\bot\ar[r,densely dashed,swap,"\exists!"] & \Lift(\XX)
213 \end{tikzcd}
214\]
215
216The 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.}
217
218\subsection{Subtleties in the synthetic world}
219
220Surprisingly, 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
221\begin{quote}
222 \em for any type $X$, the comparison map $X_\bot\to \Lift(X)$ is an equivalence,
223\end{quote}
224because 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
225\begin{equation}\label{bad-deduction}
226 \textstyle\prod_{(i:\mathbb{I})}
227 \mathsf{isEquiv}\bigl\lparen
228 (i=1)_\bot
229 \xrightarrow{\sigma_{(i=1)}}
230 \Lift(i=1)
231 \bigr\rparen
232 \tag{\textasteriskcentered}
233\end{equation}
234from which it follows that the boundary inclusion $\{0\}+\{1\}\hookrightarrow \mathbb{I}$ is an equivalence and hence that all synthetic spaces are codiscrete.
235
236When a dependent type theorist working internally to a category $\mathcal{S}$ says \emph{``Let $X$ be a type\ldots''}, what follows is taking place not in $\mathcal{S}$ but in the free extension $\mathcal{S}[X]$ of $\mathcal{S}$ by an object. 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.
237
238Those 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}.
239
240Although 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}:
241
242\begin{quote}
243 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.
244\end{quote}
245
246It 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.
247
248\subsection{Sierpi\'nski \& based Segal completeness}
249
250Notwithstanding 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
251\[
252 C^{\sigma_X} \colon C^{\Lift(X)} \to C^{X_\bot}
253\]
254is 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.
255
256Given 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.
257The 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$
258\[
259 \begin{tikzcd}
260 |[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)}"]
261 \\
262 |[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"]
263 \\
264 \{i\} \ar[r,hookrightarrow] & \II\ar[r,equals] & \II
265 \end{tikzcd}
266\]
267where $\max\colon \Spx{\Two}\to\II$ sends a coordinate $(i \geq j):\Spx{\Two}$ to $i:\II$.
268
269\subsubsection{Segal completeness}
270
271Types 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
272\[
273 \begin{tikzcd}
274 \Horn\ar[r,"\alpha"] \ar[d,hookrightarrow] & C
275 \\
276 \Spx{\Two} \ar[ur,sloped,swap,"\hat\alpha"]
277 \end{tikzcd}
278\]
279denotes the incidence of a pair of composable arrows
280\[
281 \begin{tikzcd}[column sep=small ]
282 &\alpha(1\geq 0)
283 \ar[dr,sloped,"\alpha(1\geq -)"]
284 \\
285 \alpha(0\geq 0)
286 \ar[ur,sloped,"\alpha(-\geq 0)"]
287 &&
288 \alpha(1\geq 1)
289 \end{tikzcd}
290\]
291within a commuting triangle in $C$:
292\[
293 \begin{tikzcd}[column sep=small ]
294 &\alpha(1\geq 0)
295 \ar[dr,sloped,"\alpha(1\geq -)"]
296 \ar[d,phantom,"{\Downarrow} \hat{\alpha}"]
297 \\
298 \alpha(0\geq 0)
299 \ar[ur,sloped,"\alpha(-\geq 0)"]
300 \ar[rr,sloped,swap,"{\hat{\alpha}(-,-)}"]
301 &{} &
302 \alpha(1\geq 1)
303 \end{tikzcd}
304\]
305
306Therefore 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.}
307
308\subsubsection{Based Segal completeness}
309
310\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.
311
312\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:
313
314\begin{quote}
315 \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}
316\end{quote}
317
318The 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.
319
320\subsection{Mapping cylinders and Artin glueing}
321
322The 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$:
323\[
324 \begin{tikzcd}
325 X\ar[r,equals]\ar[d,swap,"f"] & X \ar[d,open immersion,"\iota_f"]\\
326 Y\arrow[r,swap,closed immersion,"\bot_f"]\ar[ur,phantom,"{\Uparrow}\gamma_f"] & f \uparrow X
327 \end{tikzcd}
328\]
329
330Our 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''
331\[
332 \textstyle
333 \bigl\lparen\sum_{(y:Y)}\star\bigr\rparen
334 \colon
335 \bigl\lparen\sum_{(y:Y)}\mathsf{fib}_f(y)\bigr\rparen
336 \to
337 \sum_{(y:Y)}\mathbf{1}
338\]
339and 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$,
340\[
341 \begin{tikzcd}[column sep=huge]
342 \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)}"]\\
343 \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
344 \end{tikzcd}
345\]
346keeping in mind that the summing functor \[ \textstyle\sum_{Y}\colon \mathbf{Type}/Y\to \mathbf{Type} \]
347preserves 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.
348
349\subsection{Summary of results}
350
351Below we summarise our new contributions.
352
353\subsubsection{Upper and lower Segal completeness}
354
355The Sierpi\'nski cone of a space $X$ is contains $X$ as an \emph{open} subspace above a minimal closed point as depicted below:
356\[
357 \begin{tikzcd}
358 X\ar[r,equals]\ar[d] & X \ar[d,open immersion,"\iota_X"]\\
359 \One\arrow[r,swap,closed immersion,"\bot_X"]\ar[ur,phantom,"{\Uparrow}\gamma_X"] & X\mathrlap{_\bot}
360 \end{tikzcd}
361\]
362
363There 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}:
364\[
365 \begin{tikzcd}
366 X\ar[r,equals]\ar[d] & X \ar[d,closed immersion,"\Flip{\iota}_X"]\\
367 \One\arrow[r,swap,open immersion,"\top_X"]\ar[ur,phantom,"{\Downarrow}\Flip{\gamma}_X"] & X\mathrlap{^\top}
368 \end{tikzcd}
369\]
370
371We 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)}\]
372and obtain a corresponding system of comparison maps
373\[
374 \Flip{\sigma}_X \colon X^\top \to \CoLift(X)
375\]
376culminating in a decomposition of the generic inner horn inclusion into dual comparison maps:
377\[
378 \begin{tikzcd}
379 |[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)}"]
380 \\
381 |[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"]
382 \\
383 \{i\} \ar[r,hookrightarrow] & \II\ar[r,equals] & \II
384 \end{tikzcd}
385\]
386
387This 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.
388
389\subsubsection{Characterising the Sierpi\'nski complete spaces}
390
391Our 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.
392
393Dualising, 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.
394
395\subsubsection{Generalisation to mapping cylinders}
396
397Finally, 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$.
398
399\subsection{Foundational approach}
400There 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.
401
402In 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.
403
404\NewDocumentCommand\BDL{}{\mathbf{DL}}
405
406\section{Synthetic geometry in a lattice context}
407
408We 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$.
409
410We 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.
411
412\subsection{Duality between algebras and spaces}\label{sec:duality}
413
414We recall several definitions from \citet{sterling2025domainsclassifyingtopoi}.
415
416\begin{definition}
417 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}.
418\end{definition}
419
420\begin{definition}
421 The \emph{spectrum} of an $\J$-algebra $A$ is defined to be the set of $\J$-algebra homomorphisms from $A$ to $\J$:
422 \[
423 \Spec{\J} A :\equiv
424 \hom_{\ALG{\J}}(A,\J)
425 \]
426
427 The spectrum construction evidently gives a functor \[
428 \operatorname{Spec}_\J\colon \ALG{\J}^{\mathsf{op}}\to\SET
429 \]
430 whose restriction maps are given by precomposition.
431\end{definition}
432
433\begin{definition}
434 The \emph{observational $\J$-algebra} of a type $X$ is defined to be the following $X$-fold product of $\J$
435 \[
436 \Opens{\J}X :\equiv \textstyle\prod_{(x:X)}\J \equiv \J^X
437 \]
438 computed in $\ALG{\J}$. This construction restricts to a functor
439 \[
440 \Opens{\J}\colon \SET\to \ALG{\J}\Op
441 \text{.}
442 \]
443\end{definition}
444
445\begin{proposition}
446 The spectrum construction is right adjoint to the observational algebra construction for any $\J\in\BDL$:
447 \[
448 \begin{tikzcd}
449 \ALG{\J}\Op
450 \ar[rr, "\Spec{\J}"{name=0}, swap, curve={height=18pt}]
451 &&
452 \SET
453 \ar[ll, "\Opens{\J}"{name=1}, swap, curve={height=18pt}]
454 \arrow["\dashv"{anchor=center, rotate=-90, font=\normalsize}, draw=none, from=1, to=0]
455 \end{tikzcd}
456 \]
457
458 The unit and counit are computed as follows:
459 \begin{align*}
460 &\eta_X \colon X\to \Spec{\J}\Opens{\J}X\\
461 &\eta_X(x) :\equiv \lambda \chi:\Opens{X}\mathpunct{.}\chi(x)
462 \\[8pt]
463 &\epsilon_A \colon A\to \Opens{\J}\Spec{\J}A\\
464 &\epsilon_A(a) :\equiv \lambda p:\Spec{\J}A\mathpunct{.}p(a)
465 \end{align*}
466\end{proposition}
467
468Recent 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.}
469
470\begin{definition}
471 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:
472 \[
473 \begin{tikzcd}
474 \mathbf{QCoh}_\J\Op
475 \ar[rr, "\Spec{\J}"{name=0}, swap, curve={height=18pt}]
476 &&
477 \mathbf{Aff}_\J
478 \ar[ll, "\Opens{\J}"{name=1}, swap, curve={height=18pt}]
479 \arrow["\dashv"{anchor=center, rotate=-90, font = \normalsize}, draw=none, from=1, to=0]
480 \end{tikzcd}
481 \]
482\end{definition}
483
484\begin{definition}
485 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.
486\end{definition}
487
488\subsection{Geometrical constructions}
489
490Each bounded distributive lattice $\J$ generates a ``geometry'' of cubes, simplices, horns, \emph{etc.}\ that are all obtained by glueing together various $\J$-spectrums.
491
492\subsubsection{The interval; open and closed immersions}
493
494We 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.
495
496\begin{definition}
497 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$.
498\end{definition}
499
500The open and closed immersions
501\[
502 \begin{tikzcd}
503 \{0\}
504 \ar[r,closed immersion]
505 &
506 \II
507 &
508 \ar[l, open immersion]
509 \{1\}
510 \end{tikzcd}
511\]
512induce \emph{polynomial} or \emph{partial product} constructions~\citep{dyckhoff-tholen:1987, johnstone:1992, johnstone:1993}
513\begin{align*}
514 \Lift(Y) :\equiv \textstyle\sum_{(i:\II)}Y^{\IsT{i}}
515 \qquad
516 \CoLift(Y) :\equiv \textstyle\sum_{(i:\II)}Y^{\IsF{i}}
517\end{align*}
518which classify diagrams of the form
519\[
520 \begin{tikzcd}[row sep=small]
521 Y
522 &
523 |[pullback]|U
524 \ar[l]
525 \ar[d, open immersion]
526 \ar[r]
527 &
528 \{1\}
529 \ar[d, open immersion]
530 \\
531 &
532 X
533 \ar[r]
534 &
535 \II\text{,}
536 \end{tikzcd}
537 \qquad
538 \begin{tikzcd}[row sep=small]
539 Y
540 &
541 |[pullback]|K
542 \ar[l]
543 \ar[d, closed immersion]
544 \ar[r]
545 &
546 \{0\}
547 \ar[d, closed immersion]
548 \\
549 &
550 X
551 \ar[r]
552 &
553 \II
554 \end{tikzcd}
555\]
556respectively.
557
558\subsubsection{The cubes}
559
560It is instructive to view all the cubes $\II^n$ as the spaces dual to the \emph{free finitely generated} $\J$-algebras:
561\[
562 \II^n = \Spec{\J} \J[\mathsf{x}_1,\ldots,\mathsf{x}_n]
563\]
564
565\subsubsection{The simplices}
566
567The 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:
568\[
569 \Spx{n} = \Spec{\J} \J[\mathsf{x}_1, \ldots,\mathsf{x}_n] / \mathsf{x}_1\geq \cdots \geq \mathsf{x}_n
570\]
571
572\subsubsection{The generic inner horn}
573
574In type theoretic terms, we may compute the generic inner horn following \citet{riehl-shulman:2017} as the following subspace of the triangle $\Spx{\Two}$:
575\[
576 \Horn :\equiv \{ (i \geq j) : \Spx{\Two} \mid \IsT{i} \lor \IsF{j}\}
577\]
578
579From 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:
580\[
581 \begin{tikzcd}
582 |[pullback]|\mathbf{1}
583 \ar[r,closed immersion, "0"]
584 \ar[d,open immersion, "1"']
585 &
586 \II
587 \ar[d,open immersion, "(-\geq 0)"]
588 \\
589 \II
590 \ar[r,closed immersion, "(1\geq -)"']
591 &
592 |[pushout]|\Horn
593 \end{tikzcd}
594\]
595
596\subsubsection{The Sierpi\'nski cone of a type}
597Let $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
598\[
599 X_\bot :\equiv
600 \textstyle\sum_{(i:\II)}
601 \IsF{i}*X
602\]
603where $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:
604\[
605 \begin{tikzcd}
606 P\times X
607 \ar[r,hookrightarrow,"\pi_2"]
608 \ar[d,"\pi_1"']
609 &
610 X\ar[d]
611 \\
612 P\ar[r,hookrightarrow]
613 &
614 |[pushout]|P*X
615 \end{tikzcd}
616\]
617
618Because the summing functor $\sum_{\II}\colon \mathbf{Type}/\II\to \mathbf{Type}$ preserves colimits, being a left adjoint, the following is a pushout:
619\[
620 \begin{tikzcd}[column sep=large]
621 \sum_{(i:\II)}
622 \IsF{i}\times X
623 \ar[r,hookrightarrow,"\sum_{(i:\II)}\pi_2"]
624 \ar[d,"\sum_{(i :\II)}\pi_1"']
625 &
626 \sum_{(i:\II)}X\ar[d]
627 \\
628 \sum_{(i:\II)}\IsF{i}\ar[r,hookrightarrow]
629 &
630 |[pushout]| \sum_{(i:\II)} \IsF{i}*X
631 \end{tikzcd}
632\]
633
634Eliminating singletons, we therefore obtain the familiar categorical description of the Sierpi\'nski cone:
635\[
636 \begin{tikzcd}
637 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"] \\
638 \One\ar[r,swap,closed immersion,"\bot_X"] & |[pushout]|X\mathrlap{_\bot}
639 \end{tikzcd}
640\]
641
642\begin{remark}
643 Note that unless $\J$ is consistent, the inclusion $\iota_X\colon X\hookrightarrow X_\bot$ may not be an open immersion.
644\end{remark}
645
646Dually, 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
647\[
648 X^\top \equiv \textstyle\sum_{i:\II} \IsT{i}*X
649\]
650
651\subsubsection{The fibre cylinder of a family of types}
652
653We define a new notion that is analogous to mapping cylinders, but from the point of view of dependent type theory.
654%
655Let $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
656\[
657 \OpenMCyl_{(x:B)}E[x]
658 :\equiv
659 \textstyle\sum_{(x:B)}
660 E[x]_\bot
661\]
662of 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,
663\[
664 \ClosedMCyl_{(x:B)}E[x]:\equiv
665 \textstyle\sum_{(x:B)}
666 E[x]^\top\text{.}
667\]
668
669\subsubsection{The mapping cylinder of a function}
670The \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)$:
671\begin{align*}
672 \OpenMCyl_B(f) &:\equiv \OpenMCyl_{(x:B)}\mathsf{fib}_f(x)\\
673 \ClosedMCyl_B(f) &:\equiv \ClosedMCyl_{(x:B)}\mathsf{fib}_f(x)
674\end{align*}
675
676Restricting 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:
677\[
678 \begin{tikzcd}[column sep=huge]
679 \sum_{(x:B)}\mathsf{fib}_f(x)
680 \ar[r, closed immersion, "{\sum_{(x:B)}(0, \mathsf{fib}_f(x))}"]
681 \ar[d, "{\sum_{(x:B)}\star}"']
682 &
683 \sum_{(x:B)}\II\times \mathsf{fib}_f(x)
684 \ar[d, "{\sum_{(x:B)}\gamma_{\mathsf{fib}_f(x)}}"]
685 \\
686 \sum_{(x:B)}\mathbf{1}
687 \ar[r, closed immersion, "{\sum_{(x:B)}\bot_{\mathsf{fib}_f(x)}}"']
688 &
689 |[pushout]|\sum_{(x:B)} \mathsf{fib}_f(x)_\bot
690 \end{tikzcd}
691\]
692
693Adjusting 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:
694\[
695 \begin{tikzcd}
696 E
697 \ar[r,open immersion, "{(1,E)}"]
698 \ar[dr,hookrightarrow,sloped,"\iota_f"']
699 &
700 \II\times E
701 \ar[d, "\gamma_f"description]
702 &
703 E
704 \ar[r, open immersion, "{(1, E)}"]
705 \ar[l, closed immersion, "{(0, E)}"']
706 \ar[d, "f"description]
707 &
708 \II\times E
709 \ar[d, "\Flip{\gamma}_f"description]
710 &
711 E
712 \ar[l, closed immersion, "{(0,E)}"']
713 \ar[dl, hookrightarrow, sloped, "\Flip{\iota}_f"']
714 \\
715 &
716 |[sw pushout]|\OpenMCyl_B(f)
717 &
718 B
719 \ar[r, open immersion, "\top_f"']
720 \ar[l, closed immersion, "\bot_f"]
721 &
722 |[pushout]|\ClosedMCyl_B(f)
723 \end{tikzcd}
724\]
725
726From this it is clear that the open mapping cylinder $\OpenMCyl_B(f)$ is precisely the Artin glueing of $f\colon E\to B$.
727
728
729\subsection{Dominance and partial map classifiers}
730
731\subsubsection{The dominance property}
732
733Several 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.
734
735\begin{definition}
736 We will say that $\J$ is \emph{dominant} when the open immersion $\{1\}\hookrightarrow\II$ forms a dominance.
737\end{definition}
738
739\begin{example}
740 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.
741\end{example}
742
743\begin{proposition}[{\citet{sterling2025domainsclassifyingtopoi}}]
744 If $\J$ itself is stably quasi-coherent, then both $\J$ and $\J\Op$ are conservative and dominant.
745\end{proposition}
746
747\subsubsection{Partial map classifiers}
748Rosolini'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
749\[
750 \begin{tikzcd}[row sep=tiny]
751 Y& \ar[l] U\ar[r,open immersion] & X,
752 \end{tikzcd}
753 \qquad
754 \begin{tikzcd}[row sep=tiny]
755 Y& \ar[l] K\ar[r,closed immersion] & X\text{.}
756 \end{tikzcd}
757\]
758
759When $\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$.
760
761\subsubsection{The logical fibre cylinder}
762
763We 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:
764\begin{align*}
765 \Lift_{(x:B)}E[x] &:\equiv \textstyle\sum_{(x:B)}\Lift (E[x])\\
766 \CoLift_{(x:B)}E[x] &:\equiv \textstyle\sum_{(x:B)}\CoLift (E[x])
767\end{align*}
768
769We 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:
770\[
771 \begin{tikzcd}
772 U \ar[d, open immersion] \ar[r] & \sum_{(x:B)}E[x]\ar[d, "\pi_1"description] & K\ar[d,closed immersion]\ar[l]\\
773 X \ar[r] & B & \ar[l] X
774 \end{tikzcd}
775\]
776
777By this token, we might refer to the actual fibre cylinder $\OpenMCyl_{(x:B)}E[x]$ as the \emph{geometrical} fibre cylinder.
778
779\subsubsection{The logical mapping cylinder}
780
781For 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:
782\[
783 \Lift_B(f) :\equiv \Lift_{(x:B)}\mathsf{fib}_f(x)
784 \qquad
785 \CoLift_B(f) :\equiv \CoLift_{(x:B)}\mathsf{fib}_f(x)
786\]
787
788We 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.
789
790\subsection{The Sierpi\'nski comparison map}\label{sec:sierpinski-comparison-map}
791
792We 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.
793
794\begin{definition}[{\citet{rijke-shulman-spitters:2020}}]
795 Let $P$ be a proposition. Then a type $X$ is $P$-connected if and only if either of the following equivalent conditions hold:
796 \begin{enumerate}
797 \item The function space $X^P$ is contractible.
798 \item The canonical inclusion $X\to P*X$ is an equivalence.
799 \end{enumerate}
800\end{definition}
801
802
803\begin{remark}
804 Evidently, $\IsT{i}$ is $\IsF{1}$ connected for any $i:\II$.
805\end{remark}
806
807\begin{lemma}\label{lem:X-01-connected-incl-open}
808 When $X$ is $\IsF{1}$-connected, the square
809 \[
810 \begin{tikzcd}
811 % |[dotted pullback]|
812 X
813 \ar[r]
814 \ar[d, hookrightarrow, "\iota_X"']
815 &
816 \{1\}
817 \ar[d,open immersion]
818 \\
819 X_\bot
820 \ar[r,"\pi"']
821 &
822 \II
823 \end{tikzcd}
824 \]
825 is cartesian, where $\pi\colon X_\bot \to \II$ is the map obtained universally from the following square:
826 \[
827 \begin{tikzcd}
828 X\ar[r,closed immersion,"{(0,X)}"]\ar[d] & \II\times X\ar[d,"\pi_1"]
829 \\
830 \mathbf{1}\ar[r,closed immersion,"0"'] & \II
831 \end{tikzcd}
832 \]
833 Therefore, $\iota_X\colon X\hookrightarrow X_\bot$ is open for $\IsF{1}$-connected $X$.
834\end{lemma}
835
836\begin{proof}
837 Recalling the type theoretic description
838 \[
839 X_\bot \equiv \textstyle\sum_{(i:\II)}\IsF{i}*X
840 \]
841 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.
842\end{proof}
843
844Dually, 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.
845
846\begin{construction}
847 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)$:
848 \[
849 \begin{tikzcd}[column sep=large]
850 X
851 \ar[d,open immersion, "\eta_X"']
852 &
853 |[pullback, ne pullback]|\IsF{1}
854 \ar[l,"!"']
855 \ar[r, closed immersion]
856 \ar[d,open immersion]
857 &
858 \{1\}
859 \ar[d,open immersion]
860 \\
861 \Lift(X)
862 &
863 \One
864 \ar[l, densely dashed, "\mathsf{undef}_X"]
865 \ar[r,closed immersion, "0"']
866 &
867 \II
868 \end{tikzcd}
869 \]
870\end{construction}
871
872\begin{construction}
873 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:
874 \[
875 \begin{tikzcd}[column sep=large]
876 X
877 \ar[d,open immersion, "\eta_X"']
878 &
879 |[pullback, ne pullback]|X
880 \ar[l,equals]
881 \ar[r]
882 \ar[d,open immersion,"{(1,X)}"description]
883 &
884 \{1\}
885 \ar[d,open immersion]
886 \\
887 \Lift(X)
888 &
889 \II\times X
890 \ar[l, densely dashed, "\mathsf{glue}_X"]
891 \ar[r, "\pi_1"']
892 &
893 \II
894 \end{tikzcd}
895 \]
896\end{construction}
897
898
899\begin{construction}
900 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:
901 \[
902 \begin{tikzcd}[column sep=large]
903 X \ar[r, "{(0,X)}"]\ar[d]
904 & \II\times X
905 \ar[d, "\mathsf{glue}_X"]
906 \\
907 \mathbf{1}
908 \ar[r, "\mathsf{undef}_X"']
909 & \Lift(X)
910 \end{tikzcd}
911 \]
912
913 In the latter, we classify the diagram below
914 \[
915 \begin{tikzcd}[column sep=large]
916 X
917 \ar[d,open immersion, "\eta_X"']
918 &
919 |[pullback, ne pullback]|X
920 \ar[l,equals]
921 \ar[r]
922 \ar[d,open immersion,"\iota_X"description]
923 &
924 \{1\}
925 \ar[d,open immersion]
926 \\
927 \Lift(X)
928 &
929 X_\bot
930 \ar[l, densely dashed, "\sigma_X"]
931 \ar[r, "\pi"']
932 &
933 \II
934 \end{tikzcd}
935 \]
936 recalling \cref{lem:X-01-connected-incl-open}
937\end{construction}
938
939\subsection{For fibre and mapping cylinders}
940
941The 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
942\[
943 \textstyle\sum_{(x:B)}
944 \sigma_{E[x]}
945 \colon
946 \OpenMCyl_{(x:B)}E[x]
947 \to \Lift_{(x:B)}E[x]\text{,}
948\]
949and, dually, when $x:B\vdash E[x]$ is a family of $\IsT{0}$-connected types, we have the sum of dual comparison maps
950\[
951 \textstyle\sum_{(x:B)}
952 \Flip{\sigma}_{E[x]}
953 \colon
954 \ClosedMCyl_{(x:B)}E[x]
955 \to \CoLift_{(x:B)}E[x]
956 \text{.}
957\]
958
959Therefore, 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
960\[
961 \begin{tikzcd}
962 \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]}"]
963 \\
964 \Lift_B(f) \ar[r,equals] & \Lift_{(x:B)}\mathsf{fib}_f(x)\text{,}
965 \end{tikzcd}
966\]
967and 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.
968
969\section{Local subuniverses of spaces}
970
971\subsection{Preliminary definitions}
972
973\subsubsection{Segal completeness}
974
975From \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
976\[
977 (\Spx{\Two}\to C) \to (\Horn\to C)
978\]
979is 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.
980
981
982\subsubsection{Upper and lower Segal completeness}
983
984% \subsubsection{Slices and co-slices of the interval}
985
986For $i:\II$, may consider the following finitely presented $\J$-algebras:
987\begin{align*}
988 \J[\mathsf{x}\leq i] &:\equiv
989 \J[\mathsf{x}]/ (\mathsf{x}\land i =\mathsf{x})
990 \\
991 \J[\mathsf{x}\geq i] &:\equiv
992 \J[\mathsf{x}]/ (\mathsf{x}\land i = i)
993\end{align*}
994
995Applying the \emph{spectrum} functor we obtain corresponding subspaces of the interval:
996\begin{align*}
997 \II/i &:\equiv \{ j:\II\mid j \leq i \}
998 \cong \Spec{\J} \J[\mathsf{x}\leq i]
999 \\
1000 i/\II &:\equiv \{ j : \II\mid j \geq i \}
1001 \cong \Spec{\J}\J[\mathsf{x}\geq i]
1002\end{align*}
1003
1004We also have evident inclusions $\II/i \hookrightarrow \Lift\IsT{i}$ and $i/\II\hookrightarrow \CoLift\IsF{i}$ as in the following classification squares:
1005\[
1006 \begin{tikzcd}[column sep=small,cramped]
1007 \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]
1008 \\
1009 \Lift\IsT{i} & \ar[l,hookrightarrow,densely dashed, "\exists!"] \II/i\ar[r,hookrightarrow] & \II
1010 \end{tikzcd}
1011 \quad
1012 \begin{tikzcd}[column sep=small,cramped]
1013 \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]
1014 \\
1015 \CoLift\IsF{i} & \ar[l,hookrightarrow,densely dashed, "\exists!"] i/\II\ar[r,hookrightarrow] & \II
1016\end{tikzcd}
1017\]
1018
1019\begin{proposition}[{\citet{pugh-sterling-2025}}]\label{prop:lift-as-slice}
1020 When $\J$ is conservative, the inclusion $\II/i\hookrightarrow \Lift\IsT{i}$ is an equivalence.
1021\end{proposition}
1022
1023\begin{corollary}\label{cor:colift-as-coslice}
1024 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.
1025\end{corollary}
1026
1027
1028% \subsubsection{Little comparison maps}
1029
1030Recalling the definitions of the little Sierpi\'nski cones in either orientation, we have:
1031%
1032\begin{align*}
1033 \IsT{i}_\bot &\equiv \{ j : \II \mid \IsF{j}\lor \IsT{i}\}
1034 \\
1035 \IsF{i}^\top &\equiv \{ j : \II\mid \IsT{j}\lor \IsF{i} \}
1036\end{align*}
1037
1038We have evident inclusions
1039\[
1040 \IsT{i}_\bot \subseteq \II/i\subseteq \II\qquad
1041 \IsF{i}^\top \subseteq i/\II\subseteq \II
1042\]
1043
1044
1045\begin{remark}
1046 Note that the following triangles of subspaces of $\II$ commute:
1047 \[
1048 \begin{tikzcd}
1049 \IsT{i}_\bot \ar[r,hookrightarrow]\ar[dr,hookrightarrow,sloped,"\sigma_{\IsT{i}}"'] & \II/i\ar[d,hookrightarrow]\\
1050 & \Lift\IsT{i}
1051 \end{tikzcd}
1052 \qquad
1053 \begin{tikzcd}
1054 \IsF{i}^\top \ar[r,hookrightarrow]\ar[dr,hookrightarrow,sloped,"\Flip{\sigma}_{\IsF{i}}"'] & i/\II\ar[d,hookrightarrow]\\
1055 & \CoLift\IsF{i}
1056 \end{tikzcd}
1057 \]
1058\end{remark}
1059
1060\begin{definition}
1061 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
1062 $
1063 \IsF{i}^\top\hookrightarrow i/\II
1064 $ for generic $i:\II$.
1065\end{definition}
1066
1067(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$.)
1068
1069\subsubsection{Sierpi\'nski completeness}
1070
1071We shall slightly adapt the definition of \emph{Sierpi\'nski completeness} from \citet{pugh-sterling-2025} to avoid relying on global assumptions.
1072
1073\begin{definition}
1074 A type $C$ is called \emph{Sierpi\'nski complete} when it is internally right orthogonal to the comparison map
1075 \[ \sigma_X\colon X_\bot \to \Lift(X) \]
1076 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.}
1077\end{definition}
1078
1079Dually, we may define a type to be \emph{inverted Sierpi\'nski complete} when it is internally right orthogonal to
1080$
1081 \Flip{\sigma}_X\colon X^\top \to \CoLift(X)
1082$
1083for 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$.
1084
1085
1086\subsection{Comparing orthogonality laws}
1087
1088\begin{proposition}[{\citet{pugh-sterling-2025}}]
1089 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$.
1090\end{proposition}
1091
1092\begin{corollary}
1093 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.
1094\end{corollary}
1095
1096
1097\begin{proposition}[{\citet{pugh-sterling-2025}}]
1098 If $\J$ is conservative, then any Sierpi\'nski complete type with respect to $\J$ is upper Segal complete.
1099\end{proposition}
1100
1101\begin{proof}
1102 \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}$.
1103\end{proof}
1104
1105\begin{corollary}
1106 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.
1107\end{corollary}
1108
1109
1110\begin{theorem}\label{thm:sierpinski-completeness-mapping-cylinders}
1111 The following are equivalent for a type $C$:
1112 \begin{enumerate}
1113 \item The type $C$ is Sierpi\'nski complete.
1114 \item The type $C$ is internally right orthogonal to the comparison map
1115 \[ \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]$.
1116 \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$.
1117 \end{enumerate}
1118\end{theorem}
1119
1120\begin{proof}
1121 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
1122 \[
1123 \begin{tikzcd}
1124 {\bigl[\Lift_{(x:B)}E[x], C\bigr]}
1125 \ar[d]
1126 \ar[r,"\cong"]
1127 &
1128 {\prod_{(x:B)}\bigl[\Lift(E[x]), C\bigr]}
1129 \ar[d, "\cong"]
1130 \\
1131 {\bigl[\OpenMCyl_{(x:B)}E[x], C\bigr]}
1132 \ar[r,"\cong"']
1133 &
1134 {\prod_{(x:B)}\bigl[E[x]_\bot, C\bigr]}\text{,}
1135 \end{tikzcd}
1136 \]
1137 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.
1138\end{proof}
1139
1140The 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.
1141
1142\subsubsection{From upper Segal to Sierpi\'nski completeness}
1143
1144We now complete the analysis of Sierpi\'nski completeness initiated by \citet{pugh-sterling-2025}.
1145
1146\begin{theorem}
1147 Any upper Segal complete type is Sierpi\'nski complete.
1148\end{theorem}
1149\textcolor{red}{TODO}
1150
1151\section{Closure of local subuniverses under logical mapping cylinders}
1152
1153
1154\clearpage
1155
1156\bibliographystyle{ACM-Reference-Format}
1157\bibliography{refs}
1158
1159\end{document}