strong monads

A Strong Monad is Monoid in the Category of Strong Endofunctors

We encountered the notion of strength when we introduced strong monads. Strength has turned out to be an important idea, for example in discussion of commutative monads which underpin a lot of monad theory.

As strength is so important, we are going to back up, and examine it in a bit more detail, eventually arriving at a concise definition of strong monad.

Our ulterior motive is to set up some background on strong natural transformations so we can learn more about commutative, affine, relevant and cartesian monads in future posts.

Strong functors

Recall, a strength for an endofunctor

F : \mathcal{C} \rightarrow \mathcal{C}

on a monoidal category is a natural transformation

\mathsf{st} : X \otimes F(Y) \Rightarrow F (X \otimes Y)

compatible with the monoidal left unitor and associator, in that

F \lambda \cdot \mathsf{st} = \lambda

and

F \alpha \cdot \mathsf{st} = \mathsf{st} \cdot \mathsf{id} \otimes \mathsf{st} \cdot \alpha

A strong functor is a pair

(F, \mathsf{st} : X \otimes F(Y) \Rightarrow F(X \otimes Y))

consisting of an endofunctor and a choice of strength.

Strong natural transformations

We now introduce the key notion of this post. A strong natural transformation

\varphi : (F,\mathsf{st}) \rightarrow (G,\mathsf{st})

is an ordinary natural transformation

\varphi : F \Rightarrow G

which commutes with strengths. That is:

\mathsf{st} \cdot \mathsf{id} \otimes \varphi = \varphi \cdot \mathsf{st}

We will overload the symbol $\mathsf{st}$ for any strength to avoid a proliferation of symbols.

Categorical Structure

For a monoidal category $\mathcal{C}$ there is a category $\mathsf{Strong(\mathcal{C})}$ with:

Objects: Strong endofunctors on $\mathcal{C}$
Morphisms: Strong natural transformations, with composition and identities as for ordinary natural transformations.

Checking the required closure properties of strong natural transformations is a routine exercise.

Monoidal Structure

For a monoidal category $\mathcal{C}$ , there is a strict monoidal structure on $\mathsf{Strong}(\mathcal{C})$ with unit

(\mathsf{Id}_{\mathcal{C}}, \mathsf{id})

The tensor product on objects is:

(G,\mathsf{st}) \circ (F, \mathsf{st}) = (G \circ F, X \otimes GF(Y) \xrightarrow{\mathsf{st}}G(X \otimes F(Y)) \xrightarrow{G \mathsf{st}} GF(X \otimes Y))

For morphisms

\varphi : (F_1, \mathsf{st}) \Rightarrow (F_2, \mathsf{st}) \quad\text{and}\quad \gamma : (G_1, \mathsf{st}) \Rightarrow (G_2, \mathsf{st})

their tensor product is the usual composition of natural transformations

\gamma \circ \varphi : G_1 \circ F_1 \Rightarrow G_2 \circ F_2

Verifying the monoidal structure is routine, if fiddly, exercise in applying the definitions.

When we previously discussed strong monads, the definition was only sketched, with detailed deferred to other sources. We are now in a position to give a precise definition of what a strong monad is

A strong monad is a monoid in the category of strong endofunctors.

This is easy to remember, as it is a small variation on the internets favourite meme about monads:

A monad is a monoid in the category of endofunctors.

We just sprinkle the term strong over the slogan for monads, and we get the corresponding slogan for strong monads.

It is not hard to see that there is a strict monoidal forgetful functor to the ordinary category of endofunctors

\mathsf{Strong}(\mathcal{C}) \rightarrow [\mathcal{C}, \mathcal{C}]

so every strong monad is an ordinary monad, along with some additional strength data.

Unpacking the Definition

If we unpack the concise definition above, a strong monad is:

A strong endofunctor $(\mathbb{T} : \mathcal{C} \rightarrow \mathcal{C}, \mathsf{st})$
A unit strong natural transformation $(\mathsf{Id}, \mathsf{id}) \Rightarrow (\mathbb{T}, \mathsf{st})$
A multiplication strong natural transformation $(\mathbb{T},\mathsf{st}) \circ (\mathbb{T}, \mathsf{st}) \Rightarrow (\mathbb{T}, \mathsf{st})$

Such that the usual unit and multiplication axioms hold.

Applying the Definition

