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.

Context

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.

Related

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}.