Proposition [efr-0037]

Let \Delta ^{\leq 3} \subseteq \Delta be the subcategory consisting of the objects [0],[1],[2],[3]. Suppose \mathcal {C} admits pullbacks. Then an internal category in \mathcal {C} is equivalently a functor c: \Delta ^{\leq 3, \mathrm {op}} \to \mathcal {C} so that the following diagrams are pullbacks:

Proof

It is easy to see that giving the restriction of this functor to [0],[1] precisely amount to choosing objects C_0,C_1 and morphisms c,d,i between them obeying the relevant equations. Given this, C[2] must be chosen as the relevant pullback, and the only datum not automatically specified is the choice of d_1: C[2] \to C[1], which is precisely the composition operation. Defining C_3 as the pullback it has to be and unwinding the equations, we see that the only thing not automatic is the equation between two different orders of composition (applying internal face maps) that this implies, which is associativity.

Context

Triple categories [efr-0035]

Every category theorist is familiar with the horrible complications associated with higher-dimensional category theory. Even the coherence conditions for essentially two-dimensional objects like monoidal categories or double categories can be annoying to check, and this only becomes more tricky as we pass to higher dimensions. Since the category of controlled processes is a \mathsf {\mathbb Para}-type construction, and should therefore be expected to only be pseudoassociative in at least one of its dimensions, we can't get around confronting this complexity, at least to some extent.

Since verifying the axioms of a pseudo triple category seems hopeless, we must look for a more conceptual approach. Initially, the following idea seems promising

  1. Observe that categories are models (in sets) of a certain finite limit theory. Internal categories in some other category (for example, the category of categories) are just models in that category.
  2. Intuitively, we expect pseudo double categories to then be weak models in the category of categories, i.e. functors from the syntactic category which carries the limits to homotopy limits
  3. Observe that the \mathsf {\mathbb Para} construction preserves homotopy limits. Therefore it will carry a weak internal category in actegories to a weak internal category in pseudo double categories. This will then be a pseudo triple category in a suitable sense.

However, already at step two we encounter serious complications---it is not the case that every pseudo double category, even up to equivalence, can be modeled as a weakly internal category, and in general the relationship between these two classes of objects is somewhat complicated. However, it will turn out that our particular double and triple categories are of a sufficiently nice type (they are isofibrant) that this confusion goes away.

Internal category [efr-0036]

Let \mathcal {C} be a category. An internal category in \mathcal {C} consists of the following data:

  1. Objects C_0, C_1 \in \mathcal {C}
  2. Morphisms c,d: C_1 \to C_0 and i: C_0 \to C_1, and \circ : C_1 \times _0 C_1 \to C_1, where this is the pullback of c and d (which is in particular assumed to exist)
  3. Such that

    write out the equations here

An internal functor consists of two maps C_0 \to D_0, C_1 \to D_1, such that the squares for each operation commutes (where the square involving \circ has one side formed by the map induced on the pullback)

We can package this data a bit more neatly by observing that, instead of asking for a map defined out of "the" pullback, we should instead ask for a choice of pullback diagram and a map out of the given pullback object. Doing so, we realize that most of the data of a category really consists of a diagram of a certain shape (i.e a functor from a certain index category), such that a certain subdiagram is a pullback. The only thing which is not obvious is how to encode the associativity axiom, but this is easily done by adding another object:

Definition Simplicial Category [efr-0016]

The simplicial category is the category of finite, nonempty, totally ordered sets, and order-preserving functions, denoted \mathbb {\Delta }. We denote by [n] for n \geq 0 the ordered set \{0 < 1 < \dots < n\} of n+1 elements---every object on \mathbb {\Delta } is isomorphic to one of the form [n].

A simplicial object in a category \mathcal {C} is a functor \Delta ^\mathrm {op} \to \mathcal {C}.

Proposition [efr-0037]

Let \Delta ^{\leq 3} \subseteq \Delta be the subcategory consisting of the objects [0],[1],[2],[3]. Suppose \mathcal {C} admits pullbacks. Then an internal category in \mathcal {C} is equivalently a functor c: \Delta ^{\leq 3, \mathrm {op}} \to \mathcal {C} so that the following diagrams are pullbacks:

Proof

It is easy to see that giving the restriction of this functor to [0],[1] precisely amount to choosing objects C_0,C_1 and morphisms c,d,i between them obeying the relevant equations. Given this, C[2] must be chosen as the relevant pullback, and the only datum not automatically specified is the choice of d_1: C[2] \to C[1], which is precisely the composition operation. Defining C_3 as the pullback it has to be and unwinding the equations, we see that the only thing not automatic is the equation between two different orders of composition (applying internal face maps) that this implies, which is associativity.

