### Context

#### Categorical algebra

internalization and categorical algebra

universal algebra

categorical semantics

#### Computation

intuitionistic mathematics

# Contents

## Idea

Unlike the bind operation of a monad which is of type

$(\forall\alpha) (\forall\beta) \big( m\alpha \to (\alpha\to m\beta) \to m\beta \big)$

a polymonadic bind involves three abstract types:

$(\forall\alpha) (\forall\beta) \big( m_1\alpha\to(\alpha\to m_2\beta)\to m_3\beta \big) \,.$

(Note that, from a category theoretic perspective, it is more natural to change the order of the arguments to match the form of Kleisli extension, so that the operations are of the form

$(\forall\alpha) (\forall\beta) \big( (\alpha\to m_2\beta)\to (m_1\alpha\to m_3\beta) \big) \,.$

.)

## Definition

A polymonad is the data of a collection $\mathcal{M}$ of unary type constructors cointaining an element $\mathrm{Id}$, and a bind set $\Sigma_{\mathcal{M}}$ containing an element $b_{\mathrm{Id},\mathrm{Id},\mathrm{Id}}$ (reverse apply).

It must obey the following polymonad laws:

• functorial law;
• left identity;
• right identity;
• associativiy;
• paired morphisms law;
• composition closure law.

The first four laws are chosen to generalise monads, and the last two are chosen so that if certain binds can be uniquely defined in terms of other ones, then these must be present in $\Sigma$.