The Hidden Strength of Costrong Functors


Abstract

Strong functors and monads are ubiquitous in Computer Science. More recently, comonads have demonstrated their use in structuring context-dependent notions of computation. However, the dualisation of “being strong” property passed somehow unobserved so far. We argue that “being costrong” gives a different understanding of how functors can interact with monoidal structures. This work in progress aims to explore costrong functors and their natural properties, with an eye towards the semantics of computations.

1 Introduction↩︎

Category theory often offers a high-level, compositional framework for modeling complex systems and abstractions in computer science, enabling formal verification and reasoning about computational effects. Functors and (co)monads are useful tools to incorporate effects and coeffects into computations. Extending these notions, we consider in this paper costrong functors and their applications/interactions with other functional structures. Here, the (co)strength of a functor is with respect to an action of a monoidal category, a theoretical notion successfully employed in programming for encapsulating datatypes within contexts (like exceptions as a result of computations or resources demanded by computations) [@Katsumata2014; @PetricekOrchardMycroft2014]. Such an action provides a similar mechanism in that the effect of the action is moved inward or outward of the functor application by the (co)strength. Formally, if \({\mathscr{M}}\) is a monoidal category acting on two categories \({\mathscr{A}}, {\mathscr{B}}\), then a functor \(F:{\mathscr{A}}\longrightarrow{\mathscr{B}}\) is \({\mathscr{M}}\)-strong if it comes equipped with a natural transformation \(\mathsf{st}: M \cdot F(-) \longrightarrow F(M \cdot -)\), called strength, compatible with the action. The most common case is \({\mathscr{M}}={\mathscr{A}}={\mathscr{B}}=\mathbf{Set}\), where both the tensor product and action are given by the cartesian product. Dually, a functor \(F\) is called \({\mathscr{M}}\)-costrong when \(F^{\mathsf{op}}:{\mathscr{A}}^{\mathsf{op}}\longrightarrow{\mathscr{B}}^{\mathsf{op}}\) is strong, with corresponding natural transformation (costrength) \(\mathsf{cst}: F(M \cdot -) \longrightarrow M \cdot F(-)\).

Despite the centrality of strength in applications, the dual notion of costrength, and more generally costrong functors, have received comparatively little attention in the literature. This asymmetry is somewhat surprising, especially given that many categorical phenomena — such as comonadic structures, coalgebras, and context-dependent computation — naturally call for a dual treatment. In particular, we will see how costrength is useful because it “extracts” the action out of the functor. In the context of a programming language, a functor provides a container to execute computation within it, but often we want to access results of a chain of computation directly. Costrength, like the comonad counit, provides such means; however, in the case of costrength this is more nuanced, since it depends on the action with respect to which the functor is costrong. Therefore, we believe that costrength is a more flexible notion than the comonad counit.

2 Actions of monoidal categories and costrong functors↩︎

2.1 Monoidal categories and their actions on categories↩︎

Throughout the paper, \(({\mathscr{M}},\otimes, I)\) will denote a monoidal category. In the sequel, we shall not label the associativity and unit natural transformations \((M\otimes N) \otimes P \cong M \otimes (N \otimes P)\) and \(I \otimes M \cong M \cong M \otimes I\) or even omit them when the context is clear, writing as if the tensor product were strict.

Example 1.

  1. Given a category \({\mathscr{A}}\), the category \(\mathsf{End}({\mathscr{A}})\) of endofunctors \({\mathscr{A}}\longrightarrow{\mathscr{A}}\) is strict monoidal with functor composition \(\circ\) and unit the identity functor \(\mathsf{id}_{\mathscr{A}}\). 2

  2. Any cartesian category \({\mathscr{M}}\) is symmetric monoidal with binary product \(X \times Y\) as tensor, and unit the terminal object \(\mathbb{1}\). Dually, any cocartesian category is monoidal with respect to binary coproduct \(X+Y\) and initial object \(\mathbb{0}\).

  3. Any preordered monoid \(((M,\le),*,e)\) is a (skeletal) monoidal category: the elements of \(M\) are the objects of this category, morphisms are provided by the order relation, while the monoidal structure is given by the binary operation \(*\) of the monoid.

Let \(({\mathscr{M}},\otimes,I)\) be a monoidal category. A (left) \({\mathscr{M}}\)-action, or a (left) \({\mathscr{M}}\)-actegory [@Benabou1967; @McCrudden2000; @Pareigis1977] consists of a category \({\mathscr{A}}\), equipped with a functor \({\mathscr{M}}\otimes {\mathscr{A}}\longrightarrow{\mathscr{A}}\), \((M,X)\mapsto M\cdot X\) which is associative and unital up to coherent isomorphisms \((M\otimes N)\cdot X \cong M\cdot (N \cdot X)\), \(I \cdot X \cong X\) satisfying a pentagon and a triangle axiom, as given in [@McCrudden2000]. By op. cit., any action of a monoidal category is equivalent to a strict one. Consequently, in the sequel we shall either ignore the natural isomorphisms above and write as if the action was strict, or write these isomorphisms unlabelled, as we did for monoidal categories.

Example 2.

  1. The monoidal category \({\mathscr{M}}\) canonically acts on itself with tensor product as action. We shall call it the regular action of \({\mathscr{M}}\).

  2. Let \({\mathscr{A}}\) be an arbitrary category. Functor application induces a (strict) action on \({\mathscr{A}}\) of the monoidal category \((\mathsf{End}({\mathscr{A}}), \circ, \mathsf{id}_{\mathscr{A}})\).

  3. Any category with finite copowers3 is an actegory over the preordered additive monoid of natural numbers, with action given by copower.

More examples can be found in e.g. [@CapucciGavranovic2022].

Remark 1. An action of the monoidal category \({\mathscr{M}}\) on a category \({\mathscr{A}}\) is equivalent to a strong monoidal functor \(({\mathscr{M}}, \otimes, I) \longrightarrow(\mathsf{End}({\mathscr{A}}), \circ, \mathsf{id}_{\mathscr{A}})\). In certain situations, however, requiring a strong monoidal functor \(({\mathscr{M}}, \otimes, I) \longrightarrow(\mathsf{End}({\mathscr{A}}), \circ, \mathsf{id}_{\mathscr{A}})\) may be too restrictive, and lax or colax monoidal functors are instead considered. The latter are usually known as graded (co)monads [@FujiiKatsumataMelies-FoSSaCS2016]. If the monoidal category \({\mathscr{M}}\) is the terminal category, then we recover the usual notion of a (co)monad.

