I added in some common modal axioms. Could do with some commentary.

]]>That’s a point. The full quote from #79 comes after acknowledgement of the advantages of toposes over ionads, and then says:

…yet there remain good reasons for having the notion of ionad available to us. The first is that some particular applications of topos theory may be more perspicuously expressed in the language of ionads than of toposes: two examples that come to mind are the sheaf-theoretic semantics for first-order modal logic given in [1], and the generalised Stone duality of [5]. The second reason is pedagogical. Many aspects of topos theory are abstractions of corresponding aspects of general topology, but the abstraction is twice removed: first one must pass from spaces to locales, and then from locales to toposes. At the first step, one loses the points, which to many, is already to enter a quite unfamiliar world, and the second step can only compound this unfamiliarity. With the notion of ionad available, one may arrive at these same abstractions by a different route, passing first from spaces to ionads, and then from ionads to toposes. The advantage of doing so is that one retains the tangibility afforded by the presence of points for as long as possible. It seems to me that it is in this pedagogical aspect that ionads are likely to make their most useful contribution.

Hmm, maybe not too advantageous then.

]]>I would have to look at Garner’s article to see what he claims might be gained by such terminology.

I suppose he proves something about finite limit perserving comonads that has not been noticed elsewhere before?

]]>Where would it take us then if we declare:

An $\infty$-ionad is given by an $\infty$-groupoid, $X$, and a finite $\infty$-limit preserving comonad, $I_X: \infty Grpd/X \to \infty Grpd/X$?

Then we could have:

The $(\infty, 1)$-category of opens $O(X)$ of an $\infty$-ionad $X$ is the category of $I_X$-coalgebras.

This would be an $(\infty, 1)$-topos.

Presumably there would be no reason to stick to $\infty Grpd$ as the base topos.

]]>Well I’d still like to know the ’meanings’ of the comonad, $i^\ast \circ i_\ast$, and monad, $i^\ast \circ i_!$, on $\mathbf{H}/\flat X$. Is there something like an ’interior’ for a topology happening in the former? Is the analogue of putting a topology on a set just to locate a type with given image under $\flat$? Do analogues of the ionads paper work out, e.g., section 3 on generalized bases?

Maybe in a more speculative direction, if we follow Garner

there remain good reasons for having the notion of ionad available to us. The first is that some particular applications of topos theory may be more perspicuously expressed in the language of ionads than of toposes: two examples that come to mind are the sheaf-theoretic semantics for first-order modal logic given in [1], and the generalised Stone duality of [5],

then perhaps if Awodey et al. show that their sheaf semantics is complete for first order S4 modal logic, we can start to see why this is so from the larger perspective of slice $\infty$-toposes, or say something similar about modal type theory?

And there may be a higher models-theory duality, maybe for type theories, along the lines of First-Order Logical Duality and Scheme representation for first-order logic.

]]>you professionals could probably sort it out between you in 15 milliseconds

Maybe you could highlight again what exactly you’d like to see sorted out.

My impression was you already found the analogy you wanted in #74:

so the analog of the category $Set^X \simeq Set_{/X}$ of $X$-indexed sets is the slice $\mathbf{H}_{/X}$ for any object $X$ in the $\infty$-topos $\mathbf{H}$. Now you are asking for finite $\infty$-limit preserving comonads on such slices. You get one such by base change along any morphism out of $X$.

This establishes the analogy to ionads. In particular jets would be an example. Now what I don’t know is what that analogy tells us, if anything.

]]>Right, I’d better go and do something else. I’m getting more whiffs that something ionad-ish is going on when the base is set-like, and perhaps there might even be flat bundle-valued differential forms about. But you professionals could probably sort it out between you in 15 milliseconds, and I need to write some philosophy papers.

]]>Oh, I see. That’s of course, true, too.

]]>Just to clarify, my initial thought was that we had a case already of the operation of $i^{\ast}$:

$i^{\ast} (\ast \to \mathbf{B} G) = (\flat_{dR}\mathbf{B}G \to \flat \mathbf{B}G).$ ]]>Oh, I see. I though we were just working out $i^{\ast}$, and that that would have an existing name as something which flattens. But perhaps it’s easier to go for the composite straight away. I’ll go back and read with that in mind.

