Probably. But I’d like your comments here.

]]>Right, annoying $\pm 1$s. Have to rush now. But Toby has fixed it, right?

]]>Ah right, this is the old “$n$-connected” should really be interpreted as short for “$n$-simply connected” business. (H’m, that page should be connected better with Urs’s stuff.)

]]>Hmm, actually I think locally n-connected (n,1)-topos is wrong. Connectedness is one of the things where the numbering is off by one from where it “should” be: plain “connected” is the same as “0-connected” (the reason being that it’s equivalent to “$\pi_0$ is trivial”). So an (n,1)-topos whose morphism to 1 is essential should be called (n-1)-connected.

]]>OK, but I still don’t understand the numbering. Do you mean to say that overtness is local $0$-connectedness? You write

this condition is the “(0,1)-topos theoretic” version of the notion of locally connected topos and locally n-connected (n,1)-topos

but if $n = 0$, we get a locally $0$-connected $(0,1)$-topos. (And if $n = -1$, we get a locally $(-1)$-connected $(-1,1)$-topos, but that’s definitely not what we want.)

]]>I added some explanation of this to overt space.

]]>Well, that’s because what I said in #5 is wrong! According to the Elephant (at about C3.1.16), for locale maps to 1 it is *also* Frobenius reciprocity that is automatic, just like for geometric morphisms to 1. So I guess the point is rather that while one can always *define* “positivity” impredicatively, it doesn’t give you a left adjoint to $r^*$ unless the locale is overt.

I don’t understand why “locally $(-1)$-connected” should mean “open”, in either the context of $1$-toposes or $(0,1)$-toposes. But I don’t understand local connectedness in that context very well, so that should not surprise you.

I *do* see the connection between open geometric morphisms and locally connected geometric morphisms, in that both have a left adjoint to the inverse image functor (among other properties). But a locally connected geometric morphism to $1$ is the same as an essential geometric morphism, which has *only* that property, whereas an open geometric morphism to $1$ is stronger. So if a morphism to $1$ is locally $1$-connected iff it has a left adjoint, I don’t see how such a morphism is $(-1)$-connected only iff it also satisfies Frobenius reciprocity!

I was just defining “locally (-1)-connected geometric morphism” to mean “open geometric morphism.” But the definition of open geometric morphism is sort of an “internalization” to not-necessarily-localic topoi of the notion of open map of locales. I expect that by categorifying that, one could define a notion of locally k-connected (n,1)-topos for any n and k.

]]>What does “locally $(-1)$-connected” mean in this context? At locally n-connected (n,1)-topos, I only see a definition of that case, where the $n$s match. Here we have a $(0,1)$-topos (and hence an $(n,1)$-topos for $n \geq 0$), but you want it to be locally $(-1)$-connected. (I could truncate it to a $(-1,1)$-topos, but that no longer detects overtness.)

Otherwise, that all seems right to me.

]]>Ah, I think I get it. The positivity predicate is (as its name implies) the “notion of positiveness” which is definable, impredicatively. Overtness then adds the extra condition of “local positivity.”

In more topos-looking terms, the positivity predicate is the left adjoint $r_!$ of the pullback $r^* : Op(1) \to Op(X)$, which always exists impredicatively – but overtness says rather that $r: X\to 1$ is an open map, which means that not only does $r_!$ exist, it satisfies the “Frobenius reciprocity” law.

Also, a more generalizing name for overtness is “locally (-1)-connected”, and in the case of higher local-connectivity the existence of the left adjoint is not automatic even impredicatively.

Does that all seem right? If so, I will add some comments to that effect in appropriate places.

]]>Sure. As indicated in the third remark following the definition at formal topology, $\Diamond{a}$ holds iff every cover of $a$ is inhabited. So impredicatively, we can define

$a\colon S \;\vdash\; \Diamond{a} \;\coloneqq\; \forall U\colon \mathcal{P}S,\; a \lhd U \;\Rightarrow\; \exists x\colon S,\; x \in U .$But as this definition involves a quantification over subsets of $S$, it’s impredicative. (Predicatively but nonconstructively, we can also define $\Diamond{a} \;\coloneqq\; \neg(a \lhd \varnothing)$. Classically, these definitions agree.)

Now, a locale is overt iff every open has a cover consisting only of positive opens. (This is in impredicative but constructive locale theory; it should be in the Elephant.) I believe that the condition Pos on page 12 of Spitter is the analogue to this. Correcting an obvious typo and putting it in my notation, this reads

$U\colon \mathcal{P}S,\; a\colon S \;\vdash\; a \in U \;\Rightarrow\; a \lhd \{x\colon S \;|\; x \in U \;\wedge\; \Diamond{x}\} .$This is evidently stronger than my axiom (8), which I got from Sambin (first cited reference, bottom of page 3). (The other axioms in the definition on pages 11&12 all correspond, if you assume that $S$ is a semilattice, except that I don’t understand what Unit is supposed to even mean.)

]]>Can you say anything about why every formal space impredicatively has a positivity predicate, and how it differs from overtness?

]]>No.

Impredicatively (and therefore in every topos), *every* formal space has a positivity predicate, even though not every locale is overt (and of course, every formal space gives rise to a locale which ought to be the same space in different guise).

I see that some places (at least page 12 of Bas Spitter’s *Located and overt locales*) say things like

If a locale carries a positivity predicate it is said to be overt, or open

However, the definition there of ‘positivity predicate’ is stricter (and is indeed equivalent to giving rise to an overt locale).

This all reinforces my idea that there is a lot of variation in discussion of formal topology, and I’m no longer sure that following Sambin (as I did in the article) is the right thing to do.

]]>Should the predicate $\Diamond$ on a formal topology be regarded as making it into an overt space?

]]>