# Central Submonads and Notions of Computation:
## Soundness, Completeness and Internal Languages

Titouan Carette, Louis Lemonnier, Vladimir Zamdzhiev

► To cite this version:

Titouan Carette, Louis Lemonnier, Vladimir Zamdzhiev. Central Submonads and Notions of Computation: Soundness, Completeness and Internal Languages. 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jun 2023, Boston (MA), United States. 10.1109/LICS56636.2023.10175687. hal-03662565v4

HAL Id: hal-03662565

https://hal.science/hal-03662565v4

Submitted on 10 Oct 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>
Central Submonads and Notions of Computation:
Soundness, Completeness and Internal Languages

Titouan Carette*, Louis Lemonnier† and Vladimir Zamdzhiev†

* Centre for Quantum Computer Science, Faculty of Computing, University of Latvia, Raiņa 19, Riga, Latvia, LV-1586

† Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, Laboratoire Méthodes Formelles, 91190, Gif-sur-Yvette, France

Abstract

Monads in category theory are algebraic structures that can be used to model computational effects in programming languages. We show how the notion of “centre”, and more generally “centrality”, i.e., the property for an effect to commute with all other effects, may be formulated for strong monads acting on symmetric monoidal categories. We identify three equivalent conditions which characterise the existence of the centre of a strong monad (some of which relate it to the premonoidal centre of Power and Robinson) and we show that every strong monad on many well-known naturally occurring categories does admit a centre, thereby showing that this new notion is ubiquitous. More generally, we study *central submonads*, which are necessarily commutative, just like the centre of a strong monad. We provide a computational interpretation by formulating equational theories of lambda calculi equipped with central submonads, we describe categorical models for these theories and prove soundness, completeness and internal language results for our semantics.

# I. INTRODUCTION

The importance of monads in programming semantics has been demonstrated in seminal work by Moggi [1], [2]. The main idea is that monads allow us to introduce computational effects (e.g., state, input/output, recursion, probability, continuations) into pure type systems in a controlled way. The mathematical development surrounding monads has been very successful and it directly influenced modern programming language design through the introduction of monads as a programming abstraction into languages such as Haskell, Scala and others (see [3]). Inspired by this, we follow in the same spirit: we start with a mathematical question about monads, we provide the answer to it and we present a computational interpretation. The mathematical question that we ask is simple and it is inspired by the theory of monoids and groups:

> *Is there a suitable notion of "centre" that may be formulated for monads and what is a "central" submonad?*

We show that, just as every monoid $M$ (on Set) has a centre, which is a commutative submonoid of $M$, so does every (canonically strong) monad $\mathcal{T}$ on Set and the centre of $\mathcal{T}$ is a commutative submonad of $\mathcal{T}$ (§IV-A). A central<fnref n="1" /> submonad of $\mathcal{T}$ is simply a submonad of the centre of $\mathcal{T}$ (Definition 36) and the analogy to the case of monoids and groups is completely preserved. Note that our construction has nothing to do with the folklore characterisation of monads as monoid objects in a functor category, wherein the notion of commutativity is unclear. The relevant analogy with monoids in Set is fully explained in Example 19. Generalising away from the category Set, the answer is a little bit more complicated: not every monoid object $M$ on a symmetric monoidal category $C$ has a centre, and neither does every strong monad on $C$ (§IV-C). However, we show that under some reasonable assumptions, the centre does exist (Theorem 18) and we have not found any naturally occurring monads in the literature that are not centralisable (i.e., monads other than the artificially constructed one we used as a counter-example). Furthermore, we show that for many categories of interest, all strong monads on them are centralisable (§V-A) and we demonstrate that the notion of centre is ubiquitous. The centre of a strong monad satisfies interesting universal properties (Theorem 18) which may be equivalently formulated in terms of our novel notion of *central cone* or via the *premonoidal centre* of Power and Robinson [4]. The notion of a central submonad is more general and it may be defined without using the centre. When the centre exists, a central submonad may be equivalently defined as a strong submonad of the centre (Theorem 35).

The computational significance of these ideas is easy to understand: given an effect, modelled by a strong monad, such that perhaps not every pair of effectful operations commute (i.e., the order of monadic sequencing matters), identify only those effectful operations which do commute with any other possible effectful operation. The effectful operations that satisfy this property are called *central*. When the monad is centralisable, the collection of all central operations determine the centre of the monad (which is a commutative submonad). Any collection of central operations that may be organised into a strong submonad determines a central submonad (which also is commutative). We argue that central submonads have greater computational significance compared to the centre of a strong monad (§VII-B) for two main reasons: (1) central submonads are strictly more general; (2) central submonads have a simpler and considerably more practical axiomatisation via an equational theory, whereas the centre of a monad requires an axiomatisation using a more complicated logical theory. We cement our categorical semantics by proving soundness, completeness and internal language results<fnref n="2" /> (§VII).

<footnote n="1">¹Given a group *G*, a *central subgroup* is a subgroup of the centre of *G*, equivalently, a subgroup whose elements commute with every element of *G*.</footnote>

<footnote n="2">²See [5] for a convincing argument why internal language results are important and why soundness and completeness *alone* might not be sufficient.</footnote>
## II. RELATED WORK

A notion of commutants for enriched algebraic theories has been defined in [6] from which the author derives a notion of centre of an enriched algebraic theory. In the case of enriched monads, in other words, strong monads arising from enriched algebraic theories, their notion of commutant extends to monad morphisms. While not explicitly stated in the paper, applying the commutant construction on the identity monad morphism from a monad to itself provides a notion of centre of a monad that appears to coincide with ours. However, enriched algebraic theories correspond to *J*-ary *V*-enriched monads (See [6] for a definition of *J*-ary monads w.r.t. a system of arities *J*) on a symmetric monoidal closed category *V* (equivalently *J*-ary strong monads on *V*). In our paper, we show that monoidal closure of *V* is not necessary to define the centre and neither is the *J*-ary assumption on the monad. Other related work [7] considers a very general notion of commutativity in terms of certain kinds of duoidal categories. As a special case of their treatment, the authors are able to recover the commutativity of bistrong monads and with some additional effort (not outlined in the paper), it is possible to construct the centre of a bistrong monad acting on a monoidal *biclosed* category. Our construction of the centre appears to coincide with theirs in the special case of strong monads defined on symmetric monoidal *closed* categories, but as discussed above, our method does not require any kind of closure of the category. Therefore, compared to both works [7], [6], as far as symmetric monoidal (not necessarily closed) categories are concerned, our methods can be used to construct the centre for a larger class of strong monads and we establish our main results, together with our universal characterisation of the centre, under these assumptions. Furthermore, we also place a heavy emphasis on *central* submonads in our paper and these kinds of monads are not discussed in either of these works and neither is there a computational interpretation (which is our main result in §VII).

Another related work is [4], which introduces premonoidal categories. We have established important links between our development and the premonoidal centre (Theorem 18). While premonoidal categories have been influential in our understanding of effectful computation, it was less clear (to us) how to formulate an appropriate computational interpretation of the premonoidal centre for higher-order languages. Our paper shows that under some mild assumptions (which are easily satisfied see §V), the premonoidal centre of the Kleisli category of a strong monad induces an adjunction into the base category (Theorem 18) and this allows us to formulate a suitable computational interpretation by using monads, which are already well-understood [2], [1] and well-integrated into many programming languages [3].

Staton and Levy introduce the novel notion of *premulticategories* [8] in order to axiomatise impure/effectful computation in programming languages. The notion of centrality plays an important role in the development of the theory there as well. However, they do not focus, as we do, on providing suitable programming abstractions that identify both central and non-central computations (e.g., by separating them into different types like us) and from what we can tell from our reading, there are no universal properties stated for the collection of central morphisms. Also, our results provide a computational interpretation in terms of monads, which are standard and well-understood, so it is easier to incorporate them into existing languages.

Central morphisms in the context of computational effects have been studied in [9], among other sorts of *varieties* of morphisms: truncable, copyable, and discardable. The author links their notion of central morphisms with the ones from the premonoidal centre in Power and Robinson [4], and also proves under some conditions that those varieties form a subcategory with similar properties to the original category. However, they do not mention that a central submonad or a centre can be constructed out of those central morphisms. More generally, the fact that monads could be derived from those varieties is not studied at all in that paper.

The work in [9] has an impact in [10], where a Galois connection is established between call-by-value and call-by-name. In that paper, the order in which operations are done matters, and central computations are mentioned. Again, the central computations are not linked to submonads in there.

## III. BACKGROUND

We start by introducing some background on strong and commutative monads and their premonoidal structure.

### A. *Strong and Commutative Monads*

We begin by recalling the definition of a *strong monad*, which is our main object of study. These monads are more computationally relevant, compared to non-strong ones, because they allow us to work with terms that have several free variables (see [2] for more details). The additional structure, called the (*left* ) *strength*, ensures the monad interacts appropriately with the monoidal structure of the base category.

**Definition 1 (Strong Monk)**. A strong monad over a monoidal category (*C*, ⊗, *I*, α, λ, ρ) is an endofunctor T: C → C equipped with three natural transformations η_X: X → TX, μ_X: T^2 X → TX and τ_{X,Y}: X ⊗ TY → T(X ⊗ Y), called the unit, the multiplication and the (*left* ) *strength*, such that usual coherence conditions apply.

We now recall the definition of a *commutative monad*, which is of central importance in this paper. Compared to a strong monad, a commutative monad enjoys even stronger coherence properties with respect to the monoidal structure of the base category (see also §III-B).
This categorical data satisfies the axioms and coherence properties of premonoidal categories as explained in [4], but which we omit here because it is not essential for the development of our results. What is important is to note that in a premonoidal category, $f \otimes_l X'$ and $X \otimes_r g$ do not always commute. This leads us to the following definition, which plays a crucial role in the theory of premonoidal categories and has important links to our development.

**Definition 8** (Premonoidal Centre [4]). Given a strong monad $(\mathcal{T}, \eta, \mu, \tau)$ on a symmetric monoidal category $(\mathbf{C}, I, \otimes)$, we say that a morphism $f: X \to Y$ in $\mathbf{C}_\mathcal{T}$ is central if for any morphism $f': X' \to Y'$ in $\mathbf{C}_\mathcal{T}$, the diagram

<figure><img src="image_2.png" /></figure>

commutes in $\mathbf{C}_\mathcal{T}$. The premonoidal centre of $\mathbf{C}_\mathcal{T}$ is the subcategory $\mathcal{Z}(\mathbf{C}_\mathcal{T})$ which has the same objects as those of $\mathbf{C}_\mathcal{T}$ and whose morphisms are the central morphisms of $\mathbf{C}_\mathcal{T}$.

In [4], the authors prove that $\mathcal{Z}(\mathbf{C}_\mathcal{T})$, is a symmetric monoidal subcategory of $\mathbf{C}_\mathcal{T}$. In particular, this means that Kleisli composition and the tensor functors $(- \otimes_l X)$ and $(X \otimes_r -)$ preserve central morphisms. However, it does not necessarily hold that the subcategory $\mathcal{Z}(\mathbf{C}_\mathcal{T})$ is the Kleisli category for a monad over $\mathbf{C}$. Nevertheless, in this situation, the left adjoint of the Kleisli adjunction $\mathcal{J}: \mathbf{C} \to \mathbf{C}_\mathcal{T}$ always corestricts to $\mathcal{Z}(\mathbf{C}_\mathcal{T})$. We write $\hat{\mathcal{J}}: \mathbf{C} \to \mathcal{Z}(\mathbf{C}_\mathcal{T})$ to indicate this corestriction (which need not be a left adjoint).

**Remark 9.** In [4], the subcategory $\mathcal{Z}(\mathbf{C}_\mathcal{T})$ is called the centre of $\mathbf{C}_\mathcal{T}$. However, we refer to it as the premonoidal centre of a premonoidal category to avoid confusion with the new notion of the centre of a monad that we introduce next. In the sequel, we show that the two notions are very strongly related to each other (Theorem 18).

# IV. THE CENTRE OF A STRONG MONAD

We begin by showing that any (necessarily strong) monad on Set has a centre (§IV-A) and we later show how to define the centre of a strong monad on an arbitrary symmetric monoidal category (§IV-B). Unlike the former, the latter submonad does not always exist, but it does exist under mild assumptions and we show that the notion is ubiquitous.

## A. The Centre of a Monad on Set

The results we present next are a special case of our more general development from §IV-B, but we choose to devote special attention to monads on Set for illustrative purposes.

**Definition 10** (Centre). Given a strong monad $(\mathcal{T}, \eta, \mu, \tau)$ on Set with right strength $\tau'$, we say that the centre of $\mathcal{T}$ at $X$, written $\mathcal{Z}X$, is the set

$$ \mathcal{Z}X \stackrel{\text{def}}{=} \{t \in \mathcal{T}X \mid \forall Y \in \text{Ob}(\text{Set}). \forall s \in \mathcal{T}Y. \\ \qquad \mu(\mathcal{T}\tau'(\tau(t, s))) = \mu(\mathcal{T}\tau(\tau'(t, s)))\}. $$

We write $\iota_X: \mathcal{Z}X \subseteq \mathcal{T}X$ for the indicated subset inclusion.

In other words, the centre of $\mathcal{T}$ at $X$ is the subset of $\mathcal{T}X$ which contains all monadic elements for which (1) holds when the set $X$ is fixed and the set $Y$ ranges over all sets.

**Remark 11.** In the above definition and throughout the paper, we assume we are working with von Neumann-Bernays-Gödel (NBG) set theory, a conservative extension of ZFC set theory that allows us to introduce classes of sets. We do so in order to simplify notation when working with locally small categories. However, the above definition (and all others in this paper) may also be stated in ZFC set theory, because quantification over all sets is also admissible within ZFC.