It transpires that, given such a diagram, it automatically extends to the higher simplices in a canonical way. Moreover, taking in these higher simplices matters for higher categorical structures. Thus we introduce the following definition:

Definition Segal object [efr-001N]

Consider the simplicial category \Delta . For every n,m, the following square commutes:

A simplicial object X in a category \mathcal {C} is called a Segal object if each of these squares goes to a pullback square.

Example [efr-0038]

For any category \mathcal {C}, a Segal object where C[0] is terminal is equivalently a monoid object in \mathcal {C} (with the Cartesian monoidal structure). In particular, a (strict) Segal object in \mathsf {Cat} is a strict monoidal category. On the other hand, a weak Segal object is equivalently a (not necessarily strict) monoidal category.

All this would naturally lead you to believe that a pseudo double category is equivalently a weak Segal object in \mathsf {Cat}. This, however, is not true. One way to see this is that the composition operation is (up to equivalence) defined on the homotopy pullback C_1 \times _{C_0} C_1. An object of this category consists of two horizontal morphisms (i.e objects of C_1) and an isomorphism in C_0 between their respective codomain and domain. This seems logical---if two objects in C_0, say x,x' are supposed to be the same if they are isomorphic, how can we not let you compose a morphism ending in one with one starting in the other? But nevertheless such a composition operation is not implied by the structure of an ordinary double category.

Example [efr-0039]

Let C: \Delta ^\mathrm {op} \to \mathsf {Cat} be a weak Segal category. Given two compatible horizontal morphisms---that is, two objects f,g \in C[1], so that d_0(f) = d_1(g), this (coupled with the identity morphism on this object of C[0]) describes an object in the weak pullback C[1] \times _{C[0]}^\sim C[1]. This object is in the essential image of C[2] \to C[1] \times _{C[0]}^\sim C[1], (since it is an equivalence, hence essentially surjective,) but not necessarily the image. This means we can't necessarily find a composite f;g with the same domain as f, for example---the best we can do is ask for the domain to be vertically isomorphic to d(f).

It turns out that the simplifying assumption needed to make sense of these problems is one we're happy to make in the situation at hand. Namely, we would like to assume that the functor C_1 \to C_0 \times C_0 picking out the domain and codomain is an isofibration. Recall that a functor p: \mathcal {C} \to \mathcal {D} is an isofibration if, given x in the domain and f: p(x) \to y an isomorphism in the codomain, there is a lift of f to \tilde {f}: x \to \tilde {y}. (Any Grothendieck fibration or opfibration is automatically an isofibration).

These lifts give us the composition-with-f operations we need, but they also simplify the notion of weak Segal object significantly. This is because of the fact that a (strict) pullback of isofibrations is automatically also a homotopy pullback. This means we can simplify the Segal condition to asking that the induced maps C[2] \to C[1]\times _{C[0]} C[1] (where this denotes the strict pullback) are equivalences of categories (recall that C[2] would be a strict pullback if this was an isomorphism of categories), and the analogous statement holds for the higher C[n].

Example [efr-0039]

Let C: \Delta ^\mathrm {op} \to \mathsf {Cat} be a weak Segal category. Given two compatible horizontal morphisms---that is, two objects f,g \in C[1], so that d_0(f) = d_1(g), this (coupled with the identity morphism on this object of C[0]) describes an object in the weak pullback C[1] \times _{C[0]}^\sim C[1]. This object is in the essential image of C[2] \to C[1] \times _{C[0]}^\sim C[1], (since it is an equivalence, hence essentially surjective,) but not necessarily the image. This means we can't necessarily find a composite f;g with the same domain as f, for example---the best we can do is ask for the domain to be vertically isomorphic to d(f).

Definition [efr-003A]

Let X: \Delta ^\mathrm {op} \to \mathcal {C} be a simplicial object in a category, and suppose \mathcal {C} has all limits. Then the right Kan extension along the coYoneda embedding \mathrm {Ran}_yX : \mathsf {sSet}^\mathrm {op} = [\Delta ^\mathrm {op},\mathsf {Set}]^\mathrm {op} \to \mathcal {C} exists. If S is a simplicial set, we denote by a minor abuse of notation X[S] the value of this Kan extension at this set. Thus X[n] = X[\Delta ^n].

We will also use this notation when \mathcal {C} does not have all limits, as long as this Kan extension exists at the given point. For example, if \mathcal {C} has merely finite limits, it exists for all simplicial sets with finitely many nondegenerate simplices.