Example 3. [@solberg1994] The Maybe monad is often used in functional programming to encapsulate computations that might fail. Let \(M = \{\mathbf{f}(ailure), \mathbf{s}(uccess),\mathbf{m}(aybe)\}\) a three-element set with partial order \(\mathbf{f} \leq \mathbf{m}\), \(\mathbf{s} \leq \mathbf{m}\), and binary operation \[\begin{array}{c|ccc} * & \mathbf{f} & \mathbf{s} & \mathbf{m} \\ \hline \mathbf{f} & \mathbf{f} & \mathbf{f} & \mathbf{f} \\ \mathbf{s} & \mathbf{f} & \mathbf{s} & \mathbf{m} \\ \mathbf{m} & \mathbf{f} & \mathbf{m} & \mathbf{m} \end{array}\] It is easy to check that \((M,*,\le)\) is a preordered monoid with unit \(\mathbf{s}\). Then a graded monad \(T: M \longrightarrow\mathsf{End}(\mathbf{Set})\) can be defined as follows: \((T\mathbf{f})X = \mathbb{1}\), \((T\mathbf{s})X = X\) and \((T\mathbf{m})(X) = \mathtt{Maybe} \, X = \mathbb{1}+ X\), where \(T( \mathbf{f} \leq \mathbf{m})\) and \(T( \mathbf{s} \leq \mathbf{m})\) are the canonical injections. It is not an \((M,*,\le)\)-actegory, only a lax one: for instance, the natural transformation \(T(\mathbf{m}*\mathbf{f})\longrightarrow T\mathbf{m}\circ T\mathbf{f}\) is not an isomorphism.

2.2 (Co)Strong functors as morphisms of actions of monoidal categories↩︎

Let \(({\mathscr{M}},\otimes, I)\) be a monoidal category. A functor \(F:{\mathscr{M}}\longrightarrow{\mathscr{M}}\) is usually called strong4 if it is equipped with a natural transformation \(\mathsf{st}: - \otimes F(=) \longrightarrow F(- \otimes =)\), called strength, subject to certain axioms expressing compatibility between the tensor product and the action of the functor [@Kock1972]. While strong functors have origins in enriched category theory, they have since become central in the semantics of functional programming, modelling e.g. computational effects or abstract syntax [@FiorePlotkinTuri1999; @Moggi1989]. The paper [@McDermottUustalu2022] provides an overview on the theory of strong functors and strong monads. The notion of a strong functor admits a natural two-fold generalisation: first, extending from functors on \({\mathscr{M}}\) to functors on \({\mathscr{M}}\)-actegories; and second, considering functors with possibly distinct domain and codomain.

An \({\mathscr{M}}\)-strong functor (or a lax morphism of \({\mathscr{M}}\)-actegories) consists of a functor \(F:{\mathscr{A}}\longrightarrow{\mathscr{B}}\) between two \({\mathscr{M}}\)-actegories \({\mathscr{A}}\), \({\mathscr{B}}\), equipped with a natural transformation \(\mathsf{st}:M\cdot F(X) \longrightarrow F(M\cdot X)\), called strength, satisfying \[\label{eq:lax-morphism} \xymatrix@C=5pt@R=20pt{ (M\otimes N)\cdot F(X) \ar[d]_{\mathsf{st}} \ar[rr]^{\cong} & & M \cdot (N \cdot F(X)) \ar[d]^{\mathsf{id}\cdot \mathsf{st}} &&& I \cdot F(X) \ar[rr]^{\mathsf{st}} \ar[dr]_{\cong} & & F(I \cdot X) \ar[dl]^{\cong} \\ F((M \otimes N)\cdot X) \ar[dr]_{\cong} & & M \cdot F(N \cdot X) \ar[dl]^{\mathsf{st}} &&&& F(X) & \\ & F(M \cdot (N \cdot X)) }\tag{1}\]

Dually, an \({\mathscr{M}}\)-costrong functor (or colax morphism of \({\mathscr{M}}\)-actegories) is a functor \(F:{\mathscr{A}}\longrightarrow{\mathscr{B}}\) such that \(F^{\mathsf{op}}\) is a lax \({\mathscr{M}}\)-morphism from \({\mathscr{A}}^{\mathsf{op}}\) to \({{\mathscr{B}}}^{\mathsf{op}}\). Explicitly, \(F\) is equipped with a natural transformation in the opposite direction, denoted \(\mathsf{cst}:F(M\cdot X) \longrightarrow M\cdot F(X)\) and called costrength, satisfying diagrams dual to 1 : \[\label{eq:colax-morphism} \xymatrix@C=5pt@R=20pt{ F(M \cdot (N\cdot X)) \ar[d]_{\cong} \ar[rr]^{\mathsf{cst}} & & M \cdot F(N \cdot X) \ar[d]^{\mathsf{id}\cdot \mathsf{cst}} &&& F(I \cdot X) \ar[rr]^{\mathsf{cst}} \ar[dr]_{\cong} & & I \cdot F(X) \ar[dl]^{\cong} \\ F((M \otimes N)\cdot X) \ar[dr]_\mathsf{cst} & & M \cdot (N \cdot F(X)) \ar[dl]^{\cong} &&&& F(X) & \\ & (M \otimes N) \cdot F(X) }\tag{2}\]

Intuitively, if the strength of an \({\mathscr{M}}\)-strong functor pushes the action inside the functor, \({\mathscr{M}}\)-costrong functors have the opposite behaviour, namely they pull out the \({\mathscr{M}}\)-action [@HughesVollmerOrchard2021]. This makes costrong functors interesting for various coinduction principles (see Section 4.2 for a discussion).

Example 4. As mentioned at the beginning of this section, strong functors first appeared in enriched category theory. If \(({\mathscr{M}},\otimes, I)\) is monoidal closed and enriched over itself via the internal hom, then an endofunctor on \({\mathscr{M}}\) is \({\mathscr{M}}\)-strong if and only if it is an \({\mathscr{M}}\)-enriched functor [@Kock1972]. If \(({\mathscr{M}},\otimes, I)\) is the cartesian closed category of sets and functions, then any functor on \(\mathbf{Set}\) is automatically \(\mathbf{Set}\)-enriched, hence it is \((\mathbf{Set}, \times, \mathbb{1})\)-strong and its strength is unique.

Remark 2. The notions of costrong functor and costrength had first been considered, to the best of the authors’ knowledge, in [@BluteCockettSeely1997], in the framework of (co)context categories. They subsequently had scarce appearances in the literature, usually focused on a specific actegory, e.g. [@HansenKlin2011; @HeunenKarvonen2015; @McDermottUustalu2022], and without a comprehensive analysis of their properties or potential applications. While far from being exhaustive, this work in progress aims to take a first step towards a detailed study of these concepts.