Notice that $\mathcal{Z}X \supseteq \eta_X(X)$, i.e., the centre of $\mathcal{T}$ at $X$ always contains all monadic elements which are in the image of the monadic unit. This follows easily from the axioms of strong monads. In fact, the assignment $\mathcal{Z}(-)$ extends to a commutative submonad of $\mathcal{T}$. In particular, the assignment $\mathcal{Z}(-)$ extends to a functor $\mathcal{Z}: \text{Set} \to \text{Set}$ when we define $\mathcal{Z}f \stackrel{\text{def}}{=} \mathcal{T}f|_{\mathcal{Z}X}: \mathcal{Z}X \to \mathcal{Z}Y$, for any function $f: X \to Y$, where $\mathcal{T}f|_{\mathcal{Z}X}$ indicates the restriction of $\mathcal{T}f: \mathcal{T}X \to \mathcal{T}Y$ to the subset $\mathcal{Z}X$. Moreover, for any two sets $X$ and $Y$, the monadic unit $\eta_X: X \to \mathcal{T}X$, the monadic multiplication $\mu_X: \mathcal{T}^2X \to \mathcal{T}X$, and the monadic strength $\tau_{X,Y}: X \times \mathcal{T}Y \to \mathcal{T}(X \times Y)$ (co)restrict respectively to functions $\eta_X^z: X \to \mathcal{Z}X$,
$\mu_X^Z : \mathcal{Z}^2 X \to \mathcal{Z} X$ and $\tau_{X,Y}^Z : X \times \mathcal{Z} Y \to \mathcal{Z}(X \times Y)$. That the above four classes of functions (co)restrict as indicated follows from our more general treatment presented in the next section. It then follows, as a special case of Theorem 18, that the data we just described constitutes a commutative submonad of $\mathcal{T}$.

**Theorem 12.** The assignment $\mathcal{Z}(-)$ can be extended to a commutative submonad $(\mathcal{Z}, \eta^Z, \mu^Z, \tau^Z)$ of $\mathcal{T}$ with the inclusions $\iota_X : \mathcal{Z}X \subseteq \mathcal{T}X$ being the submonad morphism. Furthermore, there is a canonical isomorphism of categories $\mathrm{Set}_\mathcal{Z} \cong \mathcal{Z}(\mathrm{Set}_\mathcal{T})^3$.

The final statement of Theorem 12 shows that the Kleisli category of $\mathcal{Z}$ is canonically isomorphic to the premonoidal centre of the Kleisli category of $\mathcal{T}$. Because of this, we are justified in saying that $\mathcal{Z}$ is not just a commutative submonad of $\mathcal{T}$, but rather it is the centre of $\mathcal{T}$, which is necessarily commutative (just like the centre of a monoid is a commutative submonoid). In §V-B we provide concrete examples of monads on $\mathrm{Set}$ and their centres and we see that the construction of the centre aligns nicely with our intuition.

## B. The General Construction of the Centre

Throughout the remainder of the section, we assume we are given a symmetric monoidal category $(\mathbf{C}, \otimes, I, \alpha, \lambda, \rho, \gamma)$ and a strong monad $(\mathcal{T}, \eta, \mu, \tau)$ on it with right strength $\tau'$.

In Set, the centre is defined pointwise through subsets of $\mathcal{T}X$ which only contain elements that satisfy the coherence condition for a commutative monad. However, $\mathbf{C}$ is an arbitrary symmetric monoidal category, so we cannot easily form subobjects in the required way. This leads us to the definition of a central cone which allows us to overcome this problem.

**Definition 13 (Central Cone).** Let $X$ be an object of $\mathbf{C}$. A central cone of $\mathcal{T}$ at $X$ is given by a pair $(Z, \iota)$ of an object $Z$ and a morphism $\iota : Z \to \mathcal{T}X$, such that for any object $Y$, the diagram

<figure><img src="image_3.png" /></figure>

commutes. If $(Z, \iota)$ and $(Z', \iota')$ are two central cones of $\mathcal{T}$ at $X$, then a morphism of central cones $\varphi : (Z', \iota') \to (Z, \iota)$ is a morphism $\varphi : Z' \to Z$, such that $\iota \circ \varphi = \iota'$. Thus central cones of $\mathcal{T}$ at $X$ form a category. A terminal central cone of $\mathcal{T}$ at $X$ is a central cone $(Z, \iota)$ for $\mathcal{T}$ at $X$, such that for any central cone $(Z', \iota')$ of $\mathcal{T}$ at $X$, there exists a unique morphism of central cones $\varphi : (Z', \iota') \to (Z, \iota)$. In other words, it is the terminal object in the category of central cones of $\mathcal{T}$ at $X$.

In particular, Definition 10 gives a terminal central cone for the special case of monads on $\mathrm{Set}$. The names “central morphism” (in the premonoidal sense, see §III) and “central cone” (above) also hint that there should be a relationship between them. In fact, the two notions are equivalent.

**Proposition 14.** Let $f : X \to \mathcal{T}Y$ be a morphism in $\mathbf{C}$. The pair $(X, f)$ is a central cone of $\mathcal{T}$ at $Y$ iff $f$ is central in $\mathbf{C}_\mathcal{T}$ in the premonoidal sense (Definition 8).

From now on, we rely heavily on the fact that central cones and central morphisms are equivalent notions, and we use Proposition 14 implicitly in the sequel. On the other hand, terminal central cones are crucial for our development, but it is unclear how to introduce a similar notion of “terminal central morphism” that is useful. For this reason, we prefer to work with (terminal) central cones in this paper.

It is easy to see that if a terminal central cone for $\mathcal{T}$ at $X$ exists, then it is unique up to a unique isomorphism of central cones. Also, one can easily prove that if $(Z, \iota)$ is a terminal central cone, then $\iota$ is a monomorphism. The main definition of this subsection follows next and gives the foundation for constructing the centre of a strong monad.

**Definition 15 (Centralisable Monad).** We say that the monad $\mathcal{T}$ is centralisable if, for any object $X$, a terminal central cone of $\mathcal{T}$ at $X$ exists. In this situation, we write $(\mathcal{Z}X, \iota_X)$ for the terminal central cone of $\mathcal{T}$ at $X$.

<footnote n="3">³Theorem 18 states precisely in what sense this isomorphism is canonical.</footnote>
In fact, for a centralisable monad $\mathcal{T}$, its terminal central cones induce a commutative submonad $\mathcal{Z}$ of $\mathcal{T}$, as the next theorem shows, and its proof reveals constructively how the monad structure arises from them.

**Theorem 16.** If the monad $\mathcal{T}$ is centralisable, then the assignment $\mathcal{Z}(-)$ extends to a commutative monad $(\mathcal{Z}, \eta^{\mathcal{Z}}, \mu^{\mathcal{Z}}, \tau^{\mathcal{Z}})$ on $\mathcal{C}$. Moreover, $\mathcal{Z}$ is a commutative submonad of $\mathcal{T}$ and the morphisms $\iota_X : \mathcal{Z}X \to \mathcal{T}X$ constitute a monomorphism of strong monads $\iota : \mathcal{Z} \to \mathcal{T}$.

*Proof.* In Appendix §B.

<figure><img src="image_4.png" /></figure>

This theorem shows that centralisable monads always induce a canonical commutative submonad. Next, we justify why this submonad should be seen as the centre of $\mathcal{T}$. Note that since $\mathcal{Z}$ is a submonad of $\mathcal{T}$, we know that $C_{\mathcal{Z}}$ canonically embeds into $C_{\mathcal{T}}$ (see Proposition 7). The next theorem shows that this embedding factors through the premonoidal centre of $C_{\mathcal{T}}$, and moreover, the two categories are isomorphic.

**Theorem 17.** In the situation of Theorem 16, the canonical embedding functor $\mathcal{I} : C_{\mathcal{Z}} \to C_{\mathcal{T}}$ corestricts to an isomorphism of categories $C_{\mathcal{Z}} \cong \mathcal{Z}(C_{\mathcal{T}})$.

*Proof.* In Appendix §C.

<figure><img src="image_5.png" /></figure>

It should now be clear that Theorem 16 and Theorem 17 show that we are justified in naming the submonad $\mathcal{Z}$ as the centre of $\mathcal{T}$. The existence of terminal central cones is not only sufficient to construct the centre (as we just showed), but it also is necessary and we show this next. Furthermore, we provide another equivalent characterisation in terms of the premonoidal structure of the monad.

**Theorem 18 (Centre).** Let $\mathcal{C}$ be a symmetric monoidal category and $\mathcal{T}$ a strong monad on it. The following are equivalent:

1) For any object $X$ of $\mathcal{C}$, $\mathcal{T}$ admits a terminal central cone at $X$;

2) There exists a commutative submonad $\mathcal{Z}$ of $\mathcal{T}$ (which we call the centre of $\mathcal{T}$) such that the canonical embedding functor $\mathcal{I} : C_{\mathcal{Z}} \to C_{\mathcal{T}}$ corestricts to an isomorphism of categories $C_{\mathcal{Z}} \cong \mathcal{Z}(C_{\mathcal{T}})$;

3) The corestriction of the Kleisli left adjoint $\mathcal{J} : \mathcal{C} \to C_{\mathcal{T}}$ to the premonoidal centre $\mathcal{\hat{J}} : \mathcal{C} \to \mathcal{Z}(C_{\mathcal{T}})$ also is a left adjoint.

*Proof.* In Appendix §D.

<figure><img src="image_6.png" /></figure>

This theorem shows that Definition 15 may be stated by choosing any one of the above equivalent criteria. We note that the first condition is the easiest to verify in practice. The second one is the most useful for providing a computational interpretation, as we do in the sequel. The third condition provides an important link to premonoidal categories.

**Example 19.** Given a monoid $(M, e, m)$, consider the free monad induced by $M$, also known as the *writer monad*, which we write as $\mathcal{T} = (- \times M): \mathcal{Set} \to \mathcal{Set}$. The centre $\mathcal{Z}$ of $\mathcal{T}$ is given by the commutative monad $(- \times \mathcal{Z}(M)): \mathcal{Set} \to \mathcal{Set}$, where $\mathcal{Z}(M)$ is the centre of the monoid $M$ and where the monad data is given by the (co)restrictions of the monad data of $\mathcal{T}$. Note that $\mathcal{T}$ is a commutative monad iff $M$ is a commutative monoid. See also Example 20.

### C. A Non-centralisable Monad

In *Set*, the terminal central cones used to define the centre are defined by taking appropriate subsets. One may wonder what happens if not every subset of a given set is an object of the category. The following example describes such a situation, which gives rise to a non-centralisable strong monad.

**Example 20.** Consider the Dihedral group $D_4$, which has 8 elements. Its centre $\mathcal{Z}(D_4)$ is non-trivial and has 2 elements. Let $\mathcal{C}$ be the full subcategory of *Set* with objects that are finite products of the set $D_4$ with itself. This category has a cartesian structure, and the terminal object is the singleton set (which is the empty product). Notice that every object in this category has a cardinality that is a power of 8. Therefore the cardinality of every homset of $\mathcal{C}$ is a power of 8. Since $\mathcal{C}$ has a cartesian structure and since $D_4$ is a monoid, we can consider the writer monad $\mathcal{M} \stackrel{\text{def}}{=} (- \times D_4) : \mathcal{C} \to \mathcal{C}$ induced by $D_4$, which can be defined in the same way as in Example 19. It follows that $\mathcal{M}$ is a strong monad on $\mathcal{C}$. However, it is easy to show that this monad is not centralisable. Assume (for contradiction) that there is a monad $\mathcal{Z} : \mathcal{C} \to \mathcal{C}$ such that $C_{\mathcal{Z}} \cong \mathcal{Z}(C_{\mathcal{M}})$ (see Theorem 18). Next, observe that the homset $\mathcal{Z}(C_{\mathcal{M}})[1, 1]$ has the same cardinality as the centre of the monoid $D_4$, i.e., its cardinality is 2. However, $C_{\mathcal{Z}}$ cannot have such a homset since $C_{\mathcal{Z}}[X, Y] = C[X, \mathcal{Z}Y]$ which must have cardinality a power of 8. Therefore there exists no such monad $\mathcal{Z}$ and $\mathcal{M}$ is not centralisable.

Besides this example and any further attempts at constructing non-centralisable monads for this sole purpose, we do not know of any other strong monad in the literature that is not centralisable. In the next section, we present many examples of centralisable monads and classes of centralisable monads which show that our results are widely applicable.
# V. EXAMPLES OF CENTRES OF STRONG MONADS

In this section, we show how we can make use of the mathematical results we already established in order to reason about the centres of monads of interest.

## A. Categories whose Strong Monads are Centralisable

We saw earlier that every (strong) monad on **Set** is centralisable. In fact, this is also true for many other naturally occurring categories. For example, in many categories of interest, the objects of the category have a suitable notion of subobject (e.g., subsets in **Set**, subspaces in **Vect**) and the centre can be constructed in a similar way to the one in **Set**.

**Example 21.** Let **DCPO** be the category whose objects are directed-complete partial orders and whose morphisms are Scott-continuous maps between them. Every strong monad on **DCPO** with respect to its cartesian structure is centralisable. The easiest way to see this is to use Theorem 18 (1). Writing $\mathcal{T} : \mathbf{DCPO} \to \mathbf{DCPO}$ for an arbitrary strong monad on **DCPO**, the terminal central cone of $\mathcal{T}$ at $X$ is given by the subdcpo $\mathcal{Z}X \subseteq \mathcal{T}X$ which has the underlying set $\mathcal{Z}X \stackrel{\text{def}}{=} \{t \in \mathcal{T}X \mid \forall Y \in \text{Ob}(\mathbf{DCPO}).\forall s \in \mathcal{T}Y. \mu(\mathcal{T}\tau'(\tau(t,s))) = \mu(\mathcal{T}\tau(\tau'(t,s)))\}$. That $\mathcal{Z}X$ (with the inherited order) is a subdcpo of $\mathcal{T}X$ follows easily by using the fact that $\mu, \tau, \tau'$ and $\mathcal{T}$ are Scott-continuous. Therefore, the construction is fully analogous to the one in **Set**.

**Example 22.** Let **Top** be the category whose objects are topological spaces, and whose morphisms are continuous maps between them. Every strong monad on **Top** with respect to its cartesian structure is centralisable. Using Theorem 18 (1) and writing $\mathcal{T} : \mathbf{Top} \to \mathbf{Top}$ for an arbitrary strong monad on **Top**, the terminal central cone of $\mathcal{T}$ at $X$ is given by the space $\mathcal{Z}X \subseteq \mathcal{T}X$ which has the underlying set $\mathcal{Z}X \stackrel{\text{def}}{=} \{t \in \mathcal{T}X \mid \forall Y \in \text{Ob}(\mathbf{Top}).\forall s \in \mathcal{T}Y. \mu(\mathcal{T}\tau'(\tau(t,s))) = \mu(\mathcal{T}\tau(\tau'(t,s)))\}$ and whose topology is the subspace topology inherited from $\mathcal{T}X$.