Presumably it’s possible that composing the other way is interesting $i_! \circ i^\ast$, but all seems to point to the other way,

An

ionadis a set $X$ together with a finite limit-preserving comonad $Int_X$ on the category $Set^X$

chimes with

In the original expression, we consider the geometric morphism from the topos $Sets/|X|$ of sets indexed over a set $|X|$ to the topos $Sh(X)$ of sheaves over a topological space induced by the (continuous) identity map $id: |X| \to X$. The modal operator $\Box$ is interpreted by the interior operation $int$ that the comonad $id^{\ast} \circ id_{\ast}$ induces on the Boolean algebra $Sub_{Sets/|X|}(id^{\ast} F) \cong \mathcal{P}(F)$ of subsets of $F$.

[EDIT: These are, of course, using the right adjoint to $i^\ast$, but still the interest is starting out from the discrete side.]

]]>then why do you have $\flat B$ in both corners of that square?

I thought that’s what you were suggesting to look at. The operation $i^\ast \circ i_!$ in your #67 above is the operation that sends any $\phi \colon X \to \flat B$ to the pullback

$\array{ &\longrightarrow& X \\ {}^{\mathllap{i^\ast i_! \phi}}\downarrow && \downarrow^{\mathrlap{\phi}} \\ && \flat B \\ \downarrow && \downarrow \\ \flat B &\longrightarrow& B } \,.$I thought your point in #68 had been to observe that then the $\flat_{dR}$-operation becomes sort of a special case of the possibility-like modality $i^\ast \circ i_!$, via

$\flat_{dR} B = \ast \underset{\flat B}{\times} i^\ast i_! id_{\flat B} \,.$ ]]>Well I just meant that there’s some process which takes us from some bundle $X \to B$ to some other bundle $Y \to \flat B$. Wouldn’t we call that a ’flattening’.

Anyway, I was with you so far, but then why do you have $\flat B$ in both corners of that square?

]]>You mean: to pick trivial underlying $\infty$-groupoid $\infty$-bundles.

Consider first pointed connected coefficients, hence of the form $\mathbf{B}G$. Then the homotopy pullback $\flat_{dR}\mathbf{B}G$

$\array{ \flat_{dR}\mathbf{B}G &\longrightarrow& \flat \mathbf{B}G \\ \downarrow &\swArrow& \downarrow^{\mathrlap{\chi}} \\ \ast &\longrightarrow& \mathbf{B}G }$has the following interpretation: its generalized elements consist of

a flat connection $\nabla \in \flat \mathbf{B}G$ with underlying bundle $\chi(\nabla) \in \mathbf{B}G$;

an equivalence $\ast \simeq \chi(\mathbf{B}G)$.

Hence it’s a flat connection equipped with a trivialization of the underlying bundle. Classically this is the same as a flat (closed) differential form.

Now as you generalize this from the pointed connected $\mathbf{B}G$ to any $B$, then $B$ has the interpretation of classifying groupoid principal bundles. Now there is not a single trivial such, but there is one trivial such for each connected component of $B$. You may choose to pick all of these connected components and all of the transformations between them, and then consider the homotopy pullback $Q$ in

$\array{ Q &\longrightarrow& \flat B \\ \downarrow &\swArrow& \downarrow^{\mathrlap{\chi}} \\ \flat B &\longrightarrow& B } \,.$Clearly this has *some* relation to $\flat_{dR}$. I suppose if one picks one representative points in each connected component of $B$ and hence pulls back along some $\pi_0(\flat B) \longrightarrow \flat B$, then one obtains the “right” definition of $\flat_{dR}$ for groupoid-principal connections.

Right now I am not sure what it means to retain all the higher homotopy information of the $\flat B$ in the bottom left corner.

But I agree that this looks like a sensibel perspective from which to view $\flat_{dR}$ in generality.

]]>The must be a universal way to flatten a connection on an $\infty$-bundle.

]]>So $\flat_{dR}$ is supposed to be defined on pointed objects, and then the pullback is along the one canonical basepoint. But of course you have a point here that in the absence of a choice of such a basepoint, then it may make sense to call the construction that you are considering here a generalized $\flat_{dR}$-construction.

]]>It would probably be better for the soul to work this out myself.

