This is quite a nice way to picture things: A possibility algebra/necessity coalgebra, $A \in \mathbf{H}/W$, requires a map, $\sum_W A \to \prod_W A$. Given a point in the total space, we need a section through that point.

]]>According to Todd here, when a monad is left adjoint to a comonad, then the algebras of the former are equivalent to the coalgebras of the latter. So the jet coalgebras in #6 are the same as ’infinitesimal neighborhood’ algebras, necessity coalgebras (#3) as possibility algebras, etc., right?

]]>Yes, dependent product along a general morphism $X \longrightarrow Y$ produces “spaces-of-sections-pointwise-over-$Y$”. And, yes, since the de Rham stack projectiuon $\Sigma \to \Im \Sigma$ is a 1-epi, jet coalgebras over $\Sigma$ are equivalently objects in the slice over $\Im \Sigma$. (In algebraic geometry these are the D-modules).

]]>Looking good.

So the PDE case should go through in a similar way? Perhaps in explicit terms of SDG infinitesimals. Instead of the

$\prod_W (Q) = \Gamma_W(Q)$we need something like sections of the infinitesimal neighborhood of a point. Then base change that back. I guess that requires the language of jets.

And then the coalgebras are the ones that come from base change of bundles on $\Im(X)$? That seems to be multiplying points by infinitesimal neighborhoods.

]]>and then I have edited the text a little, trying to polish a bit more, please check if you agree.

]]>Thanks David. I have added to the section statements that are at least sufficient to conclude that $EM(\Box_W) \simeq \mathbf{H}_{/\ast}$, namely that $\mathbf{H}$ is a topos and $W$ is inhabited.

]]>I added an example concerning modalities. We should also be able to tell a similar story for the jet comonad.

I should think the trio – monadic functor, comonadic functor, monadicity theorem – could be integrated better.

]]>Added some examples to comonadic functor. Prompted by this MO discussion (does anyone know how such monadic-comonadic iterations are referred to in the literature?).

]]>