jonmsterling.com
+83
-15
lics.tex
+83
-15
lics.tex
···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:······\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 $\IsF{1}$-connected $X$ is a section and a retraction. In fact, the retraction property of $C^{\sigma_X}$ was verified unconditionally by \citet{pugh-sterling-2025}, but we have a more conceptual proof that we will show. On the other hand, the section property of $C^{\sigma_X}$ without side conditions is entirely new.+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 $\IsF{1}$-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.\begin{proposition}[{\citet{pugh-sterling-2025}}]\label[proposition]{prop:horn-tri-as-sums}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$ of the interval.+$ 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$.-\{(1\geq i)\mid i:\II\} \ar[r] \ar[d,open immersion] & \{(1\geq i)\mid i:\II\}\ar[r]\ar[d,open immersion] & \{1\} \ar[d,open immersion]+|[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]······-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+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···-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. By the three-for-two property, the left-hand map is an equivalence too.+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 an upper Segal complete type. Then for $\IsF{1}$-connected $X$ the restriction map \[ C^{\sigma_X} \colon (\Lift(X)\to C) \to (X_\bot\to C)\] has a retraction.+Let $C$ be upper Segal complete. Then for $\IsF{1}$-connected $X$ the restriction map $C^{\sigma_X} \colon (\Lift(X)\to C) \to (X_\bot\to C)$ has a retraction.···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 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 $\IsF{1}$-connected $X$, an \emph{extension} of a Sierpi\'nski cone datum $\mathbf{c}:\mathsf{SD}_X(C)$ is defined to be a mapping
+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}}