A word of caution: the terms costrong functor and costrength have also been used to describe endofunctors on monoidal categories equipped with right strenghts \(F(-)\otimes = \, \longrightarrow F(-\otimes =)\). Given that such functors are not considered here, we believe there will be no confusion.

An \({\mathscr{M}}\)-strong natural transformation between \({\mathscr{M}}\)-strong functors \((F,\mathsf{st}),(G,\mathsf{st}): {\mathscr{A}}\longrightarrow{\mathscr{B}}\) is a natural transformation \(\alpha:F \longrightarrow G\) satisfying \[\xymatrix{ M \cdot F(X) \ar[r]^{\mathsf{id}\cdot \alpha} \ar[d]_\mathsf{st} & M \cdot G(X) \ar[d]^\mathsf{st} \\ F(M\cdot X) \ar[r]_\alpha & G(M\cdot X) }\] \({\mathscr{M}}\)-costrong natural transformations between \({\mathscr{M}}\)-costrong functors are defined similarly, by reversing the direction of the vertical arrows in the diagram above.

One important aspect of \({\mathscr{M}}\)-(co)strong functors and \({\mathscr{M}}\)-(co)strong natural transformations, is their compositionality. Albeit trivial from the perspective of category theory, it has successfully been applied in the semantics of computations. Formally, \({\mathscr{M}}\)-actions, \({\mathscr{M}}\)-costrong functors and \({\mathscr{M}}\)-costrong natural transformations determine a \(2\)-category [@BluteCockettSeely1997]. We shall write \([{\mathscr{A}},{\mathscr{B}}]_{\mathsf{cst}}\) for the category of \({\mathscr{M}}\)-costrong functors and costrong natural transformations between two \({\mathscr{M}}\)-actegories \({\mathscr{A}}\) and \({\mathscr{B}}\). As it is the case in any \(2\)-category, \({\mathscr{M}}\)-costrong endofunctors determine a monoidal category \((\mathsf{End}({\mathscr{A}})_\mathsf{cst}, \circ, \mathsf{id})\) with respect to functor composition.

Example 5. In case \({\mathscr{M}}\) is braided (or even symmetric) monoidal, the action of an object \(S\) of \({\mathscr{M}}\) determines a simultaneously \({\mathscr{M}}\)-strong and \({\mathscr{M}}\)-costrong functor \(F_S:{\mathscr{A}}\longrightarrow{\mathscr{A}}\), given by \(F_S (X) = S \cdot X\) (the (co)strength being induced by the braiding/symmetry). If additionally \(S\) is a (co)monoid in \({\mathscr{M}}\), then \(F_S\) becomes a (co)monad, with associated (co)unit and (co)multiplication being \({\mathscr{M}}\)-(co)strong natural transformations. That is, \(F_S\) is an \({\mathscr{M}}\)-(co)strong (co)monad. In particular, this is the case for cartesian monoidal categories, like \((\mathbf{Set},\times,\mathbb{1})\), where every object naturally carries a comonoid structure. For example, take the \((\mathbf{Set},\times,\mathbb{1})\)-costrong comonad \(F_S (X) = S \times X\) on \(\mathbf{Set}\), usually known as the Writer comonad. As explained above, its costrength \(\mathsf{cst}: S \times M \times X \longrightarrow M \times S \times X\) is induced by the symmetry of the cartesian product. The results of Section 3 will show that this is the only possible \((\mathbf{Set}, \times, \mathbb{1})\)-costrength on the Writer comonad (even on the underlying functor part).

More examples of familiar functors on \(\mathbf{Set}\), costrong with respect to various monoidal actions, can be found below. In all these examples, whenever the functor in question is a (co)monad, both the (co)unit and the (co)multiplication are costrong:

Example 6.

  1. Consider first \((\mathbf{Set}, \times, \mathbb{1})\) acting on itself.

    1. For the Reader monad \(X \mapsto [S,X]\), \((\mathbf{Set},\times, \mathbb{1})\)-costrengths \([S,M\times X] \longrightarrow M \times [S,X]\) are in one-to-one correspondence with elements of \(S\).5

    2. Composing the \((\mathbf{Set}, \times, \mathbb{1})\)-costrong Writer comonad from Example 5 with the Reader monad mentioned in the previous above, we obtain \((\mathbf{Set}, \times, \mathbb{1})\)-costrengths (again not unique!) on the Costate comonad \(X \mapsto S \times [S,X]\).

    3. To provide a negative example, observe that \(\mathbf{Set}\)-endofunctors \(F\) for which \(F\emptyset \neq \emptyset\) cannot possess a \((\mathbf{Set}, \times, \mathbb{1})\)-costrength.

  2. Take now \((\mathbf{Set},+,\mathbb{0})\), again acting on itself.

    1. The powerset functor \(\mathcal{P}\) is \((\mathbf{Set},+,\mathbb{0})\)-costrong, where \(\mathsf{cst}:\mathcal{P}(M+X) \longrightarrow M+\mathcal{P}(X)\) forgets all possible occurences of elements of \(M\) in a subset of \(M+X\), resulting thus a subset of \(X\), which subsequently embeds in \(M+\mathcal{P}(X)\).

    2. The above example generalises to the class of filtrable functors: a filtrable functor \(F\) is a functor with a natural transformation \(\phi: F \circ Maybe \Rightarrow F\). The costrength is given by \(F(M + X) \xrightarrow{!+\mathsf{id}} F(\mathbb{1} + X) \xrightarrow{\phi} F X \xrightarrow{\mathrm{inr}} M + FX\). By extension, every functor composed with a filtrable functor on the left produces another filtrable functor. Filtrable functors cannot satisfy \(F\emptyset \neq \emptyset\) except for the constant functor in \(\emptyset\), as it would otherwise imply that \(F \mathbb{1} = F (\mathbb{1} + \emptyset) \rightarrow F \emptyset = \emptyset\).

    3. Because \(\mathbf{Set}\) is a distributive category, we obtain for free that the Writer comonad is also \((\mathbf{Set},+,\mathbb{0})\)-costrong, with costrength \(S \times (M + X) \cong (S \times M) + (S \times X) \xrightarrow{} M + (S \times X)\), where the last arrow is induced by the projection on the second component.

  3. Consider the action of \((\mathbf{Set}^{\mathsf{op}},\times, \mathbb{1})\) on \(\mathbf{Set}\) given by exponentiation. Since every functor \(F:\mathbf{Set}\longrightarrow\mathbf{Set}\) is (uniquely) \((\mathbf{Set}, \times, \mathbb{1})\)-strong, taking the mate of its strength \(M \times F(-) \longrightarrow F(M\times -)\) shows that \(F\) has a unique \((\mathbf{Set}^{\mathsf{op}},\times, \mathbb{1})\)-costrength \(\mathsf{cst}:F([M,X])\longrightarrow[M,FX]\). Explicitly, \(\mathsf{cst}(t)(m) = F(\mathsf{ev}_m(t))\), where \(\mathsf{ev}_m:[M,X]\longrightarrow X\) is given by evaluation \(\mathsf{ev}_m(f) = f(m)\) [@HansenKlin2011].

  4. Consider an arbitrary category \({\mathscr{A}}\) with copowers and the strict monoidal category \((\mathsf{End}({\mathscr{A}}),\circ, \mathsf{id}_{\mathscr{A}})\) acting on \({\mathscr{A}}\) via functor application. Copowering with a fixed set gives a \((\mathsf{End}({\mathscr{A}}),\circ, \mathsf{id}_{\mathscr{A}})\)-costrong functor \(F:{\mathscr{A}}\longrightarrow{\mathscr{A}}\), \(F(X) = S \cdot X\). The costrength now represents a distributive law of \(F\) over all functors. Its existence is guaranteed by the fact that every functor laxly preserves colimits.

  5. The last example considers the strict monoidal category \([\mathbf{Set},\mathbf{Set}]_{\mathsf{appl}}\) of applicative functors and applicative natural transformations [@McBridePaterson2008], acting on \(\mathbf{Set}\) by application. Then a \([\mathbf{Set},\mathbf{Set}]_{\mathsf{appl}}\)-costrong functor is known as traversable [@JaskelioffRypacek2012]. Traversables can be equivalently characterised as dependent polynomial functors [@Bird-et-al2013; @GambinoHyland2003].