Example [efr-003B]

C[\partial \Delta ^1] = C[0] \times C[0], and the inclusion of the boundary in the whole induces a map C[\Delta ^2] = C[2] \to C[0] \times C[0] = C[\partial \Delta ^1], which is precisely the pairing of the two face maps.

C[\partial \Delta ^2] is the "pullback" of three copies of C[1] over three copies of C[0]---one could write it as C[1] \times _{C[0]} C[1] \times {C[0] \times C[0]} C[1], where the map C[1] \times _{C[0]} C[1] \to C[0] \times C[0] picks out the domain of the first 1-cell and the codomain of the second one, and the map C[1] \to C[0]\times C[0] is the above discussed pairing of the face maps.

Thus, as expected, an element of C[\partial \Delta ^2] consists of a triple of 1-cells with compatible endpoints to make up a triangle (but no 2-cell to fill it). The restriction map C[\Delta ^2] \to C[\partial \Delta ^2], as expected, takes this boundary of a 2-cell.

Definition [efr-003C]

Let \mathcal {C} be a model category, and consider a simplicial object X: \Delta ^\mathrm {op} \to \mathcal {C}.

The latching object of X at stage r, denoted L_rX \in \mathcal {C}, is the colimit \operatorname {colim}_{s: [r] \to [k]} X[k] where s: [r] \to [k] runs over all surjections out of [r] except the identity

The matching object M_r is the limit \lim _{d: [k] \to [r]} X[k] runs over all injections into [r] except the identity.

Note that there are canonical maps L_rX \to X[r] \to M_rX. A simplicial object is Reedy cofibrant if L_rX \to X is always a cofibration, and Reedy fibrant if X \to M_rX is always a fibration.

These are of course small parts of the Reedy model structure on simplicial objects, but we will not need to discuss this in detail.

[efr-003D]

Let C be a Reedy fibrant simplicial category. Then the functors C[n] \to C[m] induced by injective [m] \hookrightarrow [n] are fibrations. In particular, C is a weak Segal category if and only if the functors C[m+n] \to C[n] \times _{C[0]} C[m] are equivalences (where this is a strict pullback). Moreover, this functor is also a fibration (whether C is weak Segal or not), so that if C is weak Segal, it is in fact a trivial fibration.

Proof

By assumption, the functor C[n] \to L_nC = C[\partial \Delta ^n] is a fibration for each n. Note that C[n] \to C[n-1] factors over this, so it suffices to show that the further map C[\partial \Delta ^n] \to C[n-1] is a fibration (since fibrations compose, this proves C[n] \to C[n-1] is a fibration, and composing these we find C[n] \to C[m] is one). Note we can express C[\partial \Delta ^n] as an iterated pullback of copies of C[n-1] over copies of C[n-2]. Assuming the maps C[n-1] \to C[n-2] are themselves fibrations, since fibrations are stable under pullback, this proves the result. By induction it suffices to prove the base case C[1] \to C[0]. The two maps of this form are the two projections of C[1] \to C[\partial \Delta ^1] = C[0] \times C[0], but note that this is a fibration and a projection out of a product is always a fibration.

Since pullbacks of fibrations are homotopy pullbacks, this proves the claim about C being a weak Segal category. The functor C[n+m] \to C[n] \times _{C[0]} C[m] factors over C[\partial \Delta ^{n+m}]. By expressing this as a pullback of copies of C[n+m-1], iteratively replacing these by their boundaries (each such replacement is a fibration, and a limit of fibrations is a fibration) until we reach dimensions n and m, whereupon we project out the rest of the pullback, suffices to prove that this morphism is a fibration.

By definition, if C is weak Segal it is also an equivalence, hence a trivial fibration.

Since trivial fibrations admit strict sections, this will give us the strict composites we were looking for.

Theorem [efr-003O]

The 2-nerve functor of Lack and Paoli \mathsf {BiCat}^{\mathrm {supic}} \to [\Delta ^\mathrm {op},\mathsf {Cat}] factors over the inclusion \mathsf {BiCat}^{\mathrm {supic}} \hookrightarrow \mathsf {PsDbl}. The resulting nerve functor N_\mathsf {Dbl}: \mathsf {PsDbl} \to [\Delta ^\mathrm {op},\mathsf {Cat}] is fully faithful. Moreover, the image of the isofibrant pseudo double categories consists exactly of the Reedy fibrant, 3-coskeletal, weak Segal categories.

Proof

