In my current project investigating the categorical semantics of attack trees we are using distributive laws to compose comonads that model various structural rules – weakening, contraction, exchange, etc – in linear logic. During the QA section of my talk at Linear logic, mathematics and computer science – see my post on my talk and the workshop for more details – Paul-André Melliès suggested using adjunctions to compose the structural rules instead of distributive laws for the obvious reason that they really compose as opposed to monads/comonads. I told him that I did try to this initially, but was not able to get it working. He was nice enough to talk with me a bit and gave me some hints to how it works which are based on a paper of his.
Instead of just looking up the details in his paper I wanted to see if I could recreate his result with his hints. I often do this for learning purposes. So that’s what I did during my flight back from France. I figured why not make it a blog post. Keep in mind that this result is due to Paul-André, but I had a lot of fun recreating his steps.
I plan to write a follow up post describing how this result can be used to to create various adjoint models of linear logic, but here we show that when we have two comonads on a category with a distributive law, then those comonads in addition to their composition can be decomposed into a composition of adjunctions between their coalgebras.
Suppose is a comonad on a category . Then it is well known that it can be decomposed into the following adjunction:
Now suppose we have the following adjunctions:
Then they can be composed into the adjunction:
Keep in mind that this gives rise to a comonad .
We are going to use these two facts to compose comonads using adjunctions. Suppose we have the comonads and both on a category with a distributive law – distributive laws for comonads are defined to be the opposite of the distributive laws for monads – . Thus, making a comonad.
Then we can decompose into a an adjunction:
Here we know that , but we also know something about . We can extend it to a comonad on .
First, we define the functor to send objects to , where , and to send morphisms to the morphism . We must show that is a coalgebra morphism, but the following diagram commutes:
The top diagram commutes because is a coalgebra morphism and the bottom diagram commutes by naturality of . Since the morphism part of is defined using the functor we know will respect composition and identities.
We now must show that is a comonad. The natural transformation has components . We must show that is a coalgebra morphism between and , but this follows from the following diagram:
The top diagram commutes by naturality of and the bottom diagram commutes by the conditions of the distributive law. Naturality for easily follows from the fact that it is defined to be .
The natural transformation has components . Just as above we must show that is a coalgebra morphism between and , but this follows from the following diagram:
The top diagram commutes by naturality of and the bottom diagram commutes by the conditions of the distributive law.
It is now easy to see that and make a comonad on , because the conditions of a comonad will be inherited from the fact that and define a comonad on .
At this point we have arrived at the following situation:
Since we have a comonad we can form the following adjunction:
The functor is the free functor, and is the forgetful functor. Thus, we can think of as the world with all the structure of extended with all of the structure brings and all the structure brings. That is, is the algebras of .
We can see that the previous two adjunctions compose:
Thus, we have a comonad . Chasing an object through this comonad yields the following:
Therefore, the above adjunction gives back the composition .
This result only works because we have a distributive law, but the distributive law is only used in the the definition of the structural map of the coalgebras. This result reveals a means that will allow us to abandon distributive laws in favor of adjunctions in the spirit of Benton’s LNL models, however, doing so comes with some different difficulties. Stay tuned!