In view of the above examples, a functor may be costrong with respect to a given \({\mathscr{M}}\)-action in more than one way, or it may not be costrong at all. It is thus desirable to find conditions guaranteeing the existence or uniqueness of costrength. Regarding existence of costrength, Section 3 provides some conditions in the particular case of a cartesian monoidal category acting upon itself. Uniqueness has first been considered by Moggi for strong monads on cartesian categories [@Moggi1991], and recently generalised by Sato for strong monads on monoidal categories, seen as actegories with the regular action [@Sato2018]. We state below the corresponding dual result for endofunctors (not necessarily (co)monads).

Proposition 3 (Uniqueness of costrength [@Moggi1991; @Sato2018]). Let \(({\mathscr{M}},\otimes, I)\) be a monoidal category. Assume the following:

  1. The monoidal unit is a cogenerator,6

  2. For any morphism \(h:X \otimes Y \longrightarrow I\) there are \(f:X \longrightarrow I\) and \(g:Y \longrightarrow I\) such that the composite \(X \otimes Y \overset{f \otimes g}{\longrightarrow}I\otimes I \cong I\) coincides with \(h\).

If \(F:{\mathscr{M}}\longrightarrow{\mathscr{M}}\) is a costrong functor with respect to the regular action of \({\mathscr{M}}\), then its costrength is uniquely determined by \[\xymatrix{ F(X \otimes Y) \ar[r]^{\mathsf{cst}} \ar[d]_{F(f \otimes \mathsf{id})} & X \otimes FY \ar[r]^-{f \otimes g} & I \otimes I \ar[d]^{\cong} \\ F(I \otimes Y) \ar[r]^{\cong} & F(Y) \ar[r]^{g} & I }\] for any objects \(X,Y\) and any morphisms \(f:X \longrightarrow I\) and \(g:FY \longrightarrow I\), where the unlabelled isomorphisms refer to the left associators of the monoidal category.

The second condition above is guaranteed in the case of cocartesian monoidal categories. Adding the requirement that the monoidal unit (that is, the initial object) be a cogenerator is more restrictive. An example comes from propositional logic: in the category of Boolean algebras, \(\mathbb{2}\) is both an initial object and a cogenerator. Another example arises from the semantics of quantum computing, more precisely from the category of (finite-dimensional) Hilbert spaces.

3 Costrong functors on cartesian categories↩︎

Among monoidal categories occurring in programming, the case most encountered is the one where the monoidal structure is given by the cartesian product, with \(\mathbf{Set}\) as main example. It is well known that every \(\mathbf{Set}\)-endofunctor is strong, in a unique way. This naturally raises the question: what can be said about costrong ones? We shall establish an isomorphism between the categories of costrong functors and copointed ones on cartesian categories.

Let thus \({\mathscr{M}}\) be a cartesian category. Consider \({\mathscr{M}}\) as an \({\mathscr{M}}\)-actegory with respect to own action given by the cartesian product.

The preliminary result below shows that if you extract the second component after reorganizing with costrength, you get exactly the same result as just mapping \(\pi_2\) over the original computation.