First, note that the inclusion \mathsf {BiCat}^\mathrm {supic} \to \mathsf {PsDbl} is fully faithful, and so we may construct our factorization simply by taking N_\mathsf {Dbl}(\mathbb {C})[n] = \mathsf {PsDbl}([n],\mathbb {C}), viewing [n] as a (vertically discrete) double category using the inclusion \mathsf {Cat} \hookrightarrow \mathsf {BiCat}^\mathrm {supic} \hookrightarrow \mathsf {PsDbl}.

Let us quickly observe that, for any pseudo double category, the nerve is 3-coskeletal. Recall this means N_\mathsf {Dbl}(\mathbb {C})[n] \to N_\mathsf {Dbl}(\mathbb {C})[\partial \Delta ^n] is an isomorphism if n>3. This is clear, since a double category has no four-dimensional information (by contrast, the case n=3 is not an isomorphism, but merely a discrete isofibration, since a 3-cell involves a diagram of 2-cells which may or may not commute).

The full faithfulness is more or less immediate. Certainly a pseudo double functor is determined by its action on objects, 1-cells and 2-cells, which are the objects and morphisms of N_\mathsf {Dbl}(\mathbb {C})[0],N_\mathsf {Dbl}(\mathbb {C})[1], and its chosen functoriality 2-cells, which are obtained by applying the functor N_\mathsf {Dbl}(\mathbb {C})[2] \to N_\mathsf {Dbl}(\mathbb {D})[2] to a commutative triangle---this proves faithfulness. Conversely, it's straightforward to verify that the preceding data always assembles into a pseudofunctor, which proves fullness (the action on the higher simplices is determined by the action of the lower simplices due to coskeletality).

Let \mathbb {C} be an isofibrant pseudo double category. We must prove its image is Reedy fibrant and weak Segal. As noted above the only things to check, in order to prove fibrancy, are the cases n=1,2,3. The case n=1 is exactly the assumption that \mathbb {C} is isofibrant, since N_\mathsf {Dbl}(\mathbb {C})[0] = \mathbb {C}[0] and N_\mathsf {Dbl}(\mathbb {C})[1] = \mathbb {C}_1.

In the case n=2, the matching category consists of triangles (not necessarily commutative) in the horizontal category, and a lift is a choice of globular isomorphism rendering it commutative. Given a triple of (not necessarily globular) isomorphisms in the base, we can clearly compose these with this commutator to get another 2-cells rendering the target triangle commutative, which is the desired lift.

In the case n=3, the matching category consists of tetrahedra, that is, quadruples of triangles choosing compositions for a triple of morphisms f,g,h. There is a unique lift of such an object if and only if the implied square of globular 2-cells commute. Clearly this commutativity is stable under isomorphism, which implies we have isomorphism lifting in this case also.

To see that it's weakly Segal, consider the functor N_\mathsf {Dbl}(\mathcal {C})[n] \to N_\mathsf {Dbl}(\mathcal {C})[1]^{\times _{N_\mathsf {Dbl}(\mathcal {C})[0]}n}, where this denotes the n-fold pullback in the obvious way. It suffices to show that these are all equivalences (since equivalences have the 2-of-3 property). By coskeletality it suffices to do this for n=2 and n=3. In both cases it is easy to see that the functor is essentially surjective (since you can lift any object by choosing composites, and associator cells). The full faithfulness can be observed by considering the following diagram:

A morphism in N_\mathsf {Dbl}(\mathcal {C})[2] is a commutative diagram such as this, with each face filled with a 2-cell, so that the triangular faces are isomorphisms, and so that the resulting diagram of 2-cells commutes also. But clearly, if we forget the 2-cell between the morphisms labeled f,f', there is a unique way to reconstruct it---it must be the composite of the other two square 2-cells with the globular 2-isomorphisms in the triangle. This proves the full faithfulness in the case n=2. The case n=3 is completely analogous.

Now conversely, given a weakly Segal Reedy fibrant simplicial category C, it is the nerve of a pseudo double category with vertical category C[0], category of 1-cells C[1], and composition given by choosing a section C[1] \times _{C[0]} C[1] \to C[2]. By considering the category C[3], we find a unique choice of associator 2-cell, and looking at C[4] proves coherence---the details are exactly as in Reference [lack-paoli-nerves-bicats] for bicategories.

