\mathsf {\mathbb Para} for a general 2-category [efr-GZH4]

We are now almost ready to prove:

Theorem [efr-I897]

Let \mathbb {C} be a 2-category which admits pullbacks, products and comma objects. Then there is a functor \mathsf {\mathbb Para}: \mathsf {Act}(\mathbb {C}) \to \mathsf {PsCat}(\mathbb {C}) from the 2-category of pseudomonoid actions and pseudolinear maps to the 2-category of pseudocategories and pseudofunctors, with \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C})_0 = \mathcal {C} and \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C})_1 = \mathcal {M} \times \mathcal {C} \downarrow \mathcal {C}. This functor preserves strict maps, limits, and filtered colimits.

The main ingredient missing is a characterization of the respective notions of pseudomorphism in terms of the limit sketches. This we do now:

Proposition [efr-NZ0X]

Let \mathbb {C} be a 2-category and let C,D : \mathcal {T}_\mathsf {PsCat} \to \mathbb {C} be pseudocategories, represented as models of the theory. Then a pseudonatural transformation F: C \to D which is strict on c,d,e and the limit projections \pi ^i_j is equivalently a pseudomorphism between the pseudocategories.

Now let (M,C), (N,D) : \mathcal {T}_\mathsf {Act} \to \mathbb {C} be pseudomonoid actions. Then a pseudonatural transformation F_m, F_c which preserves the product projections strictly is equivalently a pair of a pseudomorphism F_m : M \to N and a functor F_c: C \to D which is pseudolinear with respect to the action F_m(-) \cdot = of M on D.

Proof

Both of these are essentially a matter of unwinding the definitions. Let us start with pseudocategories. The requirement that F is strict on the product projections amounts to requiring that F_{C_2} : C_2 \to D_2 is given strictly as the pullback F_1 \times _{F_0} F_1, and not merely up to 2-isomorphism. With this, \mu is just a naturality transformation for m, and \epsilon is a naturality transformation for e. Note that since every map in \mathcal {T}_\mathsf {PsCat} is induced from m, e, c,d and the pullback structure, this means the other naturality transformations are determined by \mu , \epsilon

The composite m'(1_{F_1} \times \mu ) \mu (1 \times _{C_0} m) is the naturality transformation for the map m (1 \times m), and analogously for the composite m'(\mu \times 1_{F_1})\mu (m \times _{C_0} 1). Hence the hexagon is a pseudonaturality coherence for the 2-cell \alpha . Analogously the two squares can be obtained as coherence 2-cells. Conversely, these suffice to make F a pseudonatural transformation, again since all the other 2-cells are generated by \alpha , \rho ,\lambda .

Now let us look at pseudomonoid actions. As above, such a pseudonatural transformation is determined by the functors F_m: M \to N and F_c: C \to D plus some 2-cells involving these and their products. As a special case of the above when C_0, D_0 = * we find that the restriction F_m of the pseudonatural transformation to the pseudomonoid part is equivalently a strong monoidal functor. Now the required lineator l: \cdot _D (F_m \times F_c) \to F_m(\cdot ) is a naturality square for the multiplication map \cdot \in \mathcal {T}_\mathsf {Act}. As above this determines all the other naturality transformations because all the other maps are generated from \cdot (and the pseudomonoid structure) using the product structure. Also analogously to the above argument, the coherence pentagon is a pseudonaturality coherence for the natural isomorphism \mu , and the coherence triangle for \eta .

Remark [efr-T667]

This characterization of the notions of pseudomorphism cannot help but seem a little ad hoc. The basic idea here seems to go back to Power in Reference [power-enriched-lawvere]. After constructing an enriched Lawvere theory (which is just a special kind of limit sketch) corresponding to any finitary enriched monad, he notes that in the \mathsf {Cat}-enriched case the pseudomorphisms of monad algebras correspond to exactly those pseudonatural transformations which preserve the products strictly.

An elegant theory which generalizes this basic idea has recently been developed by Bourke, Ko, and Varkor in Reference [varkor-bourke-ko-sketches] (as we mentioned briefly before). Their theory involves decorating the sketch with a set of tight morphisms, which the transformations must be strictly natural with respect to. Beyond developing a general theory of this (not specialized to a few examples as above,) they also show how to construct the categories of (op)lax homomorphisms, and develop a commutativity of internalization principle for their models. This could be profitably applied in our case to understand better, for example, the implied notion of monoidal triple category, but we will not pursue this here.

Proof Proof of Theorem [efr-I897] [efr-0BHI]

First recall that \mathsf {Mod}(\mathcal {T},\mathbb {C}) can be identified with the subcategory of [\mathbb {C}^\mathrm {op}, \mathsf {Mod}(\mathcal {T})] spanned by the levelwise representable presheaves. Note that for \mathcal {T} = \mathcal {T}_\mathsf {PsCat}, it suffices to verify representability for C_0,C_1 \in \mathcal {T}_\mathsf {PsCat}, since the rest are pullbacks of these, and pullbacks of representable presheaves are again representable since \mathbb {C} admits pullbacks.

Postcomposition with the previously-constructed functor \mathsf {Mod}(\mathcal {T}_\mathsf {Act}) = \mathsf {Act}(\mathsf {Cat}) \to \mathsf {PsCat}(\mathsf {Act}) = \mathsf {Mod}(\mathcal {T}_\mathsf {PsCat}) gives a functor [\mathbb {C}^\mathrm {op},\mathsf {Mod}(\mathcal {T}_\mathsf {Act})] \to [\mathbb {C}^\mathrm {op},\mathsf {Mod}(\mathcal {T}_\mathsf {PsCat})]. Clearly this functor preserves representability (again, since limits of representable functors are representable). This gives the desired functor \mathsf {Mod}_s(\mathcal {T}_\mathsf {Act}, \mathbb {C}) \to \mathsf {Mod}_s(\mathcal {T}_\mathsf {PsCat}, \mathbb {C}).

Under the identification of \mathsf {Mod}(\mathcal {T},\mathbb {C}) with a subcategory of [\mathbb {C}^\mathrm {op} \times \mathcal {T}, \mathsf {Cat}], it is clear that the pseudonatural transformations of models correspond to those pseudonatural transformations which are strict on morphisms in \mathbb {C}^\mathrm {op}. This implies the full category \mathsf {Mod}_p(\mathbb {C}) of models and pseudonatural transformations can be identified with the subcategory of [\mathbb {C}^\mathrm {op},\mathsf {Mod}_p(\mathcal {T},\mathsf {Cat})] spanned by those 2-functors which come from models---that is, A: \mathbb {C}^\mathrm {op} \to \mathsf {Mod}_p(\mathcal {T}) = \mathsf {Mod}_p(\mathcal {T},\mathsf {Cat}) must factor over \mathsf {Mod}(\mathcal {T}) \hookrightarrow \mathsf {Mod}_p(\mathcal {T}).

(To be clear: the morphisms in [\mathbb {C}^\mathrm {op}, \mathsf {Mod}_p(\mathcal {T})] are strictly natural transformations between functors \mathbb {C}^\mathrm {op} \to \mathsf {Mod}_p(\mathcal {T}), but each component A(C) \to B(C) of such a natural transformation is a pseudonatural transformation of models).

Under this identification, it is clear that pseudofunctors correspond to those natural transformations in [\mathbb {C}^\mathrm {op}, \mathsf {Mod}_p(\mathcal {T}_\mathsf {PsCat})] which are valued in pseudofunctors, and analogously for pseudolinear morphisms and maps [\mathbb {C}^\mathrm {op}, \mathsf {Mod}_p(\mathcal {T}_\mathsf {Act})]. Hence it suffices to observe that the \mathsf {Cat}-valued version \mathsf {Mod}(\mathcal {T}_\mathsf {Act}) \to \mathsf {Mod}(\mathcal {T}_\mathsf {PsCat}) carries pseudolinear maps to pseudofunctors.

Note that \mathsf {\mathbb Para}: \mathsf {Mod}(\mathcal {T}_\mathsf {Act}) \to \mathsf {Mod}(\mathcal {T}_\mathsf {PsCat}) is given objectwise as a finite limit. Moreover, since the limit sketch of pseudocategories only involved finite limits, the class of pseudocategories is stable under filtered colimits in [\mathcal {T}_\mathsf {PsCat}, \mathsf {Cat}]. Hence \mathsf {\mathbb Para} commutes with filtered colimits, and is in particular accessible. Hence it admits a left adjoint L (M,C) \mapsto \operatorname {\mathrm {Hom}}_{\mathsf {Mod}(\mathcal {T}_\mathsf {Act})(L(-), (M,C))} where L: \mathcal {T}_\mathsf {PsCat}^\mathrm {op} \to [\mathcal {T}_\mathsf {Act},\mathsf {Cat}] is the restriction of the left adjoint of \mathsf {\mathbb Para}. Both forming the hom-category \operatorname {\mathrm {Hom}}(-, (M,C)) and precomposing with L are 2-functors, and as such preserve pseudonatural transformations. Thus it only remains to observe that \mathsf {\mathbb Para} also preserves the partial strictness property, but this clear.

We have not yet given any thought to functoriality in \mathbb {C}, but passing through the constructions, it is apparent that we have:

Proposition [efr-TY4G]

If \mathbb {C} \to \mathbb {D} is a 2-functor that preserves finite 2-limits, the square

commutes up to strict natural isomorphism. (In particular, the square involving the subcategories of strict homomorphisms also commutes up to natural isomorphism).

(It may seem wrong that, after working strictly all this time, this square commutes only up to natural isomorphism, but in fact that is the strict notion---the weak version of this statement would be that it commuted up to natural equivalence. Note that eg. the comma objects M \times C \downarrow C are only characterized up to isomorphism, so this is really the best we can hope for)

The main problem with Theorem [efr-I897] is that for many 2-categorical notions of interest, requiring (for example) the action \mathcal {M} \times \mathcal {C} \to \mathcal {C} to be a strict homomorphism of whatever structure under consideration is too strict to work, while working with the full category of pseudomorphisms prevents the pullbacks required for pseudocategories from existing. Thus for example, an internal pseudomonoid in \mathsf {MonCat}_s is a commutative monoidal category, which is far too strict for most purposes---generally speaking, symmetric monoidal categories can not be strictified into commutative ones.

In § [efr-ZRUZ], we will want to construct a symmetric monoidal "triple category"---that is, a symmetric monoidal pseudocategory in strict double categories. We will manage this via the preceding by noting that since \mathsf {Act}(\mathbb {C}) \to \mathsf {PsCat}(\mathbb {C}) preserves products, it carries (symmetric) pseudomonoids to pseudomonoids---in other words, we can apply the internalization the other way around, taking pseudomonoids in actions rather than actions in pseudomonoids. This works because strict products still exist in the category of pseudohomomorphisms, but for a more general categorical structure, we would be in trouble.

References

Reference Enhanced 2-categorical structures, two-dimensional limit sketches and the symmetry of internalisation [varkor-bourke-ko-sketches]

Abstract

  • December 10, 2024
  • Nathanael Arkor, John Bourke, Joanna Ko

