jonmsterling.com
+18
-17
lics.tex
+18
-17
lics.tex
···-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{$\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.···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 $\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.···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 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$.···-\[ \OpenMCyl_{(x:B)}E[x]\to \Lift_{(x:B)}E[x]\] from the geometrical to the logical open fibre cylinder for each family of $\IsF{1}$-connected types $x:B\vdash E[x]$.+\[ \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 considering the following 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···\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.+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.···-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.+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.···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+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