To show that this is not just an exercise in meme generation, we can apply the definition above to deduce what a distributive law of strong monad $(\mathbb{T}, \mathsf{st})$ over strong monad $(\mathbb{S}, \mathsf{st})$ should be. We require a strong natural transformation:

\lambda : (\mathbb{T}, \mathsf{st}) \circ (\mathbb{S}, \mathsf{st}) \Rightarrow (\mathbb{S}, \mathsf{st}) \circ (\mathbb{T}, \mathsf{st})

satisfying formally identical equations to those of an ordinary distributive law. Unpacking this, $\lambda$ must be an ordinary distributive law, also satisfying:

\mathbb{S}(\mathsf{st}) \cdot \mathsf{st} \cdot 1 \otimes \lambda = \lambda \cdot \mathbb{T}(\mathsf{st}) \cdot \mathsf{st}

This yields the same definition given in Jacobs “Semantics of Weakening and Contraction” for example.

Summary

By identifying the correct mathematical structure, we have arrived at a concise definition of strong monad paralleling one of the familiar definitions for monads.

Inquisitive readers may wonder if any of the other definitions transfer over cleanly. For example, can we define a strong monad as a monad in a different 2-category? The answer is not yet (except in a rather degenerate way)! As with most things, there is a more general definition of strength, which amongst other things allows us to move away from the restriction to endofunctors that has been conspicuous in this post. Our current level of generality will be sufficient for some forthcoming posts. We may return to this topic on a later occasion. Details can be found on the NLab for example.

Other Monad Strengths

Last time, we saw the notion of strength for a monad. These were natural transformations

$A \otimes \mathbb{T}(B) \rightarrow \mathbb{T}(A \otimes B)$

which interact well with the monoidal and monad structure. As was mentioned last time, there are other ways we might consider commuting a functor with a monoidal structure. The obvious first choice is to consider a natural transformation of type

$\mathbb{T}(A) \otimes B \rightarrow \mathbb{T}(A \otimes B)$

again, interacting sensibly with the monoidal and monad structure (as before, we leave the details of what this means aside, to concentrate on the main ideas). Such a natural transformation is called a left-strength, denoted $\mathsf{st}'$ . The strength is often referred to as a right-strength for emphasis.

Example: If $\mathcal{V}$ is a symmetric monoidal category we can build a right-strength from a left-strength

$\mathsf{st}_{A,B} : A \otimes \mathbb{T}(B) \rightarrow \mathbb{T}(A \otimes B)$

as the composite:

$\mathbb{T}(A) \otimes B \xrightarrow{\sigma_{\mathbb{T}(A),B}} B \otimes \mathbb{T}(A) \xrightarrow{\mathsf{st}_{B,A}} \mathbb{T}(B \otimes A) \xrightarrow{\mathbb{T}(\sigma_{B,A})} \mathbb{T}(A \otimes B)$

Here $\sigma$ is the symmetry isomorphism from the symmetric monoidal structure. Intuitively, we just swap the inputs, use the strength and swap them back again.

As we know every $\mathsf{Set}$ monad is strong in a unique way, so it also has a unique left-strength. For example, the left-strength for the list monad acts as follows:

$([a_1,\ldots,a_n],b) \mapsto [(a_1,b),\ldots,(a_n,b)]$

Unsurprisingly, the left-strength for the powerset is very similar, visually we just swap square (list formation) brackets for curly (set formation) brackets.

$(\{a_1,\ldots,a_n\},b) \mapsto \{(a_1,b),\ldots,(a_n,b)\}$

We can consider left-strengths beyond symmetric monoidal categories, as their definition does not require the existence of a right-strength. In the cases that will be of interest to us, it will be the interplay between left and right strengths that will matter. To keep things simple, we will assume we are working in a symmetric monoidal category, so the left-strength can be derived from the right-strength (or vice-versa), as in the example above. (To move beyond this setting, we would need to assume further compatibility conditions between any choice of left and right strength, which are automatic when one is derived from the other via a monoidal symmetry.)

Once we have a right-strength $\mathsf{st}$ and a left-strength $\mathsf{st}'$ , we can build a natural transformation of type $\mathbb{T}(A) \otimes \mathbb{T}(B) \rightarrow \mathbb{T}(A \otimes B)$ . In fact, there are two ways we can do this, either by applying the right-strength first:

$\mathsf{dst} = \mathbb{T}(A) \otimes \mathbb{T}(B) \xrightarrow{\mathsf{st}_{A,B}} \mathbb{T}(\mathbb{T}(A) \otimes B) \xrightarrow{\mathbb{T}(\mathsf{st}'_{A,B})} \mathbb{T}^2(A\otimes B) \xrightarrow{\mu_{A \otimes B}} \mathbb{T}(A \otimes B)$

or applying the left-strength first:

$\mathsf{dst}' = \mathbb{T}(A) \otimes \mathbb{T}(B) \xrightarrow{\mathsf{st}'_{A,B}} \mathbb{T}(A \otimes \mathbb{T}(B)) \xrightarrow{\mathbb{T}(\mathsf{st}_{A,B})} \mathbb{T}^2(A \otimes B) \xrightarrow{\mu_{A \otimes B}} \mathbb{T}(A \otimes B)$

Both these composites are referred to as double strengths. Whenever we see two composites of the same type in category theory, it is natural to consider if they are always the same.

Example: For the list monad, we have:

$\mathsf{dst}([a,b],[c,d]) = [(a,c),(b,c),(a,d),(b,d)]$

whereas

$\mathsf{dst}'([a,b],[c,d]) = [(a,c),(a,d),(b,c),(b,d)]$

notice the difference in the order of the middle two elements.

On the other hand, for the powerset monad, essentially because there is no ordering in subsets:

$\mathsf{dst}(\{a,b\},\{c,d\}) = \mathsf{dst}'(\{a,b\},\{c,d\}) = \{(a,c),(b,c),(a,d),(b,d) \}$

This is not an isolated example, for the powerset monad $\mathsf{dst} = \mathsf{dst}'$ .

The previous examples show us that in general $\mathsf{dst} \neq \mathsf{dst}'$ , but the two composites may agree for some monads. This question, and its implications are another key topic in the theory of monads. We shall begin exploring the details in the next post.

A Note on Terminology

An earlier version of this post used the term costrength for what is termed a left-strength above. This terminology does not align well with the conventional use of “co” in category theory. Thanks to @varkor on mathstodon for persuading me that I should move to the more modern terminology.

There is also a discussion about this terminology on the NLab.

Strong Monads

Strong monads, the topic of this post, are a somewhat technical looking topic at first glance, requiring more definitions and machinery than we have seen up until now. Unfortunately, they are key to some more interesting topics, both mathematically and in terms of computer science application. As usual when dealing with new abstract ideas, it is useful to focus on intuitions and examples to get a feeling for the formal definitions. This post is longer than might be ideal, but there are plenty of examples.

For those interested in the technical details I skip, some recommended reading:

Monoidal categories: “Categories for the Working Mathematician” by Mac Lane has a very readable account of monoidal categories, despite its reputation for requiring a lot of mathematical background.
Enriched categories: Both volume 2 of Borceux’s “Handbook of Categorical Algebra”, and Riehl’s “Categorical Homotopy Theory” have brief introductions to monoidal categories, to set up a concise introduction to enriched category theory. The standard reference for enriched category theory is Kelly’s “Basic Concepts of Enriched Category Theory”, which also contains the necessary background on monoidal categories. This book can be difficult in places, but the material we require is covered at a reasonable pace.

Monoidal Categories

A monoidal category is a category $\mathcal{V}$ with a monoidal product bifunctor, typically denoted $\otimes$ , and a unit object, $I$ . Intuitively, this is a generalization of the notion of monoid from sets to categories. There are isomorphisms

$\lambda : I \otimes A \rightarrow A \qquad \rho : A \otimes I \rightarrow A$ ,

natural in $A$ , and referred to as the left and right unitor respectively. These encode that $I$ acts as a unit for the multiplication, up to isomorphism. There are also associator isomorphisms:

$\alpha : (A \otimes B) \otimes C \rightarrow A \otimes (B \otimes C)$ ,

natural in $A, B, C$ , encoding associativity up to isomorphism. The unitors and associator are required to satisfy some compatibility equations (referred to as coherence conditions). We won’t need the details, but they can be found in any standard category theory reference.

A symmetric monoidal category is a monoidal category with a further symmetry isomorphisms encoding commutativity up to isomorphism:

$\sigma : A \otimes B \rightarrow B \otimes A$

natural in $A,B$ . Again, the symmetry is required to satisfy some coherence conditions (equations) with respect to the other structure. Finally, a (symmetric) monoidal closed category is a (symmetric) monoidal category such that for each object $A$ , there is an adjunction:

$(-) \otimes A \dashv A \multimap (-)$

Example: Any category $\mathcal{C}$ with products is a symmetric monoidal category, with

$A \otimes B = A \times B \qquad I = 1$

The left and right unitors, associator and symmetry are the “obvious” canonical maps induced by the universal property of products. If $\mathcal{C}$ is Cartesian closed, then it is symmetric monoidal closed, with $A \multimap (-)$ given by the exponential $A \Rightarrow (-)$ .

In particular, the category $\mathsf{Set}$ is symmetric monoidal closed with monoidal product given by Cartesian products, and $A \multimap (-)$ given by the function space functor $A \Rightarrow (-)$ . This is the motivating example for much of what follows, and of practical interest in algebraic examples we shall see later. When working with $\mathsf{Set}$ , if not otherwise stated the monoidal structure is taken to be the Cartesian product structure.

Strength

For a monoidal category $\mathcal{V}$ , and endofunctor $T: \mathcal{V} \rightarrow \mathcal{V}$ , a strength (sometimes referred to as a tensorial strength) for $T$ is a natural transformation

$\mathsf{st}_{A,B} : A \otimes T(B) \rightarrow T(A \otimes B)$

which satisfies two coherence conditions with respect to the monoidal structure. A strong functor is a functor with a chosen strength. A strong monad is monad $\mathbb{T}$ with a strong underlying endofunctor, satisfying additional coherence conditions with respect to the monad unit and multiplication. Again, the actual coherence conditions can be found in standard sources, we shall focus on examples and intuitions.

Example: The list and powerset monads are both strong in a unique way, with strengths:

$(a, [b_1,\ldots,b_n]) \mapsto [(a,b_1),\ldots,(a,b_n)]$

$(a, \{ b_1,\ldots, b_n \}) \mapsto \{ (a,b_1), \ldots, (a,b_n) \}$

We shall shortly see that form (and uniqueness) of the strengths for the $\mathsf{Set}$ monads in the previous example are in no way special.

So a crude first sketch of a strength is that it is a well-behaved way of commuting an endofunctor and a monoidal product. You may notice that there are other ways you might imagine commuting an endofunctor with a monoidal product. We shall return to that thought in later posts.

To get a more principled mathematical perspective on strength, unfortunately we need to introduce further abstract machinery.

Enriched Categories

Enriched category theory is a large and potentially complex topic. Fortunately we will only need a few of the basic definitions, and no deep theory. The idea of an enriched category is that often for a category $\mathcal{C}$ , the homsets $\mathcal{C}(A,B)$ carry additional mathematical structure, and this structure interacts well with composition. For example:

Example: The homsets in the category $\mathsf{Pre}$ of preorders and monotone maps actually carry a natural pointwise order:

$f \leq g \Leftrightarrow \forall a. f(a) \leq g(a)$ .

This structure satisfies:

$f_1 \leq f_2 \;\wedge\; g_1 \leq g_2 \quad\Rightarrow\quad g_1 \circ f_1 \leq g_2 \leq f_2$

when the composites are well-defined. So the homsets are actually $\mathsf{Pre}$ -objects, and the composition maps are $\mathsf{Pre}$ -morphisms

$\mathsf{Pre}(B,C) \times \mathsf{Pre}(A,B) \rightarrow \mathsf{Pre}(A,B)$

A close relative of the previous example is the following:

Example: The homsets of the category of all (small) categories $\mathsf{Cat}$ are themselves categories, with morphisms the natural transformations. Furthermore, the composition maps are bifunctors

$\mathsf{Set}(B,C) \times \mathsf{Set}(A,B) \rightarrow \mathsf{Set}(A,C)$

An important trivial example is the following:

Example: The homsets of the category $\mathsf{Set}$ are $\mathsf{Set}$ -objects, and the composition maps are $\mathsf{Set}$ -morphisms

$\mathsf{Set}(B,C) \times \mathsf{(Set}(A,B) \rightarrow \mathsf{Set}(A,B)$

Finally, a slightly different example, which motivates the level of generalization of the formal definition.

Example: The homsets of the category of Abelian groups $\mathsf{Ab}$ can be given the structure of Abelian groups pointwise. With this structure, the composition maps satisfy:

$(g_1 + g_2) \circ f = (g_1 \circ f) + (g_2 \circ f) \qquad 0 \circ f = 0$

and the dual conditions for precomposition. This is not the same as saying the composition maps are $\mathsf{Ab}$ morphisms:

$\mathsf{Ab}(B,C) \times \mathsf{Ab}(A,B) \rightarrow \mathbb{Ab}(A,C)$

This temporarily breaks the pattern with the previous examples. However, there is a monoidal structure on $\mathsf{Ab}$ such that the composition maps are $\mathsf{Ab}$ -morphisms

$\mathsf{Ab}(B,C) \otimes \mathsf{Ab}(A,B) \rightarrow \mathsf{Ab}(A,C)$

In fact this monoidal structure arises via some rather beautiful monad theory, which we will hopefully get to in later posts.

The final example motivates defining enriched categories so that the hom objects can live in monoidal categories.

For a monoidal category $\mathcal{V}$ , a $\mathcal{V}$ -enriched category $\mathcal{C}$ has:

A collection of objects $A,B,\ldots$
For each pair of objects $A,B$ , a hom object $\mathcal{C}(A,B)$ in $\mathcal{V}$ .
For each object $A$ , a morphism $j_A : I \rightarrow \mathcal{C}(A,A)$ . Intuitively, these encode the the identities in the category.
For each triple of objects $A,B,C$ , a morphism $m_{A,B,C} : \mathcal{C}(B,C)\otimes \mathcal{C}(A,B) \rightarrow \mathcal{C}(A,C)$ . These encode composition of morphisms with the enriched category.

This data must satisfy some axioms, ensuring that composition is associative and has units the identities. In fact, some mathematical structures that are far away from our motivating examples are also enriched categories. The original surprising example was that a mild generalization of metric spaces can be seen as enriched categories, as shown by Lawvere.

Example: For any monoidal closed category $\mathcal{V}$ , we can regard $\mathcal{V}$ as a $\mathcal{V}$ -category, with hom objects

$\mathcal{V}(A,B) = A \multimap B$

The identity and composition maps are derived in a reasonably routine way, and can be found in standard sources. This is usually described as $\mathcal{V}$ being canonically enriched over itself.

To connect the worlds of ordinary and enriched categories, note that any $\mathcal{V}$ -category $\mathcal{C}$ , has an underlying ordinary category $\mathcal{C}_0$ , with the same objects, and homsets:

$\mathcal{C}_0(A,B) = \mathcal{V}(I, \mathcal{C}(A,B))$

Composition and identities in $\mathcal{V}_0$ are defined in a natural way. Strictly speaking, to give an enrichment for an ordinary category $\mathcal{C}$ is to give a $\mathcal{V}$ -category $\mathcal{C}'$ , and a specified isomorphism $\mathcal{C} \cong \mathcal{C}'_0$ . Generally, this isomorphism is ignored when there is a natural choice.

Once we’ve defined a new class of objects, we should consider the morphisms between them. A $\mathcal{V}$ -functor $F : \mathcal{C} \rightarrow \mathcal{D}$ consists of:

A mapping $F$ from $\mathcal{C}$ -objects to $\mathcal{D}$ -objects.
For each pair of $\mathcal{C}$ -objects, a $\mathcal{V}$ -morphism $\varphi_{A,B} : \mathcal{C}(A,B) \rightarrow \mathcal{D}(F(A),F(B))$ . Intuitively, these describe the action on morphisms of the functor.

The morphism $\varphi_{A,B}$ are required to satisfy axioms generalizing the usual idea that identities and composition are preserved.

Example: For the constructions we have seen previous:

A $\mathsf{Pre}$ -enriched functor is a functor which is monotone, in that $f \leq g \;\Rightarrow\; F(f) \leq F(g)$ .
A $\mathsf{Cat}$ -enriched functor is a (strict) 2-functor.
A $\mathsf{Set}$ -functor is an ordinary functor.
A $\mathsf{Ab}$ -functor is a functor such that $F(0) = 0$ and $F(f + g) = F(f) + F(g)$ .

Again, it is helpful to connect back to the world of ordinary category theory. A $\mathcal{V}$ -functor $F : \mathcal{V} \rightarrow \mathcal{D}$ induces an ordinary functor $F_0 : \mathcal{C}_0 \rightarrow \mathcal{D}_0$ that agrees with $F$ on objects. Morphisms $f : A \rightarrow B$ in $\mathcal{C}_0$ are $\mathcal{V}$ -morphisms $\hat{f} : I \rightarrow \mathcal{C}(A,B)$ . Then $F_0(f)$ is given by:

$I \xrightarrow{\hat{f}} \mathcal{C}(A,B) \xrightarrow{\varphi_{A,B}} \mathcal{D}(F(A),F(B))$ .

A $\mathcal{V}$ -functor $F : \mathcal{C} \rightarrow \mathcal{D}$ is said to an enrichment of ordinary functor $F' : \mathcal{C}_0 \rightarrow \mathcal{D}_0$ if $F' = F_0$ .

Finally, a $\mathcal{V}$ -natural transformation $\alpha : F \Rightarrow G$ is a family of $\mathcal{V}$ -morphisms $\alpha_A : I \rightarrow \mathcal{D}(F(A),G(A))$ satisfying an axiom generalizing the usual notion of naturality to the enriched setting.

Strength and Enrichment

Finally, we are in a position to relate strength and enrichment. If $\mathcal{V}$ is a monoidal closed category, and $T : \mathcal{V} \rightarrow \mathcal{V}$ an ordinary endofunctor, giving a strength for $T$ is “the same thing as” giving a structure for $T$ as a $\mathcal{V}$ -functor.

Lets unpack this a bit. As described above, we view $\mathcal{V}$ as being canonically enriched over itself. Giving an enriched structure, sometimes referred to as a functorial strength, for $T$ is to give a natural family of morphisms:

$\varphi_{A,B} : A \multimap B \rightarrow T(A) \multimap T(B)$

compatible with the identity and composition maps. That these maps are natural in the sense of ordinary category is equivalent to being an enrichment of the ordinary functor $T$ is an important point that is often skimmed over.

To build such a family given a strength

$\mathsf{st}_{A,B} : A \otimes T(B) \rightarrow T(A \otimes B)$

we form the composite:

$A \multimap B \otimes T(A) \xrightarrow{\mathsf{st}_{A \multimap B, A}} T(A \multimap B \otimes A) \xrightarrow{T(\epsilon)} T(B)$

where $\epsilon$ is the counit of the adjunction, which can be seen as an evaluation morphism for function spaces. Taking the transpose of this morphism gives a map:

$A \multimap B \rightarrow T(A) \multimap T(B)$

It takes some checking, but these form the components of an enrichment for $T$ as required. In the other direction, given an enrichment, we can form the composite:

$A \xrightarrow{\eta} B \multimap (A \otimes B) \xrightarrow{\varphi_{B, A \otimes B}} T(B) \multimap T(A \otimes B)$

where $\eta$ is the unit of the adjunction. Taking the transpose of this morphism gives a map:

$A \otimes T(B) \rightarrow T(A \otimes B)$

Again, after a bit of checking, it can be seen that this results in a strength for $T$ . The passages in the two directions are mutually inverse, so for monoidal closed category $\mathcal{V}$ to give a strength for $T$ is equivalent to giving an enrichment for $T$ . This dealt with the endofunctor component, but we are really interested in monads. Here, to give a strength for a monad $\mathbb{T}$ on monoidal closed $\mathcal{V}$ is equivalent to giving an enrichment for $\mathbb{T}$ .

Example: As a special case of this result, as every $\mathsf{Set}$ monad is (trivially) enriched over $\mathsf{Set}$ in a unique way. Therefore, given the observations above, every $\mathsf{Set}$ monad has a unique strength. This has a concrete description as:

$\mathsf{st}_{A,B}(a,t) = \mathbb{T}(\lambda b. (a,b))(t)$

This formula can seem slightly magical if given without context, but it is arrived at by unravelling the strength derived from the unique enrichment. Here we use $\lambda$ notion to define a simple function. The strengths given for the list and powerset monads in the earlier example arise via this construction.

As usual, it is useful to think about algebra examples. For a monad $\mathbb{T}$ given by some equational presentation $(\Sigma,E)$ , the unique strength is given on representatives by:

$\mathsf{st}_{A,B}(a, [t]) = [t[(a,b) / b \mid b \in \mathsf{var}(t)]]$

where $\mathsf{var}(t)$ is the set of variables appearing in the representative term $t$ . As usual, square brackets are somewhat overloaded, denoting both equivalence classes and the substitution operation. In words – we replace each variable $b$ appearing in the representative term $t$ with the variable $(a,b)$ .