Many structures of interest in two-dimensional category theory have aspects that are inherently strict. This strictness is not a limitation, but rather plays a fundamental role in the theory of such structures. For instance, a monoidal fibration is - crucially - a strict monoidal functor, rather than a pseudo or lax monoidal functor. Other examples include monoidal double categories, double fibrations, and intercategories. We provide an explanation for this phenomenon from the perspective of enhanced 2-categories, which are 2-categories having a distinguished subclass of 1-cells representing the strict morphisms. As part of our development, we introduce enhanced 2-categorical limit sketches and explain how this setting addresses shortcomings in the theory of 2-categorical limit sketches. In particular, we establish the symmetry of internalisation for such structures, entailing, for instance, that a monoidal double category is equivalently a pseudomonoid in an enhanced 2-category of double categories, or a pseudocategory in an enhanced 2-category of monoidal categories. 

 @article
{varkor-bourke-ko-sketches, title={Enhanced 2-categorical structures, two-dimensional limit sketches and the symmetry of internalisation}, url={http://arxiv.org/abs/2412.07475}, DOI={10.48550/arXiv.2412.07475}, abstractNote={Many structures of interest in two-dimensional category theory have aspects that are inherently strict. This strictness is not a limitation, but rather plays a fundamental role in the theory of such structures. For instance, a monoidal fibration is - crucially - a strict monoidal functor, rather than a pseudo or lax monoidal functor. Other examples include monoidal double categories, double fibrations, and intercategories. We provide an explanation for this phenomenon from the perspective of enhanced 2-categories, which are 2-categories having a distinguished subclass of 1-cells representing the strict morphisms. As part of our development, we introduce enhanced 2-categorical limit sketches and explain how this setting addresses shortcomings in the theory of 2-categorical limit sketches. In particular, we establish the symmetry of internalisation for such structures, entailing, for instance, that a monoidal double category is equivalently a pseudomonoid in an enhanced 2-category of double categories, or a pseudocategory in an enhanced 2-category of monoidal categories.}, number={arXiv:2412.07475}, publisher={arXiv}, author={Arkor, Nathanael and Bourke, John and Ko, Joanna}, year={2024}, month={Dec} }

Reference Enriched Lawvere Theories [power-enriched-lawvere]

  • 1999
  • John Power 
 @article
{power-enriched-lawvere, title={Enriched Lawvere Theories}, volume={6}, journal={Theory and Applications of Categories}, author={Power, John}, year={1999}, pages={83-93},language={English} }

Context

The \mathsf {Para} construction in generic 2-categories [efr-000D]

Introduction [efr-003P]

Myers' theory of categorical systems theory (see § [efr-0023]) gives a rich categorical structure to a wide variety of types of dynamical system. The central idea can be summarized by saying that there are two different, but tightly related, notions of morphism at play in dynamical systems. Open dynamical systems themselves involve a bidirectional information flow, captured by the notion of lens {X' \choose X} \leftrightarrows {Y' \choose Y}, and composition of such lenses describes the composition of subsystems into systems. But morphisms between systems are unidirectional, captured by the notion of chart {X' \choose X} \rightrightarrows {Y' \choose Y},. Algebraically, the relationship between these two notions is that they assemble into a double category, which indexes the category of systems.

There is another double category involving lenses which has been considered in the categorical study of systems. That is the double category of parametrized morphisms, applied to the monoidal category of lenses. These have been studied as an abstraction for gradient descent in several papers, see eg Reference [bruno-etal-categorical-learning-2021], Reference [bruno-thesis-fundamental-components], (the idea goes back to Reference [backprop-as-functor]). Given any action of a monoidal category \mathcal {M} on another category \mathcal {C} (most simply, if \mathcal {C} is monoidal it acts on itself,) we obtain a category of parametrized morphisms f: X \cdot P \to Y (where P \in \mathcal {M}, X, Y \in \mathcal {C},) and these turn out to be extremely useful. We will mention two applications:

  1. A parametrized lens {P \choose P} \otimes {X \choose X} \to {Y \choose Y} is essentially what is called a learner in Reference [backprop-as-functor]---it contains the information necessary to compute a new parameter value p' given an existing p \in P and a sample pair x \in X, y \in Y, as well as the additional information required to compose such things. Thus the functoriality of backpropagation can be derived from two facts: the reverse derivative defines a monoidal functor \mathsf {Euc} \to \mathsf {Lens}(\mathsf {Euc}), and the construction \mathsf {Para}(-), taking a category to its category of parametrized maps, is itself functorial. This viewpoint has been significantly developed in Reference [bruno-etal-categorical-learning-2021] and other papers.
  2. An open game, in the sense of Hedges Reference [hedges-etal-comp-gametheory], is almost the same thing as a parametrized lens {\Sigma ' \choose \Sigma } \otimes {S \choose X} \leftrightarrows {R \choose Y}, equipped with a subset E \subset \Sigma \times \mathsf {Set}(\Sigma ,\Sigma '). Given a context for the game---that is, a state x \in X (describing the state of information when the decision is made) and a continuation Y \to R (describing how decisions y \in Y map to outcomes r \in R,) we obtain a function k: \Sigma \to \Sigma ', and we say \sigma \in \Sigma is an equilibrium strategy if (\sigma ,k) \in E. Since \mathsf {Set}(\Sigma ,\Sigma ') = \mathsf {Lens}(\mathsf {Set})({\Sigma ' \choose \Sigma },I), and \Sigma = \mathsf {Lens}(\mathsf {Set})(I,{\Sigma ' \choose \Sigma }), this neatly captures the extra data of an open game in terms of the category of lenses. The potential of this idea as a generalized approach to "cybernetic systems" is explored in Reference [towards-cybercat].

In this chapter, we will develop the theory of the category \mathsf {Para} of parametrized maps. We will begin by reviewing the existing literature briefly. We will describe a double categorical version of this category---this does not seem to have appeared in the literature yet, although it has been folklore for at least a few years (and there is nothing complicated about this construction, certainly). The remainder of this chapter will be dedicated to lifting this construction to a generic 2-category \mathbb {C} (with the above being the specialization to \mathbb {C} = \mathsf {Cat} ). We will derive this lifting using the machinery of 2-category theory. We will see how this generalization accounts for much structure which can be seen to exist on \mathsf {Para}, such as its symmetric monoidal structure (assuming \mathcal {M},\mathcal {C} are symmetric monoidal). But the true application of this will be in § [efr-ZRUZ], where we use this to construct a triple category of open dynamical systems.

The definition of the double category \mathsf {\mathbb Para} involves two types of categorical structure with which the reader may be unfamiliar---actegories, which are the input to the construction, and pseudo double categories, which are the output. Since we will shortly introduce the abstract internal versions of these, internal pseudomonoid actions and internal pseudocategories, we will not give a separate introduction here. The reader who is unfamiliar with these should refer to Reference [actegories-amthematician-capucci-gavranovic] for actegories, and Reference [shulman-monfibs] for (pseudo) double categories. A reader who simply needs a definition may look at Definition [efr-OFNV] and Example [efr-ZRUY].

The Para Construction as a double category [efr-002H]

In many different situations, we want to understand some morphism as parametrized by some data. For example, in machine learning one tries to find a function f: X \to Y with some desirable behaviour by choosing a parametrization F: P \times X \to Y and searching for some p \in P so that F(p,-) has this behaviour (for example by gradient descent on p).

In situations where we want to understand F as being built up as a composite of multiple functions (for example, the layers of a neural network), it is convenient to introduce a category of parametrized morphisms, where the composition combines the parameter spaces of each composite map. We can do this in a general setting with the following definition:

Definition [efr-002G]

Let \mathcal {M} be a monoidal category, and let \bullet : \mathcal {M} \times \mathcal {C} \to \mathcal {C} be an action of \mathcal {M} on another category \mathcal {C}. Then the \mathsf {Para} construction is the category \mathsf {Para}_\mathcal {M}(\mathcal {C}) where

  1. Objects are objects of \mathcal {C}
  2. Morphisms A \to B are tuples P \in \mathcal {M}, P \bullet A \to B up to the natural notion of isomorphism.
  3. Composition is by tensoring the parameter objects and composing.

The fact that the parametrization object may live in a different category than the domain and codomain objects, which initially seems like a superfluous generalization, is in fact highly useful. For example, we will often want to consider parametrized morphisms where the parameter space is decorated with some additional data, for example a probability distribution. In most such cases, the category of spaces decorated with such data will act on the category of spaces without such data (simply by forgetting the data and tensoring), and hence we can realize such parametrized morphisms as examples of this \mathsf {Para} construction. We may also want only Euclidean parameter space (so that we can run gradient descent simply), but allow the parametrized morphism to go between more general manifolds.

\mathsf {Para}, and generalizations of it, have been introduced many times. One of the earliest occurrences is by Hermida and Tennent, Reference [hermida-monoidal-indeterminates], in the special case of a symmetric monoidal category acting on another such via a functor i: \mathcal {C} \to \mathcal {D} (by a result of Capucci and Gavranović, Reference [actegories-amthematician-capucci-gavranovic], every "structure-preserving" action of a symmetric monoidal category on another has this form). Hermida and Tennent actually give a very intuitive universal property of \mathsf {Para}_\mathcal {C}(\mathcal {D}): it is freely generated by adding a morphism I \to i(C) for each C \in \mathcal {C}, subject to the equations that this must be a monoidal natural transformation. This type of idea actually goes all the way back to Pavlović in Reference [pavlovic-categorical-names].

The notation \mathsf {Para} was introduced inReference [backprop-as-functor], where the special case of parametrized morphisms of euclidean spaces was used to study gradient descent. In Reference [towards-cybercat], a bicategorical variant (replacing the quotient by isomorphism in the above variant in the obvious way) is introduced.

Example [efr-MN7C]

Let \mathcal {C} be a monoidal category, and let S: \mathcal {C} \to \mathsf {Set} be any functor. Recall that \int S is the category whose objects are pairs (X \in \mathcal {C}, s \in S(X)) and whose morphisms (X,s) \to (Y,s') are f: X \to Y so that S(f)(s) = s'. If S is lax monoidal (for (\mathsf {Set},\times ),) \int S acquires a lax monoidal structure making the forgetful functor \int S \to \mathcal {C} strong (even strict) monoidal.

With the action induced by this functor, the bicategory \mathsf {Para}_{\int S}(\mathcal {C}) has morphisms given by maps M \otimes X \to Y, m \in S(M), and maps given by reparametrizations which preserve the decoration m.

For example, let \mathcal {C} be a Markov category and let S(X) = \mathcal {C}(I,X). Then morphisms are parametrized maps equipped with a measure on the parameter space.

Example [efr-WEST]

If \mathbb {C} = \mathsf {Set} regarded as a discrete 2-category, as noted, a pseudomonoid action is just a monoid action in the ordinary sense---that is, a monoid M, a set X and a function m \cdot x so that m \cdot (n \cdot x) = (mn) \cdot x. The para construction is then the action category, whose objects are the points of X and whose morphisms x \to y are elements m so that m \cdot x = y (with multiplication as composition).

Example [efr-QH7O]

Let \operatorname {\mathsf {Ab} - \mathsf {Cat}} be the 2-category of \mathsf {Ab}-enriched categories, functors and natural transformations. Recall that a ring R is the same as a one-object category enriched in \mathsf {Ab}, and it admits a monoidal structure if and only if it is commutative (this is not particular to \mathsf {Ab}-enriched categories). An enriched R-action on an \mathsf {Ab}-category \mathcal {C} is then an R-module structure on each hom-set so that composition is R-linear in each variable.

[efr-KL7V]

If a category has coproducts, then \mathsf {Set} acts on it via S \cdot X = \coprod _{s \in S}X. (This is the \mathsf {Set}-enriched case of what in enriched categories is called a copower or tensor, the dual of the power objects from Example [efr-K3YI]). The morphisms of \mathsf {Para}_\mathsf {Set}(\mathcal {C}) are pairs (I \in \mathsf {Set}, (f_i: X \to Y \in \mathcal {C})_{i \in I}), which compose in the obvious way.

Note that this definition clearly makes sense even if \mathcal {C} does not actually have coproducts. This is an example of another construction which has been called \mathsf {Para}, which takes a monoidal category \mathcal {V} and a \mathcal {V}-enriched category \mathcal {C} and constructs a double category where the morphisms are pairs (J \in \mathcal {V}, J \to \mathcal {C}(X,Y)). It is not hard to see that this also extends to a double category in the same way, but we do not presently know the correct definition of internal enriched object that would replace pseudomonoid actions to replicate our general theory for this case. (note that the literature contains a notion of internal enriched category, Reference [internal-enriched], but these are categories enriched over internal monoidal categories---that is, the ambient category \mathcal {E} is a 1-category and the categorical structure of the base of enrichment \mathcal {V} is formulated on top of this, not as part of the structure of the objects of the category \mathcal {E})

There is a very natural double categorical version of \mathsf {Para}, where the vertical morphisms are just the unparametrized morphisms of \mathcal {C}, and the 2-cells with this boundary:

are morphisms M \to N (if f is parametrized by M, g by N) so that the square
commutes.

This notion is not original---we learned of it from Matteo Capucci---but it seems to have remained somewhat on the level of folklore. Our main goal for this section will be to construct this (pseudo) double category, and show that it is functorial---that is, given a homomorphism of actions, there is an induced functor between double categories. In fact, we will show that this construction works in any 2-category. Later we will apply it to a pseudomonoid action in (strict) double categories to construct a pseudocategory internal to double categories---our triple category of bimachines.

Theorem [efr-55CC]

Let \mathcal {M} be a monoidal category, and let \mathcal {C} be a category with an \mathcal {M}-action.

Then there is a pseudo double category \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C}), with

  1. \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C})_0 = \mathcal {C}
  2. \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C})_1 = \mathcal {M} \times \mathcal {C} \downarrow \mathcal {C}, with domain and codomain given by the two projections to \mathcal {C}
  3. The identities map \mathcal {C} \to \mathcal {M} \times \mathcal {C} \downarrow \mathcal {C} is given by (I, 1_\mathcal {C}, 1_\mathcal {C}, \lambda ), where \lambda : I \cdot - \to - is the left unitor of \mathcal {M}.
  4. The horizontal composition map is the composition in \mathsf {Para}: given M \cdot X \to Y, N \cdot Y \to Z, their composite is given by (N \otimes M) \cdot X \cong N \cdot (M \cdot X) \to N \cdot Y \to Z. The horizontal composition of 2-cells is defined analogously.

