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.

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 Pseudo-categories [pseudocategories]

Abstract

  • April 26, 2006
  • Nelson Martins Ferreira

We provide a complete description of the category of pseudo-categories (including pseudo-functors, natural and pseudo-natural transformations and pseudo modifications). A pseudo-category is a non strict version of an internal category. It was called a weak category and weak double category in some earlier papers. When internal to Cat it is at the same time a generalization of a bicategory and a double category. 

 @article
{pseudocategories, title={Pseudo-categories}, url={http://arxiv.org/abs/math/0604549}, DOI={10.48550/arXiv.math/0604549}, abstractNote={We provide a complete description of the category of pseudo-categories (including pseudo-functors, natural and pseudo-natural transformations and pseudo modifications). A pseudo-category is a non strict version of an internal category. It was called a weak category and weak double category in some earlier papers. When internal to Cat it is at the same time a generalization of a bicategory and a double category.}, number={arXiv:math/0604549}, publisher={arXiv}, author={Ferreira, Nelson Martins}, year={2006}, month={Apr} }

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

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: