Contents

### Context

#### Enriched category theory

enriched category theory

# Contents

## Idea

The notion of enriched monads is that of monads in the context of enriched category theory: For $V$ a base of enrichment, a $V$-enriched monad is a monad internal to the 2-category VCat of $V$-enriched categories.

Generally (except in the base case $V =$ Set) the structure of a $V$-enriched monad on a $V$-enriched category $\mathbf{C}$ is stronger than that of the underlying monad on the underlying Set-category $C$, whence one also speaks of strong monads (a priori a different notion, which however coincides with that of enriched monads under mild conditions, such as when $V$ is closed, see there).

The concept of enriched monads is key for the application of monads in computer science, since a monad coded verbatim in a functional programming language — where function types $X \to Y$ are to be interpreted not as external hom-sets but as internal homs in the ambient closed monoidal category $V$ of data types — is really a $V$-enriched monad (hence typicall a strong monad).

## Definition

Let

• $(V, \otimes, I)$ be a symmetric monoidal category which serves as the base of enrichment,

with $I$ denoting its unit object.

• $\mathbf{C}$ be a $V$-enriched category

with underlying Set-category denoted $C$, and

with hom-objects between any pais of objects $X, Y$ denoted $\mathbf{C}(X,Y) \,\in\, V$.

###### Definition

A $V$-enriched monad on $\mathbf{C}$ is, in Kleisli triple-presentation (eg. McDermott & Uustalu 2022, Def. 5.8):

• for every object $X \,\in\, \mathbf{C}$, an object $T(X) \,\in\,\mathbf{C}$;

• for every object $X \,\in\,\mathbf{C}$, a morphism in $V$ of the form

$ret_X \;\colon\; I \to \mathbf{C}\big(X,T(X)\big)$

• for all pairs of objects $X,Y$ of $mathbf{C}$, a morphism in $V$ of the form

$bind_{X,Y} \;\colon\; \mathbf{C}\big(X,T(Y)\big) \to \mathbf{C}\big(T(X),T(Y)\big)$

(the Kleisli extension or bind-operation)

such that the structural equations on a Kleisli triple

1. $bind(f) \circ ret_X = f$,

2. $bind(ret_X\big) = id$

3. $bind(g) \circ bind(f) = bind\big(bind(g) \circ f\big)$

hold for generalized elements $f$, $g$ of the hom-objects $\mathbf{C}\big(X,\,T(Y)\big)$, $\mathbf{C}\big(Y,\,T(Z)\big)$, which means that the following diagrams commute in $V$ for all objects $X, Y, Z$ of $\mathbf{C}$:

## Properties

### Relation to strong and monoidal monads

###### Proposition

(equivalence between $V$-strength and $V$-enrichment) For

• $V$ a closed monoidal category

• $\mathbf{C}$, $\mathbf{D}$ a pair of $V$-enriched categories

which are also $V$-tensored (=copowered)

then there is a bijection between the structures of

• $V$-strong functors and $V$-enriched functors $\mathbf{C} \to \mathbf{D}$

on the underlying functors,

and for any pair $F$, $G$ of such a bijection between

It follows in particular that there is a bijection between

on such $\mathbf{C}$.

(Ratkovic 2012, §3.2; McDermott & Uustalu 2022, Prop. 5.4, 5.8)

###### Remark

For $V$ a closed monoidal category the further assumptions in Prop. apply to $\mathbf{C} = \mathbf{D} \coloneqq \mathbf{V}$ being the canonical self-enrichment of $V$.

Moreover:

###### Proposition

For $V$ a symmetric monoidal closed category, there is a bijection between the structures of

on underlying monads on $V$.

(Kock 1972, Thm. 3.2, review in GLLN08, §7.3, §A.4, Ratkovic 2012, Prop. 3.3.9)

Hence from combining Prop. with Prop. we get:

###### Proposition

For $V$ a symmetric closed monoidal category with $\mathbf{V}$ denoting its self-enriched category, every symmetric monoidal monad on $V$ gives the structure of a $V$-enriched monad on $\mathbf{V}$.

## Examples

###### Example

In the case in of enrichment by truth values, a monad is a closure operator on a poset.

###### Remark

In the application of monads in computer science, $\mathbf{C} = \mathbf{V}$ is typically the base of enrichment itself, canonically enriched over itself. For classical computing this is typically a cartesian closed category.

Since declaring a monad in a functional programming language means to define it in the internal language of $V$, such monads in computer science are actually enriched, see the discussion there.

For example, if $V$ is the syntactic category of a programming language, then all the definable monads in the language are $V$-enriched.