Having found that pseudo double categories are a full subcategory of simplicial categories, we might hope to characterize the essential image. However, they are not all weak Segal objects (as we've seen, this requires isofibrancy), and nor are they strict Segal (this would require discreteness---the strict Segal categories are exactly the strict double categories). There may be a good way of characterizing the image of \mathsf {Dbl}, but the present theorem is suitable for our purposes

Theorem Lack Model Structure [efr-003I]

There is a model structure on the category \mathsf {BiCat}_s of bicategories and strict functors, in which

  1. The weak equivalences are precisely the biequivalences, i.e. those (strict) functors which are equivalences on each hom-category, and surjective up to equivalence on objects
  2. The fibrations are those functors F: \mathcal {C} \to \mathcal {D} with the equivalence lifting property, namely those that are isofibrations on each hom-category, and where given an object x \in \mathcal {C} and an equivalence f: F(x) \xrightarrow {\sim } y, there is a lift of f to an equivalence \tilde {f}: x \xrightarrow {\sim } \tilde {y}. We will also refer to these as equifibrations.

See Reference [lack-model-structure-bicats]. Since we are not really interested in this structure, except as we pass through it to construct the objects we're interested in, we will not dwell too much on it. Note however one important point, observed by Buckley in his work on Grothendieck 2-fibrations: all fibrations in his sense have the equivalence lifting property.

Note that there is an obvious inclusion \mathsf {Cat} \hookrightarrow \mathsf {BiCat}_s.

Definition Bicategory of pseudofunctors [efr-003J]

Let \mathcal {C},\mathcal {D} be bicategories. Then there is a bicategory \mathsf {BiCat}^\mathrm {ps}(\mathcal {C},\mathcal {D}), where

  1. The objects are the pseudofunctors \mathcal {C} \to \mathcal {D}
  2. The morphisms are the strong transformations
  3. The 2-cells are the modifications

See Reference [johnson-yau-2dim-categories]. We will use this to construct, given the 2-fibration \mathsf {Para}_\mathcal {M}(\mathcal {C}) \to B\mathcal {M} corresponding to an action, a simplicial category classifying the double category \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C}).

Lemma [efr-003H]

Let \mathcal {C} \to \mathcal {D} be a strict Buckley fibration. Then the map of simplicial bicategories \mathcal {C}^{[n]} \to \mathcal {D}^{[n]} is a Reedy fibration (with respect to the Lack model structure on bicategories)

Definition [efr-003L]

Let \mathcal {C} be a bicategory. Then its 2-nerve, denoted N(\mathcal {C}), is a simplicial category given by defining N(\mathcal {C})[n] to be the category where

  1. The objects are strictly unitary pseudofunctors [n] \to \mathcal {C}
  2. The morphisms are icons F \Rightarrow G, that is to say identity-on objects oplax natural transformations

(See again Reference [johnson-yau-2dim-categories]) It is not hard to see that the 2-nerve of a bicategory \mathcal {C} is a weak Segal category, and under the loose identification of weak Segal categories and pseudo double categories, it corresponds to the pseudo double category with horizontal bicategory \mathcal {C} and discrete vertical category. Thus, the nerve of the bicategory \mathsf {Para}_\mathcal {M}(\mathcal {C}) is not quite the gadget we're after---we need to add some vertical morphisms.

One thing we can consider is the simplicial bicategory \mathsf {BiCat}^\mathrm {ps}([n],\mathsf {Para}_\mathcal {M}(\mathcal {C})). This has all the morphisms we want---we just need to thin them out so that the vertical components always live inside \mathcal {C}, i.e. have trivial parameter. It turns out that the way to do this is to consider the pullback of this diagram:

Lemma [efr-003K]

Let p: \mathcal {C} \to \mathcal {D} be a (strict) 2-fibration, and fix a bicategory \mathcal {K}:

  1. The functor object \mathsf {BiCat}^\mathrm {ps}(\mathcal {K},\mathcal {C}) \to \mathsf {BiCat}^\mathrm {ps}(\mathcal {K},\mathcal {D}) is again a 2-fibration
  2. If \mathcal {C} is fibred in 1-categories, so is \mathsf {BiCat}^\mathrm {ps}(\mathcal {K},\mathcal {C})

Proof

First, let F, G: \mathcal {K} \to \mathcal {C} be two pseudofunctors, and consider the category \operatorname {Nat}(F,G) of strong natural transformations F \Rightarrow G and modifications between these. We must prove that p is a local fibration, i.e that \operatorname {Nat}(F,G) \to \operatorname {Nat}(pF,pG) is a 1-fibration.

Thus let \alpha : F \Rightarrow G be a strong natural transformation, and let \Gamma : p(\alpha ) \to \beta ' be a modification, where \beta ': pF \Rightarrow pG is some other strong natural transformation. Then \Gamma consists in a family of 2-cells in \mathcal {D} \Gamma _X: p(\alpha )_X \Rightarrow \beta _X'. These are 2-cells p(\alpha _X) \to \beta '_X and so we can find a family of Cartesian lifts \alpha _X \to \beta _X (where this defines \beta _X)

