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