Moreover, if \mathcal {C} \to \mathcal {D} is strict homomorphism of \mathcal {M}-modules, there is an induced pseudofunctor \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C}) \to \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {D}). If \mathcal {N} \to \mathcal {M} is a strict monoidal functor, then regarding \mathcal {C} as an \mathcal {N}-module along this map, there is an induced pseudofunctor \mathsf {\mathbb Para}_\mathcal {N}(\mathcal {C}) \to \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C}). These combine into a 2-functor \mathsf {Act}_s \to \mathsf {PsDbl}_s between the 2-category of actions and strictly linear functors and the category of pseudo double categories and strict double functors. This functor preserves (strict) limits.

Proof

Note that every actegory \mathcal {M} \curvearrowright \mathcal {C} is equivalent to a strict action of a strict monoidal category \mathcal {M}_s \curvearrowright \mathcal {C}_s (in the sense that there exists \mathcal {M}_s \xrightarrow {\sim } \mathcal {M} strong monoidal equivalence and \mathcal {C}_s \xrightarrow {\sim } \mathcal {C} an equivalence such that these maps together form a map of actegories). It follows that it suffices to show unitality and associativity for our composition in the strict case (since these are plainly preserved by equivalence).

Let \mathcal {M} \curvearrowright \mathcal {C}, \mathcal {M}' \curvearrowright \mathcal {C}', F: \mathcal {M} \to \mathcal {M}' be a strict monoidal functor, and let G: \mathcal {C} \to \mathcal {C}' be a linear functor "over F", that is a (strict) \mathcal {M}-linear functor when \mathcal {C}' is viewed as a \mathcal {M}-actegory along F. Then the induced functor \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C}) \to \mathsf {\mathbb Para}_{\mathcal {M}'}(\mathcal {C}') is given by G on the vertical category, and on the horizontal category by (M,X,X',\phi : M \cdot X \to X') \mapsto (F(M), G(X), G(X'), F(M) \cdot G(X) \simeq G(M \cdot X) \to G(X')) where the isomorphism is the linearity---noting that the M-action on \mathcal {C}' is precisely acting by F(M).

By naturality of the lineator it is straightforward to see that this is a functor, and it clearly preserves domain and codomain. It preserves units (strictly!) by the compatibility between the unitor and lineator. It remains to see that this preserves composition. For brevity, denote the induced functor H from here.

It suffices to verify this for strict actions. So the composite of M \cdot X \to Y, N \cdot Y \to Z is given by the composite (N \otimes M) \cdot X = N \cdot M \cdot X \to N \cdot Y \to Z.

Given two such composable maps, call them f,g, the two objects H(fg), H(f)H(g) are given by (F(M \otimes N), G(X), G(Z), \beta ), (F(M) \otimes F(N), G(X), G(Z), \alpha ) ,where \alpha , \beta are respectively the maps across the top and bottom of this diagram:

This proves that H preserves the composition strictly, as desired. (The rightmost triangle commutes by definition, and the leftmost rectangle is a lineator coherence)

Since the strict limits in \mathsf {PsDbl}_s and \mathsf {Act}_s are computed levelwise, it suffices to observe that the slice category also preserves limits, being a weighted limit itself.

Remark [efr-HUEE]

Note that \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C}) comes equipped with a strict functor to B\mathcal {M} (viewed as a double category). In fact, one can recover the action \cdot : \mathcal {M} \times \mathcal {C} \to \mathcal {C} from this data: the object M \cdot X is characterized up to isomorphism by its universal property: parametrized maps M \cdot X \nrightarrow Y with parameter N are in bijection with maps X \to Y parametrized by N \otimes M.

2-Limit sketches [efr-9I1M]

Definition Weighted limit [efr-L9JB]

Let \mathbb {C} be a 2-category, let D: \mathbb {I} \to \mathbb {C} be a 2-diagram in it, and let W: \mathbb {I} \to \mathsf {Cat} be another 2-functor. A limit of D weighted by {W} is an object \lim ^W D \in \mathbb {C} equipped with a natural isomorphism of categories \mathbb {C}(X,\lim ^W D) \cong [ {\mathbb {I} }, {\mathbb {C}} ] (W, \mathbb {C}(X,D(-))) (natural in X \in \mathbb {C}).

Example Particular weighted limits [efr-K3YI]

If W(-) = * is constant at the point, and \mathbb {I} is an 1-category, then a weighted limit is simply a L \to D(i) in the underlying category \mathbb {C}_0 so that there is additionally an isomorphism of categories \mathbb {C}(X,L) \xrightarrow {\sim } \lim _i \mathbb {C}(X,D(I)). Note that this is stronger than just a limit in \mathbb {C}_0. We will refer to limits of this form by their ordinary names---speaking for example of pullbacks, products, and so on.

If I = *, D(*) = D \in \mathbb {C}, and W(*) = C \in \mathsf {Cat}, the universal property of the weighted limit is that \mathbb {C}(X, \lim ^W D) = \mathsf {Cat}(C, \mathbb {C}(X,D)). In this case we write C \pitchfork D for this limit if it exists, and call it a power of D by C.

If \mathbb {I} = \{A \to B \leftarrow C\} and the weighting is given by W(B) = \{1 \to 2\}, W(A) = \{1\}, W(B) = \{2\} (with the obvious inclusions), then the weighted limit is called the comma object and will be denoted D(A) \downarrow _{D(B)} D(C). Note that if \mathbb {C} = \mathsf {Cat} this is precisely the ordinary comma category.

The analogue for a cone on an object C in the setting of weighted limits is called a cylinder: it is a natural transformation W(-) \to \mathbb {C}(C, D(-)). A cylinder on C induces a natural transformation \mathbb {C}(X,C) \to [ {\mathbb {I} }, {\mathbb {C}} ] (W(-),\mathbb {C}(X,D(-))), and we say it's a limit cylinder if this is an isomorphism.

Definition 2-limit sketch [efr-40Q5]

A 2-limit sketch is a small 2-category \mathcal {T} equipped with a (small) set of cylinders \Theta . A model of the sketch in \mathbb {C} is a 2-functor \mathcal {T} \to \mathbb {C} which carries each cylinder in \Theta to a limit cylinder. We write the category of models and natural transformations \mathsf {Mod}(\mathcal {T},\mathbb {C}) (leaving the set of cylinders implicit). If \mathbb {C} = \mathsf {Cat}, we write simply \mathsf {Mod}(\mathcal {T}).

Lemma [efr-D7EH]

Let \mathcal {T} be a 2-limit sketch. Then the functor \mathsf {Mod}(\mathcal {T},\mathbb {C}) \to [\mathbb {C}^\mathrm {op},\mathsf {Mod}(\mathcal {T})] given by A \in \mathsf {Mod}(\mathcal {T},\mathbb {C}) \mapsto (C \mapsto (S \in \mathcal {T} \mapsto \mathbb {C}(C,A(S)))) is fully faithful, and its essential image consists of those functors F so that each F(-)(S) : \mathbb {C}^\mathrm {op} \to \mathsf {Cat}, S \in \mathcal {T} is representable,

Proof

First note that the codomain can be identified with the subcategory of [\mathbb {C}^\mathrm {op} \times \mathcal {T}, \mathsf {Cat}] spanned by those F where each F(C,-) is a model. Since the Yoneda embedding preserves limits, the functor A \mapsto \operatorname {\mathrm {Hom}}(-, A(=)) from \mathsf {Mod}(\mathcal {T}) clearly lands inside here. Since \mathsf {Mod}(\mathcal {T},\mathbb {C}) is itself a full subcategory of the functor category [\mathcal {T},\mathbb {C}], this is fully faithful.

Clearly for each model A and for each S \in \mathcal {T}, the functor \mathbb {C}(-,A(S)) is representable, by A(S). Conversely, if F(C,S) is such that each F(-,S) is representable, then the currying of F \mathcal {T} \to [\mathbb {C}^\mathrm {op},\mathsf {Cat}] factors over \mathbb {C}, and since the Yoneda embedding preserves those limits that exist, this factorization must be a model as well.

Proposition [efr-9O7K]

Let \mathcal {T},\mathcal {T}' be limit sketches and suppose given a functor F: \mathsf {Mod}(\mathcal {T}) \to \mathsf {Mod}(\mathcal {T}') which preserves limits and is accessible, that is it preserved \kappa -filtered colimits for some \kappa . Then F admits a left adjoint L.

In particular, F(A)(S) = \mathsf {Mod}(\mathcal {T})(L(y(S)),A)

Pseudocategories [efr-ZRUW]

Given a 2-category \mathcal {C}, there is a natural loosening of the notion of "internal category in \mathcal {C}", given by requiring that associativity and unitality hold only up to chosen coherent isomorphism 2-cells. This is the notion of pseudocategory. We refer to Reference [pseudocategories] for a thorough description of this concept (as well as a review of the earlier literature). However, we will review the basic facts here for convenience.

Definition Internal pseudocategory [efr-ZRUX]

Let \mathcal {C} be a 2-category with pullbacks. Then an internal pseudocategory in \mathcal {C} (or simply a pseudocategory in \mathcal {C}) consists of the following data:

  1. Two objects C_0, C_1 \in \mathcal {C}
  2. Morphisms d,c: C_1 \to C_0, e: C_0 \to C_1 so that de = ce = 1_{A_0}
    3. .
  3. A morphism m: C_1 \times _{C_0} C_1 \to C_1, so that dm = d\pi _2, cm = c\pi _1
  4. Isomorphism 2-cells \alpha : m(1_{C_1} \times _{C_0} m) \to m(m \times _{C_0} 1_{C_1}), \lambda : m \langle ec, 1_{C_1} \rangle \to 1_CA_1
    5. , and \rho : m\langle 1_{A_1}, ed \rangle \to 1_{A_1}
  5. Satisfying the following equations:
    1. d \circ \lambda = 1_d = d \circ \rho
    2. c \circ \lambda = 1_c = c \circ \rho
    3. d \circ \alpha = 1_{d\pi _3}, c \circ \alpha = 1_{c\pi _1}
    4. \lambda \circ e = \rho \circ e
  6. And so that the following diagrams commute:

A homomorphism or strict functor of pseudocategories A \to B is a pair of morphisms F_1: A_1 \to B_1, F_0: A_0 \to B_0 which commute with all the structure---that is, dF_1 = F_0d, F_1 \alpha = \alpha (F_1 \times _{F_0} F_1 \times _{F_0} F_1), and so on. There is a clear notion of natural transformation of homomorphisms. We write \mathsf {PsCat}_s(\mathbb {C}) for the 2-category of pseudocategories, homomorphisms and natural transformations in \mathbb {C}.

It is important to note that, although this is a weakening of the definition of internal category, pseudocategories are themselves a strict concept---they are defined in terms of equations that must hold up to strict equality. Thus for example there is an enriched monad (a 2-monad) on \mathsf {Cat} whose strict algebras are the pseudo double categories.

Example [efr-ZRUY]
  1. An internal pseudocategory in \mathsf {Cat} is, as mentioned above, a pseudo double category.
  2. An internal pseudocategory A with A_0 terminal is the same thing as an internal pseudomonoid. If we fix a specific terminal object * and require A_0 = *, this is an isomorphism of 2-categories (both for the categories of pseudomorphisms and homomorphisms).
  3. An internal pseudocategory with \alpha ,\lambda ,\rho identities is the same thing as a (strict) internal category. In particular, internal pseudocategories in discrete 2-categories are merely internal categories.

Example [efr-LTJQ]

Let \mathsf {MonCat}_s be the 2-category of monoidal categories, strict monoidal functors and monoidal natural transformations. Note that this has pullbacks. Then the objects of \mathsf {PsCat}(\mathsf {MonCat}) are a stricter version of monoidal pseudo double categories: they are pseudo double categories C_1,C_0 where both C_1,C_0 carry a monoidal structure so that d,c,e,m are strict monoidal functors and \rho ,\lambda ,\alpha are monoidal natural transformations.

Here we are already beginning to feel the limitations of this internalization a bit---really we should ask for m, at least, to be only a strong monoidal functor. But we move on for now with this problematic definition.

Of course, there is a very crucial notion of pseudofunctor between pseudo double categories. This has an internal formulation in terms of pseudomorphisms:

Definition Pseudomorphism of pseudocategories [efr-8YZ9]

