jonmsterling.com
+149
-24
lics.tex
+149
-24
lics.tex
·········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···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:···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.······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···-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.···When $\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 mapfor 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.}-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 tofor 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$.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 open fibre cylinder 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$.+\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 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 $\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.+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.+\{(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]+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:+{[\TriLift(X), C]}\ar[d]\ar[r, "\cong"] & {\prod_{(i:\II, x:X^{\IsT{i}})}\bigl[\IsT{i}_\bot, C\bigr] }\ar[d,"\cong"]+The upper and lower maps are the 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.+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.+& \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 $[X_\bot,C]\to [\Lift(X),C]$ is immediately seen to be a retraction of $[\sigma_X,C]$.