**Example 23.** Every strong monad on the category **Meas** (whose objects are measurable spaces and the morphisms are measurable maps between them) is centralisable. The construction is fully analogous to the previous example, but instead of the subspace topology, we equip the underlying set with the subspace $\sigma$-algebra inherited from $\mathcal{T}X$ (which is the smallest $\sigma$-algebra that makes the subset inclusion map measurable).

**Example 24.** Let **Vect** be the category whose objects are vector spaces, and whose morphisms are linear maps between them. Every strong monad on **Vect** with respect to the usual symmetric monoidal structure is centralisable. One simply defines the subset $\mathcal{Z}X$ as in the other examples and shows that this is a linear subspace of $\mathcal{T}X$. That this is the terminal central cone is then obvious.

The above categories, together with the category **Set**, are not meant to provide an exhaustive list of categories for which all strong monads are centralisable. Indeed, there are many more categories for which this is true. The purpose of these examples is to illustrate how we may use Theorem 18 (1) to construct the centre of a strong monad. Changing perspective, the proof of the next proposition uses Theorem 18 (3).

**Proposition 25.** Let $\mathcal{C}$ be a symmetric monoidal closed category that is total$^4$. Then all strong monads over $\mathcal{C}$ are centralisable.

*Proof.* In Appendix §E. □

<figure><img src="image_7.png" /></figure>

**Example 26.** Any category which is the Eilenberg-Moore category of a commutative monad over **Set** is total [12]. Furthermore it is symmetric monoidal closed [13], thus all strong monads on it are centralisable. This includes: the category **Set**\* of pointed sets and point preserving functions (algebras of the lift monad); the category **CMon** of commutative monoids and monoid homomorphisms (algebras of the commutative monoid monad); the category **Conv** of convex sets and linear functions (algebras of the distribution monad); and the category **Sup** of complete semilattices and sup-preserving functions (algebras of the powerset monad).

**Example 27.** Any presheaf category **Set**$^{\mathcal{C}\mathrm{op}}$ over a small category $\mathcal{C}$ is total [12] and cartesian closed, thus all strong monads on it (with respect to the cartesian structure) are centralisable. This includes: the category **Set**$^{A^{\mathrm{op}}}$, where $A$ is the category with two objects and two parallel arrows, which can be seen as the category of directed multi-graphs and graph homomorphisms; the category **Set**$^{G^{\mathrm{op}}}$, where $G$ is a group seen as a category, which can be seen as the category of $G$-sets (sets with an action of $G$) and equivariant maps; and the topos of trees **Set**$^{\mathbb{N}^{\mathrm{op}}}$.

If $\mathcal{C}$ is symmetric monoidal, then the Day convolution product makes **Set**$^{\mathcal{C}\mathrm{dp}}$ symmetric monoidal closed [14], hence all strong monads on it with respect to the Day convolution monoidal structure also are centralisable.

**Example 28.** Any Grothendieck topos is cartesian closed and total, therefore it satisfies the conditions of Proposition 25.

<footnote>$^4$A locally small category whose Yoneda embedding has a left adjoint.</footnote>
## B. Specific Examples of Centralisable Monads

In this subsection, we consider specific monads and construct their centres.

**Example 29.** Every commutative monad is naturally isomorphic to its centre.

**Example 30.** Let $S$ be a set and consider the well-known continuation monad $\mathcal{T} = [[-, S], S] : \mathbf{Set} \to \mathbf{Set}$. Note that, if $S$ is the empty set or a singleton set, then $\mathcal{T}$ is commutative, so we are in the situation of Example 29. Otherwise, when $S$ is not trivial, one can prove (details omitted here) that $\mathcal{Z}X = \eta_X(X) \cong X$. Therefore, the centre of $\mathcal{T}$ is trivial and it is naturally isomorphic to the identity monad.

**Example 31.** Consider the well-known list monad $T : \mathbf{Set} \to \mathbf{Set}$ that is given by $TX = \bigsqcup_{n \ge 0} X^n$. Then, the centre of $\mathcal{T}$ is naturally isomorphic to the identity monad.

Example 30 shows that the centre of a monad may be trivial in the sense that it is precisely the image of the monadic unit and this is the least it can be. At the other extreme, Example 29 shows that the centre of a commutative monad coincides with itself, as one would expect. Thus, the monads that have interesting centres are those monads which are strong but not commutative, and which have non-trivial centres, such as the one in Example 19. Another interesting example of a strong monad with a non-trivial centre is provided next.

**Example 32.** Every semiring $(S, +, \cdot, \cdot, 1)$ induces a monad $\mathcal{T}_S : \mathbf{Set} \to \mathbf{Set}$ [15]. This monad maps a set $X$ to the set of finite formal sums of the form $\sum s_i x_i$, where $s_i$ are elements of $S$ and $x_i$ are elements of $X$. The monad $\mathcal{T}_S$ is commutative iff $S$ is commutative as a semiring. The centre $\mathcal{Z}$ of $\mathcal{T}_S$ is induced by the commutative semiring $Z(S)$, i.e., by the centre of $S$ in the usual sense. Therefore, $\mathcal{Z} = \mathcal{T}_{Z(S)}$.

**Example 33.** Any Lawvere theory $T$ [16] induces a finitary monad on $\mathbf{Set}$. The centre of this monad is the monad induced by the centre of $T$ in the sense of Lawvere theories [17].

**Example 34.** The valuations monad $\mathcal{V}: \mathbf{DCPO} \to \mathbf{DCPO}$ [18], [19] is similar in spirit to the Giry monad on measurable spaces [20]. It is an important monad in domain theory [21] that is used to combine probability and recursion for dcpo's. Given a dcpo $X$, the valuations monad $\mathcal{V}$ assigns the dcpo $\mathcal{V}X$ of all Scott-continuous valuations on $X$, which are Scott-continuous functions $\nu: \sigma(X) \to [0, 1]$ from the Scott-open sets of $X$ into the unit interval that satisfy some additional properties that make them suitable to model probability (details omitted here, see [19] for more information). The category $\mathbf{DCPO}$ is cartesian closed and the valuations monad $\mathcal{V}: \mathbf{DCPO} \to \mathbf{DCPO}$ is strong, but its commutativity on $\mathbf{DCPO}$ has been an open problem since 1989 [19], [18], [22], [23], [24]. The difficulty in (dis)proving the commutativity of $\mathcal{V}$ boils down to (dis)proving the following Fubini-style equation

$$ \int_X \int_Y \chi_U(x, y) d\nu d\xi = \int_Y \int_X \chi_U(x, y) d\xi d\nu $$

holds for any dcpo's $X$ and $Y$, any Scott-open subset $U \in \sigma(X \times Y)$ and any two valuations $\xi \in \mathcal{V}X$ and $\nu \in \mathcal{V}Y$. In the above equation, the notion of integration is given by the valuation integral (see [19] for more information).

The central valuations monad [22], is the submonad $\mathcal{Z}: \mathbf{DCPO} \to \mathbf{DCPO}$ that maps a dcpo $X$ to the dcpo $\mathcal{Z}X$ which has all central valuations as elements. Equivalently:

$$ \mathcal{Z}X \stackrel{\text{def}}{=} \left\{ \begin{array}{l} \xi \in \mathcal{V}(X) \mid \forall Y \in \text{Ob}(\mathbf{DCPO}). \forall U \in \sigma(X \times Y). \\ \\ \forall \nu \in \mathcal{V}(Y). \int_X \int_Y \chi_U(x, y) d\nu d\xi = \int_Y \int_X \chi_U(x, y) d\xi d\nu \end{array} \right\}. $$

But this is precisely the centre of $\mathcal{V}$, which can be seen using Theorem 18 (1) after unpacking the definition of the monad data of $\mathcal{V}$. Therefore, we see that the main result of [22] is a special case of our more general categorical treatment. We wish to note, that the centre of $\mathcal{V}$ is quite large. It contains all three commutative submonads identified in [23] and all of them may be used to model lambda calculi with recursion and discrete probabilistic choice (see [23], [22]).

# VI. CENTRAL SUBMONADS

So far, we focused primarily on the centre of a strong monad. Now we focus our attention on central submonads of a strong monad which we define by taking inspiration from the notion of central subgroup in group theory. Just like central subgroups, central submonads are more general compared to the centre. The centre of a strong monad, whenever it exists, can be intuitively understood as the largest central submonad, so the two notions are strongly related. We will later see that central submonads are more interesting computationally.
**Theorem 35 (Centrality).** Let $\mathbf{C}$ be a symmetric monoidal category and $\mathcal{T}$ a strong monad on it. Let $\mathcal{S}$ be a strong submonad of $\mathcal{T}$ with $\iota: \mathcal{S} \Rightarrow \mathcal{T}$ the strong submonad monomorphism. The following are equivalent:

1) For any object $X$ of $\mathbf{C}$, $(\mathcal{S}X, \iota_X)$ is a central cone for $\mathcal{T}$ at $X$;

2) the canonical embedding functor $\mathcal{I}: \mathcal{C}_\mathcal{S} \to \mathcal{C}_\mathcal{T}$ corestricts to an embedding of categories $\tilde{\mathcal{I}}: \mathcal{C}_\mathcal{S} \to \mathcal{Z}(\mathcal{C}_\mathcal{T})$.

Furthermore, these conditions imply that $\mathcal{S}$ is a commutative submonad of $\mathcal{T}$. Under the additional assumption that $\mathcal{T}$ is centralisable, these conditions also are equivalent to:

3) $\mathcal{S}$ is a commutative submonad of the centre of $\mathcal{T}$.

*Proof.* In Appendix §F.

<figure><img src="image_8.png" /></figure>

**Definition 36 (Central Submonad).** Given a strong submonad $\mathcal{S}$ of $\mathcal{T}$, we say that $\mathcal{S}$ is a *central submonad of* $\mathcal{T}$ if it satisfies any one of the above equivalent criteria from Theorem 35.

Just like the centre of a strong monad, any central submonad also is commutative and the above theorem shows that central submonads have a similar structure to the centre of a strong monad. The final statement shows that we may see the centre (whenever it exists) as the largest central submonad of $\mathcal{T}$. The centre of a strong monad often does exist (as we already argued), so the last criterion also provides a simple way to determine whether a submonad is central or not.

**Example 37.** By the above theorem, every centre described in §V is a central submonad.

**Example 38.** Let $\mathcal{T}$ be a strong monad on a symmetric monoidal category $\mathbf{C}$, such that all unit maps $\eta_X: X \to \mathcal{T}X$ are monomorphisms (this is often the case in practice). Then, the identity monad on $\mathbf{C}$ is a central submonad of $\mathcal{T}$.

**Example 39.** Given a monoid $M$, let $\mathcal{T} = (M \times -)$ be the monad on Set from Example 19. Any submonoid $\mathcal{S}$ of $\mathcal{Z}(M)$ induces a central submonad $(S \times -)$ of $\mathcal{T}$.

**Example 40.** Given a semiring $R$, consider the monad $\mathcal{T}_R$ from Example 32. Any subsemiring $\mathcal{S}$ of $\mathcal{Z}(R)$ induces a central submonad $\mathcal{T}_S$ of $\mathcal{T}_R$.

**Example 41.** A notion of *central Lawvere subtheory* can be introduced in an obvious way. It induces a central submonad of the monad induced by the original Lawvere theory.

**Example 42.** The three commutative submonads identified in [23] are central submonads of the valuations monad $\mathcal{V}$ from Example 34, because each one of them is a commutative submonad of the centre of $\mathcal{V}$ [22].

*Remark 43.* Given an arbitrary monoid $M$ (on Set), there could be a commutative submonoid $\mathcal{S}$ of $M$ that is not central (i.e., its elements do not commute with all elements of $M$). The same holds for strong monads. For instance, let $M = \mathbb{D}_4$ (see Example 20) and let $\mathcal{S}$ be the submonoid of $M$ that contains only the rotations (of which there are four). Then, $\mathcal{S}$ is a commutative submonoid that is not central. By taking the free monads induced by these monoids (see Example 19) on Set, we get an example of a commutative submonad that is not central. Moreover, if we take $\mathbf{D}$ to be the full subcategory of Set whose objects have cardinality that is different from two, then $\mathbf{D}$ has a cartesian structure and the writer monads induced by $\mathcal{S}$ and $M$ on $\mathbf{D}$ give an example of a non-centralisable strong monad that admits a commutative non-central submonad. In this situation, the identity monad on $\mathbf{D}$ gives an example of a central (commutative) submonad even though the ambient monad (induced by $M$) is not centralisable.

## VII. COMPUTATIONAL INTERPRETATION

In this section, we provide a computational interpretation of our ideas. We consider a simply-typed lambda calculus together with a strong monad $\mathcal{T}$ and a *central submonad* $\mathcal{S}$ of $\mathcal{T}$. We call this system the *Central Submonad Calculus (CSC)*. We describe its equational theories, formulate appropriate categorical models for it and we prove soundness, completeness and internal language results for our semantics.

### A. *Syntactic Structure of the Central Submonad Calculus*

We begin by describing the types we use. The grammar of types (see Figure 1) are just the usual ones with one addition – we extend the grammar by adding the family of types $\mathcal{S}A$. The type $\mathcal{T}A$ represents the type of monadic computations for our monad $\mathcal{T}$ that produce values of type $A$ (together with a potential side effect described by $\mathcal{T}$). The type $\mathcal{S}A$ represents the type of *central* monadic computations for our monad $\mathcal{T}$ that produce values of type $A$ (together with a potential *central* side effect that is in the submonad $\mathcal{S}$). Some terms and formation rules can be expressed in the same way for types of the form $\mathcal{S}A$ or $\mathcal{T}A$ and in this case we simply write $\mathcal{X}A$ to indicate that $\mathcal{X}$ may range over $\{\mathcal{S}, \mathcal{T}\}$.