Let C = (C_0,C_1, d,c,e,m,\alpha ,\lambda ,\rho ) D = (D_0,D_1, d',c',e',m',\alpha ',\lambda ',\rho ') be internal pseudocategories in a 2-category \mathbb {C}. A pseudomorphism F: C \to D consists of the following data:

  1. Morphisms F_0: C_0 \to D_0, F_1:C_1 \to D_1 in \mathbb {C}
  2. Isomorphism 2-cells \mu : F_1m \to m(F_1 \times _{F_0} F_1) and \epsilon : F_1e \to eF_0
So that the following equations hold:
  1. d'F_1 = F_0d, c'F_1 = F_0c
  2. d' \circ \mu = 1_{F_0}d\pi _2, c' \circ \mu = 1_{F_0c\pi _1}
  3. d' \circ \epsilon = 1_{F_0}, c'\circ \epsilon = 1_{F_0}
And so that the following diagrams commute:

One should not spend too much time looking at Definition [efr-8YZ9]. This is clearly a horrible concept, and we will prefer to work around it rather than referring to it explicitly. It may be a useful exercise to convince oneself that, when C_0 = * and the pseudocategory is a pseudomonoid---eg a monoidal category---this coincides with the notion of strong monoidal functor.

One can also define lax and oplax functors between pseudo double categories, but we will not need that concept here.

Proposition [efr-7ZZG]

There exists a \mathsf {Cat}-limit sketch (\mathcal {T}_\mathsf {PsCat}, \Theta _\mathsf {PsCat}) whose strict models are internal pseudocategories, and whose strict natural transformations are homomorphisms.

Proof

There is nothing surprising about this to those familiar with limit sketch presentations of other algebraic gadgets, but for completeness we give an explicit construction here.

Take \mathcal {T}_\mathsf {PsMon} to have objects C_0,C_1,C_2,C_3,C_4. The 2-category is freely generated by these objects and the following data:

  1. Morphisms d,c : C_1 \to C_0
  2. Morphisms \pi _1^i, \pi _2^i: C_{i+1} \to C_i for i=1,2,3, so that
    commutes.
  3. Morphisms m: C_2 \to C_1 and e: C_0 \to C_1 satisfying dm = d\pi _1^1, cm = c\pi _2^1, de = ce = 1_{C_0}
  4. Further morphisms, and invertible 2-cells \alpha ,\lambda ,\rho , as in the following diagrams:
    and all the other induced morphisms appearing in Definition [efr-ZRUX], subject to those equations holding.
  5. Equations asserting that the morphisms and 2-cells with codomain C_i, i>1 behave as expected under postcomposition with the pullback projections.

The prescribed pullback cones \Theta are the diagrams involving \pi _j^i for i=0,1,2.

An explicit description of this sketch seems not to have appeared in the literature until Reference [varkor-bourke-ko-sketches] (example 5.13). Note that they construct a richer object, what they term an \mathcal {F}-sketch, which includes the information that the domain and codomain are "tight" and must be preserved strictly by pseudofunctors, but composition and identities are "loose" and may be preserved only up to natural isomorphism. This idea will be highly useful later, although we will not go into a full treatment of their theory.

Actegories [efr-NI76]

Definition Actegory [efr-OFNV]

Let \mathcal {M} be a monoidal category. A \mathcal {M}-actegory (also \mathcal {M}-module, \mathcal {M}-action) is a category \mathcal {C} equipped with a functor \cdot : \mathcal {M} \times \mathcal {C} \to \mathcal {C} called the action (written infix, M \cdot C), and natural isomorphisms \mu : (M \otimes M') \cdot C \to M \cdot (M' \cdot C), \eta : I \cdot C \to C satisfying the following coherence equations:

Actegories are a very natural concept, and as one would expect their history goes back a long way. The concept has been considered by Benabou all the way back in Reference [benabou-bicategories], and used many times since them. We will not delve too deeply into their theory here---see Reference [actegories-amthematician-capucci-gavranovic] for a thorough treatment.

Just as pseudo double categories, actegories really make sense in every 2-category, as a weakening of monoid actions.

Definition Pseudomonoid action [efr-IOLJ]

Let \mathbb {C} be a 2-category. A pseudomonoid action internal to \mathbb {C} consists of the following data: An internal pseudomonoid M, an object C, a morphism \cdot : M \times C \to C, natural isomorphisms \mu : \cdot (\otimes \times 1_C) \to \cdot (1_M \times \cdot ) and \eta : \cdot \langle e, 1_C \rangle \to 1_C, satisfying the coherence equations from Definition [efr-OFNV].

A strict homomorphism of actions is a pair F_m: M \to M', F_c: C \to C' so that F_m is a strictly monoidal functor and F_c preserves the action strictly, i.e F_m(M) \cdot F_c(C) = F_c(M \cdot C), F_c(\eta ) = \eta ', etc. Note that this makes sense even if the monoidal category or action is not itself strict.

Proposition [efr-6S13]

There is a limit sketch \mathcal {T}_\mathsf {Act}, \Theta _\mathsf {Act} whose models are tuples (M,C,\cdot ) of a pseudomonoid M = (M,\otimes ,I), an object C and an action \cdot of M on C. The strict natural transformations between models are strictly linear functors.

Proof

As above, there is nothing difficult about this. Let \mathcal {T}_\mathsf {Act} contain as a subcategory the sketch of pseudomonoids \mathcal {T}_\mathsf {PsMon}, along with three additional objects C, MC, MMC, projections \pi ^1_M, \pi ^1_C: MC \to M,C, \pi ^2_{M_1}, \pi ^2_{M_2}, \pi ^2_{C} : MMC \to M, M, C, and limit cones expressing these as the products M \times C and M \times M \times C respectively, a morphism \cdot : MC \to C, and isomorphism 2-cells \eta : 1_C \Rightarrow \cdot \langle I, 1_C \rangle and \mu : \cdot \langle \pi ^2_{M_1}, \cdot \langle \pi ^2_{M_2}, \pi ^2_C \rangle \rangle \to \cdot \langle \otimes \langle \pi ^2_{M_1}, \pi ^2_{M_2} \rangle , \pi ^2_C \rangle , subject to the coherence equations in Definition [efr-OFNV].

Example Discrete pseudomonoid [efr-I33G]

If \mathbb {C} = \mathcal {C} is an ordinary category with finite products (viewed as a discrete 2-category), a pseudomonoid is simply an internal monoid, and an action is just a monoid action in the ordinary sense.

Example Monoidal and symmetric monoidal actegories [efr-ARIX]

In Reference [actegories-amthematician-capucci-gavranovic], the authors study actegories with extra monoidal structure. Although they do not introduce pseudomonoid actions in a general 2-category, they study actegories internal to monoidal categories, which they call monoidal actegories. It is straightforward to check that pseudomonoid actions in \mathsf {MonCat} agree with their notion: such an action consists of a braided monoidal category \mathcal {M}, an ordinary monoidal category \mathcal {C}, a monoidal functor \mathcal {M} \times \mathcal {C} \to \mathcal {C}, and monoidal natural transformations \mu ,\eta satisfying the coherence equations for an actegory.

(Note that since the functor \otimes appears on one side of \mu , to speak of \mu being a monoidal natural transformation we must have a monoidal structure on \otimes ---this makes \mathcal {M} into a braided monoidal category).

For the case of symmetric monoidal actegories, since \mathsf {SymMonCat} is cocartesian, \mathsf {PsMon}(\mathsf {SymMonCat}) \simeq \mathsf {SymMonCat}. Given two symmetric monoidal categories \mathcal {M},\mathcal {C}, Reference [actegories-amthematician-capucci-gavranovic] show that an action is simply given by a strong symmetric monoidal functor f: \mathcal {M} \to \mathcal {C} (and in this case the action is M \cdot C = F(M) \otimes C). Unwinding this construction we see that \mathsf {Act}_s(\mathsf {SymMonCat}) is bi-equivalent to a category which has as objects strong (but not strict) symmetric monoidal functors C \to C', and morphisms squares

of symmetric monoidal functors, where the top map is strict, and which commute strictly.

Again, as expected, the notion of strict linear morphism is usually too strict. One can expect an equation like F_m(M) \cdot F_c(C) = F_c(M \cdot C) to hold only up to coherent isomorphism. Let us now make this clear:

Definition Pseudolinear map [efr-L5QG]

Let \mathbb {C} be a 2-category, and let (M,C,\cdot ), (N,D,\star ) be internal pseudomonoid actions. A pseudolinear map (or just linear) is a pair of maps F_m: M \to N, F_c: C \to D, equipped with a pseudomonoid pseudohomomorphism structure \phi , \tau on F_m and a natural isomorphism l: F_m(-) \cdot F_c(=) \to F_c(- \cdot =) satisfying the following coherence conditions (note that writing functors using element-notation like this is well-defined)

In Reference [actegories-amthematician-capucci-gavranovic], these are defined in two steps: first linear functors for the same \mathcal {M} (those with F_m = 1_\mathcal {M}) are considered. Then, given a strong monoidal \mathcal {M} \to \mathcal {N}, a functorial assignment of an \mathcal {M}-action to every \mathcal {N}-action is constructed, and the full category of actions is defined as the Grothendieck construction of this. There is nothing preventing this from working in the setting of a general 2-category, and it is straightforward to verify that our notion of linear morphism of actions agrees with theirs.

\mathsf {\mathbb Para} for a general 2-category [efr-GZH4]

We are now almost ready to prove:

Theorem [efr-I897]

Let \mathbb {C} be a 2-category which admits pullbacks, products and comma objects. Then there is a functor \mathsf {\mathbb Para}: \mathsf {Act}(\mathbb {C}) \to \mathsf {PsCat}(\mathbb {C}) from the 2-category of pseudomonoid actions and pseudolinear maps to the 2-category of pseudocategories and pseudofunctors, with \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C})_0 = \mathcal {C} and \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C})_1 = \mathcal {M} \times \mathcal {C} \downarrow \mathcal {C}. This functor preserves strict maps, limits, and filtered colimits.

The main ingredient missing is a characterization of the respective notions of pseudomorphism in terms of the limit sketches. This we do now:

Proposition [efr-NZ0X]

Let \mathbb {C} be a 2-category and let C,D : \mathcal {T}_\mathsf {PsCat} \to \mathbb {C} be pseudocategories, represented as models of the theory. Then a pseudonatural transformation F: C \to D which is strict on c,d,e and the limit projections \pi ^i_j is equivalently a pseudomorphism between the pseudocategories.

Now let (M,C), (N,D) : \mathcal {T}_\mathsf {Act} \to \mathbb {C} be pseudomonoid actions. Then a pseudonatural transformation F_m, F_c which preserves the product projections strictly is equivalently a pair of a pseudomorphism F_m : M \to N and a functor F_c: C \to D which is pseudolinear with respect to the action F_m(-) \cdot = of M on D.

Proof

Both of these are essentially a matter of unwinding the definitions. Let us start with pseudocategories. The requirement that F is strict on the product projections amounts to requiring that F_{C_2} : C_2 \to D_2 is given strictly as the pullback F_1 \times _{F_0} F_1, and not merely up to 2-isomorphism. With this, \mu is just a naturality transformation for m, and \epsilon is a naturality transformation for e. Note that since every map in \mathcal {T}_\mathsf {PsCat} is induced from m, e, c,d and the pullback structure, this means the other naturality transformations are determined by \mu , \epsilon

The composite m'(1_{F_1} \times \mu ) \mu (1 \times _{C_0} m) is the naturality transformation for the map m (1 \times m), and analogously for the composite m'(\mu \times 1_{F_1})\mu (m \times _{C_0} 1). Hence the hexagon is a pseudonaturality coherence for the 2-cell \alpha . Analogously the two squares can be obtained as coherence 2-cells. Conversely, these suffice to make F a pseudonatural transformation, again since all the other 2-cells are generated by \alpha , \rho ,\lambda .

Now let us look at pseudomonoid actions. As above, such a pseudonatural transformation is determined by the functors F_m: M \to N and F_c: C \to D plus some 2-cells involving these and their products. As a special case of the above when C_0, D_0 = * we find that the restriction F_m of the pseudonatural transformation to the pseudomonoid part is equivalently a strong monoidal functor. Now the required lineator l: \cdot _D (F_m \times F_c) \to F_m(\cdot ) is a naturality square for the multiplication map \cdot \in \mathcal {T}_\mathsf {Act}. As above this determines all the other naturality transformations because all the other maps are generated from \cdot (and the pseudomonoid structure) using the product structure. Also analogously to the above argument, the coherence pentagon is a pseudonaturality coherence for the natural isomorphism \mu , and the coherence triangle for \eta .

Remark [efr-T667]

This characterization of the notions of pseudomorphism cannot help but seem a little ad hoc. The basic idea here seems to go back to Power in Reference [power-enriched-lawvere]. After constructing an enriched Lawvere theory (which is just a special kind of limit sketch) corresponding to any finitary enriched monad, he notes that in the \mathsf {Cat}-enriched case the pseudomorphisms of monad algebras correspond to exactly those pseudonatural transformations which preserve the products strictly.

An elegant theory which generalizes this basic idea has recently been developed by Bourke, Ko, and Varkor in Reference [varkor-bourke-ko-sketches] (as we mentioned briefly before). Their theory involves decorating the sketch with a set of tight morphisms, which the transformations must be strictly natural with respect to. Beyond developing a general theory of this (not specialized to a few examples as above,) they also show how to construct the categories of (op)lax homomorphisms, and develop a commutativity of internalization principle for their models. This could be profitably applied in our case to understand better, for example, the implied notion of monoidal triple category, but we will not pursue this here.

Proof Proof of Theorem [efr-I897] [efr-0BHI]

