jonmsterling.com
+135
-111
lics.tex
+135
-111
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}-\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"] \\···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"]-|[pullback]|\XX\ar[r,equals]\ar[d,open immersion,swap,"\iota_\XX"] & \XX\ar[d,open immersion,"\eta_\XX"]\\···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))_\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}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}···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$.············Eliminating singletons, we therefore obtain the familiar categorical description of the Sierpi\'nski cone:-X\ar[r,closed immersion,"{(0,X)}"]\ar[d] & \II\times X \ar[d,"\gamma_X"description] & X\ar[l,open immersion,swap,"{(1,X)}"]\ar[dl,sloped,swap,hookrightarrow,"\iota_X"] \\-Note that unless $\J$ is consistent, the inclusion $\iota_X\colon X\hookrightarrow X_\bot$ may not be an open immersion.Dually, we define the \emph{inverted} Sierpi\'nski cone $X^\top$ of $X$ to be the Sierpi\'nski cone in the geometric context of the distributed lattice $\J\Op$. In particular, we have···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.-We will say that $\J$ is \emph{dominant} when the open immersion $\{1\}\hookrightarrow\II$ forms a dominance.-As an example, the dual lattice $\J\Op$ is dominant if and only if the closed immersion $\{0\}\hookrightarrow\II$ for $\J$ forms a dominance.···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]\\······is cartesian, where $\pi\colon X_\bot \to \II$ is the map obtained universally from the following square:···of the Sierpi\'nski cone, the described map $\pi\colon X_\bot \to \II$ is precisely the first projection function, whose fibre over generic $i:\II$ is $\IsF{i}*X$. We are asked to check that the fibre of $\pi$ at $1:\II$ is precisely $X$, \emph{i.e.}\ that the canonical map $X \to \IsF{1}*X$ is an equivalence. But this is one of the equivalent formulations of $X$ being $\IsF{1}$-connected.-Dually, the embedding $\Flip{\iota}_X\colon X\hookrightarrow X^\top$ is a closed immersion for $\IsT{0}$-connected $X$. Furthermore, the embeddings $\iota_f\colon E\hookrightarrow \OpenMCyl_B(f)$ and $\Flip{\iota}_f\colon E\hookrightarrow \ClosedMCyl_B(f)$ are open and closed respectively when $f\colon E\to B$ is a $\IsF{1}$-connected map. Of course, $\IsT{0}\cong \IsF{1}$ so $\IsF{1}$-connectedness and $\IsT{0}$-connectedness coincide, but they are \emph{definitionally} distinct properties.When $X$ is $\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 also have evident inclusions $\II/i \hookrightarrow \Lift\IsT{i}$ and $i/\II\hookrightarrow \CoLift\IsF{i}$ as in the following classification squares:-\IsT{i}\ar[d,open immersion, "\eta_{\IsT{i}}"'] & |[pullback,ne pullback]|\IsT{i} \ar[r]\ar[l, equals] \ar[d,open immersion]& \{1\}\ar[d,open immersion]\Lift\IsT{i} & \ar[l,hookrightarrow,densely dashed, "\exists!"] \II/i\ar[r,hookrightarrow] & \II-\IsF{i}\ar[d,closed immersion, "\Flip{\eta}_{\IsF{i}}"'] & |[pullback,ne pullback]|\IsF{i} \ar[r]\ar[l,equals] \ar[d,closed immersion]& \{0\}\ar[d,closed immersion]\CoLift\IsF{i} & \ar[l,hookrightarrow,densely dashed, "\exists!"] i/\II\ar[r,hookrightarrow] & \II······-|[pullback]|\{(1\geq i)\mid i:\II\} \ar[r] \ar[d,open immersion] & |[pullback]|\{(1\geq i)\mid i:\II\}\ar[r]\ar[d,open immersion] & \{1\} \ar[d,open immersion]···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"]···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.···\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}$.···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 constractible. Hence from the fundamental theorem of identity types~\citep{Rijke_2025} we obtain a canonical family of equivalences-For $\IsF{1}$-connected $X$, the \emph{Sierpi\'nski restriction} of a $f\colon \Lift(X)\to C$ is defined be the following Sierpi\'nski cone datum over $C$:-\textcolor{red}{I think I actually need to replace $\IsF{1}$-connectedness with $\IsT{0}$-connectedness.}Now we reformulate the data of a section to $C^{\sigma_X}$ in terms of \emph{extensions} of Sierpi\'nski cone data.-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 mapping
······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 embedding,"\bot_\XX"]\ar[ur,phantom,"{\Uparrow}\gamma_\XX"] & \XX\mathrlap{_\bot}+\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 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 embedding,swap,"\iota_\XX"] & \XX\ar[d,open embedding,"\eta_\XX"]\\···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 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 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 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 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$.············Eliminating singletons, we therefore obtain the familiar categorical description of the Sierpi\'nski cone:+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 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 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 embedding $\{1\}\hookrightarrow\II$ 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 embedding] \ar[r] & \sum_{(x:B)}E[x]\ar[d, "\pi_1"description] & K\ar[d,closed embedding]\ar[l]\\······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 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 $\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 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 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 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] & \II······+|[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"]···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.···\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}$.···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.