Lemma [efr-001P]

Let X: \Delta ^\mathrm {op} \to \mathsf {Cat} be a (strict) simplicial category (note that every simplicial category is equivalent to a strict one). Suppose further the face maps X[1] \rightrightarrows X[0] are both isofibrations. Then if X is a Segal category in the strict sense, it is automatically a Segal category in the pseudo sense.

Proof

Since, up to isomorphism of categories, the higher X[n] are pullbacks of the two indicated face maps, and the projections in the diagram

are compositions of pullback projections, and pullbacks and composition of isofibrations are again isofibrations, it follows that all of these squares are pullbacks of two isofibrations. Such a pullback is always also a homotopy pullback, which proves the first statement.

Context

Constructing the triple category of controlled processes [efr-000G]

Triple categories are very complicated objects. And our life is further complicated by the fact that, in one direction, our triple category is not in general strict, in the sense that composition is only associative up to globular isomorphism (because the tensor product is only pseudoassociative, the composition of controlled processes inherits this defect).

Hence, our life will be greatly simplified if we can approach the construction of this triple category by more conceptual means. Our strategy will essentially be the following:

  1. We will note that the notion of internal pseudocategory is classified by a limit sketch---that is, there is a bicategory (actually, a 1-category) \mathcal {I} and class of diagrams K so that a pseudocategory internal in \mathcal {C} is precisely a pseudofunctor \mathcal {I} \to \mathcal {C} which carries all the diagrams in K to homotopy limits
  2. We will prove that the double categorical \mathsf {\mathbb Para}(-) construction preserves homotopy limits.
  3. Hence, by the preceding point, applying it to a pseudocategory internal to the bicategory of category actions will produce a pseudocategory internal to pseudo double categories---a triple category.

Definition Limit sketch [efr-001M]

A limit sketch consists of a (small) category \mathcal {I} equipped with a collection of cones (J_i \in \mathsf {Cat}, D_i: J_i^\triangleleft \to \mathcal {I}) (recall that J^\triangleleft is the "cone on J", the result of freely adjoining an initial object to J).

If \mathcal {C} is a category, a model of the limit sketch is a functor M: \mathcal {I} \to \mathcal {C} so that each composite J_i^\triangleleft \to \mathcal {I} \to \mathcal {C} is a limit cone. A morphism of models is any natural transformation. In other words, the category of models is the full subcategory of the functor category spanned by the models. It is denoted \mathsf {Mod}_\mathcal {I}(\mathcal {C}) (the collection of diagrams is left implicit).

Given a bicategory or other higher category \mathcal {C}, a model is a pseudofunctor \mathcal {I} \to \mathcal {C} which carries every diagram to a homotopy limit cone. \mathsf {Mod}_\mathcal {I}(\mathcal {C}) \subseteq \mathsf {Fun}(\mathcal {I},\mathcal {C}) is again the full sub-bicategory of the bicategory of pseudofunctors spanned by the models.

We will see that there are limit sketches classifying both internal categories (giving double categories) and symmetric pseudomonoids (giving symmetric monoidal categories), which will be important going forward.

Remark Pseudocategories and categories of categories [efr-001O]

We will want to say that the category of pseudo double categories is the category of internal pseudocategories---modeled as Segal objects---in the bicategory of categories. There are two issues with this statement as written.

First of all, a priori, a weak Segal category is quite different from a pseudo double category. Not only is there not a canonical choice of composition given two horizontal maps f: x \nrightarrow y, g: y \nrightarrow z, we cannot even (a priori) guarantee the existence of a choice of composition gf which has the right boundaries on the nose---only up to vertical isomorphism (so we can find a composite x' \nrightarrow y' and isomorphisms x \cong x', y \cong y'). On the other hand, a weak Segal category is also stronger than a pseudo double category, in the sense that every vertical isomorphism has a companion.

We will see that the first defect can always be remedied after replacing our weak Segal category with an equivalent one. The issue of companions is a fundamental difference, but luckily all of the relevant double categories we want to consider have these companion pairs.