So $i_!$ is a forgetting of the flatness of a connection.

Then $i^{\ast}$ provides a pullback, so is a general version of the dR-flat modality.

]]>I was trying to work out some of the modalities to arise from those modalities we know and love via base change and adjoints. If you consider the eleven (non-identity) modalities of the cohesion - table, then for each one there is the corresponding (co)unit. For a given object, $X$, we can then base change along the (co)unit and form its left and right adjoint. These in turn can be composed to generate four (co)monads.

Why consider these 44? Well we have 6 data points that some are interesting.

- The monad $\ast$ and $X$ a set: necessarily, possibly, reader monad, writer comonad.
- The monad $\Im$: jet comonad, infinitesimal disk bundle,…

So I’d like to work out some others.

As I said above, there might be something useful to do with the counit of the comodality $i: \flat(X) \to X$?

$(i_! \dashv i^\ast \dashv i_\ast) \;\colon\; \mathbf{H}_{/\flat (X)} \stackrel{\overset{i_!}{\longrightarrow}}{\stackrel{\overset{i^\ast}{\longleftarrow}}{\underset{i_\ast}{\longrightarrow}}} \mathbf{H}_{/X} \,.$Again four (co)monads from the composites. Can we name any of them?

]]>There are some comments in Remark 7.7 of my realcohesion paper about how spatial type theory is related to the Awodey et. al. semantics for modal logic, in case that is helpful.

]]>To return (after a long while) to ionads and modal logic (#33 and #40), looking back at the quote in the post linked from (#33) from Awodey and Kishida:

In the original expression, we consider the geometric morphism from the topos $Sets/|X|$ of sets indexed over a set $|X|$ to the topos $Sh(X)$ of sheaves over a topological space induced by the (continuous) identity map $id: |X| \to X$. The modal operator $\Box$ is interpreted by the interior operation $int$ that the comonad $id^{\ast} \circ id_{\ast}$ induces on the Boolean algebra $Sub_{Sets/|X|}(id^{\ast} F) \cong \mathcal{P}(F)$ of subsets of $F$,

it sounds reminiscent of the $\flat$ modality. Did we ever consider using other units/counits of our favourite modalities?

I mean, we noted the similarity between the jet comonad and ordinary necessity as arising from units of modalities, $\Im$ and $\ast$, in Urs’s cohesion - table:

$Jet \coloneqq i^\ast i_\ast \;\colon\; \mathbf{H}_{/X} \to \mathbf{H}_{/X} \,.$and

$\Box_W: \mathbf{H}_{/W} \to \mathbf{H}_{/W} \,.$What could we do with the counit of the comodality $i: \flat(X) \to X$?

$\mathbf{H}_{/\flat (X)} \stackrel{\overset{i^\ast}{\longleftarrow}}{\underset{i_\ast}{\longrightarrow}} \mathbf{H}_{/X} \,.$So we have $i^\ast i_\ast$ again acting on $\mathbf{H}_{/\flat (X)}$, rather like the Awodey-Kishida case. I wonder if any other such (co)monads arising from base change along units and counits of the table and adjunctions give interesting modalities.

]]>have added to modal logic the reference

- Dana Scott,
*Advice on Modal Logic*, in Karel Lambert (ed.)*Philosophical problems in Logic – Some recent developments*, Reidel 1970

and the quote (p. 161)

]]>Here is what I consider one of the biggest mistakes in all of modal logic: concentration on a system with just

onemodal operator.

It does now. There was an http:// missing.

]]>Link to the paper of Goldblatt at modal logic does not work.

]]>Chasing references that David Corfield pointed to elsewhere, I realized that the *Stanford Encyclopedia of Philosophy* has (at least) two entries on modal logic. Earlier I had only seen the one titled *Modal logic* but now I see there is also *Modern Origins of Modal Logic*. The second one is well suited as first reading/motivation for the first one, I find.

So I went and added a pointer to this prominently right in the idea-section of *modal logic*. In the course of this I also ended up editing the Idea-section a little bit more.

Split off first-order modal logic, but no time to do anything substantial.

]]>