The grammar of terms and their formation rules are described in Figure 1. The first six rules in Figure 1 are just the usual formation rules for a simply-typed lambda calculus with pair types. Contexts are considered up to permutation and without repetition and all judgements we consider are implicitly closed under weakening (which is important when adding constants).
(Types) $A, B ::= 1 \mid A \to B \mid A \times B \mid SA \mid TA$

(Terms)
$M, N ::= x \mid * \mid \lambda x^A . M \mid MN \mid \langle M, N \rangle$
$| \pi_i M \mid \mathrm{ret}_S M \mid \iota M \mid \mathrm{ret}_T M$
$| \mathrm{do}_S x \leftarrow M; N \mid \mathrm{do}_T x \leftarrow M; N$

$$
\begin{array}{ccc}
\underline{\Gamma, x : A \vdash x : A} & \underline{\Gamma \vdash M : A \to B \quad \Gamma \vdash N : A} & \\
\underline{\Gamma \vdash * : 1} & \underline{\Gamma, x : A \vdash M : B \quad \Gamma \vdash \lambda x^A . M : A \to B} & \underline{\Gamma \vdash M : A_1 \times A_2 \quad \Gamma \vdash \pi_i M : A_i} \\
\underline{\Gamma \vdash M : A \quad \Gamma \vdash N : B} & \underline{\Gamma \vdash \langle M, N \rangle : A \times B} & \underline{\Gamma \vdash M : A \quad \Gamma \vdash \mathrm{ret}_\chi M : \chi A} \\
\underline{\Gamma \vdash M : SA} & \underline{\Gamma \vdash M : \chi A \quad \Gamma, x : A \vdash N : \chi B} & \underline{\Gamma \vdash \mathrm{do}_\chi x \leftarrow M; N : \chi B}
\end{array}
$$

<caption>Fig. 1. Grammars and formation rules.</caption>

$$
\begin{array}{ccc}
\frac{}{\vdash A : \text{type}} & \frac{}{\vdash A = B : \text{type}} & \frac{}{\vdash A = B : \text{type} \quad \vdash B = C : \text{type}} \\
\frac{\vdash A = A : \text{type}}{} & \frac{\vdash B = A : \text{type}}{} & \frac{}{\vdash A = C : \text{type}} \\
\frac{\vdash A = A' : \text{type} \quad \vdash B = B' : \text{type}}{\vdash A \times B = A' \times B' : \text{type}} & \frac{\vdash A = A' : \text{type} \quad \vdash B = B' : \text{type}}{\vdash A \to B = A' \to B' : \text{type}} & \frac{\vdash A = B : \text{type}}{\vdash \chi A = \chi B : \text{type}}
\end{array}
$$

<caption>Fig. 2. Equational rules for types.</caption>

The $\mathrm{ret}_\chi M$ term is used as an introduction rule for the monadic types and it allows us to see the pure (i.e., non-effectful) computation described by the term $M$ as a monadic one. The term $\iota M$ allows us to view a central monadic computation as a monadic (not necessarily central) one. Semantically, it corresponds to applying the $\iota$ submonad inclusion we saw in previous sections. Finally, we have two terms for monadic sequencing that use the familiar do-notation. The monadic sequencing of two central computations remains central, which is represented via the $\mathrm{do}_S$ terms; the $\mathrm{do}_T$ terms are used for monadic sequencing of (not necessarily central) computations.

## B. Equational Theories of the Central Submonad Calculus

Next, we describe equational theories for our calculus. We follow the vocabulary and the terminology in [5] in order to formulate an appropriate notion of CSC-theory.

**Definition 44 (CSC-theory).** A CSC-theory is an extension of the Central Submonad Calculus (see §VII-A) with new ground types, new term constants (which we assume are well-formed in any context, including the empty one) and new equalities between types and between terms.

In a CSC-theory, we have four types of judgements: the judgement $\vdash A : \text{type}$ indicates that $A$ is a (simple) type; the judgement $\vdash A = B : \text{type}$ indicates that types $A$ and $B$ are equal; the judgement $\Gamma \vdash M : A$ indicates that $M$ is a well-formed term of type $A$ in context $\Gamma$, as usual; finally, the judgement $\Gamma \vdash M = N : A$ indicates that the two well-formed terms $M$ and $N$ are equal.

Type judgements and term judgements are described in Figure 1 and type equality judgements in Figure 2. Following the principle of judgemental equality, we add type conversion rules in Figure 3. The rules in Figure 4 are the usual rules that describe the equational theory of the simply-typed lambda calculus. As often done by many authors, we implicitly identify terms that are $\alpha$-equivalent. The rules for $\beta$-equivalence and $\eta$-equivalence are explicitly specified.

In Figure 5, we present the equational rules for monadic computation. The rules on the first three lines – (ret.eq), (do.eq), $(\mathcal{X}.\beta)$, $(\mathcal{X}.\eta)$, $(\mathcal{X}.\mathrm{assoc})$ – axiomatise the structure of a strong monad. Because of this, these rules are stated for both monads $\mathcal{T}$ and $\mathcal{S}$. The rules $(\iota.\mathrm{mono})$, $(\iota\mathcal{S}.\mathrm{ret})$ and $(\iota\mathcal{S}.\mathrm{comp})$ are used to axiomatise the structure of $\mathcal{S}$ as a submonad of $\mathcal{T}$. Intuitively, these rules can be understood as specifying that central monadic computations can be seen as (general) monadic computations of the ambient monad $\mathcal{T}$. The remainder of the rules are used to axiomatise the behaviour of $\mathcal{S}$ as a central submonad of $\mathcal{T}$. The rule $(\mathcal{S}.\mathrm{central})$ is undoubtedly the most important one, because it ensures that central computations commute with any other (not necessarily central) computation when performing monadic sequencing with the $\mathcal{T}$ monad.
$$ \frac{\Gamma \vdash A = B : \mathit{type} \quad \Gamma \vdash C = D : \mathit{type} \quad \Gamma, x : A \vdash M : C \quad \Gamma \vdash A = B : \mathit{type} \quad \Gamma \vdash C = D : \mathit{type} \quad \Gamma, x : A \vdash M = N : C}{\Gamma, x : B \vdash M : D \qquad \Gamma, x : B \vdash M = N : D} $$

<caption>Fig. 3. Type conversion rules.</caption>

$$ \frac{\Gamma \vdash M : A \quad (\mathit{refl}) \quad \Gamma \vdash N = M : A \quad (\mathit{symm}) \quad \Gamma \vdash M = N : A \quad \Gamma \vdash N = P : A \quad (\mathit{trans})}{\Gamma \vdash M = M : A} \qquad \frac{\Gamma \vdash M : A \quad \Gamma, x : A \vdash N = P : B \quad (\mathit{subst}) \quad \Gamma \vdash M = M' : A \quad \Gamma \vdash N = N' : B \quad (\langle, \rangle.\mathit{eq})}{\Gamma, x : 1 \vdash * = x : 1} (1.\eta) \\
\frac{\Gamma \vdash M_1 : A_1 \quad \Gamma \vdash M_2 : A_2 \quad (\times.\beta) \quad \Gamma \vdash M : A \times B \quad (\times.\eta)}{\Gamma \vdash \pi_i \langle M_1, M_2 \rangle = M_i : A_i} \\
\frac{\Gamma \vdash M = M' : A \rightarrow B \quad \Gamma \vdash N = N' : A \quad (\mathit{app}\cdot\mathit{eq}) \quad \Gamma, x : A \vdash M = N : B \quad \Gamma \vdash \lambda x^A.M = \lambda x^A.N : A \rightarrow B}{\Gamma \vdash MN = M'N' : B} (\lambda.\mathit{eq}) \\
\frac{\Gamma, x : A \vdash M : B \quad \Gamma \vdash N : A \quad (\lambda.\beta) \quad \Gamma \vdash M : A \rightarrow B \quad (\lambda.\eta)}{\Gamma \vdash (\lambda x^A.M)N = M[N/x] : B} (\mathit{weak}) $$

<caption>Fig. 4. Equational rules of the simply-typed λ-calculus.</caption>

**Example 45.** Let us consider an example of a CSC-theory. Given a monoid $(M, e, m)$ we now axiomatise the writer monad induced by $M$. A theory for this monad does not add any new types, but it adds constants for each element $c$ of $M$: $\Gamma \vdash \mathit{act}_{\mathcal{T}}(c) : \mathcal{T} 1$. In this specific theory, we may think of the side-effect computed by monadic sequencing as being simply an element of $M$. The term $\mathit{act}_{\mathcal{T}}(c)$ can be understood as performing the monoid multiplication on the right with argument $c$, i.e., it applies the function $m(-, c)$ to whatever is the current state of the program.

Let $S$ be a submonoid of the centre $Z(M)$ of $M$. This makes $S$ a central submonoid of $M$ (this can be defined in a similar way to central subgroups). We enrich the theory with the following constant and rule for each $s$ in $S$:

$$ \overline{\Gamma \vdash \mathit{act}_S(s) : S 1} \qquad \overline{\Gamma \vdash \iota \mathit{act}_S(s) = \mathit{act}_{\mathcal{T}}(s) : \mathcal{T} 1} $$

The application of $\mathit{ret}_\chi$ is equivalent to acting on the monoid data with the neutral element:

$$ \overline{\Gamma \vdash \mathit{ret}_\chi * = \mathit{act}_\chi(e) : S 1} $$

Of course, the actions compose:

$$ \frac{\Gamma \vdash M : \mathcal{X}A}{\Gamma \vdash \mathit{do}_{\mathcal{X}} * \leftarrow \mathit{act}_{\mathcal{X}}(c); \mathit{do}_{\mathcal{X}} * \leftarrow \mathit{act}_{\mathcal{X}}(c'); M \\ = \mathit{do}_{\mathcal{X}} * \leftarrow \mathit{act}_{\mathcal{X}}(m(c, c')); M : \mathcal{X}A} $$

where we have used some (hopefully obvious) syntactic sugar. We write $\mathfrak{S}_M$ to refer to this theory.

$$ \frac{\Gamma \vdash M = N : A \quad (\mathit{ret}\cdot\mathit{eq}) \quad \Gamma \vdash M = M' : \mathcal{X}A \quad \Gamma, x : A \vdash N = N' : \mathcal{X}B \quad (\mathit{do}\cdot\mathit{eq})}{\Gamma \vdash \mathit{ret}_\chi M = \mathit{ret}_\chi N : \mathcal{X}A} \qquad \frac{\Gamma \vdash M : \mathcal{X}A \quad \Gamma, x : A \vdash N : \mathcal{X}B \quad (\mathcal{X}\cdot\beta) \quad \Gamma \vdash M : \mathcal{X}A \quad \Gamma \vdash \mathit{do}_\chi x \leftarrow M ; N = \mathit{do}_\chi x \leftarrow M' ; N' : \mathcal{X}B}{\Gamma \vdash \mathit{do}_\chi x \leftarrow \mathit{ret}_\chi M ; N = N[M/x] : \mathcal{X}B} (\mathcal{X}\cdot\eta) \\
\frac{\Gamma \vdash M : \mathcal{X}A \quad \Gamma \vdash N : \mathcal{X}B \quad \Gamma, x : A, y : B \vdash P : \mathcal{X}C \quad (\mathcal{X}\cdot\mathit{assoc})}{\Gamma \vdash \mathit{do}_\chi y \leftarrow (\mathit{do}_\chi x \leftarrow M ; N) ; P = \mathit{do}_\chi x \leftarrow M ; \mathit{do}_\chi y \leftarrow N ; P : \mathcal{X}C} (\mathcal{X}\cdot\mathit{assoc}) \\
\frac{\Gamma \vdash M : \mathcal{S}A \quad \Gamma \vdash N : \mathcal{T}B \quad \Gamma, x : A, y : B \vdash P : \mathcal{T}C \quad (\mathcal{S}\cdot\mathit{central})}{\Gamma \vdash \mathit{do}_\mathcal{T} x \leftarrow \iota M ; \mathit{do}_\mathcal{T} y \leftarrow N ; P = \mathit{do}_\mathcal{T} y \leftarrow N ; \mathit{do}_\mathcal{T} x \leftarrow \iota M ; P : \mathcal{T}C} (\iota\mathit{mono}) \\
\frac{\Gamma \vdash M : \mathcal{S}A \quad \Gamma, x : A \vdash N : \mathcal{S}B \quad (\iota\mathcal{S}\cdot\mathit{comp}) \quad \Gamma \vdash M : A \quad \Gamma \vdash \iota \mathit{ret}_S M = \mathit{ret}_\mathcal{T} M : \mathcal{T}A}{\Gamma \vdash \mathit{do}_\mathcal{T} x \leftarrow \iota M ; \iota N = \iota \mathit{do}_S x \leftarrow M ; N : \mathcal{T}B} (\iota\mathcal{S}\cdot\mathit{ret}) $$

<caption>Fig. 5. Equational rules for terms of monadic types of CSC.</caption>
**Remark 46.** As we have now seen, the equational theories of central submonads admit a presentation that is similar in spirit to that of the simply-typed λ-calculus. However, that is not the case with the centre of a strong monad. The reason is that the theory $\mathfrak{T}$ can introduce a central effect – one that commutes with all others – as a constant $c$ that is not assigned the type $SA$, but the type $TA$, for some $A$. However, the centre, being the largest central submonad, must contain all such effects, so the constant $c$ has to be equal to a term of the form $\iota c'$. One solution to this problem would be to use a more expressive logic and introduce a rule as follows (writing inline because of space): given $c : TA$ and $x : A, y : B \vdash P : TC$, such that $\forall N : TB. \vdash \mathrm{do}_T x \leftarrow c; \mathrm{do}_T y \leftarrow N; P = \mathrm{do}_T y \leftarrow N; \mathrm{do}_T x \leftarrow c; P : TC$ then $\exists c' : SA. \vdash c = \iota c' : TA$. However, the addition of such a rule seems unnecessary to prove our main point and it increases the complexity of the logic. Because of this, our choice is to focus on central submonads. Another reason to prefer central submonads over the centre is that they are more general and it is not required to identify all central effects (which would be the case for the centre). Overall, our choice for central submonads is motivated by the advantages they provide in terms of generality, simplicity and practicality of their equational theories compared to the centre.

Now that we have introduced theories, we explain how they can be translated into one another in an appropriate way.

