jonmsterling.com
+581
Martinfest/main.typ
+581
Martinfest/main.typ
···+So you put on your pith helmet and come in with your big and loud machines and terraform the mathematical world. It is a good day’s work.+Everything is very “civilised”: the sticky saps dry up, the buzzing insects zip away, and the last scurrying critters scatter to their holes.+Finally, all resistance muzzled, we can…show that the spectrum of a ring is a topological space.+But the thing about those little critters and buzzing bees and the sap that gets between your toes is—these entities were already an ecosystem with its own topology, geometry, arithmetic, computation—all intertwined together.+I wish to be as quiet as I possibly can, so I may hear the chirping, #pause chittering, #pause barking, #pause and buzzing #pause of the little creatures of little mathematics who,\ #pause+I would like to share with you some things I have learned recently about partial map classifiers and their generalisations.+Some of this I learned from my collaborations with my students Leoni Pugh and Lingyuan Ye respectively.+A $Sigma$-algebra is a bounded distributive lattice equipped with a homomorphism from $Sigma$, _i.e._ an object of $ALG :equiv Sigma arrow.b #DL$.+Each lattice $Sigma$ determines an “intrinsic” or “synthetic” topology, \ notions of open and closed subspace, partial map, _etc_.+Similar to _synthetic (domain theory, topology, algebraic geometry, _etc._)_ \ and _Abstract Stone Duality_ (Taylor), but we do not assume axioms\ globally: our language is HoTT/UF.+Delta^n &= Spec Sigma[sans(x)_1,...,sans(x)_n] #math.class("relation", sym.slash) sans(x)_i >= sans(x)_(i+1)+Some important shapes are _not_ spectrums, _e.g._ the generic inner horn $Horn$ obtained by glueing the interval onto itself end-to-end.+The interval $II$ is both a space (the spectrum of $Sigma[sans(x)]$) and the underlying \ set of the algebra $Sigma$.++ For any element $alpha in A^II$ we have $alpha(i) = alpha(0) or floor.l i floor.r and alpha(1)$.+Phoa's principle from _synthetic domain theory_ states $Sigma$ itself satisfies the property above. Implications for synthetic higher categories too.++ $Sigma$ is _dominant_ when it is conservative and the subuniverse $[-]colon Sigma arrow.r.hook PROP$ is closed under internal sums.+*NB*: if every quotient of $Sigma$ by finitely many equations is quasi-coherent, then both $Sigma$ and $Sigma^(op)$ are dominant (S. & Ye; _cf._ Cherubini _et al._).+Let $X$ be a space. An _observation_ of $X$ is an element of the observational algebra $Obs(X)$, _i.e._ a function $phi colon X -> II$.+We shall refer to an arrow of the form $U arrow.r.hook X$ arising from some observation as an _open embedding_. A _cloven open embedding_ is defined \ to be an open embedding equipped with an observation whence it arises.+By duality, a _closed embedding_ is an embedding $K arrow.r.hook X$ arising from an observation $phi in CoObs(X)$ in the *dual lattice context*. In terms of $Sigma$, this\ is a pullback of the inclusion ${0} arrow.r.hook II$.+A _cloven_ open partial map from $X$ to $Y$ is a partial map equipped with a _cleaving_ for its constituent open embedding:+The _partial product_ of the generic open embedding ${1} arrow.r.hook II$ with a\ space $Y$ classifies cloven open partial maps into $Y$. Defining+Every cloven open partial map from $X$ to $Y$ arises from a _unique_ function $X -> Lift(Y)$ in the following way:+Y edge("d", "hook->") & U edge("d", "hook->") edge("l", ->) edge("r", ->) & {1} edge("d", "hook->")\+Lift(Y) & X edge("l", "-->", label: exists!, label-side: #left) edge("r", ->, label-side: #right) & II+X edge("d", "hook->") & bold(0) edge("d", "hook->") edge("l", "hook->", label: !_X) edge("r", ->) & {1} edge("d", "hook->")\+Lift(X) & bold(1) edge("l", "hook-->", label: "und"_X, label-side: #left) edge("r", ->, label-side: #right, label: "0") & II+In ordinary domain/category/topos theory, the open partial map classifier $Lift(X)$ is _also_ the *Sierpiński cone* $X_bot$, which freely adds a bottom point.+X edge("d", ->) edge("r", ->, label: 1_X) & X edge("d", "hook->", label: iota_X, label-side: #left)\+X edge("d", ->) edge("r", "hook->", label: (0,X)) & II times X edge("d", "hook->", label: gamma_X, label-side: #center) & edge("l", "hook->", (1,X)) X edge("dl", "hook->", label: iota_X, label-angle: #auto, label-side: #left)\+*NB*: $bot$ is _closed_ in $X_bot$, and $iota_X$ is an _open embedding_ as soon as $Sigma$ is strict.+X edge("d", "hook->") edge("r", ->, label: (0, X)) & II times X edge("d", "hook->", label-side: #left, label: "glue"_X)\+If induced comparison map $X_bot -> Lift(X)$ is an equivalence for _generic_ $X$, then naturally each $[i]_bot -> Lift [i]$ is an equivalence. But+and so for any $j <= i$ we may conclude either $j=0$ or $i=1$. Considering $j :equiv i$ we therefore have $i=0 or i=1$, which makes all spaces codiscrete. When $II$ is strict, this makes the boundary inclusion $bold(2) arrow.r.hook II$ an equivalence.+In domains/categories/toposes, $X_bot -> Lift(X)$ is an equivalence for _global_ $X$, not for _generic_ $X$. We could use a $flat$-modality or switch to the Mitchell--Bénabou language to safely assert it only for global things.+But I am more interested in powering down the engines so that we can _hear_ what the spaces are telling us in their own terms.++ It is not fair to compare $X_bot$ with $Lift(X)$ without fixing a universe of discourse, which (in synthetic mathematics) means an _accessible reflective subuniverse_ in which to compute the pushout $X_bot$.++ “All” the comparison maps $X_bot -> Lift(X)$ is far too large a left class to generate a reflective subuniverse, but *this localisation is nonetheless accessible and reflective*, and the presentation is _extremely_ small.++ For free we get a _limit-style_ computation of _mapping cylinders_ (Artin glueings) without higher inductive types.+_*Definition.*_ A type $X$ is called _$[0]$-connected_ when either of the following equivalent conditions hold:+_*Remark.*_ When $Sigma$ is conservative, the above is a slight _strengthening_ of the Segal condition for synthetic $(infinity,1)$-categories.+Last year I proved a restricted version for $0$-truncated $C$. Last month, I proved it unconditionally in Martin-Löf’s intensional type theory with function extensionality, for an arbitrary bounded partial order $Sigma$.+Many geometrical constructions expressed globally are actually _sums_ of simpler structures that can only be written down in type theory.+Here, open/closed refers not to the topology induced by $Sigma$ but rather to the partitioning of the ambient higher topos $cal(E)$ into open/closed subtoposes. Nonetheless, there is a startling connection.+The partial map classifier with respect to $Sigma$ is the _sum_ of all the open modalities $opmod([i])$, as we have $Lift(X) equiv mysum(i,II) opmod([i]) X$. Conversely, letting $ isf(-) colon II -> PROP $ be the indicator function for $0 in II$,+we will see that the Sierpiński cone is the sum of all the _closed modalities_ $clmod(isf(i))$, _i.e._+A beautiful symmetry emerging from the failure of De Morgan’s laws in constructive mathematics, which I learned from Reid Barton.+#only("2-")[Then we apply the left adjoint $mysum(i,II) colon TYPE_(slash (i:II)) -> TYPE$, which preserves colimits.] #only("3-")[Then we simplify.]+E edge("d", ->, label: f) edge("r", ->, label: 1_E) & E edge("d", "hook->", label: iota_f, label-side: #left)\+E edge("d", ->) edge("r", "hook->", label: (0,E)) & II times E edge("d", "hook->", label: gamma_f, label-side: #center) & edge("l", "hook->", (1,E)) E edge("dl", "hook->", label: iota_f, label-angle: #auto, label-side: #left)\+*NB*: $B arrow.r.hook MCyl(f)$ is a closed embedding; when $f colon E -> B$ is a $[0]$-connected map, then $iota_f colon E arrow.r.hook MCyl(f)$ is an open embedding.+The open mapping cylinder $MCyl(f)$ turns out to be the sum of all the Sierpiński cones of the _fibres_ of $f$. #only("2-")[We compute generically in $x:B$.] #only("3-")[Then we apply the left adjoint $mysum(x,B) colon TYPE_(slash (x:B)) -> TYPE$.] #only("4-")[Simplify with Frobenius,] #only("5-")[ and straightening/unstraightening.]+mysum(x,B) fib(f,x) edge("d", ->) edge("r", "hook->") & mysum(x,B) II times fib(f,x) edge("d", ->) \+mysum(x,B) fib(f,x) edge("d", ->) edge("r", "hook->") & II times mysum(x,B) fib(f,x) edge("d", ->) \+From a type theoretic point of view, the function $f colon E -> B$ could be viewed instead as a family $x:B tack.r E[-] : TYPE$, whose open mapping cylinder we can define more directly.+All this suggests a “logical” or limit-style counterpart to the open mapping cylinder, using the partial map classifier:\+Let $x:B tack.r E[x]$ be a family of $[0]$-connected types. Then we have an evident universal comparison map $MCylFam_((x:B)) E[x] -> LiftFam_((x:B)) E[x]$.+_*Corollary.*_ Let $C$ be Sierpínski complete. Then for any family $x:B tack.r E[x]$ of $[0]$-connected types, $C$ is orthogonal to this comparison map, _i.e._+Several years ago, I asked whether the Artin glueing of a geometric morphism classifies models of an interesting theory.+Our results imply an answer to the analogous question for *synthetic topology*: in suitable reflective subuniverses, mapping cylinders may be computed as sums of partial map classifiers. The subtlety is to ensure the reflective subuniverse is closed under mapping cylinders of _suitable_#footnote[Take care: the appropriate condition on the family is _not_ fiberwise: we need the _fibration_ $mysum(b,B)E[x] -> B$ and the base $B$ to be local.] families.+All these notions and results can be dualised to _closed embeddings_ by considering the dual lattice $Sigma^"op"$. We have Hyland's co-partial map classifier $CoLift(X)$ and the inverted Sierpiński cone $X^top$, and the closed mapping cylinders $ClMCyl(f)$.
+351
-134
lics.tex
+351
-134
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}+\One\arrow[r,swap,closed embedding,"\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"] \\+\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 immersion]\ar[r,gray,-{Triangle[fill=gray]}, hook] & |[gray]|\XX \ar[u,swap,gray,open immersion,"\eta_\XX"]+|[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 immersion,swap,"\iota_\XX"] & \XX\ar[d,open immersion,"\eta_\XX"]\\+|[pullback]|\XX\ar[r,equals]\ar[d,open embedding,swap,"\iota_\XX"] & \XX\ar[d,open embedding,"\eta_\XX"]\\···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···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))_\bot+\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 immersion,"\bot_X"]\ar[ur,phantom,"{\Uparrow}\gamma_X"] & X\mathrlap{_\bot}+\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 immersion,"\top_X"]\ar[ur,phantom,"{\Downarrow}\Flip{\gamma}_X"] & X\mathrlap{^\top}+\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 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$.+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$.·········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:···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"] \\+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 immersion.+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 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.+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 immersion $\{1\}\hookrightarrow\II$ forms a dominance.+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 immersion $\{0\}\hookrightarrow\II$ for $\J$ 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 immersion] \ar[r] & \sum_{(x:B)}E[x]\ar[d, "\pi_1"description] & K\ar[d,closed immersion]\ar[l]\\+U \ar[d, open embedding] \ar[r] & \sum_{(x:B)}E[x]\ar[d, "\pi_1"description] & K\ar[d,closed embedding]\ar[l]\\···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.+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.······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.+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 $\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.-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.···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]+\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 immersion, "\Flip{\eta}_{\IsF{i}}"'] & |[pullback,ne pullback]|\IsF{i} \ar[r]\ar[l,equals] \ar[d,closed immersion]& \{0\}\ar[d,closed immersion]+\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] & \IIWhen $\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 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 internally right orthogonal to+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$.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 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$.+\[ \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 consider the following (definitionally) 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-in which we must verify that the left-hand map is an equivalence. The upper and lower maps are the dependent currying/uncurrying equivalences, and the eastern map is the functorial action of the \emph{product} functor on the family of equivalences given by the Sierpi\'nski completeness of $C$. By the three-for-two property of equivalences, it follows that the left-hand map is an equivalence.+in which we aim to verify that the left-hand map is an equivalence. The upper and lower maps are the dependent currying equivalences, and the eastern map is the functorial action of the \emph{product} functor on the family of equivalences given by the Sierpi\'nski completeness of $C$. By the three-for-two property of equivalences, it follows that the left-hand map is an equivalence.-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.+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 $\IsT{0}$-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.+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$.+|[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"]+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:+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.+& \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 $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 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.
+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}}