I don’t remember whether I made this connection back in November, but I’m recording it here now for future reference. Over in that thread a day after this one, we concluded that at least for $Sh(CartSp)$, the codiscrete modality $\sharp$ is localization at the maps $\Delta \mathbb{R}^n \to R^n$. Since these are all monomorphisms, $\sharp$ should be a topological localization, answering the question asked at the beginning of this thread.

Therefore, since it is also a Boolean and dense subtopos, by this result it also consists of the double-negation sheaves (by which in an $\infty$-context I mean the localization at the class of $\neg\neg$-dense monos).

]]>The issue is that an internally defined modality is a stable factorization system, but it may not be a reflective one.

Oh, okay, thanks. I don’t think about this often enough to remember all the fine print. But I should.

I’m hoping to write a nice exposition once I’ve got it all implemented in the new HoTT Coq library.

That sounds good. Am looking forward to that!

]]>Ah, yes. The issue is that an internally defined modality is a stable factorization system, but it may not be a reflective one. Even though it is “determined by the class $M/1$” in some way (internally; externally not even this is true), it’s not determined in the same way as a reflective FS: we define $M$ to be the maps with fibers in $M/1$, and $E$ to be the maps whose reflection into $M/1$ is trivial. This $E$ is pullback-stable, but in general not every map inverted in $M/1$ lies in $E$. Think of the $n$-connected/truncated FS: a map is $n$-connected if it is iso on $\pi_{\le n}$ and surjective on $\pi_{n+1}$, whereas the first condition is enough for it to be inverted by $n$-truncation.

I have a pretty good picture of the landscape in my head by now, but unfortunately it isn’t written out very clearly anywhere. I’m hoping to write a nice exposition once I’ve got it all implemented in the new HoTT Coq library.

]]>I was thinking of this statement that a reflective factorization system is stable iff the reflector is lex.

There is by now a plethora of different internal versions of the naive concept of reflection. Do you personally keep some map of the territory, or is it just all manifest to you by now?

]]>A reflective subuniverse phrased internally is automatically an exponential ideal, and a modality phrased internally automatically has stable units. Those are both left-exactness properties, but neither of them is as strong as full left exactness.

]]>Thanks. I am following what you say about smallness, but I am momentarily confused about the motivation.

Wasn’t the point that a modality phrased internally is automatically externally lex? We used to discuss the issue of how to get rid of this left exactness. Now you seem to want to get hold of it.

]]>It occurred to me to wonder because in formalizing lex modalities, I’ve discovered the issue of universes requires a bit more care. In HoTT we can’t actually say “$\bigcirc$ preserves finite limits” because it is a quantification over all types. We can quantify over all types in a particular universe, but that isn’t quite the same. I do know how (I think) to prove that an internal localization at a family of hprops is automatically lex, so that would be a “small” way of ensuring that a modality is lex; hence I wondered whether the modalities we care about are of that form, which is at least closely related to being topological. This is also what prompted this question.

]]>Hm, nothing that seems to lead to the conclusion of topological localization.

Let’s see. I suppose $\sharp$ is equivalent to localization at $\flat$-equivalences,which are the same as $\Gamma$-equivalence (equivalences under global sections).

Factoring $\Gamma$-equivalences into 1-epis followed by 1-monos, we are left with having to show that localization at 1-epis that are $\Gamma$-equivalences might be given by localization at monos.

What could we do?

Using a site of definition we know that the condition of 1-epi + $\Gamma$-equivalence means that the morphism is an equivalence on points and an epi on stalks after 0-truncation. Is that enough to even build a retract, let alone show that it may be assumed 1-mono, without restriction of generality?

I am a bit out of ideas here.

(So probably you are after topological localization now because it simplifies some formalization, is that so?)

]]>Any thoughts about $\sharp$?

]]>Ok, so localization at a morphism that has a section is the same as localization at the section, and since $Spec(W)$ is an hset, the inclusion of its point is a mono. Thanks!

]]>In the Cahiers topos $Sh(\{\mathbb{R}^n \times Spec(W)\}_{n,W})$ the infinitesimal shape modality is localization at the morphisms $(-) \times Spec(W)\to (-)$ that contract the infinitesimally thickened points away ($W$ ranging over “Weil algebras” $W = \mathbb{R} \oplus finite\;dimensional\;nilpotent\;ideal$). Regarding this as localization at the unique point inclusions $(-) \hookrightarrow (-)\times Spec(W)$, all these are monomorphisms. So this should be a topological localization.

]]>The codiscrete objects in a cohesive $(\infty,1)$-topos, and the coreduced objects in a differentially cohesive one, are subtoposes, i.e. accessible left exact localizations. Are they (in the primary examples) *topological* localizations, in the sense of HTT 6.2.1?