**Definition 47 (CSC-translation).** A translation $V$ between two CSC-theories $\mathfrak{T}$ and $\mathfrak{T}'$ is a function that maps types of $\mathfrak{T}$ to types of $\mathfrak{T}'$ and terms of $\mathfrak{T}$ to terms of $\mathfrak{T}'$ that preserves the provability of all type judgements, term judgements, type equality judgements and term equality judgements. Moreover, such a translation is required to satisfy the following structural requirements on types:

$$V(1) = 1 \quad V(\mathfrak{T}A) = \mathfrak{T}V(A) \quad V(SA) = SV(B) \\ V(A \to B) = V(A) \to V(B) \quad V(A \times B) = V(A) \times V(B)$$

and on terms:

$$V(*) = * \\ V(\lambda x^A.M) = \lambda x^A.V(M) \quad V(MN) = V(M)V(N) \\ V(\langle M, N \rangle) = \langle V(M), V(N) \rangle \quad V(\pi_i M) = \pi_i V(M) \\ V(\iota M) = \iota V(M) \quad V(\mathrm{ret}_X M) = \mathrm{ret}_X V(M) \\ V(\mathrm{do}_X x \leftarrow M; N) = \mathrm{do}_X x \leftarrow V(M); V(N)$$

**Remark 48.** The above equations do not imply preservation of the relevant judgements for constants. Because of this, the first part of the definition also is necessary.

Of course, it is easy to see that CSC-theories and CSC-translations form a category. However, in order to precisely state our main result, we have to consider the 2-categorical structure of CSC-theories. Intuitively, we may view every CSC-theory as a category itself (with types as objects and terms as morphisms) and every CSC-translation as a functor that strictly preserves the relevant structure. Then, intuitively, an appropriate notion of a 2-morphism would be a natural transformation between such functors. This is made precise (in non-categorical terms) by our next definition.

**Definition 49 (CSC-translation Transformation).** Given two CSC-theories $\mathfrak{T}$ and $\mathfrak{T}'$, and two CSC-translations $V$ and $V'$ between them, a CSC-translation transformation $\alpha : V \Rightarrow V'$ is a type-indexed family of term judgements $x : V(A) \vdash \alpha_A : V'(A)$ such that, for any valid judgement $x : A \vdash f : B$ in $\mathfrak{T}$

$$x : V(A) \vdash \alpha_B[V(f)/x] = V'(f)[\alpha_A/x] : V'(B)$$

also is derivable in $\mathfrak{T}'$.

**Proposition 50.** CSC-theories, CSC-translations and CSC-translation transformations form a 2-category $\mathrm{Th}(\mathrm{CSC})$.

### C. Categorical Models of CSC

Now we describe what are the appropriate categorical models for providing a semantic interpretation of our calculus.

**Definition 51 (CSC-model).** A CSC-model is a cartesian closed category $\mathcal{C}$ equipped with both a strong monad $\mathcal{T}$ and a central submonad $\mathcal{S}^\mathcal{T}$ of $\mathcal{T}$ with submonad monomorphism written as $\iota^\mathcal{T} : \mathcal{S}^\mathcal{T} \Rightarrow \mathcal{T}$. We often use a quadruple $(\mathcal{C}, \mathcal{T}, \mathcal{S}^\mathcal{T}, \iota^\mathcal{T})$ to refer to a CSC-model.

We will soon show that CSC-models correspond to CSC-theories in a precise way. This correspondence covers CSC-translations too and for this we introduce our next definition.

**Definition 52 (CSC-model Morphism).** Given two CSC-models $(\mathcal{C}, \mathcal{T}, \mathcal{S}^\mathcal{T}, \iota^\mathcal{T})$ and $(\mathcal{D}, \mathcal{M}, \mathcal{S}^\mathcal{M}, \iota^\mathcal{M})$, a CSC-model morphism is a strict cartesian closed functor $F : \mathcal{C} \to \mathcal{D}$ that satisfies the following additional coherence properties:

$$F(\mathcal{T}X) = \mathcal{M}(FX) \quad F(\mathcal{S}^\mathcal{T}X) = \mathcal{S}^\mathcal{M}(FX) \\ F\iota_X^\mathcal{T} = \iota_{FX}^\mathcal{M} \quad F\eta_X^\mathcal{T} = \eta_{FX}^\mathcal{M} \\ F\mu_X^\mathcal{T} = \mu_{FX}^\mathcal{M} \quad F\tau_{X,Y}^\mathcal{T} = \tau_{FX,FY}^\mathcal{M}.$$
Notice that a CSC-model morphism strictly preserves all of the relevant categorical structure. This is done on purpose so that we can establish an exact correspondence with CSC-translations, which also strictly preserve the relevant structure. To match the notion of a CSC-translation transformation, we just have to consider natural transformations between CSC-model morphisms.

**Proposition 53.** CSC-models, CSC-model morphisms and natural transformations between them form a 2-category Mod(CSC).

## D. Semantic Interpretation

Now we explain how to introduce a denotational semantics for our theories using our models. An interpretation of a CSC-theory $\mathfrak{T}$ in a CSC-model $\mathbf{C}$ is a function $\llbracket - \rrbracket$ that maps types of $\mathfrak{T}$ to objects of $\mathbf{C}$ and well-formed terms of $\mathfrak{T}$ to morphisms of $\mathbf{C}$. We provide the details below.

For each ground type $G$, we assume there is an appropriate corresponding object $\llbracket G \rrbracket$ of $\mathbf{C}$. The remaining types are interpreted as objects in $\mathbf{C}$ as follows: $\llbracket 1 \rrbracket \stackrel{\text{def}}{=} 1$; $\llbracket A \to B \rrbracket \stackrel{\text{def}}{=} \llbracket B \rrbracket^{[A]}$; $\llbracket A \times B \rrbracket \stackrel{\text{def}}{=} \llbracket A \rrbracket \times \llbracket B \rrbracket$; $\llbracket SA \rrbracket \stackrel{\text{def}}{=} S \llbracket A \rrbracket$; $\llbracket \mathcal{T}A \rrbracket \stackrel{\text{def}}{=} \mathcal{T} \llbracket A \rrbracket$. Variable contexts $\Gamma = x_1 : A_1 \dots x_n : A_n$ are interpreted as usual as $\llbracket \Gamma \rrbracket \stackrel{\text{def}}{=} \llbracket A_1 \dots A_n \rrbracket$. Terms are interpreted as morphisms $\llbracket \Gamma \vdash M : A \rrbracket : \llbracket \Gamma \rrbracket \to \llbracket A \rrbracket$ of $\mathbf{C}$. When the context and the type of a term $M$ are understood, then we simply write $\llbracket M \rrbracket$ as a shorthand for $\llbracket \Gamma \vdash M : A \rrbracket$. The interpretation of term constants and the terms of the simply-typed $\lambda$-calculus is defined in the usual way (details omitted). The interpretation of the monadic terms is given by:

$$ \begin{align*} \llbracket \Gamma \vdash \mathrm{ret}_\mathcal{X} M : \mathcal{X} A \rrbracket &= \eta_{\llbracket A \rrbracket}^\mathcal{X} \circ \llbracket M \rrbracket \\ \llbracket \Gamma \vdash \iota M : \mathcal{T} A \rrbracket &= \iota_{\llbracket A \rrbracket} \circ \llbracket M \rrbracket \\ \llbracket \Gamma \vdash \mathrm{do}_\mathcal{X} x \leftarrow M; N : \mathcal{X} B \rrbracket \\ &= \mu_{\llbracket B \rrbracket}^\mathcal{X} \circ \mathcal{X} \llbracket N \rrbracket \circ \tau_{\llbracket \Gamma \rrbracket, \llbracket A \rrbracket}^\mathcal{X} \circ \langle \mathrm{id}, \llbracket M \rrbracket \rangle \end{align*} $$

where we use $\mathcal{X}$ to range over $\mathcal{T}$ or its central submonad $\mathcal{S}$.

**Definition 54 (Soundness and Completeness).** An interpretation $\llbracket - \rrbracket$ of a CSC-theory $\mathfrak{T}$ in a CSC-model $\mathbf{C}$ is said to be sound if for any type equality judgement $\vdash A = B : \mathrm{type}$ in $\mathfrak{T}$, we have that $\llbracket A \rrbracket = \llbracket B \rrbracket$ in $\mathbf{C}$, and for any equality judgement $\Gamma \vdash M = N : A$ in $\mathfrak{T}$, we have that $\llbracket \Gamma \vdash M : A \rrbracket = \llbracket \Gamma \vdash N : A \rrbracket$ in $\mathbf{C}$. An interpretation $\llbracket - \rrbracket$ is said to be complete when $\vdash A = B : \mathrm{type}$ iff $\llbracket A \rrbracket = \llbracket B \rrbracket$ and $\Gamma \vdash M = N : A$ iff $\llbracket \Gamma \vdash M : A \rrbracket = \llbracket \Gamma \vdash N : A \rrbracket$. If, moreover, the interpretation is clear from context, then we may simply say that the model $\mathbf{C}$ itself is sound and complete for the CSC-theory $\mathfrak{T}$.

**Remark 55.** There are different definitions of what constitutes a “model” in the literature. For example, a “model” in [25] corresponds to a sound interpretation in our sense.

**Example 56.** A categorical model for the CSC-theory $\mathfrak{T}_M$ of Example 45 is given by the category Set together with the writer monad $\mathcal{T} \stackrel{\text{def}}{=} (- \times M) : \mathrm{Set} \to \mathrm{Set}$ and the central submonad $\mathcal{S} \stackrel{\text{def}}{=} (- \times S) : \mathrm{Set} \to \mathrm{Set}$. More specifically, the monad data for $\mathcal{T}$ is given by:

$$ \begin{align*} \eta_A : A &\to A \times M :: a \mapsto (a, e) \\ \mu_A : (A \times M) \times M &\to A \times M :: ((a, c), c') \mapsto (a, m(c, c')) \\ \tau_{A,B} : A \times (B \times M) &\to (A \times B) \times M :: \\ (a, (b, c)) &\mapsto ((a, b), c) \end{align*} $$

and the monad data for $\mathcal{S}$ is defined in the same way by (co)restricting to the submonoid $\mathcal{S}$. The interpretation of the term constants is given by:

$$ \begin{align*} \llbracket \Gamma \vdash \mathrm{act}_\mathcal{T}(c) : \mathcal{T} 1 \rrbracket : \llbracket \Gamma \rrbracket &\to 1 \times M :: \gamma \mapsto (*, c) \\ \llbracket \Gamma \vdash \mathrm{act}_\mathcal{S}(c) : \mathcal{S} 1 \rrbracket : \llbracket \Gamma \rrbracket &\to 1 \times S :: \gamma \mapsto (*, c) \end{align*} $$

This interpretation of the theory $\mathfrak{T}_M$ is sound and complete.

## E. Equivalence between Theories and Models

Our final result in this paper is to show that CSC-theories and CSC-models are strongly related. To do this, we define the syntactic CSC-model $\mathcal{S}(\mathfrak{T})$ of CSC-theory $\mathfrak{T}$, and the internal language $L(\mathbf{C})$ that maps a CSC-model $\mathbf{C}$ to its internal language viewed as a CSC-theory. These two assignments give rise to our desired equivalence (Theorem 66).
1) The Syntactic CSC-model: Assume throughout the subsection that we are given a CSC-theory $\mathfrak{T}$. We show how to construct a sound and complete model $S(\mathfrak{T})$ of $\mathfrak{T}$ by building its categorical data using the syntax provided by $\mathfrak{T}$.