Lemma 1. Let \(F:{\mathscr{M}}\longrightarrow{\mathscr{M}}\) be a costrong functor, with costrength \(\mathsf{cst}: F(M \times X) \longrightarrow M \times F(X)\). Then the costrength commutes with the second projection: \(\pi_2 \circ \mathsf{cst}= F(\pi_2):F(M \times X) \longrightarrow F(X)\). \[\label{eq:cst-proj2} \xymatrix@R=17pt{ F(M \times X) \ar[r]^-{\mathsf{cst}} \ar`d[dr]_(.75){F (\pi_2)}[dr] & M \times F(X) \ar[d]^-{\pi_2} \\ & F(X) }\tag{3}\]

Proof. This follows from \[\xymatrix{ & F(M\times X) \ar[r]^-{\mathsf{cst}} \ar[d]|-{F(! \times \mathsf{id})} & M \times F(X) \ar[r]^-{\pi_2} \ar[d]|-{! \times \mathsf{id}} & F(X) \ar@{=}[d] \\ & F(\mathbb{1}\times X) \ar[r]^-{\mathsf{cst}} \ar[d]|-{F\pi_2} & \mathbb{1}\times F(X) \ar[r]^-{\pi_2} & F(X) \ar@{-}@<+.25ex>`d[dll][dll] \ar@{-}@<-.25ex>`d[dll][dll] \\ & F(X) \ar@{<-}`l[luu]`[uu]^-{F\pi_2}[uu] }\] where \(!\) denotes the unique arrow to the terminal object \(\mathbb{1}\) of \({\mathscr{M}}\). ◻

Recall now that an endofunctor \(F:{\mathscr{M}}\longrightarrow{\mathscr{M}}\) is called copointed if it is endowed with a natural transformation \(\epsilon:F \longrightarrow\mathsf{id}_{\mathscr{M}}\). A natural transformation between copointed endofunctors \(\alpha:F \longrightarrow G\) is itself called copointed if \[\xymatrix{ F \ar[rr]^{\alpha} \ar[dr]_{\epsilon} & & G \ar[dl]^{\epsilon} \\ & \mathsf{id}_{{\mathscr{M}}} & }\] We obtain thus the category of copointed endofunctors and copointed natural transformations, that is, the slice category \([{\mathscr{M}},{\mathscr{M}}]\downarrow \mathsf{id}_{\mathscr{M}}\). Of course, this category makes sense regardless of \({\mathscr{M}}\) being cartesian. The forgetful functor \([{\mathscr{M}},{\mathscr{M}}]\downarrow \mathsf{id}_{\mathscr{M}}\longrightarrow[{\mathscr{M}},{\mathscr{M}}]\) is comonadic if \({\mathscr{M}}\) is cartesian, with right adjoint sending an arbitrary functor \(F:{\mathscr{M}}\longrightarrow{\mathscr{M}}\) to \(\mathsf{id}_{\mathscr{M}}\times F\).

Consider also the category \([{\mathscr{M}},{\mathscr{M}}]_{\mathsf{cst}}\) of costrong endofunctors on \({\mathscr{M}}\) and costrong natural transformations.

Theorem 4. Let \({\mathscr{M}}\) be a cartesian category. There is an isomorphism between the category \([{\mathscr{M}},{\mathscr{M}}]_{\mathsf{cst}}\) of costrong endofunctors on \({\mathscr{M}}\), and the category of copointed endofunctors \([{\mathscr{M}},{\mathscr{M}}]\downarrow \mathsf{id}_{\mathscr{M}}\).

Proof. The correspondences are as follows: First, \(\Phi:[{\mathscr{M}},{\mathscr{M}}]_\mathsf{cst}\longrightarrow[{\mathscr{M}},{\mathscr{M}}]\downarrow \mathsf{id}_{\mathscr{M}}\) maps \((F, \mathsf{cst})\) to \((F,\epsilon)\) where \[\epsilon: \xymatrix{ F(M) \ar[r]^-{\cong} & F(M \times \mathbb{1}) \ar[r]^{\mathsf{cst}} & M \times F(\mathbb{1}) \ar[r]^-{\pi_1} & M }\]

Next, \(\Psi:[{\mathscr{M}},{\mathscr{M}}]\downarrow \mathsf{id}_{\mathscr{M}}\longrightarrow[{\mathscr{M}},{\mathscr{M}}]_\mathsf{cst}\) maps a copointed \((F, \epsilon)\) to \((F, \mathsf{cst})\), with costrength given by \[\mathsf{cst}:\xymatrix@C=50pt{ F(M \times X) \ar[r]^-{\langle F\pi_1,F\pi_2\rangle} & F(M) \times F(X) \ar[r]^-{\epsilon \times \mathsf{id}} & M \times F(X) }\] where \(\langle-,-\rangle\) denotes the pairing into the product. That \(\mathsf{cst}\) satisfies 2 follows from the fact that any functor on a cartesian category is automatically colax monoidal, and so is any natural transformation. Both \(\Phi\) and \(\Psi\) act as identity on arrows. It can easily be checked that \(\Phi\) and \(\Psi\) are well defined. Standard diagram chasing shows that \(\Phi\) and \(\Psi\) are functors inverses to each other: \(\Psi \circ \Phi=\mathsf{id}\) follows easily, while \(\Phi \circ \Psi = \mathsf{id}\) is a consequence of the previous lemma. ◻

The gist of the above theorem is that on a cartesian category, to give a costrength for an endofunctor is the same as to give a copoint, that is, a natural transformation with codomain the identity functor. In particular, we see now that costrengths for the Reader monad \([S,-]\) on \(\mathbf{Set}\) are in one-to-one correspondence with natural transformations \([S,X]\longrightarrow X\), which by Yoneda lemma, correspond to points (elements) of \(S\). Regarding the Writer functor (comonad) \(S \times -\), another application of the Yoneda lemma shows that there is only one natural transformation \(S \times X \longrightarrow X\), namely the second projection, hence there is only one way in which the Writer functor can be \((\mathbf{Set},\times \mathbb{1})\)-costrong.

Corollary 1. Comonads on cartesian categories are costrong.

Corollary 2. For every endofunctor \(F\) on a cartesian category \({\mathscr{M}}\), the cofree copointed functor over \(F\), namely \(\mathsf{id}_{\mathscr{M}}\times F\) [@LPW2000], is costrong.

The above two corollaries show that there is a plethora of examples of costrong endofunctors on cartesian categories. In particular, the counit of a comonad produces a costrength, but a comonad may be costrong in a different way, see the case of the Costate comonad from Example 6.([ex:costrong-comonad-not-unique-cst]).

Remark 5. A careful inspection of the diagrams involved in the proofs of Lemma 1 and of Theorem 4 shows that the hypothesis that \({\mathscr{M}}\) is a cartesian category can be relaxed to a semicartesian category [@Fritz2020; @semicartesian2; @semicartesian]. A semicartesian category is a monoidal category where the unit object is terminal. Equivalently, it can be described as a “monoidal category with projections”. The arguments above carry unchanged in the semicartesian case, under the proviso that copointed endofunctors should be replaced by copointed colax monoidal endofunctors (where both the functor component and the “copoint” component are colax monoidal).

4 Applications↩︎

We present below two possible applications of costrong functors. Other possible directions of study are sketched at the end of the paper and left for future research.

4.1 Costrong functors and (mixed) optics↩︎

Optics are bidirectional data accessors, offering a powerful abstraction for accessing data in a compositional manner. For a programmer’s perspective, one can intuitively think of an optic as decomposing a type or data structure through a monoidal action, enabling access to a nested structure. The result of the decomposition is a context or residual, which can later recompose with other data to get a composite object. We are considering here mixed optics for a pair of actions of a monoidal category \({\mathscr{M}}\); these work independently from one another and only interact through the residuals.

While the existing literature focuses on changing optics via a single monoidal functor preserving the tensor product up to an isomorphism and acting on all components, here we allow pairs of \({\mathscr{M}}\)-morphisms of mixed strength, acting individually on each \({\mathscr{M}}\)-action of the optic rather than simultaneously on both.

A careful inspection in the definition of optics (to be recalled below) will convince the reader that the two actions can in fact be relaxed to a graded monad and a graded comonad, connected via the monoidal category \(\mathcal{M}\) that provides the grading.7 We leave the exploration of optics arising from a graded monad-comonad pair for future research, and focus now on genuine \({\mathscr{M}}\)-actions.

Let \({\mathscr{M}}\) be a monoidal category acting on two categories \({\mathscr{A}}\) and \({\mathscr{B}}\). The category of (mixed) optics \(\mathbf{Optic}_{{\mathscr{A}},{\mathscr{B}}}\)8 has as objects pairs of objects of \({\mathscr{A}}\) and \({\mathscr{B}}\), respectively, and hom-sets \[\mathbf{Optic}_{{\mathscr{A}},{\mathscr{B}}}((X',Y'),(X,Y)) = \int^{M\in {\mathscr{M}}} {\mathscr{A}}(X',M\cdot X)\times {\mathscr{B}}(M\cdot Y,Y')\]

Examples [@CEGLMPR2020] include cases where \({\mathscr{A}},{\mathscr{B}}\) are not necessarily small, but the above coend still exists. There is an identity-on-objects functor \({\mathscr{A}}^{\mathsf{op}}\otimes {\mathscr{B}}\longrightarrow\mathbf{Optic}_{{\mathscr{A}},{\mathscr{B}}}\) exhibiting \(\mathbf{Optic}_{{\mathscr{A}},{\mathscr{B}}}\) as the Kleisli category of a promonad in the bicategory of profunctors.

In previous work [@BalanPantelimon2024], the authors of this paper have observed that optics are in fact parametric in the two \({\mathscr{M}}\)-actions, in the sense that pairs of \({\mathscr{M}}\)-costrong/\({\mathscr{M}}\)-strong functors act as optics transformers. More in detail, an \({\mathscr{M}}\)-costrong functor between \({\mathscr{M}}\)-actegories \(F:{\mathscr{A}}\longrightarrow{\mathscr{A}}'\) and an \({\mathscr{M}}\)-strong one \(G:{\mathscr{B}}\longrightarrow{\mathscr{B}}'\) induce a functor between categories of optics \(\mathbf{Optic}(F,G):\mathbf{Optic}_{{\mathscr{A}},{\mathscr{B}}}\longrightarrow\mathbf{Optic}_{{\mathscr{A}}', {\mathscr{B}}'}\) as follows: on objects, \(F\) and \(G\) act component-wise by \((X,Y) \mapsto (F(X),G(Y))\). The action on morphisms, that is, on optics, is globally induced by the composite \[{!}{\xymatrix@C=8pt{ {{\mathscr{A}}}(X',{M}{\cdot} X){\otimes} {{\mathscr{B}}}({M}{\cdot} Y,Y') \ar[r] & {{\mathscr{A}}}'(F(X'),F({M}{\cdot} X)){\otimes} {{\mathscr{B}}}'(G({M}{\cdot} Y),G(Y')) \ar[r] & {\mathscr{A}}'(F(X'),{M}{\cdot} F(X)){\otimes} {\mathscr{B}}'({M}{\cdot} G(Y),G(Y')) }}\] The correspondence \(({\mathscr{A}},{\mathscr{B}})\mapsto \mathbf{Optic}_{{\mathscr{A}},{\mathscr{B}}}\) determines now a \(2\)-functor \[\mathbf{Optic}: {\mathscr{M}}-{\mathbf{Act}}_\mathsf{cst}\times {\mathscr{M}}-{\mathbf{Act}}_\mathsf{st}\longrightarrow\mathbf{Cat}\] from the product of the \(2\)-categories of \({\mathscr{M}}\)-actions, \({\mathscr{M}}\)-costrong functors and \({\mathscr{M}}\)-costrong natural transformations \({\mathscr{M}}-{\mathbf{Act}}_\mathsf{cst}\), respectively \({\mathscr{M}}\)-actions, strong functors and strong natural transformations \({\mathscr{M}}-{\mathbf{Act}}_\mathsf{st}\) into \(\mathbf{Cat}\).

4.2 Costrong functors and streams↩︎

In the sequel, we shall consider \((\mathbf{Set},\times, \mathbb{1})\) with the cartesian closed structure acting upon itself. Let \(F:\mathbf{Set}\longrightarrow\mathbf{Set}\) a \((\mathbf{Set},\times, \mathbb{1})\)-costrong functor. As explained in Section 6, we can interpret the costrength of \(F\) as a distributive law of \(F\) over the Writer functor \(G(X) = M \times X\), uniform in the parameter \(M\). That is, a stream GSOS specifications [@Klin2011]. This distributive law allows \(F\) to lift to \(G\)-coalgebras.

Recall that a \(G\)-coalgebra is a set \(C\), endowed with a map \(\langle {\mathtt{out}}, {\mathtt{next}}\rangle: C \longrightarrow M\times C\), that is, a stream automata. The final \(G\)-coalgebra is the set of streams \(M^\omega\), with coalgebra structure given by the usual pairing of maps \(\langle {\mathtt{head}}, {\mathtt{tail}}\rangle: M^\omega \longrightarrow M\times M^\omega\). The unique map from the \(G\)-coalgebra \(C\) into \(M^\omega\) sends a state \(c\in C\) to the stream of outputs originated in that state: \[\llbracket c \rrbracket = (\mathtt {out}(c), \mathtt{out}(\mathtt {next}(c), \mathtt{out}(\mathtt {next}(\mathtt{next}(c)), \ldots )\] Let us now examine the effect of applying an arbitrary functor \(F\) to the coalgebra. Intuitively, one can think of \(F\) as introducing a context that encapsulates the transition system. While the internal dynamics persist, it becomes hidden from an external observer due to this contextual wrapping. Generally, there is no way of extracting the outputs from within the context, unless \(F\) is \({\mathscr{M}}\)-costrong: \[\xymatrix@C=50pt{ F(C) \ar[r]^-{F\langle {\mathtt{out}}, {\mathtt{next}}\rangle} & F(M \times C) \ar[r]^{\mathsf{cst}} & M \times F(C) }\] Hence now the stream of \(M\)-outputs is preserved exactly as it was originally, remaining accessible, although the transition to the next state happens inside the context. This behaviour is formally captured by the final coalgebra, as follows: \[\xymatrix@C=50pt{ C \ar[r]^-{\langle {\mathtt{out}}, {\mathtt{next}}\rangle } \ar[d]_-{\llbracket - \rrbracket } & M \times C \ar[d]^{\mathsf{id}\times \llbracket - \rrbracket } & \phantom{aa}F(C) \phantom{i} \ar@{}[l]^(.25){}="a" \ar[r]^-{F\langle {\mathtt{out}}, {\mathtt{next}}\rangle} \ar[d]_-{F\llbracket - \rrbracket} & F(M \times C) \ar[r]^{\mathsf{cst}} \ar[d] & M \times F(C) \ar[d]^-{\mathsf{id}\times \llbracket -\rrbracket} \\ M^\omega \ar[r]^-{\langle {\mathtt{head}}, {\mathtt{tail}}\rangle } & M \times M^\omega & F(M^\omega ) \ar[r]^-{F\langle {\mathtt{head}}, {\mathtt{tail}}\rangle } \ar[d]_-{\llbracket - \rrbracket} & F(M \times M^\omega) \ar[r]^\mathsf{cst} & M \times F(M^\omega) \ar[d] \\ && M^\omega \ar@{}[l]^(.25){}="b" \ar@<+0.75ex>@{<-}`l[uu]`[uu][uu] \ar[rr]^-{\langle {\mathtt{head}}, {\mathtt{tail}}\rangle } & & M \times M^\omega }\]

Another well-known coalgebraic principle captured using \((\mathbf{Set}, \times, \mathbb{1})\)-costrong functors is coinduction up-to: first, observe that the costrength of \(F\) induces in particular an \(F\)-algebra structure on the final \(G\)-coalgebra of streams, denoted above by \(\llbracket-\rrbracket: F(M^\omega) \longrightarrow M^\omega\). Next, given a function \(f: X \longrightarrow M^\omega\), it is often the case that there is no \(G\)-coalgebra structure on \(X\) such that the associated behaviour map to be precisely \(f\). Coinduction up-to remedies in many cases this issue: the \(F\)-algebra structure on streams guarantees, for any \(M \times F(-)\)-coalgebra \(\phi:X \longrightarrow M \times F(X)\), a unique arrow \(\tilde{\phi}: X \longrightarrow M^\omega\) making the diagram below commute [@Bartels2003]: \[\xymatrix@R=18pt@C=50pt{&& F(M^\omega) \ar[d]^{\llbracket - \rrbracket} \\ X \ar@{.>}[rr]^{\exists ! \tilde{\phi}} \ar[d]_{\phi} & & M^\omega \ar[d]^{\langle {\mathtt{head}}, {\mathtt{tail}}\rangle} \\ M \times F(X) \ar[r]^{\mathsf{id}\times F(\tilde{\phi})} & M \times F(M^\omega) \ar[r]^{\mathsf{id}\times \llbracket - \rrbracket} & M \times M^\omega }\] If the original \(f:X \longrightarrow M^\omega\) happens to satisfy the diagram, then by uniqueness, there is a coinductive definition for \(f\) (up-to \(\llbracket-\rrbracket\)).

5 Conclusions↩︎

The authors’ interest in costrong functors with respect to actions of monoidal categories emerged when studying transformations of profunctor optics as pairs of strong/costrong functors between actegories. By dualising the well-established notion of strong functors, we observed that costrength naturally arises in a variety of categorical constructions, particularly when considering coalgebraic structures and context interaction. Our results hint that costrength can be fruitfully understood through the lens of distributive laws, and that it provides a principled way to mediate between monoidal actions and coalgebraic behaviour specifications, beyond abstract formalism. Many directions remain open for further exploration. These include among other the development of a comprehensive theory of costrong functors, the study of costrength in enriched and higher-categorical contexts, and potential applications in effect-coeffect systems and compositional semantics.

In the appendix, we included several category-theoretical properties of costrong functors to be exploited in the future.

Acknowledgments↩︎

We thank the anonymous reviewers for the useful suggestions.

6 Costrong functors, categorically↩︎

In this section we gather a series of results on costrong functors. Some of them are direct consequences of the fact that \({\mathscr{M}}\)-actegories are the pseudo-algebras for the pseudomonad \({\mathscr{M}}\times -\) on \(\mathbf{Cat}\), while \({\mathscr{M}}\)-(co)strong functors between \({\mathscr{M}}\)-actegories are the corresponding (co)lax morphisms of algebras (and the same goes for (co)strong natural transformations).

6.0.0.1 Costrong functors as colax algebra morphisms.

Proposition 6. Let \(({\mathscr{M}}, \otimes,I)\) be a braided (or symmetric) monoidal category. Consider \({\mathscr{M}}\) as an \({\mathscr{M}}\)-actegory, with the regular action.

  1. There is an adjunction between \({\mathscr{M}}\) and the category \([{\mathscr{M}},{\mathscr{M}}]_\mathsf{cst}\) of \({\mathscr{M}}\)-costrong endofunctors on \({\mathscr{M}}\) and \({\mathscr{M}}\)-costrong natural transformations: \[\xymatrix@C=60pt{ {\mathscr{M}} \ar@<+1.1ex>[r]^-{M \mapsto M \otimes -} \ar@{}[r]|-{\top} & [{\mathscr{M}},{\mathscr{M}}]_\mathsf{cst} \ar@<+1.1ex>[l]^-{F \mapsto F(I)} }\]

  2. ([@HeunenKarvonen2015]) This adjunction lifts to an adjunction between the categories of comonoids in \({\mathscr{M}}\) and \({\mathscr{M}}\)-costrong comonads on \({\mathscr{M}}\): \[\xymatrix@C=60pt{ \mathbf{Comonoids}({\mathscr{M}}) \ar@<+1.1ex>[r]^{C \mapsto C \otimes -} \ar@{}[r]|-{\top} & \mathbf{Comonads}({\mathscr{M}})_\mathsf{cst} \ar@<+1.1ex>[l]^{\mathbb{D} \mapsto \mathbb{D}(I)} }\]

Proposition 7 (Doctrinal adjunction [@Kelly-Doctrinal]). Let \({\mathscr{M}}\) be a monoidal category and \({\mathscr{A}},{\mathscr{B}}\) two \({\mathscr{M}}\)-actegories related by an adjunction \(F \dashv G:{\mathscr{B}}\longrightarrow{\mathscr{A}}\). Then the following hold:

  1. The left adjoint \(F\) is \({\mathscr{M}}\)-costrong if and only if the right adjoint \(G\) is \({\mathscr{M}}\)-strong.

  2. The adjunction lifts to an adjunction in the \(2\)-category \({\mathscr{M}}\)-\(\mathbf{Act}_{\mathsf{cst}}\) if and only if the strength of the right adjoint \(G\) is a natural isomorphism.

Proposition 8 (Non-canonical isomorphism [@LucatelliNunes2019]). Let \((F,\mathsf{cst})\) be a costrong functor between \({\mathscr{M}}\)-actegories \({\mathscr{A}}\) and \({\mathscr{B}}\). If there exists an isomorphism \(F(M\cdot X) \longrightarrow M\cdot F(X)\), natural in both \(M\) and \(X\), then \(\mathsf{cst}:F(M\cdot X) \longrightarrow M\cdot F(X)\) is also a natural isomorphism.

6.0.0.2 Colimits of costrong functors.

Let \({\mathscr{A}}\) be a cocomplete \({\mathscr{M}}\)-actegory. Then \(\mathsf{End}({\mathscr{A}})\) is cocomplete, with colimits computed pointwise [@Kelly-book]. It is not hard to see that the inclusion functor
\(\mathsf{End}({\mathscr{A}})_\mathsf{cst}\longrightarrow\mathsf{End}({\mathscr{A}})\) creates colimits. In particular, coproducts of \({\mathscr{M}}\)-costrong functors are again costrong, and the coproduct injections are costrong natural transformations.

6.0.0.3 Free monads inherit costrength.

Given a functor \(F:{\mathscr{A}}\longrightarrow{\mathscr{A}}\), recall that a monad \(T\) on \({\mathscr{A}}\) is (algebraically) free on \(F\) if the forgetful functor \(\mathbf{Alg}(F) \longrightarrow{\mathscr{A}}\) is right adjoint, and the monad it generates is precisely \(T\) [@Kelly1980].

Proposition 9. Let \({\mathscr{A}}\) be a locally presentable \({\mathscr{M}}\)-actegory and \(F:{\mathscr{A}}\longrightarrow{\mathscr{A}}\) an accessible \({\mathscr{M}}\)-costrong functor. Then the free monad on \(F\) exists, and it is an \({\mathscr{M}}\)-costrong monad.

Proof. The existence of the free monad on \(F\) under the given hypotheses is well known. In particular, it can be obtained as \(TX = \mu Y.X+FY\). It remains to show that it is an \({\mathscr{M}}\)-costrong monad. The \({\mathscr{M}}\)-costrength of \(T\), denoted \(\mathsf{cst}^T\), is obtained as the unique morphism from the initial algebra in the diagram below. To save space, we denoted the \({\mathscr{M}}\)-action by juxtaposition: \[\xymatrix@C=50pt{ (M X)+ FT(M X) \ar[d]_{\mathsf{id}+ \mathsf{cst}^T} \ar[rrr]^{\mathsf{in}} & & & T(M X) \ar@{.>}[d]^{\mathsf{cst}^T} \\ (M X) + F(M T(X)) \ar[r]^{\mathsf{id}+\mathsf{cst}} & (M X)+(M FT(X)) \ar[r]^-{[\mathsf{id}\cdot \mathsf{inl}, \mathsf{id}\cdot \mathsf{inr}]} & M (X+FT(X)) \ar[r]^-{\mathsf{id}\cdot \mathsf{in}} & M T(X) }\] In the diagram above, the top arrow \(\mathsf{in}\) is the initial algebra isomorphism, while \(\mathsf{inl}\), \(\mathsf{inr}\) are the coproduct injections. Standard but tedious verifications show that \(\mathsf{cst}^T\) is natural both in \(M\) and in \(X\) and that \((T,\mathsf{cst}^T)\) is indeed an \({\mathscr{M}}\)-strong monad. ◻

6.0.0.4 Costrong functors and liftings to (co)algebras.

Let again \({\mathscr{A}}\) be an \({\mathscr{M}}\)-actegory. \({\mathscr{M}}\)-costrengths on a functor \(F:{\mathscr{A}}\longrightarrow{\mathscr{A}}\) are in one-to-one correspondences with liftings of the \({\mathscr{M}}\)-action from \({\mathscr{A}}\) to the category of \(F\)-algebras \(\mathbf{Alg}(F)\). This is analogue to the lifting of the monoidal structure to the Eilenberg-Moore category of algebras for a comonoidal monad [@Moerdijk2002], or to the lifting of an \({\mathscr{M}}\)-action to the Eilenberg-Moore category of algebras of an \({\mathscr{M}}\)-monad [@Skoda2004]. There is also a dual perspective: for every object \(M\) of the monoidal category \({\mathscr{M}}\) there is an endofunctor \(M\cdot -\) on every \({\mathscr{M}}\)-actegory. Then an \({\mathscr{M}}\)-costrength for a functor \(F:{\mathscr{A}}\longrightarrow{\mathscr{B}}\) induces a lifting of \(F\) between the categories of coalgebras for \(M \cdot -\), that is, between monoidal stream \(M\)-automata. Moreover, this lifting is uniform in \(M\). More details were discussed in Section 4.2, specifically regarding the case of the cartesian category of sets acting on itself.


  1. Support by the research project GNaC2023 ARUT 88/11.10.2023 Tensor Products and Nuclearity is acknowledged.↩︎

  2. We shall ignore size issues which might cause \(\mathsf{End}({\mathscr{A}})\) to be a large category.↩︎

  3. The copower of an object \(X\) by a natural number \(n\) is the coproduct of \(n\)-many copies of \(X\).↩︎

  4. A strong functor is not the same as a strong monoidal functor, the latter being equipped with an isomorphism \(I \cong F(I)\) and a natural isomorphism \(F(-)\otimes F(=) \cong F(-\otimes =)\) compatible with the associator and the unit of the monoidal category.↩︎

  5. For a formal argument, see Section 3.↩︎

  6. Recall that an object \(I\) in a category \({\mathscr{M}}\) is called a cogenerator if for any pair of arrows \(f,g:X \longrightarrow Y\) in \({\mathscr{M}}\), \(f=g\) if and only if \(h \circ f = h \circ g\) for any \(h:Y \longrightarrow I\). For example, in \(\mathbf{Set}\), any set with at least two elements is a cogenerator. A category possessing a generator (the dual notion) is also said to be well-pointed, or having enough points.↩︎

  7. More generally, via a mixed graded distributive law [@faul].↩︎

  8. Strictly speaking, optics depend not on the underlying categories \({\mathscr{A}}\), \({\mathscr{B}}\) but on their \({\mathscr{M}}\)-actions.↩︎