First recall that \mathsf {Mod}(\mathcal {T},\mathbb {C}) can be identified with the subcategory of [\mathbb {C}^\mathrm {op}, \mathsf {Mod}(\mathcal {T})] spanned by the levelwise representable presheaves. Note that for \mathcal {T} = \mathcal {T}_\mathsf {PsCat}, it suffices to verify representability for C_0,C_1 \in \mathcal {T}_\mathsf {PsCat}, since the rest are pullbacks of these, and pullbacks of representable presheaves are again representable since \mathbb {C} admits pullbacks.

Postcomposition with the previously-constructed functor \mathsf {Mod}(\mathcal {T}_\mathsf {Act}) = \mathsf {Act}(\mathsf {Cat}) \to \mathsf {PsCat}(\mathsf {Act}) = \mathsf {Mod}(\mathcal {T}_\mathsf {PsCat}) gives a functor [\mathbb {C}^\mathrm {op},\mathsf {Mod}(\mathcal {T}_\mathsf {Act})] \to [\mathbb {C}^\mathrm {op},\mathsf {Mod}(\mathcal {T}_\mathsf {PsCat})]. Clearly this functor preserves representability (again, since limits of representable functors are representable). This gives the desired functor \mathsf {Mod}_s(\mathcal {T}_\mathsf {Act}, \mathbb {C}) \to \mathsf {Mod}_s(\mathcal {T}_\mathsf {PsCat}, \mathbb {C}).

Under the identification of \mathsf {Mod}(\mathcal {T},\mathbb {C}) with a subcategory of [\mathbb {C}^\mathrm {op} \times \mathcal {T}, \mathsf {Cat}], it is clear that the pseudonatural transformations of models correspond to those pseudonatural transformations which are strict on morphisms in \mathbb {C}^\mathrm {op}. This implies the full category \mathsf {Mod}_p(\mathbb {C}) of models and pseudonatural transformations can be identified with the subcategory of [\mathbb {C}^\mathrm {op},\mathsf {Mod}_p(\mathcal {T},\mathsf {Cat})] spanned by those 2-functors which come from models---that is, A: \mathbb {C}^\mathrm {op} \to \mathsf {Mod}_p(\mathcal {T}) = \mathsf {Mod}_p(\mathcal {T},\mathsf {Cat}) must factor over \mathsf {Mod}(\mathcal {T}) \hookrightarrow \mathsf {Mod}_p(\mathcal {T}).

(To be clear: the morphisms in [\mathbb {C}^\mathrm {op}, \mathsf {Mod}_p(\mathcal {T})] are strictly natural transformations between functors \mathbb {C}^\mathrm {op} \to \mathsf {Mod}_p(\mathcal {T}), but each component A(C) \to B(C) of such a natural transformation is a pseudonatural transformation of models).

Under this identification, it is clear that pseudofunctors correspond to those natural transformations in [\mathbb {C}^\mathrm {op}, \mathsf {Mod}_p(\mathcal {T}_\mathsf {PsCat})] which are valued in pseudofunctors, and analogously for pseudolinear morphisms and maps [\mathbb {C}^\mathrm {op}, \mathsf {Mod}_p(\mathcal {T}_\mathsf {Act})]. Hence it suffices to observe that the \mathsf {Cat}-valued version \mathsf {Mod}(\mathcal {T}_\mathsf {Act}) \to \mathsf {Mod}(\mathcal {T}_\mathsf {PsCat}) carries pseudolinear maps to pseudofunctors.

Note that \mathsf {\mathbb Para}: \mathsf {Mod}(\mathcal {T}_\mathsf {Act}) \to \mathsf {Mod}(\mathcal {T}_\mathsf {PsCat}) is given objectwise as a finite limit. Moreover, since the limit sketch of pseudocategories only involved finite limits, the class of pseudocategories is stable under filtered colimits in [\mathcal {T}_\mathsf {PsCat}, \mathsf {Cat}]. Hence \mathsf {\mathbb Para} commutes with filtered colimits, and is in particular accessible. Hence it admits a left adjoint L (M,C) \mapsto \operatorname {\mathrm {Hom}}_{\mathsf {Mod}(\mathcal {T}_\mathsf {Act})(L(-), (M,C))} where L: \mathcal {T}_\mathsf {PsCat}^\mathrm {op} \to [\mathcal {T}_\mathsf {Act},\mathsf {Cat}] is the restriction of the left adjoint of \mathsf {\mathbb Para}. Both forming the hom-category \operatorname {\mathrm {Hom}}(-, (M,C)) and precomposing with L are 2-functors, and as such preserve pseudonatural transformations. Thus it only remains to observe that \mathsf {\mathbb Para} also preserves the partial strictness property, but this clear.

We have not yet given any thought to functoriality in \mathbb {C}, but passing through the constructions, it is apparent that we have:

Proposition [efr-TY4G]

If \mathbb {C} \to \mathbb {D} is a 2-functor that preserves finite 2-limits, the square

commutes up to strict natural isomorphism. (In particular, the square involving the subcategories of strict homomorphisms also commutes up to natural isomorphism).

(It may seem wrong that, after working strictly all this time, this square commutes only up to natural isomorphism, but in fact that is the strict notion---the weak version of this statement would be that it commuted up to natural equivalence. Note that eg. the comma objects M \times C \downarrow C are only characterized up to isomorphism, so this is really the best we can hope for)

The main problem with Theorem [efr-I897] is that for many 2-categorical notions of interest, requiring (for example) the action \mathcal {M} \times \mathcal {C} \to \mathcal {C} to be a strict homomorphism of whatever structure under consideration is too strict to work, while working with the full category of pseudomorphisms prevents the pullbacks required for pseudocategories from existing. Thus for example, an internal pseudomonoid in \mathsf {MonCat}_s is a commutative monoidal category, which is far too strict for most purposes---generally speaking, symmetric monoidal categories can not be strictified into commutative ones.

In § [efr-ZRUZ], we will want to construct a symmetric monoidal "triple category"---that is, a symmetric monoidal pseudocategory in strict double categories. We will manage this via the preceding by noting that since \mathsf {Act}(\mathbb {C}) \to \mathsf {PsCat}(\mathbb {C}) preserves products, it carries (symmetric) pseudomonoids to pseudomonoids---in other words, we can apply the internalization the other way around, taking pseudomonoids in actions rather than actions in pseudomonoids. This works because strict products still exist in the category of pseudohomomorphisms, but for a more general categorical structure, we would be in trouble.

Related

Theorem [efr-I897]

Let \mathbb {C} be a 2-category which admits pullbacks, products and comma objects. Then there is a functor \mathsf {\mathbb Para}: \mathsf {Act}(\mathbb {C}) \to \mathsf {PsCat}(\mathbb {C}) from the 2-category of pseudomonoid actions and pseudolinear maps to the 2-category of pseudocategories and pseudofunctors, with \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C})_0 = \mathcal {C} and \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C})_1 = \mathcal {M} \times \mathcal {C} \downarrow \mathcal {C}. This functor preserves strict maps, limits, and filtered colimits.

Categories of stochastic dynamical systems [efr-ZRUZ]

Introduction [efr-5QC5]

Given a set of inputs A and a set of outputs B, there are essentially two make sense of the informal description "finite-state automaton which reads inputs from A and produces outputs in B". These are the notions of Mealy machine and Moore machine. Simply put, if the set of states is S, a mealy machine is a function A \times S \to B \times S, whereas a Moore machine is a pair A \times S \to S, S \to B. In other words, in a Moore machine the output does not depend on the current input, but only on previous inputs (through their effect on the state), but in a Mealy machine, the input can be passed through directly.

Using the language of categorical systems theory, we can make the following definitions:

Definition Moore Machine [efr-0006]

In a dynamical systems theory, a Moore machine with state space S and interface A is a lens TS \leftrightarrows A. The category of Moore machines with interface A is the slice category of the functor T over A---that is, a morphism of Moore machines is a morphism S \to S' so that the obvious triangle commutes.

Definition Mealy Machine [efr-0005]

In a dynamical systems theory, a Mealy machine with state space S and interface A consists of a costate lens TS \otimes A \leftrightarrows I. The category of Mealy machines with interface A is the comma category of the functor T(-) \otimes A over I---that is, a morphism of Mealy machines is S \to S' so that the obvious triangle commutes.

A Moore machine in the sense of Definition [efr-0006] is what Myers calls a (open) dynamical system, and they are the central object of study in Reference [myers-cst]. Arguably, both Moore machines and Mealy machines deserve the name of "open dynamical system"---the difference is how they interact with the external world.

Observe in particular that, if A=I, the categories of Mealy and Moore machines agree, both being equal to the slice of T over the unit I. In other words, the two notions of closed dynamical system coincide.

It is clear that both Mealy and Moore machines, in this sense, are special kinds of parametrized morphism in lenses, namely those parametrized by an object of the form TS. This leads naturally to the idea that there should be a triple category of morphisms of this type, charts, and lenses.

We call the parametrized lenses TS \otimes \bar {A} \leftrightarrows \bar {B} bisystems since they generalize the two types of machine, Moore and Mealy (but we choose to stick with "system" rather than "machine").

Example Machine Learning as a bisystem [efr-000E]

It is an observation which goes back at least to Reference [backprop-as-functor], and was more thoroughly developed in Reference [bruno-etal-categorical-learning-2021], that the process of training a machine learning algorithm by gradient descent can be abstracted in the following way:

  • Wanting to learn a function X \to Y, we choose a parametrized function f: X \times P \to Y, where all these are, in the simplest case, Euclidean spaces \mathbb {R}^k
  • We take the backwards derivative of f, obtaining a lens: (f,Df): {TX \choose X} \otimes {TP \choose P} \leftrightarrows {TY \choose Y}
  • For each datum (x_n,y_n), we compute the loss gradient \nabla L(-,y_n) : Y \to TY, and combining this with x_n \in X and the current parameter p, we get a gradient on the parameter space which we can use to update

Thus a machine learning algorithm is a sort of bisystem. Indeed our bisystems are essentially an abstracted version of the learners of Fong--Spivak--Tuyeras. The functoriality of this assignment is the main point of the above-mentioned papers.

In this chapter, we will put together the ingredients we have assembled so far and construct a triple category of stochastic dynamical systems. We will also give the construction of triple categories of systems in the ordinary case.

Note that the theory of Markov fibrations does not quite generalize the ordinary theory of fibrations---only fibrations with a Cartesian base (Example [efr-CJTH] and Proposition [efr-Z75A]). Since the pullbacks in \mathcal {C}_\mathrm {det} play such a key role in the theory, it is not clear that this can be dispensed with. Although Cartesian bases certainly cover the vast majority of examples from the literature on categorical systems, it is of course worth noting that they are not a requirement. Moreover, we will see that the construction of the double category of lenses and charts encounters certain problems for a general Markov fibration not seen for ordinary fibrations. Hence we will give a separate description of the triple categories in each of the two cases.

The notions of Mealy and Moore machine are both quite old, going back to Reference [mealy-circuits], Reference [moore-gedanken-sequential]. While we do obtain finite-state automata of these types as special cases, our interest is primarily in the analysis of dynamical systems, which tends to ask rather different questions than automata theory. Thus, despite using the terminology, we will not be particularly interested in the actual theory of Mealy and Moore machines. We do mention one recent paper, Reference [semibicategory-of-moore-automata], which has a category-theoretic approach similar in spirit to our own. Their category of Mealy machines can be obtained, not as our category of Mealy machines above, but by considering maps TS \otimes A \to B in the case where A = {* \choose A}, B = {* \choose B} are trivial in the secondary component. In the discrete case, such a map is given by A \times S \to B \times S.

It should also be noted that the idea of embedding Mealy machines as the morphisms TS \otimes A \to I is not original, but was communicated to the author by Matteo Capucci. It seems not to have appeared in the literature so far. The idea that there "should" be a triple category of systems, like the one we will construct, has also circulated as folklore, although again an explicit construction has yet to appear. Very similar ideas appear in the work of Shapiro and Spivak, see for example Reference [shapiro-spivak-dynamic-operads].

We begin this chapter with a treatment of double categories of charts and lenses in the context of Markov fibrations (and stochastic modules). The construction does not work quite as well as in the classical case---the difficulty is essentially that the equivalence relation which defines stochastic charts has a directed nature, and given a 2-cell defined in an obvious way \phi \to \psi , and an equation \psi \xleftarrow {\sim } \psi ', there is not (apparently) in general a way to lift this to an arrow \phi ' \to \psi ' (with \phi ' \simeq \phi ). However, we can construct a double category whose globular horizontal 2-category have connected components given by the stochastic charts (or lenses).