The second question is somewhat subtler (but also less important). The category of internal pseudocategories, computed in any higher category, has a priori the same homotopy level as the input---just as the category of monoids is a 1-category (like \mathsf {Set},) but the category of monoidal categories is a bicategory. This makes sense if we view categories as just a plain (generalized) algebraic theory, but we usually want to think of categories of categories as having some extra homotopy theory coming from the category structure---the category of categories in \mathsf {Set} is a bicategory (actually a 2-category, i.e it's strict), not a plain category. The preceding construction does not account for this---the homotopy limits implicit in the phrase "a pseudocategory in pseudo double categories" are, for us, merely homotopy limits of plain categories, not accounting for the extra categorical structure in a double category.

It is not clear what this means in general (and in any case, our output category will actually be strict in two directions,) but it is an important subtlety to remember.

(A category viewed as an object merely of the 1-category of categories is sometimes called a strict category, but obviously we can't speak about "strict pseudo double categories")

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.

Lemma [efr-001P]

Let X: \Delta ^\mathrm {op} \to \mathsf {Cat} be a (strict) simplicial category (note that every simplicial category is equivalent to a strict one). Suppose further the face maps X[1] \rightrightarrows X[0] are both isofibrations. Then if X is a Segal category in the strict sense, it is automatically a Segal category in the pseudo sense.

Proof

Since, up to isomorphism of categories, the higher X[n] are pullbacks of the two indicated face maps, and the projections in the diagram

are compositions of pullback projections, and pullbacks and composition of isofibrations are again isofibrations, it follows that all of these squares are pullbacks of two isofibrations. Such a pullback is always also a homotopy pullback, which proves the first statement.

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-0017]

Let \mathcal {C} be a category with finite limits. The internal nerve functor \mathsf {Cat}(\mathcal {C}) \to \mathsf {Simp}\mathcal {C} is fully faithful, and the essential image consists exactly of those simplicial objects X where the maps p_i: X[n] \to X[1] given by evaluating at p^i: [1] \to [n] : k \mapsto k+i, i = 0,\dots n-1 exhibits X[n] as the iterated pullback X[1] \times _{X[0]} \dots \times _{X[0]} X[1]

Proposition [efr-0018]

A pseudo double category is equivalently a simplicial object in \mathsf {Cat} so that the diagrams X[n] \to X[1] are homotopy pullbacks.

Lemma Commutativity of internalization [efr-001Q]

Let \mathcal {I},\mathcal {J} be limit sketches, and let \mathcal {C} be a bicategory. Then \mathsf {Mod}_\mathcal {I}(\mathsf {Mod}_\mathcal {J}(\mathcal {C})) \simeq \mathsf {Fun}'(\mathcal {I} \times \mathcal {J}, \mathcal {C}) \simeq \mathsf {Mod}_\mathcal {J}(\mathsf {Mod}_\mathcal {I}(\mathcal {C})), where \mathsf {Fun}'(\mathcal {I} \times \mathcal {J},\mathcal {C}) denotes the full subcategory of the functor bicategory spanned by those pseudofunctors F so that, for each I \in \mathcal {I},, F(I,-) is a model of \mathcal {J}, and for each J \in \mathcal {J}, F(-,J) is a model of \mathcal {I}.

Proof

Each isomorphism is an immediate consequence of the obvious fact that (pseudo)limits in model (bi)categories are computed pointwise, and the standard currying equivalence.

Remark

Note that if \mathcal {C} is a 2-category, so that we can speak of both pseudolimits and ordinary limits in \mathcal {C}, taking strict models does not generally commute with taking pseudo models, since it is not generally the case that pseudolimits commute with limits.

Remark [efr-001R]

A weak Segal category is similar to a virtual double category: we don't directly have a composition operator \mathbb {C}_1 \times _{\mathbb {C}_0} \mathbb {C}_1---rather, we have a category of "compositions" \mathbb {C}_2, each of which contains three faces in \mathbb {C}_1. Hence we have a choice of composites for every composable pair, although it is uniquely defined up to contractible choice.

Definition Coherent nerve of pseudo double category [efr-001S]

Let \mathbb {C} be a pseudo double category. Then the coherent nerve is the simplicial category N(\mathbb {C}) defined as follows:

  1. N(\mathbb {C})_0 = \mathbb {C}_0
  2. N(\mathbb {C})_1 = \mathbb {C}_1
  3. The objects of N(\mathbb {C})_2 are tuples f: x \nrightarrow y, g: y \nrightarrow z, h: x \nrightarrow z, \alpha : gf \simeq h, where x,y,z are objects of \mathbb {C}_0, f,g,h are horizontal morphisms, and \alpha is a globular isomorphism in \mathbb {C}_1
  4. The morphisms of N(\mathbb {C})_2 are triples of 2-cells \phi : f \to f', \psi : g \to g', \xi : h \to h' so that the two possible 2-cells gf \to h' agree
  5. Given four compatible objects of \N (\mathbb {C})_2 defining a 3-boundary (a tetrahedron), there is a unique objects of \N (\mathbb {C})_3 filling it if and only if the square of globular isomorphisms commute
  6. Given four compatible morphisms of \N (\mathbb {C})_2, there is always a unique morphism in \N (\mathbb {C})_3 filling the boundary
  7. The face- and degeneracy functors are the obvious ones
  8. \N (\mathbb {C}) is 3-coskeletal, which defines the rest of the structure

Theorem [efr-001T]

  1. A pseudo double functor \mathbb {C} \to \mathbb {D} is equivalent to a natural transformation N(\mathbb {C}) \to N(\mathbb {D})
  2. If \mathbb {C} is a double category in which each vertical isomorphism has a companion, N(\mathbb {C}) is a weak Segal category
  3. Every weak Segal category is equivalent to one of the form N(\mathbb {C}) for \mathbb {C} a pseudo double category of this type.

Let \mathbb {C} be a double category in which every vertical isomorphism has a companion. Then by

reference here, Shulman stuff,

the source and target functors are isofibrant. To prove N(\mathbb {C}) is a weak Segal category, it therefore suffices to prove that N(\mathbb {C})[2] \to N(\mathbb {C})[1] \times _{N(\mathbb {C})[0]} N(\mathbb {C})[1] is an equivalence of categories, and the analogous statement in level 3 (it follows for the higher levels by coskeletality).

Now, let X be a weak Segal. By

reference

, every simplicial category is equivalent to one which is Reedy fibrant. Note that being a Segal category is preserved by equivalence, so without loss of generality, assume X is Reedy fibrant.

This means the functor X[n] \to X(\partial \Delta ^n) is an isofibration for each n. First, let n=1. This means X[1] \to X[0] \times X[0] is an isofibration. Since such fibrations are stable under pullback, this implies that the projection X(\partial \Delta ^2) \to X[1] \times _{X[0]} X[1] is again an isofibration, which means the composite X[2] \to X[1] \times _{X[0]} X[1] is an isofibration. Since this pullback is a homotopy pullback, and X is weak Segal, it is an equivalence, and hence a trivial equivalence. Choose a (strict!) section s.

By a completely analogous argument, choose a section of X[3] \to X[1] \times _{X[0]} X[1] \times _{X[0]} X[1], which is again a trivial fibration.

Let our pseudo double category have X[1] \rightrightarrows X[0] as the underlying reflective graph, composition defined by the composite X[1] \times _{X[0]} X[1] \to X[2] \xrightarrow {d_1} X[1], associator defined using the degeneracies, and unitor defined using the section of X[3]. Call this pseudo double category \mathbb {X}

It is easy to see there is a functor X \to N(\mathbb {X}), which is the identity on the first two levels. Since the higher levels are homotopy pullbacks of the lower levels, this implies it is an equivalence at each level, concluding the proof.

Theorem \dblPara preserves homotopy limits [efr-000H]

The pseudofunctor \mathsf {\mathbb Para}: \mathsf {Arr}(\mathsf {SymMonCat}) \to \mathsf {PsDbl}, which carries a symmetric monoidal functor \mathcal {C} \to \mathcal {D} to the pseudo double category \mathsf {\mathbb Para}_\mathcal {C}(\mathcal {D}), preserves homotopy limits.

Proof

Note that homotopy limits on both sides are computed levelwise (using the observation that both are categories of models of (homotopy) limit sketches in the bicategory \mathsf {Cat}.)

Since \mathsf {\mathbb Para}_\mathcal {C}(\mathcal {D})_0 = \mathcal {D}, this immediately implies that \mathsf {\mathbb Para}(-)_0 preserves homotopy limits. It suffices to verify that \mathsf {\mathbb Para}(-)_1 also preserves them. But note that \mathsf {\mathbb Para}_\mathcal {C}(\mathcal {D})_1 can be written as the comma object of the cospan \mathcal {C} \times \mathcal {D} \to \mathcal {D} = \mathcal {D}, and since comma objects are PIE limits, they commute with homotopy limits (pseudolimits). This concludes the proof.

Note that (pseudo-) monoids M equipped with a left module C in a general bicategory \mathcal {C} are also classified by a limit sketch, and both the underlying object of the module and the map C \times M \to M are in the image of this limit sketch. By instantiating this for \mathcal {C} being the bicategories of categories (or monoidal categories, etc), we recover alternative versions of Theorem [efr-000H] for category actions that are not symmetric. We will mainly concern ourselves with the symmetric case, however.

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

Proposition [efr-000J]

The objects of \mathsf {\mathbb Ctrl} are arenas.

The three directions of morphism in \mathsf {\mathbb Ctrl} are lenses, charts, and controlled processes.

The lens-chart double category is isomorphically \mathsf {\mathbb Arena}---in particular, composition of both lenses and charts is strictly associative.

The process-chart double category has 2-cells the chart reparametrizations. The process-lens double category has 2-cells the lens isoparametrizations. They both compose in the obvious way.

Processes compose as morphisms of \mathsf {Para}_{\mathcal {C}^\simeq }(\mathsf {Lens})---that is, (S,TS \otimes A \to B) ; (S', TS' \otimes B \to C) = (S' \otimes S, T(S' \otimes S) \otimes A \cong TS' \otimes TS \otimes A \to TS' \otimes B \to C), this is associative up to a coherent choice of globular isoparametrization.

