Coalgebraic-modal extensions of doctrines

The modelling of phenomena is an iterative process; one’s understanding of something and the very scope of interest evolves over time. This poses a challenge to logicians: if you settle on a specific logic to describe an object, you may soon find it inappropriate.

This is notably the case in the study of systems. On one hand, the language itself may need to be expanded if new features and behaviours are to be studied (e.g., add modalities to form new predicates), and on another hand you may wish to change the flavour of system under consideration (therefore changing the logical contexts and the underlying type theory). Often, both procedures are necessary. For example, one may wish to go from having Boolean predicates about machine states to having temporal predicates about streams of states.

This talk will address the following main question: when is one procedure compatible with the other in such a way that our starting logic can be “upgraded" to a modal one on the new type of system? More formally, given a basic hyperdoctrine $P:{𝒞}^{\text{op}}\to 𝒟$, a comonad $F$ on $𝒞$, and a monad $L$ on $𝒟$, we are concerned with determining the lax monad morphisms $F^{\text{op}}\to L$ with underlying $1$-morphism $P$ for which the induced map of Eilenberg-Moore categories is again a hyperdoctrine.

This is best studied by working with double categories instead, as (regular) hyperdoctrines can be equivalently described as certain symmetric monoidal double pseudofunctors $𝕊pan{(𝒞)}^{\text{op}}\to \mathbb{Q}t(𝒟)$ [1], and the flavours of systems themselves can be expressed usefully in double-categorical language [2]. In this light, we will introduce a 2-category $𝒟oct$ of double pseudofunctors between cartesian double categories and consider its Eilenberg-Moore objects. We will discuss when the logical extension scenarios we are interested in correspond to monoidal pseudomonads in $𝒟oct$, so that their Eilenberg-Moore objects provide the desired coalgebraic-modal extensions of the starting logic. If time permits, I will also comment on how this approach relates to traditional coalgebraic modal logic [3].