We proceed to give an account of categorical systems theory for these double categories. The chief problem posed by the above is that we may not have any good clock systems (Example [efr-9WQU]). Two equivalent charts should represent the same system, but they may receive different sets of maps from the supposed clock system (and thus have different sets of trajectories). We resolve this by proving that, for lenses with a deterministic base, every equivalence class of lenses has an initial representative. Moreover, mapping out of this initial representative to a representative of some other lens, a 2-cell exists filling a given square if and only if it commutes as a map of lenses and charts in the classical case (recall that over deterministic bases, Markov fibrations become ordinary fibrations). In particular the trajectories of a system with respect to such a clock system depend only on their equivalence class.

We follow this up by constructing the above discussed triple categories of "bimachines", that is systems which combine Mealy and Moore machines. We do this both for stochastic and the ordinary case---the procedure is exactly the same, but of course they are different objects, neither generalizing the other.

We end by constructing a stochastic dynamical systems theory for smooth dynamical systems---requiring a brief detour to construct a suitable Markov category of smooth kernels.

Double categories of stochastic charts and lenses [efr-SIE7]

To construct the double category \mathsf {\mathbb Arena}(\mathcal {A}) of charts and lenses for an ordinary fibration \mathcal {A} \to \mathcal {C}, one can use the following procedure:

  1. Form the square double category \mathcal {A}^\to \rightrightarrows \mathcal {A}
  2. Take the fiberwise opposite of these objects: (\mathcal {A}^\to )^\mathrm {fop} \rightrightarrows \mathcal {A}^\mathrm {fop}.
  3. Observe that fiberwise opposite preserves pullbacks, and hence this is again a double category.

Here we used the following result: If \mathcal {D} \to \mathcal {C} is a Grothendieck fibration and \mathcal {A} is any category, then \mathcal {D}^\mathcal {A} \to \mathcal {C}^\mathcal {A} is again a fibration (which classifies the lax limits of the composite \mathcal {A}^\mathrm {op} \to \mathcal {C}^\mathrm {op} \to \mathsf {Cat}), and a natural transformation is Cartesian iff it is levelwise Cartesian. It would be neat to obtain a similar result for Markov fibrations.

The first problem with this is that \mathcal {C}^\mathcal {A} does not generally inherit a Markov structure from \mathcal {C}. As we noted when we introduced diagram Markov categories, one has to consider the category \mathsf {Fun}(\mathcal {A},\mathcal {C}) of deterministic diagrams instead.

First, we will see that this indeed works for Markov prefibrations. This implies that (-)^\mathcal {A} lifts from fibrations to stochastic modules.

Proposition [efr-6G7N]

Let \mathcal {D} \to \mathcal {C} be a Markov prefibration. Recall that by \mathcal {C}^\to we denote the category of deterministic arrows in \mathcal {C}. Let \mathsf {Ar}(\mathcal {C}) denote the ordinary arrow category. Let now \mathcal {D}^\to denote the category \mathsf {Ar}(\mathcal {D}) \times _{\mathsf {Ar}(\mathcal {C})} \mathcal {C}^\to consisting of those arrows in \mathcal {D} which lie over a deterministic base (but again, where the morphisms consist of commutative squares whose other sides do not necessarily have deterministic bases). Then \mathcal {D}^\to \to \mathcal {C}^\to is a Markov prefibration.

This yields a functor \mathsf {MarkPreFib}(\mathcal {C}) \to \mathsf {MarkPreFib}(\mathcal {C}^\to ), so that (\mathcal {D}^\to )|_\mathrm {det} = (\mathcal {D}|_\mathrm {det})^\to . This equation induces a natural transformation \overline {(\mathcal {D}_0^\to )}|_\mathrm {det} \to (\overline {\mathcal {D}_0}|_\mathrm {det})^\to , which in turns gives a lift of (-)^\to to the category of stochastic module fibrations, where the induced algebra structure acts pointwise.

Proof

Noting that \mathcal {C}^\to is a Markov category with the "pointwise" structure, and the deterministic maps consist precisely of the pointwise deterministic maps, clearly \mathcal {D}^\to |_\mathrm {det} = \mathcal {D}|_\mathrm {det}^\to , and fibrations are stable under the formation of arrow categories, with Cartesian maps formed pointwise.

It is not trivial that this is a prefibration, because given a triangle in \mathcal {C}_\mathrm {det}^\to ---a "prism"---and a Cartesian lifting, we only know that the maps "at the ends" are Cartesian, not the maps between the triangles. Therefore we can not immediately apply the unique lifting property to say that the square between the induced lifts \bar {Y_i}_{X_i} \to \bar {Y_i}_{Z_i} commute, given some map \bar {Y}_0 \to \bar {Y}_1 over Y_0 \to Y_1. However, by taking the pullback on both sides (and noting that pullbacks are functorial,) we can factor this square into two which live entirely over a deterministic base, and where the Cartesian property therefore imply commutativity.

We have already argued that this commutes with restriction to the deterministic part. The natural transformation is induced for completely abstract reasons, by applying (-)^\to to the unit to obtain a map \mathcal {D}_0^\to \to (\overline {\mathcal {D}_0}|_\mathrm {det})^\to = (\overline {\mathcal {D}_0}^\to )|_\mathrm {det}, which by the universal property of \overline {(-)} induces the desired map \overline {(\mathcal {D}_0^\to )}|_\mathrm {det} \to (\overline {\mathcal {D}_0}|_\mathrm {det})^\to .

Corollary [efr-DXJR]

Let \mathcal {A} be a small category, and let \mathcal {D} \to \mathcal {C} be a Markov prefibration. Let \mathsf {Fun}(\mathcal {A},\mathcal {D}) := \mathcal {D}^\mathcal {A} \times _{\mathcal {C}^\mathcal {A}} \mathsf {Fun}(\mathcal {A},\mathcal {C}). Then the functor \mathsf {Fun}(\mathcal {A},\mathcal {D}) \to \mathsf {Fun}(\mathcal {A},\mathcal {C}) is a Markov prefibration.

Proof

Note that \mathsf {Fun}(\mathcal {A},\mathcal {D}) is a limit of the categories \mathcal {D}^\to and prefibrations are stable under these limits.

The question is now

  1. If \mathcal {D} is a Markov fibration, we get a stochastic module structure on \mathcal {D}|_\mathrm {det}^\mathcal {A}---does it present a markov fibration?
  2. There is an induced map \mathsf {SChart}(\mathsf {Fun}(\mathcal {A},\mathcal {D}|_\mathrm {det})) \to \mathsf {Fun}(\mathcal {A},\mathcal {D}) (where the latter is taken by convention to mean the full subcategory of functors whose image in \mathcal {C} consists of deterministic arrows). Is this an isomorphism? (If it is, clearly this implies point 1)

Unfortunately it's not clear that either of these are true---the surjectivity of \mathsf {SChart}(\mathcal {D}|_\mathrm {det}) \to \mathcal {D} cannot a priori be lifted to the arrow category. The issue is that, given a map in \mathcal {D}^\to consisting of, say \phi _0,\phi _1, it is not sufficient to find charts representing each of these---we must find a chart of squares representing the square. This is not guaranteed by the Markov fibration structure, and a similar issue comes into play for the equivalence witnesses.

We may attempt to ignore this issue and simply try to form a double category \mathsf {SLens}(\mathcal {D}^\to ) \rightrightarrows \mathsf {SLens}(\mathcal {D}), given a stochastic module \mathcal {D}, but here the problem is that \mathsf {SLens} does not commute with limits in general. Hence we can not easily define a composition on the 2-cells of lenses obtained this way.

There are various ways we might attempt to remedy this problem. One approach would be to formulate a behavioural notion of "commutativity" for squares of stochastic lenses and charts, but the problem with this is that it is not obvious whether this property is stable under composition.

