added pointer to:
also touched and slightly expanded the last paragraphs in the Idea section (the ones on models, starting here)
]]>added (here) a screenshot of the first page from Lemmon & Scott (1977)
(the most satisfactory monograph account I have seen, by a margin)
]]>added pointer to English translation of Becker’s old text:
added pointer to:
I ended up making a fair bit of adjustments to the wording in the Idea-section (here).
Generally, i find that our entries on modal logics leave much room for improvement, but I’ll leave it at this for the moment.
]]>I have added publication data and hyperlinks to these previously existing bibitems:
Patrick Blackburn, Maarten de Rijke, Yde Venema, Modal Logic, Cambridge Tracts in Theoretical Computer Science 53 (2001) [doi:10.1017/CBO9781107050884]
Patrick Blackburn, Johan van Benthem, Frank Wolter (eds.), The Handbook of Modal Logic, Elsevier Amsterdam (2007) [book webpage, publisher page]
and then I added this further textbook pointer:
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 -ionad is given by an -groupoid, , and a finite -limit preserving comonad, ?
Then we could have:
The -category of opens of an -ionad is the category of -coalgebras.
This would be an -topos.
Presumably there would be no reason to stick to as the base topos.
]]>Well I’d still like to know the ’meanings’ of the comonad, , and monad, , on . 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 ? 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 -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 of -indexed sets is the slice for any object in the -topos . Now you are asking for finite -limit preserving comonads on such slices. You get one such by base change along any morphism out of .
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 :
]]>Oh, I see. I though we were just working out , 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 , but all seems to point to the other way,
An ionad is a set together with a finite limit-preserving comonad on the category
chimes with
In the original expression, we consider the geometric morphism from the topos of sets indexed over a set to the topos of sheaves over a topological space induced by the (continuous) identity map . The modal operator is interpreted by the interior operation that the comonad induces on the Boolean algebra of subsets of .
[EDIT: These are, of course, using the right adjoint to , but still the interest is starting out from the discrete side.]
]]>then why do you have in both corners of that square?
I thought that’s what you were suggesting to look at. The operation in your #67 above is the operation that sends any to the pullback
I thought your point in #68 had been to observe that then the -operation becomes sort of a special case of the possibility-like modality , via
]]>Well I just meant that there’s some process which takes us from some bundle to some other bundle . Wouldn’t we call that a ’flattening’.
Anyway, I was with you so far, but then why do you have in both corners of that square?
]]>You mean: to pick trivial underlying -groupoid -bundles.
Consider first pointed connected coefficients, hence of the form . Then the homotopy pullback
has the following interpretation: its generalized elements consist of
a flat connection with underlying bundle ;
an equivalence .
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 to any , then 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 . You may choose to pick all of these connected components and all of the transformations between them, and then consider the homotopy pullback in
Clearly this has some relation to . I suppose if one picks one representative points in each connected component of and hence pulls back along some , then one obtains the “right” definition of for groupoid-principal connections.
Right now I am not sure what it means to retain all the higher homotopy information of the in the bottom left corner.
But I agree that this looks like a sensibel perspective from which to view in generality.
]]>The must be a universal way to flatten a connection on an -bundle.
]]>So 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 -construction.
]]>It would probably be better for the soul to work this out myself.
So is a forgetting of the flatness of a connection.
Then 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, , 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.
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 ?
Again four (co)monads from the composites. Can we name any of them?
]]>