**Definition 57 (Syntactic Category).** Let $S(\mathfrak{T})$ be the category whose objects are the types of $\mathfrak{T}$ modulo type equality, i.e., the objects are equivalence classes $[A]$ of types with $A' \in [A]$ iff $\vdash A' = A : \text{type}$ in $\mathfrak{T}$. The morphisms $S(\mathfrak{T})([A], [B])$ are equivalence classes of judgements $[x : A \vdash f : B]$, where $(x : A' \vdash f' : B') \in [x : A \vdash f : B]$ iff $\vdash A' = A : \text{type}$ and $\vdash B' = B : \text{type}$ and $x : A \vdash f = f' : B$. Identities are given by $[x : A \vdash x : A]$ and composition is defined by

$$[y : B \vdash g : C] \circ [x : A \vdash f : B'] = [x : A \vdash g[f/y] : C],$$

with $B' \in [B]$.

**Lemma 58.** The above definition is independent of the choice of representatives and the syntactic category $S(\mathfrak{T})$ is a well-defined cartesian closed category.

*Proof.* In Appendix §G. □

*Remark 59.* Note that by using Scott's trick [26] we can take quotients without having to go up higher in the class hierarchy, so foundational issues can be avoided.

**Lemma 60.** The following assignments:

$$ \begin{align*} \mathcal{T}([A]) &= [\mathcal{T}A] \\ \mathcal{T}([x : A \vdash f : B]) &= [y : \mathcal{T}A \vdash \mathrm{do}_{\mathcal{T}} x \leftarrow y; \mathrm{ret}_{\mathcal{T}} f : \mathcal{T}B] \\ \eta_{[A]} &= [x : A \vdash \mathrm{ret}_{\mathcal{T}} x : \mathcal{T}A] \\ \mu_{[A]} &= [x : \mathcal{T}A \vdash \mathrm{do}_{\mathcal{T}} y \leftarrow x; y : \mathcal{T}A] \\ \tau_{[A], [B]} &= [x : A \times \mathcal{T}B \vdash \\ & \qquad \mathrm{do}_{\mathcal{T}} y \leftarrow \pi_2 x; \mathrm{ret}_{\mathcal{T}} (\pi_1 x, y) : \mathcal{T}(A \times B)] \end{align*} $$

are independent of the choice of representatives and define a strong monad $(\mathcal{T}, \eta, \mu, \tau)$ on $S(\mathfrak{T})$.

**Lemma 61.** In a similar way to Lemma 58, we can define a strong monad $(S, \eta^S, \mu^S, \tau^S)$ on $S(\mathfrak{T})$ by using the corresponding monadic primitives. Then, the assignment:

$$\iota_{[A]} = [x : SA \vdash \iota x : TA]$$

is independent of the choice of representative and gives a strong submonad monomorphism $\iota : S \Rightarrow \mathcal{T}$ that makes $S$ a central submonad of $\mathcal{T}$.

*Proof.* In Appendix §H. □

Now we can prove our completeness result.

**Theorem 62 (Completeness).** The quadruple $(S(\mathfrak{T}), \mathcal{T}, S, \iota)$ is a sound and complete CSC-model for the CSC-theory $\mathfrak{T}$.

*Proof.* There exists an (obvious) interpretation $\llbracket - \rrbracket$ of $\mathfrak{T}$ into $S(\mathfrak{T})$ which follows the structure outlined in §VII-D. Standard arguments then show that $\Gamma \vdash M = N : A$ in $\mathfrak{T}$ iff $\llbracket \Gamma \vdash M : A \rrbracket = \llbracket \Gamma \vdash N : A \rrbracket$ in $S(\mathfrak{T})$. □

*Remark 63.* Note that the obvious canonical interpretation of $\mathfrak{T}$ in $S(\mathfrak{T})$ is initial as one may expect: any sound interpretation of $\mathfrak{T}$ in a CSC-model $\mathbf{C}$ factorises uniquely through the canonical interpretation via a CSC-model morphism.

2) **Internal Language:** With completeness proven, we now wish to establish an internal language result.

**Definition 64 (Internal Language).** Given a CSC-model $\mathbf{C}$, we define a CSC-theory $L(\mathbf{C})$ as follows:

* For each object $A$ of $\mathbf{C}$ we add a ground type which we name $A^*$.

* Every ground type $A^*$ is interpreted in $\mathbf{C}$ by setting $\llbracket A^* \rrbracket \stackrel{\mathrm{def}}{=} A$. This uniquely determines an interpretation on all types.

* If $A$ and $B$ are two (not necessarily ground) types, we add a type equality $\vdash A = B : \text{type}$ iff $\llbracket A \rrbracket = \llbracket B \rrbracket$.

* For every morphism $f : A \to B$ in $\mathbf{C}$, we add a term constant $\vdash c_f : A^* \to B^*$. Its interpretation in $\mathbf{C}$ is defined to be $\llbracket c_f \rrbracket \stackrel{\mathrm{def}}{=} \mathrm{curry}(f \circ \cong) : 1 \to B^A$, i.e., it is defined by currying the morphism $f$ in the obvious way. This uniquely determines an interpretation on all well-formed terms.

* New term equality axioms $\Gamma \vdash M = N : B$ iff $\llbracket \Gamma \vdash M : B \rrbracket = \llbracket \Gamma \vdash N : B \rrbracket$.

**Theorem 65.** For any CSC-model $\mathbf{C}$ the above definition gives a well-defined CSC-theory $L(\mathbf{C})$. Moreover, the model $\mathbf{C}$ is sound and complete for $L(\mathbf{C})$.
*Proof.* Well-definedness is straightforward and follows by a simple induction argument using the fact that the semantic interpretation $[\neg]$ defined in §VII-D is always sound. Completeness is then immediate by the last condition in Definition 64. □

3) *Equivalence Theorem:* Finally, we show that both the construction of the syntactic category and the assignment of the internal language give rise to appropriate equivalences.

**Theorem 66.** The relationship between the internal language and the syntactic model enjoys the following properties in the 2-categories Mod(CSC) and Th(CSC), respectively:

1) For any CSC-model $C$, we have that $C \simeq SL(C)$, i.e., there exist CSC-model morphisms $F : C \to SL(C)$ and $G : SL(C) \to C$ such that $F \circ G \cong \text{Id}$ and $\text{Id} \cong G \circ F$.

2) For any CSC-theory $\mathfrak{T}$, we have that $\mathfrak{T} \simeq LS(\mathfrak{T})$, i.e., there exist CSC-translations $V : \mathfrak{T} \to LS(\mathfrak{T})$ and $W : LS(\mathfrak{T}) \to \mathfrak{T}$ such that $V \circ W \cong \text{Id}$ and $\text{Id} \cong W \circ V$.

*Proof.* In Appendix §I. □

*Remark 67.* We introduced type equalities so that we can prove Theorem 66. This is also the approach taken in [5] and without this, technical difficulties arise. Theory translations are defined strictly (up to equality, not up to isomorphism) and in order to match this with the corresponding notion of model morphism, we use type equalities. Without type equalities, the symmetry within Theorem 66 can only be established if we make further changes. One potential solution would be to weaken the notion of theory translation by requiring that it preserves types up to type isomorphism (i.e., make it strong instead of strict), but this is technically cumbersome.

VIII. CONCLUSION AND FUTURE WORK

We showed that, under some mild assumptions, strong monads indeed admit a centre, which is a commutative submonad, and we provided three equivalent characterisations for the existence of this centre (Theorem 18) which also establish important links to the theory of premonoidal categories. In particular, every (canonically strong) monad on Set is centralisable (§IV-A) and we showed that the same is true for many other categories of interest (§V-A) and we identified specific monads with interesting centres (§V-B). More generally, we considered central submonads and we provided a computational interpretation of our ideas (§VII) which has the added benefit of allowing us to easily keep track of which monadic operations are central, i.e., which effectful operations commute under monadic sequencing with any other (not necessarily central) effectful operation. We cemented our semantics by proving soundness, completeness and internal language results.

One direction for future work is to consider a theory of *commutants* or *centralisers* for monads (in the spirit of [6], [7]) and to develop a computational interpretation with the expected properties (soundness, completeness and internal language). Another opportunity for future work includes studying the relationship between the centres of strong monads and distributive laws. In particular, given two strong monads and a strong/commutative distributive law between them, can we show that the distributive law also holds for their centres (or for some central submonads)? If so, this would allow us to use the distributive law to combine not just the original monads, but their centres/central submonads as well. Moreover, the interaction of the centre with operations on monadic theories can be investigated.

Our definition of central submonads makes essential use of the notion of monomorphism of strong monads. Another possibility for future work is to investigate an alternative approach where we consider an appropriate class of factorisation systems instead of monomorphisms to define central submonads. Yet another possibility for future work is to investigate if central submonads of a given strong monad have some interesting poset structure.
ACKNOWLEDGMENTS

We thank the anonymous reviewers for their feedback which led to multiple improvements of the paper. We also are grateful
to Richard Garner, Jean Goubault-Larrecq, Rory Lucyshyn-Wright, Maxime Ramzi, Sam Staton and the Inria QuaCS team for
useful comments and discussions. Titouan Carette was supported by the ERDF project 1.1.1.5/18/A/020 "Quantum algorithms:
from complexity theory to experiment". Louis Lemonnier wishes to thank the organisers of the ACT 2022 conference for
providing financial support that allowed him to attend the conference and to give a talk about some of our results. Vladimir
Zamdzhiev gratefully acknowledges financial support from the French project ANR-17-CE25-0009 SoftQPro. A part of this
research was performed while Vladimir Zamdzhiev was a member of the MOCQUA team in Loria/Inria Nancy - Grand Est. The
authors also wish to thank the organisers of the "Logic of Probabilistic Programming" meeting at CIRM (Centre International
de Rencontres Mathématiques) in 2022 where we initiated our collaboration on this research project and we thank CIRM for
accommodation support during that meeting.

REFERENCES

[1] E. Moggi, "Computational lambda-calculus and monads," in *Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), Pacific Grove, California, USA, June 5-8, 1989*. IEEE Computer Society, 1989, pp. 14--23. [Online]. Available: https://doi.org/10.1109/LICS.1989.39155

[2] —, "Notions of computation and monads," *Inf. Comput.*, vol. 93, no. 1, pp. 55-92, 1991. [Online]. Available: https://doi.org/10.1016/0890-5401(91)90052-4

[3] N. Benton, "Categorical monads and computer programming," *LMS Impact150 Stories*, vol. 1, pp. 9–13, 2015.

[4] J. Power and E. P. Robinson, "Premonoidal categories and notions of computation," *Math. Struct. Comput. Sci.*, vol. 7, pp. 453–468, 1997.

[5] M. Maietti, P. Maneggia, V. De Paiva, and E. Ritter, "Relating categorical semantics for intuitionistic linear logic," *Applied Categorical Structures*, vol. 13, pp. 1–36, 01 2005.

[6] R. B. B. Lucyshyn-Wright, "Commutants for enriched algebraic theories and monads," *Appl. Categorical Struct.*, vol. 26, no. 3, pp. 559–596, 2018. [Online]. Available: https://doi.org/10.1007/s10485-017-9503-1

[7] R. Garner and I. L. Franco, "Commutativity," *Journal of Pure and Applied Algebra*, vol. 220, no. 5, pp. 1707–1751, may 2016. [Online]. Available: https://doi.org/10.1016%2Fj.jpaa.2015.09.003

[8] S. Staton and P. B. Levy, "Universal properties of impure programming languages," in *The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, Rome, Italy - January 23 - 25, 2013*, R. Giacobazzi and R. Cousot, Eds. *ACM*, 2013, pp. 179–192. [Online]. Available: https://doi.org/10.1145/2429069.2429091

[9] C. Führmann, "Direct models of the computational lambda-calculus," *Electronic Notes in Theoretical Computer Science*, vol. 20, pp. 245–292, 1999, mFPS XV, Mathematical Foundations of Programming Semantics, Fifteenth Conference. [Online]. Available: https://www.sciencedirect.com/science/article/pii/S1571066104800781

[10] D. McDermott and A. Mycroft, "Galois connecting call-by-value and call-by-name," 2022. [Online]. Available: https://arxiv.org/abs/2202.08246

[11] B. Jacobs, *Introduction to Coalgebra: Towards Mathematics of States and Observation*, ser. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016, vol. 59. [Online]. Available: https://doi.org/10.1017/CBO9781316823187

[12] G. M. Kelly, "A survey of totality for enriched and ordinary categories," *Cahiers de Topologie et Géométrie Différentielle Catégoriques*, vol. 27, pp. 109–132, 1986.

[13] W. F. Keigher, "Symmetric monoidal closed categories generated by commutative adjoint monads," *Cahiers de topologie et géométrie différentielle catégoriques*, vol. 19, no. 3, pp. 269–293, 1978.

[14] B. J. Day, "Construction of biclosed categories," Ph.D. dissertation, University of New South Wales PhD thesis, 1970.

[15] T. Jakl, D. Marsden, and N. Shah, "Generalizations of bilinear maps – technical report," 2022. [Online]. Available: https://arxiv.org/abs/2205.05382

[16] M. Hyland and J. Power, "The category theoretic understanding of universal algebra: Lawvere theories and monads," *Electr. Notes Theor. Comput. Sci.*, vol. 172, pp. 437–458, 04 2007.

[17] G. C. Wraith, *Algebraic Theories*. Aarhus universitet, Matematisk institut, 1970.

[18] C. Jones and G. D. Plotkin, "A probabilistic powerdomain of evaluations," in *Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), Pacific Grove, California, USA, June 5-8, 1989*. IEEE Computer Society, 1989, pp. 186–195. [Online]. Available: https://doi.org/10.1109/LICS.1989.39173

[19] C. Jones, "Probabilistic Non-determinism," Ph.D. dissertation, University of Edinburgh, UK, 1990. [Online]. Available: http://hdl.handle.net/1842/413

[20] M. Giry, "A categorical approach to probability theory," in *Categorical Aspects of Topology and Analysis*, B. Banaschewski, Ed. Berlin, Heidelberg: Springer Berlin Heidelberg, 1982, pp. 68–85.

[21] G. Gierz, K. H. Hofmann, K. Keimel, J. D. Lawson, M. Mislove, and D. S. Scott, *A compendium of continuous lattices*. Springer Science & Business Media, 2012.

[22] X. Jia, M. W. Mislove, and V. Zamdzhiev, "The central valuations monad (early ideas)," in *9th Conference on Algebra and Coalgebra in Computer Science, CALCO 2021, August 31 to September 3, 2021, Salzburg, Austria*, ser. LIPIcs, F. Gadducci and A. Silva, Eds., vol. 211. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021, pp. 18:1–18:5. [Online]. Available: https://doi.org/10.4230/LIPIcs.CALCO.2021.18

[23] X. Jia, B. Lindenhovius, M. W. Mislove, and V. Zamdzhiev, "Commutative monads for probabilistic programming languages," in *36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021*. IEEE, 2021, pp. 1–14. [Online]. Available: https://doi.org/10.1109/LICS52264.2021.9470611

[24] J. Goubault-Larrecq, X. Jia, and C. Théron, "A domain-theoretic approach to statistical programming languages," *CoRR*, vol. abs/2106.16190, 2021. [Online]. Available: https://arxiv.org/abs/2106.16190

[25] R. L. Crole, *Categories for Types*. Cambridge University Press, 1994.

[26] D. Scott, "Definitions by abstraction in axiomatic set theory," *Bull. Amer. Math. Soc*, vol. 61, no. 442, p. 1955, 1955.

[27] R. Street and R. Walters, "Yoneda structures on 2-categories," *Journal of Algebra*, vol. 50, no. 2, pp. 350–379, 1978.
A. *Proof of Proposition 14*

*Proof.* Let $(X, f)$ be a central cone and let $f' : X' \to TY'$ be a morphism. The following diagram:

<figure><img src="image_9.png" /></figure>

commutes because: (1) $\mathbf{C}$ is monoidal; (2) $\tau'$ is natural; (3) $\tau$ is natural; and (4) the pair $(X, f)$ is a central cone. Therefore, the morphism $f$ is central in the premonoidal sense.

For the other direction, if $f$ is central in $C_{\mathcal{T}}$, the following diagram:

<figure><img src="image_10.png" /></figure>

commutes because: (1) $\tau$ is natural; (2) $f$ is a central morphism; all remaining subdiagrams commute trivially. This shows the pair $(X, f)$ is a central cone. $\square$

**Lemma 68.** If $(X, f : X \to TY)$ is a central cone of $\mathcal{T}$ at $Y$, then for any $g : Z \to X$, it follows that $(Z, f \circ g)$ is a central cone of $\mathcal{T}$ at $Y$.

*Proof.* This is obtained by precomposing the definition of central cone by $g \otimes \text{id}$.

<figure><img src="image_11.png" /></figure>
commutes directly from the definition of central cone for $f$. □