The basic problem stems from the fact that chart equivalences have a "directed" nature, and given a morphism of precharts (M,\phi ) \to (N,\psi ) and an equivalence (N,\psi ) \leftarrow (N',\psi ') (for example given by a stochastic section N' \to N satisfying suitable conditions), there is not in general a way to lift this back into an equivalent (M',\phi ') with a map to N'.

This observation leads to the idea that we might define a double category of precharts which has the directed equivalences among its morphisms (going only in one direction). We will begin by constructing this double category.

Definition [efr-KO4T]

Let \mathcal {D} \to \mathcal {C} be a (Grothendieck) fibration, and let \mathcal {C} \to \mathcal {C}' be a faithful, identity-on-objects functor. Suppose \mathcal {C} admits pullbacks, and given a pair of morphisms P \to X,Y \in \mathcal {C}' over Z, where P \to X is in \mathcal {C}, there is a unique common factorization P \to X \times _Z Y.

  1. The double category \mathsf {\mathbb Span}_{\mathcal {C}'}(\mathcal {C}) has \mathcal {C} as the vertical category, spans X \leftarrow P \to Y in \mathcal {C} equipped with a section X \to P \in {\mathcal {C}'} as horizontal cells, and maps of spans which commute with the sections as 2-cells.
  2. The double category \mathsf {\mathbb Span}_{\mathcal {C}'}(\mathcal {D} / \mathcal {C}) lying over \mathsf {\mathbb Span}_{\mathcal {C}'}(\mathcal {C}) has \mathcal {D} as the vertical category, and spans \bar {X} \xleftarrow {f} \bar {P} \xrightarrow {g} \bar {Y} where f is Cartesian, decorated with a section X \to P in \mathcal {C}' as the horizontal cells, and maps of such spans (so that the underlying thing commutes with the sections) as the 2-cells. We will call the horizontal cells decorated spans.
  3. There is an apparent forgetful functor \mathsf {\mathbb Span}_{\mathcal {C}'}(\mathcal {D} / \mathcal {C}) \to \mathsf {\mathbb Span}_{\mathcal {C}'}(\mathcal {C})

To spell it out, a 2-cell in \mathsf {\mathbb Span}_{\mathcal {C}'}(\mathcal {D} / \mathcal {C}) consists of a diagram of this form in \mathcal {D}, where f_1,f_2 are Cartesian, and (writing X_1 for the object underlying \overline {X_1}, and so on) two sections s_1,s_2 of the underlying maps in \mathcal {C}', so that the second diagram also commutes in \mathcal {C}':

Naturally, we are interested in the case of \mathsf {\mathbb Span}_{\mathcal {C}}(\mathcal {D} / \mathcal {C}_\mathrm {det}) for a stochastic module \mathcal {D}. Then the decorated spans are representatives for stochastic charts. We will start by introducing a loosed notion of 2-cell for these spans, which combines the directed equivalences with the ordinary deterministic 2-cells of spans.

Definition [efr-RD28]

Let \mathcal {C} be a Markov category and let \mathcal {D} be a stochastic module over \mathcal {C}. Let (M_1, \phi _1): \bar {X_1} \leftrightarrows \bar {Y_1}, (M_2, \phi _2): \bar {X_2} \leftrightarrows \bar {Y_2} be decorated spans in \mathsf {\mathbb Span}_{\mathcal {C}}(\mathcal {D} / \mathcal {C}_\mathrm {det}), and let f: \bar {X_1} \rightrightarrows \bar {X_2}, g: \bar {Y_1} \to \bar {Y_2} be morphisms in \mathcal {D}, so that we have a square

A 2-cell of decorated spans for this data consists of a morphism m: M_1 \to M_2 \in \mathcal {C} (that is, possibly stochastic), satisfying the following two conditions. First, the diagram

in the base must commute. Given this, there is an induced square
in \mathcal {D}_{M_1}, where the bottom map is given by pulling back \phi _2 along m, in the sense of Lemma [efr-VF6V]. The second condition is that this square must also commute.

Lemma [efr-DRU6]

2-cells of decorated spans compose---that is, given a diagram

where the horizontal maps are decorated spans, and the vertical maps are maps in \mathcal {D} with deterministic base, and given maps of decorated spans \phi _1 \xrightarrow {\alpha } \phi _2 \xrightarrow {\beta } \phi _3, there is a map of decorated spans \phi _1 \to \phi _3

Proof

We can easily compose the two maps to get M_1 \to M_3. Now, the question is whether the perimeter of this diagram commutes:

Note that the top square is commutative by assumption, since pullbacks compose (even along stochastic maps) and this is the assumption that \alpha is a cell. The bottom square is the result of pulling back a commutative square over M_2 again along \alpha . Note that pullback along stochastic morphisms is not in general functorial---but since the vertical parts of this square are themselves pulled back from X_2,Y_2, this composition is preserved by pullback along \alpha : M_1 \to M_2. This finishes the proof.

Proposition [efr-L7X0]

2-cells of decorated spans compose horizontally: Given a square

where the horizontal maps are precharts and the vertical maps are morphisms in \mathcal {D}|_\mathrm {det}, and given \alpha : \phi _1 \to \phi _2 and \beta : \psi _1 \to \psi _2, there is a prechart morphism \psi _1\phi _1 \to \psi _2\phi _2.

Proof

Unlike the proof of Lemma [efr-DRU6], this is straightforward: If the carrier of \phi _i is M_i, and of \psi _i, N_i (for i=1,2), then by definition the composites are carried by the pullback M_i \times _{Y_i} N_i. There is a canonical map M_1 \times _{Y_1} N_1 \to M_2 \times _{Y_2} N_2 over M_2, N_2, given by the independent pairing of \alpha and \beta .

Since pullbacks compose, the square over M_1 \times _{Y_1} N_1 that must commute is given by the two commutative squares induced by \alpha ,\beta , pulled back and composed with each other. Here we are pulling back along the deterministic projections from the pullback, and hence these commutative squares are preserved, and hence the composite square commutes as well.

Corollary [efr-MUNG]

Let \mathcal {D} be a stochastic module over \mathcal {C}. There is a double category \widetilde {\mathsf {\mathbb Span}}(\mathcal {D})^\mathrm {chart} which has decorated spans as its horizontal maps, morphisms in \mathcal {D}|_\mathrm {det} as its vertical maps, and decorated span 2-cells as its 2-cells.

Moreover, there is another double category \widetilde {\mathsf {\mathbb Span}}(\mathcal {D})^\mathrm {lens} which has decorated spans in \mathcal {D}^\mathrm {fop} as its horizontal maps instead.

(The modification of everything above to lenses instead of charts is obvious).

In fact, the globular 2-cells are in a sense exactly the equations defining the set of charts:

Lemma [efr-CU3J]

Let \phi , \psi : \bar {A} \to \bar {B} be parallel decorated spans in \widetilde {\mathsf {\mathbb Span}}(\mathcal {D})^\mathrm {chart} (or \widetilde {\mathsf {\mathbb Span}}(\mathcal {D})^\mathrm {lens} ).

They represent the same stochastic chart (lens) if and only if there exists a zig-zag of globular 2-cells between them.

Proof

Unwinding the definitions, a 2-cell M_\phi \to M_\psi is precisely a map exhibiting the equality of the two decorated spans, as in Lemma [efr-26SF]

The following straightforward lemma shows that charts over deterministic bases have initial representatives as spans. This will be important later:

Proposition [efr-10CM]

Suppose given a square

in \widetilde {\mathsf {\mathbb Span}}(\mathcal {D})^\mathrm {lens} (or \widetilde {\mathsf {\mathbb Span}}(\mathcal {D})^\mathrm {chart}) Suppose further the underlying square in \mathcal {C} is deterministic. Then:

  1. If there exists a filling decorated span 2-cell, the image in \mathsf {\mathbb Arena}(\mathcal {D}|_\mathrm {det}) commutes.
  2. If M_1 is the carrier of \phi _1 and the left leg M_1 \to X_1 is an isomorphism, then this implication is an equivalence.

Proof

Given a stochastic chart carried by X \leftarrow M \to Y, so that X \to Y is deterministic, recall that we can first pull back to the equalizer M' \hookrightarrow M of the two maps M \to X \to Y, M \to Y, then along the prescribed section X \to M'. Note that this gives a 2-cell from this canonical representative with carrier X to the initial representative.

Given two such cells, we get a square

But as part of the square surrounding the 2-cell, there is given a map X_1 \to X_2, which must make this square commute. The functoriality of base change (pulling back the map \phi _2) proves this bottom map is again a 2-cell.

But the property for this map to be a 2-cell is exactly the property for this square to be a commutative square in \mathsf {\mathbb Arena}{\mathcal {D}|_\mathrm {det}}. This proves both parts of the statement.

Double Categories of Stochastic Dynamical System [efr-7DV5]

Definition Stochastic Dynamical Systems Theories [efr-HS7G]

A stochastic dynamical systems theory consists of a stochastic module \mathcal {D} over \mathcal {C} equipped with a section T: \mathcal {C}_\mathrm {det} \to \mathcal {D}|_\mathrm {det} of the underlying fibration.

We adopt the notation \widetilde {\mathsf {\mathbb Arena}}(\mathcal {D}) for the double category which was denoted \widetilde {\mathsf {\mathbb Span}}(\mathcal {D})^\mathrm {lens} above. We use the symbol \leftrightarrows for the horizontal (span) morphisms and \rightrightarrows for the vertical morphisms (in \mathcal {D}).

Given a stochastic dynamical systems theory (\mathcal {D}, T), the double category of dynamical systems \mathsf {Sys}(\mathcal {D},T) has

  1. Objects triples S \in \mathcal {C}, \bar {A} \in \mathcal {D}, \xi : TS \leftrightarrows \bar {A} \in \widetilde {\mathsf {\mathbb Arena}}
  2. Horizontal morphisms given by a pair f: S \to S', g: \bar {A} \rightrightarrows \bar {B} \in \mathcal {D}, c where c is a square filling \xi , \xi ', Tf, g
  3. Vertical morphisms given by a pair f: S \to S', g: \bar {A} \leftrightarrows \bar {B} \in \overline {\mathcal {D}}, c where c is a square filling Tf, g \xi , \xi ', 1_{\bar {B}}

Proposition [efr-N5V5]

Let T,\mathcal {D} be a stochastic dynamical systems theory. Then T,\mathcal {D}|_\mathrm {det} is an ordinary dynamical systems theory. There is a double functor \mathsf {Sys}(T,\mathcal {D}|_\mathrm {det}) \to \mathsf {Sys}(T,\mathcal {C}). This functor is full on vertical morphisms, and on 2-cells.

Let \mathsf {Sys}(T,\mathcal {D})_\mathrm {det} denote the subcategory spanned by systems with deterministic readout, prelenses with deterministic base, and all the morphisms of \mathcal {D}. Then the restricted functor \mathsf {Sys}(T,\mathcal {D}|_\mathrm {det}) \to \mathsf {Sys}(T,\mathcal {D})_\mathrm {det} admits a chartwise right adjoint, which assigns to each system or prelens its equivalence class.

Proof

The functor simply acts as the functor in Proposition [efr-JQI9]. Since that inclusion is full on 2-cells, this one is full on vertical morphisms, and since a 2-cell in \mathsf {Sys} is merely a 2-cell in \mathsf {\mathbb Arena} between specific objects, it is also full on 2-cells.

The right adjoint property likewise follows from the analogous property of the inclusion functor on arenas.

Proposition [efr-JQI9]

Let \mathcal {D} be a Markov prefibration. Then there is a double functor \mathsf {\mathbb Arena}(\mathcal {D}|_\mathrm {det}) \to \widetilde {\mathsf {\mathbb Arena}}(\mathcal {D}), which acts as identity on the morphisms of \mathcal {D}, and carries each lens (f: X \to Y, \phi : f^*\bar {Y} \to \bar {X}) to the prelens (X \leftarrow X \to Y, \phi ). This double functor is full on 2-cells.

The restriction to \mathsf {\mathbb Arena}(\mathcal {D}|_\mathrm {det}) \to \mathsf {\mathbb Arena}(\mathcal {D})_\mathrm {det} admits a right adjoint, which carries every prelens to its equivalence class.

Proof

First we must verify functoriality with respect to lens composition. To that end, let X \xrightarrow {f} Y \xrightarrow {g} Z be deterministic morphisms and \phi ,\psi be lenses over them. Their composite as prelenses has carrier X \times _Y Y = X and f^*(\psi )\phi as the morphism in the fiber, which is exactly the prelens associated to their composite as lenses.

Second, we must verify fullness on 2-cells. But this is a special case of Proposition [efr-10CM].

Finally, Proposition [efr-10CM] is precisely the statement that assigning a prelens to its equivalence class lens is right adjoint to this (and in particular that it forms a functor)

Recall that in Myers' categorical dynamical systems theory, trajectories of a system \xi : TS \leftrightarrows \bar {A} are identified with chart morphisms from a "clock" system---thus for example trajectories of a smooth dynamical system M \to TM are exactly those maps \gamma : \mathbb {R} \to M which, when \mathbb {R} is equipped with the vectorfield dx/dt = 1, are homomorphisms.

In general this presents an issue for our replacement category \mathsf {Sys}(T,\mathcal {D})---since we wish to regard two systems given by equivalent lenses as equivalent, but their set of homomorphisms from a given clock system is not necessarily in bijection. In the general case, we do not presently have a way around this problem---but at least for clock systems with deterministic readout, the above presents a solution: choosing the initial representative for such a system, we find that the set of trajectories does not depend on the equivalence class of the target system.

The triple category of dynamical systems [efr-MWCE]

Having done the prep-work in § [efr-000D] (and § [efr-0023]), we can jump directly into the construction:

Definition \mathsf {BiSys} [efr-EPI9]

Let \mathcal {A} \to \mathcal {C}, T: \mathcal {C} \to \mathcal {A} be a symmetric monoidal dynamical systems theory. Then this diagram:

depicts two strict double categories, each with a symmetric monoidal structure, and a strict double functor between them which is (non-strictly) a symmetric monoidal functor. This induces an object of \mathsf {SymMon}(\mathsf {Act}(\mathsf {DblCat})). Applying \mathsf {\mathbb Para}(-) under \mathsf {SymMon}(-), we obtain a symmetric pseudomonoid in internal pseudocategories in \mathsf {DblCat}. Denote by \mathsf {BiSys}(\mathcal {C},\mathcal {A},T) this induced object.

Remark The Structure of \mathsf {BiSys} [efr-WX1V]

\mathsf {BiSys}(\mathcal {C},\mathcal {A},T) has the following structure: The objects are simply the objects of \mathcal {A}---the bundles.

There are three types of 1-cell: Lenses, that is morphism in \mathcal {A}^\mathrm {fop}, which we write A \leftrightarrows B, charts, that is morphisms in \mathcal {A}, which we write A \rightrightarrows B, and bisystems, which are pairs (S \in \mathcal {C}, TS \otimes A \leftrightarrows B), and which we write A \nrightarrow B.

Moreover there are three types of 2-cell:

  1. Lens-chart cells, which are the 2-cells of \mathsf {\mathbb Arena}(\mathcal {A}). Note that this double category is thin. We will say a square of lenses and charts commutes if it is filled by such a 2-cell.
  2. Chart-bisystem cells---given charts A_1 \rightrightarrows B_1, A_2 \rightrightarrows B_2 and systems TS \otimes A_1 \leftrightarrows A_2, TS' \otimes A_2 \leftrightarrows B_2, a square filling this is a choice of map S \to S' \in \mathcal {C} so that the resulting lens-chart square
    commutes.
  3. Lens-bisystem cells. Given lenses A_1 \leftrightarrows B_1, A_2 \leftrightarrows B_2, and systems TS' \otimes A_1 \leftrightarrows A_2, TS' \otimes B_1 \leftrightarrows B_2, a 2-cell consists of an isomorphism S' \xrightarrow {\sim } S' so that the resulting square of lenses commutes (recall that isomorphism charts are the same as isomorphism lenses).

The charts, bisystems and chart-bisystem cells form a pseudo double category with the obvious composition. So do the lenses, bisystems and lens-bisystem cells. Finally, there is a notion of 3-cell given by a box whose sides are 2-cells of each kind, so that the resulting diagram in \mathcal {C} (with isomorphisms on two sides) commutes.

The lens-bisystem double category is \mathsf {\mathbb Para}_{\mathcal {C}^\simeq }(\mathsf {\mathbb Arena}{\mathcal {A}}_0) (recall that \mathsf {\mathbb Arena}{\mathcal {A}}_0 = \mathcal {A}^\mathrm {fop}), with the action given by the functor T (restricted to isomorphisms). The chart-bisystem double category is the result of taking \mathsf {BiSys}(\mathcal {C},\mathcal {A},T), a pseudocategory in double categories, and applying \mathsf {PsCat}((-)_h) : \mathsf {PsCat}(\mathsf {DblCat}) \to \mathsf {PsCat}(\mathsf {Cat}) where (-)_h takes the horizontal category of a (strict) double category.

The 3-cells, of course, are the 2-cells of \mathsf {\mathbb Para}_{(\mathcal {C}^\to )^\simeq }(\mathsf {\mathbb Arena}(\mathcal {A})_1). Analogously to the above, for each class of 1-cells, there is a double category with those as the objects, the two types of cell as the two morphisms, and the 3-cells as the 2-cells.

All of these six double categories admit a symmetric monoidal structure.

We can recover the ordinary category of (Moore) systems as the slice over I, in the following sense:

Proposition [efr-2M0M]

There is a pullback diagram

in \mathsf {DblCat}

In a double category \mathbb {C}, there is a "horizontal slice" 1-category having objects the horizontal maps A \to B and morphisms given by 2-cells that are identity on the left boundary, composed vertically. Similarly there is a "vertical slice". This is given by a similar pullback in \mathsf {Cat}---we simply do this one level up.

Note that Myers' construction of the double fibration \mathsf {Sys}(\mathcal {C},\mathcal {A},T) \to \mathsf {\mathbb Arena}{\mathsf {Cat}} in fact uses the vertical slice in this sense.

This somewhat trivial observation means that any composition in \mathsf {BiSys}(\mathcal {C},\mathcal {A},T) which produces 2-cell under I in fact produces a morphism of systems in the ordinary sense. Replacing I with another object, we may regard the slices as further-parametrized versions of \mathsf {Sys}(\mathcal {C},\mathcal {A},T).

There is essentially no difficulty in applying this to the Markov case:

Definition \mathsf {BiSys}^M [efr-W413]

Let (\mathcal {C}, \mathcal {A}, T) be a stochastic dynamical systems theory. Consider the double category whose vertical category is \mathcal {C}_\mathrm {det} and horizontal category is \mathcal {C}, with commutative squares as the 2-cells (this is the transpose of \mathcal {C}^\to \rightrightarrows \mathcal {C}). This carries an obvious symmetric monoidal structure, and acts on the double category of stochastic arenas \widetilde {\mathsf {\mathbb Arena}}(\mathcal {A}) via the functor T. Denote by \mathsf {BiSys}^M(\mathcal {C},\mathcal {A},T) the symmetric monoidal triple category induced as in Definition [efr-EPI9] by this data.

The information contained in \mathsf {BiSys}^M(\mathcal {C},\mathcal {A},T) is much as above, although the complications involved in the double category of stochastic arenas remain present.

Our bisystems are reminiscent of the energy-driven systems of Capucci, Lynch, and Spivak (Reference [energy-driven-systems]). Indeed, their \mathbb {C} \mathsf {org} is essentially the bisystems in the (ordinary) doctrine of smooth dynamical systems. As we mentioned in the introduction, Shapiro and Spivak (Reference [shapiro-spivak-dynamic-operads]) have previous developed a structure \mathbb {O} \mathsf {rg} which consists of the bisystems for the discrete dynamical systems doctrine (i.e \mathsf {Set}^\to \to \mathsf {Set}). \mathbb {O} \mathsf {rg} has a tremendous amount of structure coming from the representation of lenses in this doctrine as the category of polynomial functors, which can't be replicated for a general systems theory (and certainly not for a general stochastic systems theory).

A Stochastic Dynamical Systems Theory of Smooth Manifolds [efr-9J8G]

In this section, as the title suggests, we construct a stochastic dynamical systems theory of smooth manifolds, with the usual tangent bundle. The main point is to construct a Markov category containing the smooth manifolds which is pullback-positive. We do this by considering the larger category of diffeological spaces. In order to make the topology work, we need to complicate the notion of diffeological space a bit, but having done so, we obtain a representable Markov category which is pullback-positive, and contains \mathsf {SmMfd} as a full subcategory of the deterministic maps. A kernel p: M \to N is a Markov kernel valued in Radon measures which is weakly continuous---so induces a linear map C(N) \to C(M) taking \phi to the function x \mapsto E_{p_x}\phi on the spaces of continuous functions---and which furthermore smooth in the sense that this operation preserves the smooth functions.

This Markov category of "smooth stochastic maps" may be of some independent interest.

Definition \mathsf {CartSp} [efr-CBBU]

Let \mathsf {CartSp} denote the full subcategory of \mathsf {SmMfd} spanned by the objects \mathbb {R}^n for each n. Note that \mathsf {CartSp} has finite products, and is generated by the object \mathbb {R} under finite products.

Definition Diffeological Space [efr-E1SZ]

A smooth space is a sheaf on \mathsf {SmMfd} in the standard topology of open covers. A smooth space X is a diffeological space if, for each M \in \mathsf {SmMfd}, the map X(M) \to \prod _{p \in M} X(\{p\}) is injective.

A diffeological space with underlying set X is called a diffeology on X, and consists of specifying which maps \mathbb {R}^n \to X are smooth. We call these maps smooth plots.

Given a subset X' \subset X, there is an obvious canonical diffeology on X' given by taking the plots to be those functions whose image in X is smooth. We call this the subspace diffeology.

A morphism of diffeological spaces is called a smooth map. It is equivalently a function X \to Y which carries smooth plots to smooth plots.

Definition Diffeo-Topological space [efr-DX6S]

A diffeo-topological space is a diffeological space X equipped with a topology \tau so that all the smooth plots are continuous. A map of diffeo-topological spaces is a smooth map (for the diffeology) which is also continuous (for the topology).

Given a subset X' \subset X, there is an obvious canonical diffeo-topology on X' given by taking the plots to be those functions whose image in X is smooth, and equipping X' with the subspace topology.

Lemma [efr-42SC]

The category of diffeo-topological spaces admits all limits, given by taking the limits in topological spaces and diffeological spaces (which have the same underlying set).

Proposition [efr-7RS2]

Let X be a diffeo-topological space whose underlying space is Tychonoff. Then the space of probability measures P(X) has a canonical diffeology given by those plots f: U \to P(X) so that for each continuous function g on X, the resulting map u \mapsto E_{f(u)g} is continuous, and if g is smooth, then this is smooth as well. With this diffeology, and the topology of weak convergence, P(X) is a diffeo-topological space. This defines a commutative affine monad on \mathsf {TychDiff}, the category of such diffeo-topological spaces.

Proof

The topology of weak convergence on P(X) is such that A \to P(X) is continuous if and only if the expectation map carries continuous functions to continuous functions. But this is part of the requirement to be a smooth plot, so certainly this is a diffeo-topological space.

Since the linear operator associated to x \in X under the unit X \to P(X) is merely evaluation at x, the unit is clearly smooth. Consider \mu : PPX \to PX. To test this is smooth, let f: U \to PP(X) be a plot. We must show \mu f is a plot. So let v: X \to \mathbb {R} be a continuous (resp. smooth) function. We must show its expectation a is continuous (resp. smooth) function of u \in U.

By construction E(v) : PX \to \mathbb {R} is continuous (resp. smooth), and so since f is a plot, the map u \mapsto E_{f(u)}E(v) is continuous (resp. smooth). But this is exactly what we wanted.

The monad laws follow from their holding in \mathsf {Tych}. Since a commutative monad is equivalently a strong monad satisfying a certain equation (which holds for this monad in \mathsf {Tych} and therefore also here), it suffices to show that the strength P(X) \times Y \to P(X \times Y) is smooth. This follows by a completely analogous argument.

Corollary [efr-S87B]

The category \mathsf {TychDiffStoch} of Tychonoff diffeological spaces and Kleisli maps for the monad P described in Proposition [efr-7RS2] is a pullback-positive Markov category. Its deterministic category is \mathsf {TychDiff}. There is a fully faithful functor \mathsf {SmMfd} \to \mathsf {TychDiff} which preserves transverse pullbacks. The maps between smooth manifolds are given by weakly continuous families of Radon probability measures, so that the expectation operator carries smooth maps to smooth maps.

Remark [efr-LPX2]

Since we describe properties of kernels in terms of their corresponding linear operator on function spaces, it would seem natural to take the function spaces as the basic object. Hence we might consider the category C^\infty -algebras with some relaxed notion of maps between them. The tricky part there is to find some reasonable class of maps so that the tensor product (coproduct) of C^\infty -algebras extends to these. (Since it is not the same as the tensor product of \mathbb {R}-algebras, linear maps do not automatically extend to the tensor product). In particular, when considering kernels *_1 \to X where *_1 is a "fat point of order 1"---that is, functions on 1_* have a value at the point and a derivative---it is not clear what sort of continuity condition the derivative operation on C^\infty (X) should satisfy, nor how to define this in a general way for all C^\infty -algebras. It would certainly be of interest to synthetic computational geometry to have such a Markov category, but we leave this for future work.

We will now give an example of how to represent the training dynamics of a machine learning system using the tools developed so far. As discussed previously, given a parameterized function F: P \times X \to Y, its reverse derivative naturally becomes a parameterized lens, and the composition of these describe how gradient vectors are passed around to compute an update during training. It is natural to want to compose this lens with the data-generating distribution I \to X \otimes Y, (along with some more context describing the loss function, etc) to obtain the training dynamics of such a model. This requires a category of parameterized lenses which allows stochastic maps in the base. The goal of combining this feature with non-trivial tangent bundles was one of the original motivations for developing a theory of stochastic lenses.

Example [efr-IMZ3]

Consider the Markov prefibration \mathsf {TychDiffStoch}^\to \to \mathsf {TychDiffStoch}. Equip this with the section T(X) = X \otimes X \xrightarrow {\pi _0} X - this described discrete-time systems (whose update is required to be smooth in the input and present state). This is clearly a symmetric monoidal functor and thus defines a systems theory. Note that this is completely different from the ordinary tangent bundle, despite the coincidence of notation.

Let m_1: TS_2 \otimes X_1 \leftrightarrows Y_1 and m_2: TS_2 \otimes X_2 \leftrightarrows Y_2 be two bisystems in this theory. As in § [efr-SREZ], we may define a parameterized lens (TS_1 \& TS_2) \otimes (X_1 \oplus X_2) \leftrightarrows (Y_1 \oplus X_2), denoting by \oplus the coproduct in lenses, and by \& the Markov structure defined in Corollary [efr-FT8J]. Observe that TS_1 \& TS_2 is simply the indexed set (S_1 \coprod S_2) \otimes S_1 \otimes S_2 \to S_1\otimes S_2. There is an obvious indexed map from this to T(S_1 \otimes S_2) = S_1 \otimes S_2 \otimes S_1 \otimes S_2, given by (\operatorname {inl} s_1', s_1,s_2) \mapsto (s_1', s_2, s_1, s_2) and (\operatorname {inr} s_2', s_1, s_2) \mapsto (s_1,s_2',s_1,s_2). In words, we receive an update either to the S-state or to the S'-state. We apply this update to the relevant state and leave the other alone. This defines a lens T(S_1 \otimes S_2) \leftrightarrows T(S_1) \& T(S_2), which we may compose with the above to obtain a bisystem T(S_1 \otimes S_2) \otimes (X_1 \oplus X_2) \leftrightarrows Y_1 \oplus Y_2. Let us denote this by m_1 \oplus m_2.

This has very much the same flavor as the external choice for open games, although we will not develop the theory of this operation in detail here.

Now, given a smooth (deterministic) map F: P \times X \to Y, where P,X,Y are smooth manifolds (not merely diffeo-toplogical spaces), we obtain a lens T^*(F): {T^*P \choose P} \otimes {T^*X \choose X} \leftrightarrows {T^*Y \choose Y}, where T^*(-) denotes the cotangent bundle. (This does not, prima facie, make sense for a general diffeo-topological space).

Let us take as given some family of lenses T(S) = {S \otimes S \choose S} \leftrightarrows {T^*S \choose S} for various S. Such an operation amounts to choosing a way of updating s \in S given a cotangent vector---hence we can see it as an optimization algorithm. One example of such would be gradient descent, which given a choice of Riemann structure on S, takes a step of a given length in the direction which most quickly decreases the given covector.

(It should be noted that there are more complicated optimization strategies which don't fit this particular pattern - for example, momentum algorithms have to maintain some extra internal state other than s \in S. But let's stick with this pattern for this example). Note also that we're not assuming the optimizers are a natural transformation or anything like that.

Now we are ready to build the neural network architecture known as a generative adversarial network, or GAN (Reference [gan-paper]). Let us first describe the idea. Our goal is to generate additional samples from some distribution, given a set of existing samples---for example, our goal may be to generate more pictures in the same style as an existing corpus. Suppose our data is of type X, and let d: I \to X be the data distribution. We fix some latent distribution \lambda : I \to L, where L is any space of our choice---usually, L is \mathbb {R}^n and \lambda is a Gaussian. Finally we choose two neural networks, the generator G: P_G \otimes L \to X, and the discriminator D: P_D \otimes X \to \mathbb {R}. The goal of the discriminator is to discriminate real samples from the data from generated samples, by providing a low value on the generated samples and a high value on the true samples.

The training process now goes as follows: for each step of training, we either sample from the latent distribution, and have the generator use this to generate a sample, or draw a sample from the data distribution (choosing between these with some probability p). Then in either case, we have the discriminator score the generated sample. If the sample was generated by the generator, the discriminator's loss is equal to its output, otherwise it is equal to -1 times its output. We update the discriminator according to the gradient of this loss (minimizing it), and update the generator (if we are in the branch where it was run) according to the negative of the gradient of this loss with respect to the generator parameters---this amounts to doing a gradient descent update on the generator for the negative of the discriminator loss.

We can represent this schematically using the following tape diagram (see Reference [tape-diags-monoidal-monads]):

The two "tapes" branching off at the start represent two maps (bisystems) composed by \oplus , while the backwards wires indicate the flow of the gradients. The ground symbol indicates a value being discarded. Note that the theory of tape diagrams has only been developed formally for distributive categories, and for essentilly the same reason as in § [efr-SREZ], we do not have distributivity in this case. However, the interpretation of this diagram is still unambiguous---distributivity is required to make tape diagrams complete, not to make them sound. Concretely, if we tried to represent the tensoring of this system with another system, we would have no way of doing it, but if the category was distributive we could do so by adding this additional system to each of the branches. Still, the figure is best viewed as a visual aid rather than a formal representation.