jonmsterling.com
+351
-134
lics.tex
+351
-134
lics.tex
·········The two-handedness of $\II$ extends to an identification between the \emph{Sierpi\'nski cone} and the \emph{partial map classifier} of any space $\XX$, which we illuminate below. The Sierpi\'nski cone $\XX_\bot$ of a space $\XX$ is the following co-comma square, which we may compute by means of a pushout:-\One\arrow[r,swap,closed immersion,"\bot_\XX"]\ar[ur,phantom,"{\Uparrow}\gamma_\XX"] & \XX\mathrlap{_\bot}+\One\arrow[r,swap,closed embedding,"\bot_\XX"]\ar[ur,phantom,"{\Uparrow}\gamma_\XX"] & \XX\mathrlap{_\bot}-\XX\ar[r,closed immersion,"{(0,\XX)}"]\ar[d] & \II\times\XX \ar[d,"\gamma_\XX"description] & \XX\ar[l,open immersion,swap,"{(1,\XX)}"]\ar[dl,sloped,swap,open immersion,"\iota_\XX"] \\+\XX\ar[r,closed 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"] \\···The (open) partial map classifier $\eta_\XX\colon \XX\hookrightarrow \Lift(\XX)$ is, on the other hand, the partial product of $\XX$ with the open embedding $\{1\}\hookrightarrow \II$ and classifies spanswhere $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:···-|[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"]+|[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"]-|[pullback]|\XX\ar[r,equals]\ar[d,open immersion,swap,"\iota_\XX"] & \XX\ar[d,open immersion,"\eta_\XX"]\\+|[pullback]|\XX\ar[r,equals]\ar[d,open embedding,swap,"\iota_\XX"] & \XX\ar[d,open embedding,"\eta_\XX"]\\···because statements in type theory are automatically invariant under change-of-context.\footnote{Indeed, context invariance is in some sense the entire reason for dependent type theory to exist at all.} Indeed, \citet{pugh-sterling-2025} noted that under this assumption, we could deduce···The Sierpi\'nski cone is a special case of a more general co-comma construction that yields the \emph{Artin glueing} or \emph{closed mapping cylinder} of a function $f\colon X\to Y$:···and under this identification, the Artin glueing of $f$ becomes the sum of all the Sierpi\'nski cones of the fibres of $f\colon X\to Y$,-\sum_{(y:Y)}\mathsf{fib}_f(y)\ar[r,equals]\ar[d,swap,"\sum_{(y:Y)}\star"] & \sum_{(y:Y)}\mathsf{fib}_f(y) \ar[d,open immersion,"\sum_{(y:Y)}\iota_{\mathsf{fib}_f(y)}"]\\-\sum_{(y:Y)}\mathbf{1}\arrow[r,swap,closed immersion,"\sum_{(y:Y)}\bot_{\mathsf{fib}_f(y)}"]\ar[ur,phantom,"{\Uparrow}\sum_{(y:Y)}\gamma_{\mathsf{fib}_f(y)}"] & \sum_{(y:Y)} (\mathsf{fib}_f(y))_\bot+\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)}"]\\+\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))_\botkeeping in mind that the summing functor \[ \textstyle\sum_{Y}\colon \mathbf{Type}/Y\to \mathbf{Type} \]···The Sierpi\'nski cone of a space $X$ is contains $X$ as an \emph{open} subspace above a minimal closed point as depicted below:-\One\arrow[r,swap,closed immersion,"\bot_X"]\ar[ur,phantom,"{\Uparrow}\gamma_X"] & X\mathrlap{_\bot}+\One\arrow[r,swap,closed embedding,"\bot_X"]\ar[ur,phantom,"{\Uparrow}\gamma_X"] & X\mathrlap{_\bot}There is a dual construction $X^\top$ in which we change the orientation of the cylinder so as to obtain $X$ as a \emph{closed} subspace under a maximal open point, \citet{taylor:2000} refers to as \emph{inverted Sierpi\'nski cone}:-\One\arrow[r,swap,open immersion,"\top_X"]\ar[ur,phantom,"{\Downarrow}\Flip{\gamma}_X"] & X\mathrlap{^\top}+\One\arrow[r,swap,open embedding,"\top_X"]\ar[ur,phantom,"{\Downarrow}\Flip{\gamma}_X"] & X\mathrlap{^\top}···Each bounded distributive lattice $\J$ generates a ``geometry'' of cubes, simplices, horns, \emph{etc.}\ that are all obtained by glueing together various $\J$-spectrums.We will write $\II$ to denote the ``interval'', which we may define to be the underlying set of $\J$ itself. The ``observational topology'' $\Opens{\J}X \equiv \J^X$ of a space $X$ therefore has $\II^X$ as its underlying set/space. The role of the interval in representing the intrinsic topology of a given space leads to a simple description of \emph{open} and \emph{closed} subspaces.-An embedding $X\hookrightarrow Y$ is called an \emph{open immersion} when it arises as the pullback of the inclusion $\{1\}\hookrightarrow \II$, and a \emph{closed immersion} when it arises as a pullback of the inclusion $\{0\}\hookrightarrow \II$.+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$.·········In type theoretic terms, we may compute the generic inner horn following \citet{riehl-shulman:2017} as the following subspace of the triangle $\Spx{\Two}$:From a geometrical point of view, the above amounts to glueing the interval onto itself end-to-end with the images of each copy of the interval forming open and closed subspaces respectively of the horn as follows:···Eliminating singletons, we therefore obtain the familiar categorical description of the Sierpi\'nski cone:-X\ar[r,closed immersion,"{(0,X)}"]\ar[d] & \II\times X \ar[d,"\gamma_X"description] & X\ar[l,open immersion,swap,"{(1,X)}"]\ar[dl,sloped,swap,hookrightarrow,"\iota_X"] \\+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"] \\-Note that unless $\J$ is consistent, the inclusion $\iota_X\colon X\hookrightarrow X_\bot$ may not be an open immersion.+Note that unless $\J$ is consistent, the inclusion $\iota_X\colon X\hookrightarrow X_\bot$ may not be an open embedding.Dually, we define the \emph{inverted} Sierpi\'nski cone $X^\top$ of $X$ to be the Sierpi\'nski cone in the geometric context of the distributed lattice $\J\Op$. In particular, we have···The \emph{(open, closed) mapping cylinder} of a function $f\colon E\to B$ is defined to be (closed, open) fibre cylinder of the family $x:B\vdash \mathsf{fib}_f(x)$:Restricting attention to the open mapping cylinder, we recall that the summing functor $\sum_B\colon\mathbf{Type}/B\to\mathbf{Type}$ preserves colimits and so the following is a pushout square:······-Several results depend on the generic open immersion $\{1\}\hookrightarrow \II$ forming a dominance in the sense of \citet{rosolini:1986}, which is to say that $\J$ is conservative and open immersions are closed under composition.+Several 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.-We will say that $\J$ is \emph{dominant} when the open immersion $\{1\}\hookrightarrow\II$ forms a dominance.+We will say that $\J$ is \emph{dominant} when the open embedding $\{1\}\hookrightarrow\II$ forms a dominance.-As an example, the dual lattice $\J\Op$ is dominant if and only if the closed immersion $\{0\}\hookrightarrow\II$ for $\J$ forms a dominance.+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.···Rosolini's dominances gives rise to an evident theory of partial maps and partial map classifier. In particular, we define a $\J$-partial map from $X$ to $Y$ to be a function $Z\to Y$ defined on an open subspace $Z$ of $X$. Dually, a $\J\Op$-partial map from $X$ to $Y$ would be a function $Z\to Y$ defined on a closed subspace $Z$ of $X$. When $\J$ is conservative, the partial products $\Lift(Y)$ and $\CoLift(Y)$ classify $\J$-partial and $\J\Op$-partial maps \emph{qua} spans···We refer to the above as the (open, closed) \emph{logical} fibre cylinders of $E$ over $B$ respectively. When $\J$ is conservative, these classify the following kinds of squares respectively:-U \ar[d, open immersion] \ar[r] & \sum_{(x:B)}E[x]\ar[d, "\pi_1"description] & K\ar[d,closed immersion]\ar[l]\\+U \ar[d, open embedding] \ar[r] & \sum_{(x:B)}E[x]\ar[d, "\pi_1"description] & K\ar[d,closed embedding]\ar[l]\\···We shall refer to these as the logical open/closed mapping cylinders respectively. At times, we may refer to the ordinary mapping cylinders $\OpenMCyl_B(f),\ClosedMCyl_B(f)$ as \emph{geometrical} mapping cylinders.-We will now describe the comparison maps $\sigma_X\colon X_\bot\to \Lift(X)$ and, dually, $\Flip{\sigma}_X\colon X^\top\to\CoLift(X)$. These comparison maps always exist as soon as $\J$ is consistent, but it will actually streamline subsequent matters slightly if we relax this assumption and instead consider $X$ drawn from the reflective subuniverse of \emph{$\IsF{1}$-connected} types, specified below.+We 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.Let $P$ be a proposition. Then a type $X$ is $P$-connected if and only if either of the following equivalent conditions hold:···+Of 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.······is cartesian, where $\pi\colon X_\bot \to \II$ is the map obtained universally from the following square:···of the Sierpi\'nski cone, the described map $\pi\colon X_\bot \to \II$ is precisely the first projection function, whose fibre over generic $i:\II$ is $\IsF{i}*X$. We are asked to check that the fibre of $\pi$ at $1:\II$ is precisely $X$, \emph{i.e.}\ that the canonical map $X \to \IsF{1}*X$ is an equivalence. But this is one of the equivalent formulations of $X$ being $\IsF{1}$-connected.-Dually, the embedding $\Flip{\iota}_X\colon X\hookrightarrow X^\top$ is a closed immersion for $\IsT{0}$-connected $X$. Furthermore, the embeddings $\iota_f\colon E\hookrightarrow \OpenMCyl_B(f)$ and $\Flip{\iota}_f\colon E\hookrightarrow \ClosedMCyl_B(f)$ are open and closed respectively when $f\colon E\to B$ is a $\IsF{1}$-connected map. Of course, $\IsT{0}\cong \IsF{1}$ so $\IsF{1}$-connectedness and $\IsT{0}$-connectedness coincide, but they are \emph{definitionally} distinct properties.+Dually, 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.-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)$:+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)$:···-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:+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:···-The comparison map $\sigma_X\colon X_\bot\to\Lift(X)$ for $\IsF{1}$-connected $X$ can be equivalently constructed using either the universal property of $X_\bot$ or the universal property of $\Lift(X)$. In the former case, we consider the square below:+The 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:······-The Sierpi\'nski comparison maps (\S~\ref{sec:sierpinski-comparison-map}) also allow a comparison between the ``geometrical'' and ``logical'' fibre cylinders. In particular, when $x:B\vdash E[x]$ is a family of $\IsF{1}$-connected types, we have the sum of comparison maps+The Sierpi\'nski comparison maps (\S~\ref{sec:sierpinski-comparison-map}) also allow a comparison between the ``geometrical'' and ``logical'' fibre cylinders. In particular, when $x:B\vdash E[x]$ is a family of $\IsT{0}$-connected types, we have the sum of comparison maps···-and, dually, when $x:B\vdash E[x]$ is a family of $\IsT{0}$-connected types, we have the sum of dual comparison maps+and, dually, when $x:B\vdash E[x]$ is a family of $\IsF{1}$-connected types, we have the sum of dual comparison maps···-Therefore, when $f\colon E\to B$ is a $\IsF{1}$-connected map, the above gives rise to comparison maps from the geometrical to the logical open mapping cylinder+Therefore, 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\OpenMCyl_B(f) \ar[r,equals] \ar[d,densely dashed] & \OpenMCyl_{(x:B)}\mathsf{fib}_f(x)\ar[d, "\sum_{(x:B)}\sigma_{E[x]}"]···-and dually for $\IsT{0}$-connected $f\colon E\to B$ a dual comparison map $\ClosedMCyl_B(f)\to \CoLift_B(f)$ for the closed mapping cylinders.+and 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.-From \citet{riehl-shulman:2017} we recall that a type $C$ is called \emph{Segal complete} when it is internally right orthogonal to the comparison map $\Horn\hookrightarrow\Spx{\Two}$. To be precise, this means that the restriction map+From \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 mapis an equivalence. The Segal complete types form an \emph{accessible} reflective subuniverse---because the localising class $\mathcal{L}_{\textit{Segal}} \equiv \{\Horn\hookrightarrow\Spx{\Two}\}$ is very small indeed.···We also have evident inclusions $\II/i \hookrightarrow \Lift\IsT{i}$ and $i/\II\hookrightarrow \CoLift\IsF{i}$ as in the following classification squares:-\IsT{i}\ar[d,open immersion, "\eta_{\IsT{i}}"'] & |[pullback,ne pullback]|\IsT{i} \ar[r]\ar[l, equals] \ar[d,open immersion]& \{1\}\ar[d,open immersion]+\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]\Lift\IsT{i} & \ar[l,hookrightarrow,densely dashed, "\exists!"] \II/i\ar[r,hookrightarrow] & \II-\IsF{i}\ar[d,closed immersion, "\Flip{\eta}_{\IsF{i}}"'] & |[pullback,ne pullback]|\IsF{i} \ar[r]\ar[l,equals] \ar[d,closed immersion]& \{0\}\ar[d,closed immersion]+\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]\CoLift\IsF{i} & \ar[l,hookrightarrow,densely dashed, "\exists!"] i/\II\ar[r,hookrightarrow] & \IIWhen $\J$ is conservative, the inclusion $\II/i\hookrightarrow \Lift\IsT{i}$ is an equivalence.Dually when $\J\Op$ is conservative, the comparison map $i/\II\to\CoLift\IsF{i}$ is an equivalence. Hence, when $\J$ is stably quasi-coherent, both comparison maps are equivalences.···(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$.)We shall slightly adapt the definition of \emph{Sierpi\'nski completeness} from \citet{pugh-sterling-2025} to avoid relying on global assumptions.-A type $C$ is called \emph{Sierpi\'nski complete} when it is internally right orthogonal to the comparison map+A type $C$ is called \emph{Sierpi\'nski complete} when it is right orthogonal to the comparison map-for generic $\IsF{1}$-connected $X$.\footnote{Compare with \citet{pugh-sterling-2025}, who gave the definition of Sierpi\'nski completeness only under the global assumption that the $\J$ is non-trivial, so that \emph{every} $X$ is $\IsF{1}$-connected.}+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.}-Dually, we may define a type to be \emph{inverted Sierpi\'nski complete} when it is internally right orthogonal to+Dually, we may define a type to be \emph{inverted Sierpi\'nski complete} when it is right orthogonal to-for generic $\IsT{0}$-connected $X$. Evidently a type is Sierpi\'nski complete with respect to $\J$ if and only if it is inverted Sierpi\'nski complete with respect to $\J\Op$.+for 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$.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$.···-\[ \OpenMCyl_{(x:B)}E[x]\to \Lift_{(x:B)}E[x]\] from the geometrical to the logical for each family of $\IsF{1}$-connected types $x:B\vdash E[x]$.-\item The type $C$ is internally right orthogonal to the comparison map \[ \OpenMCyl_B(f)\to \Lift_B(f)\] for each $\IsF{1}$-connected function $f\colon E\to B$.+\[ \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]$.+\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$.-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+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-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.+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.-The thrust of \cref{thm:sierpinski-completeness-mapping-cylinders} is to say that in any subuniverse in which partial map classifiers exist and satisfy the universal property of the Sierpi\'nski cone, it \emph{also} follows that logical mapping cylinders (if they exist) must satisfy the universal property of (geometrical) mapping cylinders.+The thrust of \cref{thm:sierpinski-completeness-mapping-cylinders} is to say that in any subuniverse in which partial map classifiers exist and satisfy the universal property of the Sierpi\'nski cone, it \emph{also} follows that logical mapping cylinders (if they exist) must satisfy the universal property of (geometrical) mapping cylinders. 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$.We now complete the analysis of Sierpi\'nski completeness initiated by \citet{pugh-sterling-2025}.+\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.+We 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.+In 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.+The generic inner horn $\Horn \equiv \{ (i,j) \mid \IsF{j} \lor \IsT{i}\}$ is the sum $\textstyle\sum_{(i:\II)} \IsT{i}_\bot+$ 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$.+|[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]+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$.+\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"]\\+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'':+\HornLift(X) \ar[d,hookrightarrow] \ar[r,densely dashed,"\epsilon_X^{\Lambda}"] & X_\bot\ar[d, "\sigma_X"]+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+Note that the other evaluation map $\epsilon^\Lambda_X\colon \HornLift(X)\to X_\bot$ will \emph{not} generally have a section.+Any upper Segal complete type is right orthogonal to the inclusion $\HornLift(X)\hookrightarrow\TriLift(X)$ for generic $X$.+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:+C^{\TriLift(X)}\ar[d]\ar[r, "\cong"] & {\prod_{(i:\II, x:X^{\IsT{i}})}C^{\IsT{i}_\bot}}\ar[d,"\cong"]+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.+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.+& \HornLift(X) \ar[d,hookrightarrow] \ar[r, "\epsilon_X^{\Lambda}"] & X_\bot\ar[d, "\sigma_X"]+\Lift(X) \ar[r,"\tau_X"] \ar[rr, equals,curve={height=18pt}] & \TriLift(X)\ar[r,"\epsilon_X^\Delta"] & \Lift(X)+Recalling \cref{lem:segal-complete-right-orth-hornlift-trilift}, we obtain the following square by dualising with respect to $C$:+The composite map $C^{X_\bot}\to C^{\Lift(X)}$ traced above is immediately seen to be a retraction of $C^{\sigma_X}$.+Constructing 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}.+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$:+This is simply the universal property of $X_\bot$: the space of maps out of a pushout form a pullback.+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+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:+&\mathsf{restrict}_X^H~\chi~f~x :\equiv \mathsf{ap}_{f(0,-)} (\mathsf{paths}_\chi~(\lambda\_\mathpunct{.}x))+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.+Now we reformulate the data of a section to $C^{\sigma_X}$ in terms of \emph{extensions} of Sierpi\'nski cone data.+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:+%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 %%+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.+of extensions of Sierpi\'nski cone data to $\Lift(X)$. It is \emph{this} assignment that we shall construct.
+12
-1
refs.bib
+12
-1
refs.bib
···+@book{Rijke_2025, place={Cambridge}, series={Cambridge Studies in Advanced Mathematics}, title={Introduction to Homotopy Type Theory}, publisher={Cambridge University Press}, author={Rijke, Egbert}, year={2025}, collection={Cambridge Studies in Advanced Mathematics}}