**Lemma 69.** If $(X, f : X \to TY)$ is a central cone of $T$ at $Y$ then for any $g : Y \to Z$, it follows that $(X, Tg \circ f)$ is a central cone of $T$ at $Z$.

*Proof.* The naturality of $\tau$ and $\mu$ allow us to push the application of $g$ to the last postcomposition, in order to use the central property of $f$. In more details, the following diagram:

<figure><img src="image_12.png" /></figure>

commutes, because: (1) $f$ is a central cone, (2) $\tau'$ is natural, (3) $\tau$ is natural, (4) $\mu$ is natural (5) $\tau$ is natural, (6) $\tau'$ is natural, (7) $\mu$ is natural. □

**Lemma 70.** If $(Z, \iota)$ is a terminal central cone of $T$ at $X$, then $\iota$ is a monomorphism.

*Proof.* Let us consider $f, g : Y \to Z$ such that $\iota \circ f = \iota \circ g$; this morphism is a central cone at $X$ (Lemma 68), and since $(Z, \iota)$ is a terminal central cone, it factors uniquely through $\iota$. Thus $f = g$ and therefore $\iota$ is monic. □

## B. *Proof of Theorem 16*

*Proof.* First let us describe the functorial structure of $\mathcal{Z}$. Recall that $\mathcal{Z}$ maps every object $X$ to its terminal central cone at $X$. Let $f : X \to Y$ be a morphism. We know that $Tf \circ \iota_X : \mathcal{Z}X \to TY$ is a central cone according to Lemma 69. Therefore, we define $\mathcal{Z}f$ as the unique map such that the following diagram commutes:

<figure><img src="image_13.png" /></figure>

It follows directly that $\mathcal{Z}$ maps the identity to the identity, and that $\iota$ is natural. $\mathcal{Z}$ also preserves composition, which follows by the commutative diagram below.

<figure><img src="image_14.png" /></figure>
This proves that $\mathcal{Z}$ is a functor. Next, we describe its monad structure and after that we show that it is commutative.
The monadic unit $\eta_X$ is central, because it is the identity morphism in $\mathcal{Z}(C_\tau)$, thus it factors through $\iota_X$ to define $\eta_X^\mathcal{Z}$.

<figure><img src="image_15.png" /></figure>

Next, observe that, by definition, $\mu_X \circ \mathcal{T}\iota_X \circ \iota_{\mathcal{Z}X} = \iota_X \odot \iota_{\mathcal{Z}X}$, where $(- \odot -)$ indicates Kleisli composition. Since $\iota$ is central and Kleisli composition preserves central morphisms, it follows that this morphism factors through $\iota_X$ and we use this to define $\mu_X^\mathcal{Z}$ as in the diagram below.

<figure><img src="image_16.png" /></figure>

Again, by definition, $\tau_{A,B} \circ (A \otimes \iota_B) = A \otimes_r \iota_B$. Central morphisms are preserved by the premonoidal products (as we noted in Section III) and therefore, this morphism factors through $\iota_{A \otimes B}$ which we use to define $\tau_{A,B}^\mathcal{Z}$ as in the diagram below.

<figure><img src="image_17.png" /></figure>

Note that the last three diagrams are exactly those of a morphism of strong monads (see Definition 4).
Using the fact that $\iota$ is monic (see Lemma 70) we show that the following commutative diagram shows that $\eta^\mathcal{Z}$ is natural.

<figure><img src="image_18.png" /></figure>

(1) definition of $\eta^\mathcal{Z}$, (2) $\iota$ is natural, (3) $\eta$ is natural and (4) definition of $\eta^\mathcal{Z}$. Thus we have proven that for any $f: X \to Y$,
$\iota_Y \circ \mathcal{Z}f \circ \eta_X^\mathcal{Z} = \iota_Y \circ \eta_Y^\mathcal{Z} \circ f$. Besides, $\iota$ is monic, thus $\mathcal{Z}f \circ \eta_X^\mathcal{Z} = \eta_Y^\mathcal{Z} \circ f$ which proves that $\eta^\mathcal{Z}$ is natural. We will prove all
the remaining diagrams with the same reasoning.
The following commutative diagram shows that $\mu^Z$ is natural.

<figure><img src="image_19.png" /></figure>

(1) definition of $\mu^Z$, (2) $\iota$ is natural, (3) $\mu$ is natural, (4) $\iota$ is natural and (5) definition of $\mu^Z$.
The following commutative diagrams shows that $\tau^Z$ is natural.

<figure><img src="image_20.png" /></figure>

(1) definition of $\tau^Z$, (2) $\iota$ is natural, (3) $\tau$ is natural, (4) $\iota$ is natural and (5) definition of $\tau^Z$.

<figure><img src="image_21.png" /></figure>

(1) definition of $\tau^Z$, (2) $\iota$ is natural, (3) $\tau$ is natural, (4) $\iota$ is natural and (5) definition of $\tau^Z$.
The following commutative diagrams prove that $\mathcal{Z}$ is a monad.

<figure><img src="image_22.png" /></figure>

(1) and (2) involve the definition of $\mu^Z$ and the naturality of $\iota$ and $\mu^{\bar{Z}}$, (3) is by definition of monad, (4) definition of $\mu^Z$ and (5) also. (6) and (7) involve the definition of $\eta^Z$ and the naturality of $\iota$ and $\eta^{\bar{Z}}$, (8) is by definition of monad, (9) definition of $\mu^Z$ and (10) also.

$\mathcal{Z}$ is proven strong with very similar diagrams. The commutative diagram:

<figure><img src="image_23.png" /></figure>

proves that $\mathcal{Z}$ is a commutative monad, with (1) $\tau'^Z$ is natural, (2) definition of $\tau^Z$, (3) $\tau^Z$ is natural, (4) $\mathcal{C}$ is monoidal, (5) definition of $\tau'^{\bar{Z}}$, (6) $\iota$ is natural, (7) definition of $\mu^{\bar{Z}}$, (8) definition of $\tau^{\bar{Z}}$, (9) $\iota$ is central, (10) definition of $\tau'^{\bar{Z}}$, (11) $\iota$ is natural and (12) definition of $\mu^{\bar{Z}}$. $\square$

### C. Proof of Theorem 17

*Proof.* $\mathcal{I}$ corestricts as indicated follows easily: for any morphism $f: X \to \mathcal{Z}Y$, we have that $\mathcal{I}f = \iota_Y \circ f$ which is central by Lemma 68. Let us write $\hat{\mathcal{I}}$ for the corestriction of $\mathcal{I}$ to $Z(C_T)$. Next, to prove that $\hat{\mathcal{I}}: C_Z \to Z(C_T)$ is an isomorphism, we define the inverse functor $G: Z(C_T) \to C_Z$.

On objects, $G(X) \stackrel{\text{def}}{=} X$. To define its mapping on morphisms, observe that if $f: X \to TY$ is a central morphism (in the premonoidal sense), then $(X, f)$ is a central cone of $T$ at $Y$ (Proposition 14) and therefore there exists a unique morphism $f^Z: X \to \mathcal{Z}Y$ such that $\iota_Y \circ f^Z = f$; we define $Gf \stackrel{\text{def}}{=} f^Z$. The proof that $G$ is a functor is direct considering that any $f^Z$ is a morphism of central cones and that all components of $\iota$ are monomorphisms.

To show that $\hat{\mathcal{I}}$ and $G$ are mutual inverses, let $f: X \to TY$ be a morphism of $Z(C_T)$, i.e., a central morphism. Then, $\hat{\mathcal{I}}Gf = \iota_Y \circ f^Z = f$ by definition of morphism of central cones (see Definition 13). For the other direction, let $g: X \to \mathcal{Z}Y$ be a morphism in $\mathcal{C}$. Then, $\iota_Y \circ G\hat{\mathcal{I}}g = \iota_Y \circ (\iota_Y \circ g)^Z = \iota_Y \circ g$ by Definition 13 and thus $G\hat{\mathcal{I}}g = g$ since $\iota_Y$ is a monomorphism (Lemma 70). $\square$
D. *Proof of Theorem 18*

*Proof.*

(1 $\Rightarrow$ 2) : By Theorem 16 and Theorem 17.

(2 $\Rightarrow$ 3) : Let us consider the Kleisli left adjoint $\mathcal{J}^Z$ associated to the monad $\mathcal{Z}$. All our hypotheses can be summarised by the diagram

<figure><img src="image_24.png" /></figure>

where $\hat{\mathcal{I}}: \mathcal{C}_\mathcal{Z} \cong \mathcal{Z}(\mathcal{C}_\mathcal{T})$ is the corestriction of $\mathcal{I}$. This diagram commutes, because $\mathcal{Z}$ is a submonad of $\mathcal{T}$ (recall also that $\hat{\mathcal{J}}$ is the indicated corestriction of $\mathcal{J}$, see §III). Since $\hat{\mathcal{I}}$ is an isomorphism, then $\hat{\mathcal{J}} = \hat{\mathcal{I}} \circ \mathcal{J}^Z$ is the composition of two left adjoints and it is therefore also a left adjoint.

(3 $\Rightarrow$ 1) : Let $\mathcal{R} : \mathcal{Z}(\mathcal{C}_\mathcal{T}) \to \mathcal{C}$ be the right adjoint of $\hat{\mathcal{J}}$ and let $\varepsilon$ be the counit of the adjunction. We will show that the pair $(\mathcal{R}X, \varepsilon_X)$ is the terminal central cone of $\mathcal{T}$ at $X$.

First, since $\varepsilon_X$ is a morphism in $\mathcal{Z}(\mathcal{C}_\mathcal{T})$, it follows that it is central. Thus the pair $(\mathcal{R}X, \varepsilon_X)$ is a central cone of $\mathcal{T}$ at $X$. Next, let $\Phi : \mathcal{Z}(\mathcal{C}_\mathcal{T})[\hat{\mathcal{J}}Y, X] \cong \mathcal{C}[Y, \mathcal{R}X]$ be the natural bijection induced by the adjunction. If $f : Y \to \mathcal{T}X$ is central, meaning a morphism of $\mathcal{Z}(\mathcal{C}_\mathcal{T})$, the diagram below left commutes in $\mathcal{Z}(\mathcal{C}_\mathcal{T})$, or equivalently, the diagram below right commutes in $\mathcal{C}$:

<figure><img src="image_25.png" /></figure>

<figure><img src="image_26.png" /></figure>

Note that the pair $(Y, f)$ is equivalently a central cone for $\mathcal{T}$ at $X$ (by Proposition 14). Thus $f$ uniquely factors through the counit $\varepsilon_X : \mathcal{R}X \to \mathcal{T}X$ and therefore $(\mathcal{R}X, \varepsilon_X)$ is the terminal central cone of $\mathcal{T}$ at $X$. $\square$

E. *Proof of Proposition 25*

*Proof.* Given any strong monad on $\mathcal{C}$, we first show that the co-restriction of the Kleisli inclusion is co-continuous. We consider an initial co-cone $\epsilon : \Delta_c \Rightarrow J$ over a diagram $J : D \to \mathcal{C}$ in $\mathcal{C}$. Its image $\hat{\mathcal{J}}\epsilon : \Delta_c \Rightarrow \hat{\mathcal{J}} \circ J$ is a co-cone in $\mathcal{Z}(\mathcal{C}_\mathcal{T})$, we will show that it is initial. We consider another co-cone $\epsilon' : \Delta_{c'} \Rightarrow \hat{\mathcal{J}} \circ J$ in $\mathcal{Z}(\mathcal{C}_\mathcal{T})$. Since $\mathcal{J}$ is a left adjoint, it is co-continuous and then $\mathcal{J}\epsilon : \Delta_c \Rightarrow \mathcal{J} \circ J$ is an initial co-cone in $\mathcal{C}_\mathcal{T}$. So there is a unique arrow $h : c \to c'$ in $\mathcal{C}_\mathcal{T}$ such that $h \circ \mathcal{J}\epsilon = \epsilon'$. The question is to show that $h$ also is in $\mathcal{Z}(\mathcal{C}_\mathcal{T})$, in other words, that the following diagram commutes for all $f : X \to Y$:

<figure><img src="image_27.png" /></figure>

$\epsilon$ is an initial co-cone in $\mathcal{C}$ so, since the functors $- \otimes X$ are assumed to be co-continuous, $\mathcal{J}(\epsilon \otimes X)$ also is an initial co-cone in $\mathcal{C}_\mathcal{T}$. Its components are then jointly epic and checking the commutativity of the diagram below amounts to check the commutativity of the following diagrams for each components:
<figure><img src="image_28.png" /></figure>

Since, the composition $f \circ \mathcal{J}(g)$ in $C_T$ corresponds to $f \circ g$ in $C$, this is equivalent to the following diagram in $C$:

<figure><img src="image_29.png" /></figure>

Where: (1) is the definition of $h$, (2) is the exchange law, (3) is the naturality of the strength, (4) is again the definition of $h$ together with functoriality of $\mathcal{T}(- \otimes Y)$, and (5) is the fact that $\epsilon'_A$ is by definition central.

We can then conclude that $h$ is central and so that the co-restriction $\hat{\mathcal{J}}$ is co-continuous.

Then by the adjoint functor theorem for total categories [27], $\hat{\mathcal{J}}$ is a left adjoint, and by Theorem 18 it follows that the corresponding strong monad is centralisable. $\square$

### F. Proof of Theorem 35

#### Proof.

(1 $\Rightarrow$ 2) : The proof of Th. 17 contains the necessary elements for this proof. In details, we know that all the components of $\iota$ are central, and we also know that precomposing a central morphism keeps being central (see Lemma 68).

(2 $\Rightarrow$ 1) : The hypothesis ensures that $\hat{\mathcal{I}}(id_X) = \iota_X$ is central.

The diagram (2) in §B proves that the centre of a centralisable monad is commutative. Assuming (1) – or (2) – is true, then the same diagram replacing $\mathcal{Z}$ by $S$ proves that $S$ is a commutative monad.

(1 $\Rightarrow$ 3) : Moreover, each $\iota_X^S : SX \Rightarrow TX$ factorises through the terminal central cone $\iota_X^{\mathcal{Z}}$. A strong monad morphism $S \Rightarrow \mathcal{Z}$ arises from those factorisations.