[efr-000U]

We can consider two strategies for constructing the "full" triple category of controlled processes:

  1. Give a construction of the double category of controlled processes and all lens reparametrizations, in a functorial way so that we can extend this to a triple category
  2. Prove that freely(?) adding companions, in a suitable sense, of each globular chart reparametrization, gives the right thing (this should amount to checking a composition rule)

Proposition [efr-000V]

Let \mathsf {\mathbb Ctrl}_1 \to \tilde {\mathsf {\mathbb Ctrl}_1} be constructed by freely adding companions of every globular chart reparametrization. Then \tilde {\mathsf {\mathbb Ctrl}_1} admits the following description:

  1. The objects are the objects of \mathsf {\mathbb Ctrl}_1, i.e tuples A,B,S, TS \otimes A \leftrightarrows B
  2. The vertical morphisms are chart reparametrizations
  3. The horizontal morphisms are lens reparametrizations
  4. \mathsf {\mathbb Ctrl}_1 is thin, and a square exists if and only if the underlying square in \mathcal {C} commutes.
Moreover, the internal category structure \mathsf {\mathbb Ctrl}_1 \rightrightarrows \mathsf {\mathbb Ctrl}_0, and the symmetric monoidal structure, both extend to \tilde {\mathsf {\mathbb Ctrl}_1}, so that we obtain a symmetric monoidal triple category \tilde {\mathsf {\mathbb Ctrl}_1}.

Fix the notation of \mathsf {\mathbb Ctrl} vs \tilde {\mathsf {\mathbb Ctrl}}

Proof

It is apparent that the given data describes a double category which receives a functor from \mathsf {\mathbb Ctrl}_1. It is also apparent that globular chart reparametrizations have companions in this double category, given by the equivalent globular lens reparametrization. Since, as developed in

insert example here

, we have seen that every lens reparametrization factors as a composite of companions of lens isoparametrizations and companions of globular chart reparametrizations...

finish this

.