The Cartesian-ness of the lift \alpha _X \to \beta _X suffices to generate the necessary naturality squares

DIAGRAM HERE

, and it is similarly not too hard to see that the equations hold. The equations for being a modification hold by construction, so that the lifted maps \alpha _X \to \beta _X assemble into a modification. The same argument will show that, given some other modification \gamma \to \alpha and a factorization over \beta ' in the base, it lifts and lifts uniquely to the total category.

Let us stop here to note that, if the hom-fibrations of \mathcal {C}(X,Y) \to \mathcal {D}(pX,pY) are discrete fibrations, then the lifts above will be unique, and hence the modification lifting \Gamma will be unique, and so also \mathsf {BiCat}^\mathrm {ps}(\mathcal {K},\mathcal {C})(F,G) \to \mathsf {BiCat}^\mathrm {ps}(\mathcal {K},\mathcal {D})(pF,pG) will be a discrete fibration. Since this is what it means to be fibred in 1-categories, this proves part 2 of the lemma.

Now if F: \mathcal {K} \to \mathcal {C} is a functor, and \alpha : G' \Rightarrow pF is a natural transformation, we must construct again a Cartesian lift. As before, since the uniqueness properties making something Cartesian can more or less be checked object-wise, the difficult part is verifying that the individual objects \alpha _X^*F(X) assemble into a pseudofunctor.

But once again, this can be done piecewise. Since the map \alpha _Y^*F(Y) \to F(Y) is Cartesian, given each f: X \to Y \in \mathcal {K}, there is an essentially unique filler in the below diagram:

which defines the action on morphisms and the naturality squares for the lift of \alpha , and one proceeds like this.

Lemma [efr-003M]

Let p: \mathcal {C} \to \mathcal {D} be an equifibration. Equip the functor category [\Delta ^\mathrm {op},\mathsf {BiCat}_s] with the Reedy model structure with respect to the Lack model structure on bicategories. Then \mathsf {BiCat}^\mathrm {ps}([\bullet ],\mathcal {C}) \to \mathsf {BiCat}^\mathrm {ps}([\bullet ],\mathcal {C}) is a fibration.

Proof

First note that \mathcal {C}^{[n]} \to \mathcal {C}^{\partial \Delta ^n} = M_n\mathcal {C} is an isomorphism when n \geq 4, since a pseudofunctor involves only 3-dimensional information. In this case the functor \mathcal {C}^{[n]} \to M_n\mathcal {C} \times _{M_n\mathcal {D}} \mathcal {D} is an isomorphism, and so certainly a fibration.

When n=3, the objects of the codomain correspond to triples of morphisms f,g,h with two choices of composite, and such an object is in the image if and only if the given diagram of 2-cells commutes---the functor is locally an isomorphism. Hence the functor \mathcal {C}^{[3]} \to M_3\mathcal {C} \times _{M_3\mathcal {D}} \mathcal {D} is locally an isomorphism, so it suffices to prove it has the equivalence lifting property for 1-cells.

To see this, observe that since \mathcal {D}^{[3]} \to M_3\mathcal {D} is a local isomorphism, to give a morphism in the pullback is just to give a morphism in M_3\mathcal {C}. But since the property of commuting is certainly stable under equivalence, indeed we can lift such a morphism.

When n=2, the objects of the matching bicategory M_2\mathcal {C} are simply triangles, and to lift a triangle is to choose a 2-isomorphism rendering it commutative. Now \mathcal {C}^{[2]} \to M_2\mathcal {C} merely has discrete fibers.

In this case, let \sigma : [2] \to \mathcal {C} be a pseudofunctor, i.e a commutative triangle. An isomorphism starting at the image of \sigma in the pullback M_2\mathcal {C} \times _{M_2\mathcal {D}}\mathcal {D}^{[2]} consists of

  1. A choice of three 2-isomorphisms in \mathcal {C}, one for each side
  2. A choice of isomorphism p(\sigma ) \to \gamma ' in \mathcal {D}^{[2]} (consisting of a 2-isomorphism for each side, so that composing them all with the 2-isomorphism filling p(\sigma ) yields the one filling p(\gamma ))
  3. Such that the 2-isomorphisms in \mathcal {C} are taken to the ones in \mathcal {D}
There is only one possible lift, namely the isomorphism \sigma \to \gamma where \gamma is defined as the composite of the given 2-isomorphisms. But now commutativity of the square precisely implies this must be a lift of the isomorphism in \mathcal {D}^{[2]} as well, and we're done.

