Abstract

Street’s 1972 paper A formal theory of Monads defines the 2-category of graded monads over a 2-category k, and the corresponding functor on 2Cat. This provides a setting for the internalization of many properties of monads. This formal treatment of monads makes them a desirable object of study and furthermore an exceedingly useful tool in both functional programming and logic.

Graded monads, i.e. a lax monoidal functor, are a relatively new and (imo) trendy topic that have shown to have many applications in the areas of effect systems and substructural logic. Driven by applications in both categorical logic and functional programming we aim to give a similar formal treatment as Street provided for monads to graded monads.

In this talk we will explore different constructions in 2Cat to define the 2-category of graded monads in a way that is consistent both with the intuitions of functional programmers and the current understanding of graded monads in the categorical setting.