Organising and scaffolding

Changed files
+29 -14
+29 -14
lics.tex
···
\section{Local subuniverses of spaces}
-
\subsection{Segal completeness}
+
\subsection{Preliminary definitions}
+
+
\subsubsection{Segal completeness}
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
\[
···
is 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.
-
\subsection{Upper and lower Segal completeness}
+
\subsubsection{Upper and lower Segal completeness}
% \subsubsection{Slices and co-slices of the interval}
···
\]
\end{remark}
-
\subsubsection{Upper and lower Segal completeness}
-
\begin{definition}
A type $C$ is said to be \emph{upper Segal complete} when it is orthogonal to the inclusion $\IsT{i}_\bot \hookrightarrow \II/i$ for generic $i:\II$. Dually, $C$ is said to be \emph{lower Segal complete} when it is orthogonal to the inclusion
···
(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$.)
-
-
\begin{corollary}[{\citet{pugh-sterling-2025}}]
-
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$.
-
\end{corollary}
-
-
\begin{corollary}
-
Dually, when $\J\Op$ is conservative, $C$ is lower Segal complete if and only if it is orthogonal to the dual comparison map $\Flip{\sigma}_{\IsF{i}}\colon \IsF{i}^\top\hookrightarrow \CoLift\IsF{i}$ for generic $i:\II$. Therefore, when $\Sigma$ is stably quasi-coherent, the upper and lower Segal conditions are precisely equivalent to being orthogonal to each $\sigma_{\IsT{i}}$ and $\Flip{\sigma}_{\IsF{i}}$ respectively.
-
\end{corollary}
-
-
\subsection{Sierpi\'nski completeness}
+
\subsubsection{Sierpi\'nski completeness}
We shall slightly adapt the definition of \emph{Sierpi\'nski completeness} from \citet{pugh-sterling-2025} to avoid relying on global assumptions.
···
\Flip{\sigma}_X\colon X^\top \to \CoLift(X)
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$.
+
+
+
\subsection{Comparing orthogonality laws}
+
+
\begin{proposition}[{\citet{pugh-sterling-2025}}]
+
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$.
+
\end{proposition}
+
+
\begin{corollary}
+
Dually, when $\J\Op$ is conservative, $C$ is lower Segal complete if and only if it is orthogonal to the dual comparison map $\Flip{\sigma}_{\IsF{i}}\colon \IsF{i}^\top\hookrightarrow \CoLift\IsF{i}$ for generic $i:\II$. Therefore, when $\Sigma$ is stably quasi-coherent, the upper and lower Segal conditions are precisely equivalent to being orthogonal to each $\sigma_{\IsT{i}}$ and $\Flip{\sigma}_{\IsF{i}}$ respectively.
+
\end{corollary}
+
\begin{proposition}[{\citet{pugh-sterling-2025}}]
If $\J$ is conservative, then any Sierpi\'nski complete type with respect to $\J$ is upper Segal complete.
···
\begin{corollary}
When $\J\Op$ is conservative, dually, any inverted Sierpi\'nski complete type with respect to $\J$ is \emph{lower} Segal complete. Therefore, when $\J$ is stably quasi-coherent, Sierpi\'nski completeness (\emph{resp.}\ inverted Sierpi\'nski completeness) implies upper (\emph{resp.}\ lower) Segal completeness.
\end{corollary}
+
\begin{theorem}\label{thm:sierpinski-completeness-mapping-cylinders}
The following are equivalent for a type $C$:
···
\end{proof}
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.
+
+
\subsubsection{From upper Segal to Sierpi\'nski completeness}
+
+
We now complete the analysis of Sierpi\'nski completeness initiated by \citet{pugh-sterling-2025}.
+
+
\begin{theorem}
+
Any upper Segal complete type is Sierpi\'nski complete.
+
\end{theorem}
+
\textcolor{red}{TODO}
+
+
\section{Closure of local subuniverses under logical mapping cylinders}
\clearpage