(3 $\Rightarrow$ 1) : Let us write $\mathcal{Z}$ the centre of $\mathcal{T}$, $\iota_S^S : S \Rightarrow \mathcal{Z}$ and $\iota^{\mathcal{Z}} : \mathcal{Z} \Rightarrow \mathcal{T}$ the submonad morphisms. The components of $\iota^{\mathcal{Z}}$ are terminal central cones, and are in particular central, so $\iota^{\mathcal{Z}} \circ \iota^S$ is also central by Lemma 68. Thus the components of the submonad morphism from $S$ to $\mathcal{T}$ are central. $\square$

### G. Proof of Lemma 58

**Proof.** Suppose given two morphisms $f : A \to B, g : B \to C$, and a choice $[x : A' \vdash f' : B'_f] = f$ and $[y : B'_g \vdash g' : C'] = g$. Note that $B = [B'_f] = [B'_g]$, and in particular $y : B'_f \vdash g' : C'$ is derivable with $[y : B'_g \vdash g' : C'] = [y : B'_f \vdash g' : C']$. Thus, $x : A' \vdash g'[f'/y] : C'$ is derivable. We then prove that the choice $[x : A' \vdash f' : B'_f] = f$ and $[y : B'_f \vdash g' : C'] = g$ does not matter. We consider now new term judgments for some terms $f''$ and $g''$ such that $[x : A' \vdash f' : B'_f] = [x : A'' \vdash f'' : B''_f]$ and $[y : B'_f \vdash g' : C'] = [y : B''_f \vdash g'' : C'']$. By definition, $[A'] = [A''], [B'_f] = [B''_f]$ and $[C'] = [C'']$, and we wish to prove that $[x : A' \vdash g'[f'/y] : C'] = [x : A'' \vdash g''[f''/y] : C'']$.

$$ \begin{array}{ccc} \begin{array}{c} x : A, y : B' \vdash g' : C' \\ \hline x : A' \vdash f' : C' \end{array} & \begin{array}{c} x : A' \vdash \lambda y B'_f . g' : C' \\ \hline x : A' \vdash f' = f'' : C' \end{array} & \begin{array}{c} x : A', y : B'' \vdash g'' : C' \\ \hline x : A' \vdash f'' : B''_f \end{array} \\ \begin{array}{c} x : A', y : B'_f \vdash g' : C' \\ \hline x : A' \vdash g'[f'/y] = (\lambda y B'_f . g') f' : C' \end{array} & (\lambda, \beta) & (\lambda, \beta) \\ \hline \begin{array}{c} x : A' \vdash g'[f'/y] = g''[f''/y] : C' \\ \hline x : A' \vdash (\lambda y B'_f . g') f' = g''[f''/y] : C' \end{array} & (\text{trans}) & (\text{trans}) \end{array} $$
Thus, it is safe to define $g \circ f$ as $[x : A' \vdash g'[f'/y] : C']$.

Given a choice of $A'$ in $[A]$, $[x : A' \vdash x : A']$ is the identity morphism for the type $[A]$. Considering $[x : A' \vdash f : B']$ and $[y : C' \vdash g : A']$, we have:

$$[x : A' \vdash f : B'] \circ [x : A' \vdash x : A'] = [x : A' \vdash f[x/x] : B'] = [x : A' \vdash f : B'],$$

and

$$[x : A' \vdash x : A'] \circ [y : C' \vdash g : A'] = [y : C' \vdash x[g/x] : A'] = [y : C' \vdash g : A'],$$

One can notice that, for example, $x : A' \vdash f : B'$ has conveniently be chosen with the right type $A'$. It is authorised, because we have proven above that the choice of representative does not matter in composition matters.

The cartesian closure is a usual result for a syntactic category from a simply-typed $\lambda$-calculus, and it is preserved in our context. □

## H. Proof of Lemma 61

*Proof of Lemma 61.* In all the following proofs, we consider convenient members of equivalence classes, because the choice of representative does not change the result, thanks to Lemma 58.

$\iota$ is a submonad morphism:

$$
\begin{align*}
& \stackrel{\iota_A \circ \eta_A^S}{=} && \text{def.} \\
& \stackrel{[y : SA \vdash \iota y : TA] \circ [x : A \vdash \text{ret}_S x : SA]}{=} && \text{comp.} \\
& \stackrel{[x : A \vdash \iota \text{ret}_S x : TA]}{=} && (\iota S. \text{ret}) \\
& \stackrel{[x : A \vdash \text{ret}_T x : TA]}{=} && \text{def.} \\
& \stackrel{\eta_A^T}{=} && \text{comp.} \\
& \stackrel{[z : TTA \vdash \text{do}_T y \leftarrow z; y : TA] \circ [y' : TSA \vdash \text{do}_T x \leftarrow y'; \text{ret}_T \iota x : TTA] \circ [x' : SSA \vdash \iota x' : TSA]}{=} && (T. \text{assoc}) \\
& \stackrel{[x' : SSA \vdash \text{do}_T y \leftarrow (\text{do}_T x \leftarrow \iota x'; \text{ret}_T \iota x); y : TA]}{=} && (T. \beta) \\
& \stackrel{[x' : SSA \vdash \text{do}_T x \leftarrow \iota x'; \iota x : TA]}{=} && (\iota S. \text{comp}) \\
& \stackrel{[x' : SSA \vdash \iota \text{do}_S x \leftarrow x'; x : TA]}{=} && \text{comp.} \\
& \stackrel{[y : SA \vdash \iota y : TA] \circ [x' : SSA \vdash \text{do}_S x \leftarrow x'; x : SA]}{=} && \text{def.} \\
& \stackrel{\iota_A \circ \mu_A^S}{=} && \text{comp.} \\
& \stackrel{[z : S(A \times B) \vdash \iota x : T(A \times B)] \circ [z : A \times SB \vdash \text{do}_S y \leftarrow \pi_2 z; \text{ret}_S \langle \pi_1 z, y \rangle : S(A \times B)]}{=} && (\iota S. \text{comp}) \\
& \stackrel{[z : A \times SB \vdash \iota (\text{do}_S y \leftarrow \pi_2 z; \text{ret}_S \langle \pi_1 z, y \rangle) : T(A \times B)]}{=} && (\iota S. \text{comp}) \\
& \stackrel{[z : A \times SB \vdash \text{do}_T y \leftarrow \iota \pi_2 z; \iota \text{ret}_S \langle \pi_1 z, y \rangle : T(A \times B)]}{=} && (\iota S. \text{ret}) \\
& \stackrel{[z : A \times SB \vdash \text{do}_T y \leftarrow \iota \pi_2 z; \text{ret}_T \langle \pi_1 z, y \rangle : T(A \times B)]}{=} && (\times. \beta) \\
& \stackrel{[z : A \times SB \vdash \text{do}_T y \leftarrow \pi_2 \langle \pi_1 z, \iota \pi_2 z \rangle; \text{ret}_T \langle \pi_1 \langle \pi_1 z, \iota \pi_2 z \rangle, y \rangle : T(A \times B)]}{=} && \text{comp.} \\
& \stackrel{[x : A \times TB \vdash \text{do}_T y \leftarrow \pi_2 x; \text{ret}_T \langle \pi_1 x, y \rangle : T(A \times B)] \circ [z : A \times SB \vdash \langle \pi_1 z, \iota \pi_2 z \rangle : A \times TB]}{=} && \text{def.}
\end{align*}
$$

$\iota$ is a monomorphism because of the $(\iota.\text{mono})$ rule.
Finally, $\mathcal{Z}$ is a central submonad of $\mathcal{T}$:

$$
\begin{align*}
& \mathrm{dst}_{A,B} \circ (\iota \times \mathcal{T}B) \\
\mathrm{def.+comp.} & \quad [z : \mathcal{S}A \times \mathcal{T}B \vdash \mathrm{do}_{\mathcal{T}} x \leftarrow (\mathrm{do}_{\mathcal{T}} y \leftarrow \iota \pi_1 z; \mathrm{ret}_{\mathcal{T}} (\mathrm{do}_{\mathcal{T}} y' \leftarrow \pi_2 z; \mathrm{ret}_{\mathcal{T}} \langle y, y' \rangle)); x : \mathcal{T}(A \times B)] \\
(\mathcal{T}.\mathrm{assoc}) & \quad [z : \mathcal{S}A \times \mathcal{T}B \vdash \mathrm{do}_{\mathcal{T}} y \leftarrow \iota \pi_1 z; \mathrm{do}_{\mathcal{T}} x \leftarrow \mathrm{ret}_{\mathcal{T}} (\mathrm{do}_{\mathcal{T}} y' \leftarrow \pi_2 z; \mathrm{ret}_{\mathcal{T}} \langle y, y' \rangle); x : \mathcal{T}(A \times B)] \\
(\mathcal{T}.\beta) & \quad [z : \mathcal{S}A \times \mathcal{T}B \vdash \mathrm{do}_{\mathcal{T}} y \leftarrow \iota \pi_1 z; \mathrm{do}_{\mathcal{T}} y' \leftarrow \pi_2 z; \mathrm{ret}_{\mathcal{T}} \langle y, y' \rangle : \mathcal{T}(A \times B)] \\
(S.\mathrm{central}) & \quad [z : \mathcal{S}A \times \mathcal{T}B \vdash \mathrm{do}_{\mathcal{T}} y' \leftarrow \pi_2 z; \mathrm{do}_{\mathcal{T}} y \leftarrow \iota \pi_1 z; \mathrm{ret}_{\mathcal{T}} \langle y, y' \rangle : \mathcal{T}(A \times B)] \\
(\mathcal{T}.\beta) & \quad [z : \mathcal{S}A \times \mathcal{T}B \vdash \mathrm{do}_{\mathcal{T}} y' \leftarrow \pi_2 z; \mathrm{do}_{\mathcal{T}} x \leftarrow \mathrm{ret}_{\mathcal{T}} (\mathrm{do}_{\mathcal{T}} y \leftarrow \iota \pi_1 z; \mathrm{ret}_{\mathcal{T}} \langle y, y' \rangle); x : \mathcal{T}(A \times B)] \\
(\mathcal{T}.\mathrm{assoc}) & \quad [z : \mathcal{S}A \times \mathcal{T}B \vdash \mathrm{do}_{\mathcal{T}} x \leftarrow (\mathrm{do}_{\mathcal{T}} y' \leftarrow \pi_2 z; \mathrm{ret}_{\mathcal{T}} (\mathrm{do}_{\mathcal{T}} y \leftarrow \iota \pi_1 z; \mathrm{ret}_{\mathcal{T}} \langle y, y' \rangle)); x : \mathcal{T}(A \times B)] \\
\mathrm{comp.+def.} & \quad \mathrm{dst}'_{A,B} \circ (\iota \times \mathcal{T}B)
\end{align*}
$$

□

I. *Proof of Theorem 66*

*Proof.* Given $\mathbf{C}$ an object of $\mathbf{Mod}(\mathbf{CSC})$, we wish to prove that $\mathbf{C}$ is equivalent to $\mathbf{SL}(\mathbf{C})$. To do so, we introduce two strict cartesian closed functors $F : \mathbf{C} \to \mathbf{SL}(\mathbf{C})$ and $G : \mathbf{SL}(\mathbf{C}) \to \mathbf{C}$, such that there are isomorphisms $\mathrm{Id} \Rightarrow \mathrm{GF}$ and $\mathrm{FG} \Rightarrow \mathrm{Id}$.

* $F$ maps an object $A$ of $\mathbf{C}$ to $[A^*]$. It maps a morphism $f : A \to B$ to $[x : A^* \vdash c_f x : B^*]$.

* $G$ maps an object $[A]$ to $[[A]]$, the interpretation of the type $A$ in $\mathbf{C}$, because the choice of representative of $[A]$ does not change the interpretation. $G$ maps a morphism $[x : A \vdash g : B]$ to $[[x : A \vdash g : B]]$.

Then it is easy to check that $\mathrm{GF} = \mathrm{Id}$ and $\mathrm{FG} = \mathrm{Id}$. Therefore $\mathbf{C}$ is isomorphic to $\mathbf{SL}(\mathbf{C})$.

Furthermore, given a CSC-theory $\mathfrak{T}$, we wish to prove that $\mathfrak{T}$ is equivalent to $\mathbf{LS}(\mathfrak{T})$. To do so, we introduce two CSC-translations $V : \mathfrak{T} \to \mathbf{LS}(\mathfrak{T})$ and $W : \mathbf{LS}(\mathfrak{T}) \to \mathfrak{T}$ such that there are isomorphic CSC-translation transformations $VW \Rightarrow \mathrm{Id}$ and $\mathrm{Id} \Rightarrow WV$.

* $V$ maps a type $A$ in $\mathfrak{T}$ to $[A]^*$, and term judgements $x : A \vdash f : B$ to $x : [A]^* \vdash c_{[x:A \vdash f:B]} x : [B]^*$.

* Observe that for each type $A$ in $\mathbf{LS}(\mathfrak{T})$, there is a type of the form $[B]^*$ such that $\vdash A = [B]^* : \mathrm{type}$ in $\mathbf{LS}(\mathfrak{T})$. We define $W(A) \stackrel{\mathrm{def}}{=} B$ (the choice of $B$ does not matter). Then, for term constants we define $W(\vdash c_{[x:A \vdash f:B]} : B^*) \stackrel{\mathrm{def}}{=} (\vdash \lambda x.f : A \to B)$ and this uniquely determines the action of $W$ on the remaining terms (the choice of $f$ does not matter).

Given a type $A$ in $\mathfrak{T}$, $x : W(V(A)) \vdash x : A$ is derivable in $\mathfrak{T}$ because $\vdash W(V(A)) = A : \mathrm{type}$, and $\alpha_A : x : W(V(A)) \vdash x : A$ defines an isomorphic CSC-translation transformation: postcomposing (resp. composing) it with $x : A \vdash x : W(V(A))$ gives $x : W(V(A)) \vdash x : W(V(A))$ (resp. $x : A \vdash x : A$). Given a type $A'$ in $\mathbf{LS}(\mathfrak{T})$, the same is true for $\beta_{A'} = x : A' \vdash x : V(W(A'))$. Thus, for every CSC-theory, $\mathfrak{T}$ is equivalent to $\mathbf{LS}(\mathfrak{T})$. $\square$