Finally, the case of n=1 is completely analogous to n=2. M_1\mathcal {C} \cong \mathcal {C}^2, and the fiber over two objects is the hom-category. Here we use the isomorphism lifting property for the individual hom-categories.

Proposition [efr-003G]

Let \mathcal {M} be a monoidal category which acts on \mathcal {C}. Let \hat {\mathcal {C}} \to B\mathcal {M} be the fibration of bicategories which classifies this action. For each [n] \in \Delta , we have an induced fibration \hat {\mathcal {C}}^{[n]} \to B\mathcal {M}^{[n]}. Let \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C})[n] denote the fiber of the composite functor \mathcal {C}^{[n]} \to B\mathcal {M}^{[n]} \to B\mathcal {M}^{n+1} over the unique object (*,\dots ,*), where the latter functor is just evaluation at the n+1 objects of [n] (this is not a 2-fibration in general---although it is an isofibration, so the fiber is still well-behaved). Then

  1. Each such fiber is actually a 1-category
  2. This construction is functorial in [n], so that \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C})[-] is a simplicial category
  3. This simplicial category is a Reedy fibrant weak Segal category. Up to equivalence, it classifies \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C}), so that the notation makes sense.

Proof

Note that, since pullbacks compose, \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C})[n] can equivalently be computed as the fiber over B\mathcal {M}^{[n]} \times _{B\mathcal {M}^{n+1}} * \hookrightarrow B\mathcal {M}^{[n]}. It is not too hard to see that this pullback is exactly equivalent to \mathcal {M}^n. Now, by construction, \hat {\mathcal {C}} is fibred in 1-categories, and it follows that the 2-fibration \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C})[n] \to \mathcal {M}^n is also fibred in 1-categories. But since \mathcal {M}^n is itself an 1-category, the total category must be an 1-category (namely the Grothendieck construction of the functor \mathcal {M}^{n,\mathrm {op}} \to \mathsf {Cat} classifying the fibration).

The functoriality is clear, since every construction above is functorial in [n].

By construction, we have the following pullback diagram:

Since the right-hand map is a Buckley fibration, it is an equifibration

make sure these are introduced

, and hence these pullbacks are homotopy pullbacks of bicategories. Since the tautological cosimplicial object \Delta \hookrightarrow \mathsf {BiCat} is coSegal (in that its dual, a simplicial object in \mathsf {BiCat}^\mathrm {op}, is a Segal object), the functor [n] \mapsto \mathcal {D}^{[n]} is a Segal object of [\Delta ^\mathrm {op},\mathsf {BiCat}], which is weak Segal (with respect to the Lack model structure on bicategories) because the forgetful functors \mathcal {D}^{[n]} \to \mathcal {D}^{[m]} are equifibrations. It is easy to see that \mathcal {M}^n is also a Segal object, and hence \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C})[-], as a simplicial bicategory, is a weak Segal object. But the subcategory of 1-categories within bicategories is stable under homotopy limits, so that this implies that it is a weak Segal object as a simplicial category as well.

By the same argument, using lemma Lemma [efr-003M], and the fact that pullbacks of fibrations preserve fibrations, the natural transformation \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C})[n] \to \mathcal {M}^{n} = N(B\mathcal {M}) is a Reedy fibration. Since \mathcal {M}^n is easily seen to be Reedy fibrant, the same holds for \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C})

Thus we have a functor from monoidal category actions to isofibrant pseudo double categories (in their guise as Reedy fibrant weakly Segal simplicial categories). Moreover, as it is given as a limit---and, since the limit in question is a pullback of a fibration, and hence a homotopy limit---it will be fairly straightforward to show that this construction preserves internal categories. Hence we will be able to use it to construct a pseudo triple category, as we wanted.

Definition Iwss triple category [efr-003Q]

Need a good name here!

