Coherence for Monoidal Monads and Comonads

TL;DR

This paper establishes coherence results for monoidal monads and comonads in various monoidal categories, including symmetric, with finite products or coproducts, relevant to logic and category theory.

Contribution

It provides the first coherence proofs for monoidal monads and comonads in non-symmetric and structured monoidal categories, extending previous results.

Findings

Coherence results proved for monoidal monads and comonads without symmetry.

Results include categories with finite products or coproducts.

Application to modeling identity of deductions in modal logic S4.

Abstract

The goal of this paper is to prove coherence results with respect to relational graphs for monoidal monads and comonads, i.e. monads and comonads in a monoidal category such that the endofunctor of the monad or comonad is a monoidal functor (this means that it preserves the monoidal structure up to a natural transformation that need not be an isomorphism). These results are proved first in the absence of symmetry in the monoidal structure, and then with this symmetry. The monoidal structure is also allowed to be given with finite products or finite coproducts. Monoidal comonads with finite products axiomatize a plausible notion of identity of deductions in a fragment of the modal logic S4.