Dialectica Comonads (Invited Talk)

Dialectica categories are interesting categorical models of Linear Logic which preserve the differences between linear connectives that the logic is supposed to make, unlike some of the most traditional models like coherence spaces. They arise from the categorical modelling of Godel’s Dialectica interpretation and seem to be having a revival: connections between Dialectica constructions and containers, lenses and polynomials have been described recently in the literature. In this note I will recap the basic Dialectica constructions and then go on to describe the less well-known interplay of comonads, coalgebras and comonoids that characterizes the composite functor standing for the "of course!" operator in dialectica categories. This composition of comonads evokes some work on stateful games by Laird and others, also discussed in the setting of Reddy’s system LLMS (Linear Logic Model of State).