An iwss triple category (isofibrant weak-strict-strict) is a bisimplicial category \mathbb {C}: \Delta ^\mathrm {op} \times \Delta ^\mathrm {op} \to \mathsf {Cat} so that for each n, \mathbb {C}[n,-] is a fibrant strict Segal category, and \mathbb {C}[-,n] is a fibrant weak Segal category.

  1. A object of the triple category \mathbb {C} is an object of \mathbb {C}[0,0].
  2. The morphisms of \mathbb {C}[0,0] are called the vertical morphisms of \mathbb {C}. They form a category denoted \mathbb {C}_{0,0,-}
  3. The objects of \mathbb {C}[0,1] are called the horizontal morphisms of \mathbb {C}. They form a category denoted \mathbb {C}_{0,-,0}
  4. The objects of \mathbb {C}[1,0] are called the transverse morphisms of \mathbb {C}, or the protomorphisms.
  5. The vertical and horizontal morphisms form a strict double category (the one with nerve \mathbb {C}[0,-]), whose 2-cells are the morphisms of \mathbb {C}[0,1]. We call this the planar double category, and denote it \mathbb {C}_{0,-,-}
  6. The vertical and transverse morphisms form a pseudo double category (the one with nerve \mathbb {C}[-,0]), whose 2-cells are the morphisms of \mathbb {C}[1,0]. We call this the vertical double category, and denote it \mathbb {C}_{-,0,-}
  7. The horizontal transverse morphisms also form a pseudo double category, which has nerve \operatorname {\mathbf {ob}} \mathbb {C}[-,-]---its 2-cells are the objects of \mathbb {C}[1,1]. We call this the horizontal double category, and denote it \mathbb {C}_{-,-,0}
  8. For each of the three classes of morphism, there is a double category with it as the objects, the two classes of 2-cells involving it as the 1-cells, and the morphisms of \mathbb {C}[1,1] as the 2-cells. These are denoted \mathbb {C}_{1,-,-}, etc. There is no good way to name them.
  9. The globular horizontal 2-cell isomorphisms, and the globular vertical 2-cell isomorphisms, are the same (in the sense that each has a companion in \mathbb {C}_{1,-,-}, and hence the two sets of isomorphisms between any two transverse morphisms are canonically and functorially in bijection). Taking either of these sets as the 2-cells, there is a bicategory with the transverse morphisms as its morphisms, denoted \mathbb {C}_{0,-,0}

Remark

One could replace each category \mathbb {C} with its nerve, obtaining a trisimplicial set \mathbb {C}[n,m,k]---the notations \mathbb {C}_{-,0,-} and so on for the sub-double categories should be understood in this way. Of course, analogously we could restrict to a simplicial strict double category. However, the homotopy theory of diagram categories is in some ways easier to think about, so we prefer this presentation.

Remark

The functoriality ensures every type of coherence between these objects that you could wish for. Since there is only one dimension of weakness, writing down coherence equations would probably be feasible---nevertheless, given the huge number of different data involved, the compact presentation of Definition [efr-003Q] seems preferable. In general, because of this huge amount of data, we expect mostly to work with fragments of this triple category.

Theorem [efr-003R]

Let \mathbb {M} be a monoidal strict double category, which acts on a strict double category \mathbb {C}. Then for each n \in \Delta ^\mathrm {op}, we have an actegory \mathbb {M}[n] acting on \mathbb {C}[n]. This yields a bisimplicial category [n,m] \mapsto \mathsf {\mathbb Para}_{\mathbb {M}[m]}(\mathbb {C}[m])[n]. This is an iwss triple category

In particular, let \mathbb {M} \to \mathbb {C} be a functor of symmetric monoidal strict double categories. Then the canonical action of \mathbb {M} on \mathbb {C} gives a double category as above.

Definition \mathsf {\mathbb Ctrl} [efr-000I]

Let \mathcal {C}, \mathcal {A}(-), T be a dynamical systems theory, let \mathsf {\mathbb Arena} be the associated category of arenas. Recall that \mathsf {\mathbb Arena}_0 is the category of lenses. Consider the (strict) category internal to \mathsf {Arr}(\mathsf {SymMonCat}) given by the following diagram:

By Theorem [efr-003R], the image of this internal category under \mathsf {\mathbb Para}(-) is a iwss triple category. We call this triple category the triple category of controlled processes, and denote it by \mathsf {\mathbb Ctrl}, or \mathsf {\mathbb Ctrl}_{T,\mathcal {C},\mathcal {A}} if we want to disambiguate the choice of doctrine.

(Note the difference between \mathsf {Arr}(\mathcal {C})^\simeq and \mathsf {Arr}(\mathcal {C}^\simeq )---the former has objects all morphisms of \mathcal {C}, and the morphisms between them given by isomorphisms, whereas the latter has objects only the isomorphisms in \mathcal {C})

Remark

By construction, \mathsf {\mathbb Ctrl}_{0,-,-} = \mathsf {\mathbb Arena}, \mathsf {\mathbb Ctrl}_{-,0,-} is a double category consisting of parametrized lenses and chart reparametrizations between them, and \mathsf {\mathbb Ctrl}_{-,-,0} is a double category consisting of parametrized lenses and lens isoparametrizations between them.