Theory and Applications of Categories, Vol. 27, No. 16, 2013, pp. 393–444.

COMPOSITION OF MODULES FOR LAX FUNCTORS

ROBERT PARÉ

Abstract. We study the composition of modules between lax functors of weak double categories. We adapt the bicategorical notion of local cocompleteness to weak double categories, which the codomain of our lax functors will be assumed to satisfy. We introduce a notion of factorization of cells, which most weak double categories of interest possess, and which is sufficient to guarantee the strong representability of composites of modules between lax functors whose domain satisfies it.

Introduction

We are interested in lax functors between weak double categories. There are several reasons for this. One is that representables for weak double categories are lax functors [15]. Another is that V-categories can be viewed as lax functors in various ways [17], [3]. Monads are lax functors defined on 1. In fact in the first paper on bicategories [1], lax functors were called “morphisms of bicategories”, thus underlining their fundamental nature.

The notion of transformation between lax functors is a little less obvious. In [1], lax and oplax transformations were defined but these present some problems. For one thing, no notion of transformation made bicategories with lax functors and transformations into a bicategory or a tricategory, a feature which seemed desirable. It also seemed a bit mysterious that there was no preferred choice between lax and oplax transformation. Over the years various other notions of transformation have appeared, for example the ICONs of [12], and the modules of [5]. Here we will see how all these notions fit together to form a virtual double category [6], and under the hypothesis of our main theorem 4.0.1 an actual weak double category, and this not just for bicategories but for weak double categories too.

In the context of double categories it is natural to look for horizontal and vertical transformations. There is a natural notion of horizontal morphism between lax functors, which we call simply natural transformations (of lax functors, if confusion is possible). The theory presents no problem. For 2-categories considered as horizontal double categories (i.e. vertical arrows are identities), natural transformations are exactly 2-natural transformations. For bicategories considered as vertical weak double categories, they correspond to (dual) ICONs.

Research supported by an NSERC grant.

Received by the editors 2012-05-21 and, in revised form, 2013-04-02.

Published on 2013-04-03 in the volume of articles from CT2011.

2010 Mathematics Subject Classification: 18D05,18D25.

Key words and phrases: double category, lax functor, module, modulation, representability.

\begin{matrix}c \\ ◯ \end{matrix} Robert Paré, 2013. Permission to copy for private use granted.

Vertical morphisms of lax functors are a little trickier but there is still a natural candidate, a kind of multiobject profunctor, which in fact reduces to profunctors in the case where the domain is 1 and the codomain 𝕊et or, more generally, V-profunctors for V-𝕊et. This was introduced in [5] for bicategories, and called “module”. The definition given there is easily adapted to weak double categories. A notion of 2-cell, called “modulation”, is given in [5], which is also easily lifted to the weak double category setting.

These vertical morphisms come up in the study of double limits and colimits where it is important to understand their dependence on vertical morphisms of diagrams. This is already suggested by the two dimensional property of limits introduced in [8].

Another context where vertical morphisms can be interesting is in model theory. A first order theory can be viewed as a weak double category in a way completely analogous to Lawvere theories, with terms giving horizontal morphisms and formulas the vertical ones [14]. Then a model is a product preserving functor into 𝕊et, so modules give important extra structure which seems to have been ignored so far.

The composition of modules is however not straightforward, and this is something which must be addressed if the theory is to proceed. Part of the problem already appears for V-profunctors where completeness conditions on V are required, and the composite is given by a coend formula. So it is clear that certain cocompleteness properties of the recipient category will be needed.

But this is just part of the problem. A variation on this coend formula is given in [5] but it does not apply, as is, to the weak double category case. The problem is that their formula is not horizontally functorial on general double cells, although for special cells it is, and for bicategories, all cells are special. We isolate a certain factorization property of double cells which holds in many important cases, among which are bicategories, and for which a modification of the formula from [5] does indeed give composition of modules. We consider this to be the major contribution of the present work.

This property, which we call AFP, is only one of many similar ones which have come up in our work on double categories, e.g. double Kan extensions. What it means to factor an arrow, being a one dimensional entity, is clear. It is a composite of two arrows, an epi-like one followed by a mono-like one. By contrast, cells being two dimensional, a whole panorama of factorization schemes such as our AFP is opened up. We foresee many other kinds of factorizations playing a central role in double category theory.

The subject of this paper presents an expository challenge. The proof of the main theorem requires checking a large number of details, each of which is more or less straightforward once everything has been properly set up. Conventional mathematical writing style would probably suggest they be omitted, but doing so certainly leaves a lingering doubt that something important has been missed. So we have written down all the details, which are there for anyone to check. Notationally, this is non-trivial, and we consider this to be the secondary contribution of the paper. Our notation, though not perfect, is a vast improvement over previous drafts.

Section 1 recalls the necessary background. We give the relevant definitions listing the conditions in point form for easy reference later on.

In section 2 we begin the construction of the composition of modules.

Section 3 contains our main definition, AFP, and completes the construction.

A complete proof of the main theorem is given in section 4.

The paper ends with a section tying up some loose ends. We show that identities are always strongly representable, which together with theorem 4.0.1, shows that modules provide the vertical structure for a weak double category of lax functors (under the hypotheses of the theorem of course). We show that our construction reduces to that of [5] in the case of bicategories, although not in a completely straightforward way. This validates their claim that composition of modules is associative.

1. Preliminaries

1.1. Lax Functors, Modules, Modulations We summarize here the basic definitions for easy reference. The two dimensional cell diagrams are given fully in [15], to which the reader is referred for more detail and examples.

1.1.1. Convention. By “double category” we always, unless otherwise specified, “weak double category”.

To say that a double category is weak means that vertical composition is associative and unitary up to coherent special isomorphisms

𝔞 = 𝔞_{v_{3},v_{2},v_{1}} : v_{3} · (v_{2} · v_{1}) ⇒ (v_{3} · v_{2}) · v_{1}
𝔯 = 𝔯_{v} : v · id_{A} ⇒ v
𝔩 = 𝔩_{v} : idĀ · v ⇒ v

satisfying the same coherence conditions as bicategories, i.e. pentagon, etc. The double arrow indicates that we are talking about a special cell, i.e. one whose vertical domain and codomain are identities. For example 𝔩 looks like

[figure: Ā; Ā; Ā; Ā; •; ^{idĀ}; Ā; Ā; Ā; A; Ā; •; v; A; A; A; Ā; Ā; A; Ā; A; A; A; Ā; •; v; 𝔩]

In what follows we will omit the associativity isomorphisms and treat them as equalities, otherwise the already complicated formulas would risk becoming incomprehensible. They are easily added in for anyone wishing to do so. We sometimes also omit the unit isomorphisms when we feel it helps, although it’s usually better not to.

396  ROBERT PARÉ

1.1.2. Definition. A lax functor F : 𝔸 [figure] 𝕏 consists of the following data: (LF1) Functions, all denoted F, taking objects, arrows and cells of 𝔸 to similar ones in 𝕏,

respecting boundaries (domains and codomains); (LF2) (Laxity cells) for every object A of 𝔸 a special cell ϕA : id_{F A} ⇒ F (id_{A}) and for every

pair of vertical arrows A [figure: •; v] Ā [figure: •; v̄] Ã a special cell ϕ(v̄, v) : F (v̄) · F (v) ⇒ F (v̄· v). They are required to satisfy: (LF3) (Horizontal functoriality) F (1_{A}) = 1_{F A}, F (1_{v}) = 1_{F v}, F (f′f) = F (f′)F (f), F (α′α) =

F (α′)F (α); (LF4) (Naturality of ϕ) F (id_{f})(ϕA) = (ϕA′)(id_{F f}), F (ᾱ · α)ϕ(v̄, v) = ϕ(v̄, v)(F ᾱ · F α); (LF5) (Unit and associativity laws for ϕ) ϕ(idĀ, v)(ϕF Ā · F v) = can, ϕ(v, id_{A})(F v · ϕA) =

can, ϕ(ṽ, v̄ · v)(F ṽ · ϕ(v̄, v)) = ϕ(ṽ, ·v̄, v)(ϕ(ṽ, v̄) · F v). 1.1.3. Remark. The first condition of (LF4) is vacuous for bicategories. 1.1.4. Remark. As much as possible we use a Greek letter corresponding to the name of the functor to represent the laxity cells. 1.1.5. Definition. If F, G : 𝔸 [figure] 𝕏 are lax functors, a natural transformation t : F [figure] G consists of the following data: (NT1) Functions, both denoted t, taking objects A of 𝔸 to horizontal arrows tA : F A [figure] GA

in 𝕏, and taking vertical arrows v of 𝔸 to cells

[figure: F Ā; GĀ; tĀ; F A; F Ā; •; F v; F A; GA; tA; GA; GĀ; •; Gv; tv]

in 𝕏. These are required to satisfy: (NT2) (Horizontal naturality)

[figure: F B; GB; tB; F A; F B; F f; F A; GA; tA; GA; GB; Gf; F w; Gw; tw; F v; F w; F α; F v; Gv; tv; Gv; Gw; Gα; and]

commute for all horizontal arrows f and cells α; (NT3) (Vertical functoriality)

[figure: _{id_{GA}}; G(id_{A}); γA; ^{id^{F A}}; _{id_{GA}}; ^{id^{tA}}; ^{id^{F A}}; F (id_{A}); ϕA; F (id_{A}); G(id_{A}); t(id_{A}); Gv̄ · Gv; G(v̄ · v); γ(v̄,v); F v̄ · F v; Gv̄ · Gv; tv̄·tv; F v̄ · F v; F (v̄ · v); ϕ(v̄,v); F (v̄ · v); G(v̄ · v); t(v̄·v); and]

commute for all objects A and composable pairs of vertical arrows v, v̄.

Natural transformations compose in the obvious way and give a category. They are the horizontal arrows between lax functors and admit as special cases 2-natural transformations, when 𝔸 and 𝕏 are 2-categories (i.e. double categories whose vertical arrows are identities), and (the dual of) ICONs when 𝔸 and 𝕏 are bicategories (i.e. double categories whose horizontal arrows are identities).

Our main concern will be with the vertical morphisms between lax functors. This is more difficult. They were studied in some detail in [15] and in fact in [5] for bicategories before that and for poly-bicategories in [4] even before that. We are referring, of course, to modules, a kind of “multiobject profunctor”.

1.1.6. Definition. Let F, G : 𝔸 [figure] 𝕏 be lax functors. A module m : F [figure: •] G consists of the following data:

(M1) Functions, both denoted m, taking vertical arrows v : A [figure: •] Ā in 𝔸 to vertical arrows mv : F A [figure: •] GĀ, and cells σ : v [figure] w in 𝔸 to cells mσ : F v [figure] Gw;

(M2) (Left and right actions) For every pair of vertical arrows A [figure: •; v] Ā [figure: •; v̄] Ã, special

cells

λ(v̄, v) : Gv̄ · mv ⇒ m(v̄ · v)
ρ(v̄, v) : mv̄ · F v ⇒ m(v̄ · v).

These are required to satisfy:

(M3) (Horizontal functoriality) m(1_{v}) = 1_{m(v)}, m(α′α) = m(α′)m(α);

(M4) (Naturality of λ and ρ)

[figure: Gw̄ · mw; m(w̄ · w); λ(w̄,w); Gv̄ · mv; Gw̄ · mw; Gᾱ·mα; Gv̄ · mv; m(v̄ · v); λ(v̄,v); m(v̄ · v); m(w̄ · w); m(ᾱ·α); and; mw̄ · F w; m(w̄ · w); ρ(w̄,w); mv̄ · F v; mw̄ · F w; mᾱ·F α; mv̄ · F v; m(v̄ · v); ρ(v̄,v); m(v̄ · v); m(w̄ · w); m(ᾱ·α)]

commute.

398  ROBERT PARÉ

(M5) (Unit laws)

[figure: id_{G(Ā)} · m(v); G(idĀ) · m(v); γĀ·m(v); id_{G(Ā)} · m(v); m(idĀ · v); ≅; G(idĀ) · m(v); m(idĀ · v); λ(idĀ,v); and; m(v) · id_{F A}; m(v) · F (id_{A}); m(v)·ϕA; m(v) · id_{F A}; m(v · id_{A}); ≅; m(v) · F (id_{A}); m(v · id_{A}); ρ(v,id_{A})]

commute. (M6) (Associativity)

[figure: G(ṽ · v̄) · mv; m(ṽ · v̄ · v); λ(ṽ·v̄,v); Gṽ · Gv̄ · mv; G(ṽ · v̄) · mv; γ(ṽ,v̄)·mv; Gṽ · Gv̄ · mv; Gṽ · m(v̄ · v); Gṽ·λ(v̄,v); Gṽ · m(v̄ · v); m(ṽ · v̄ · v); λ(ṽ,v̄·v); Gṽ · m(v̄ · v); m(ṽ · v̄ · v); λ(ṽ,v̄·v); Gṽ · mv̄ · F v; Gṽ · m(v̄ · v); Gṽ·ρ(v̄,v); Gṽ · mv̄ · F v; m(ṽ · v̄) · F v; λ(ṽ,v̄)·F v; m(ṽ · v̄) · F v; m(ṽ · v̄ · v); ρ(ṽ·v̄,v)]

[figure: mṽ · F (v̄ · v); m(ṽ · v̄ · v); ρ(ṽ,v̄·v); mṽ · F v̄ · F v; mṽ · F (v̄ · v); mṽ·ϕ(v̄,v); mṽ · F v̄ · F v; m(ṽ · v̄) · F v; ρ(ṽ,v̄)·F v; m(ṽ · v̄) · F v; m(ṽ · v̄ · v); ρ(ṽ·v̄,v); and]

commute. There is also a notion of cell in [5], modulation, which we adapt to our situation.

1.1.7. Definition. Let t : F [figure] F′ and s : G [figure] G′ be natural transformations and m : F [figure: •] G and m′ : F′ [figure: •] G′ be modules. A modulation μ with boundary

[figure: G; G′; s; F; G; •; m; F; F′; t; F′; G′; •; m′]

consists of the following data: (m1) For vertical arrows v : A [figure: •] Ā we are given cells

[figure: GĀ; G′Ā; sĀ; F A; GĀ; •; mv; F A; F′A; tA; F′A; G′Ā; •; m′v; μv]

which are required to satisfy (m2) (Horizontal naturality) For every cell α : v [figure] v′

[figure: mv′; m′v′; μv′; mv; mv′; mα; mv; m′v; μv; m′v; m′v′; m′α]

commutes.

(m3) (Equivariance) For all pairs A [figure: •; v] Ā [figure: •; v̄] Ã

[figure: m(v̄ · v); m′(v̄ · v); μ(v̄·v); Gv̄ · mv; m(v̄ · v); λ(v̄,v); Gv̄ · mv; G′v̄ · m′v; sv̄·μv; G′v̄ · m′v; m′(v̄ · v); λ′(v̄,v); and; m(v̄ · v); m′(v̄ · v); μ(v̄·v); mv̄ · F v; m(v̄ · v); ρ(v̄,v); mv̄ · F v; m′v̄ · F′v; μv̄·tv; m′v̄ · F′v; m′(v̄ · v); ρ′(v̄,v)]

commute.

If 𝔸 and 𝕏 are bicategories (only identity horizontal arrows) then our definition of module is the same as that of [5]. If furthermore s and t are identities, then our definition of modulation is also the same as theirs. Note, however, that even for bicategories there can be non-identity s and t (dual ICONs) so our definition allows for more modulations.

1.2. Virtual Double Categories The problem which is the focus of this paper is the composition of modules. In order to properly formulate it, we must introduce virtual double categories.

These have been variously called T-catégories [2], “fc-multicategories” [13], “multicategories with several objects” [10], “multibicategories” [5] and “lax double categories” [7]. We adopt the name “virtual double category” from [6] to which we refer the reader for more details. There, an elegant and convincing case is made for the importance of this central concept. We simply sketch the relevant parts here.

A virtual double category has objects, horizontal and vertical arrows and multicells whose boundaries look like

[figure: ⋮; B_{1}; ⋮; A_{n}; •; v_{n}; B_{1}; A_{n}; f_{1}; ⋮; B_{1}; A_{1}; ⋮; •; v_{2}; A_{1}; B_{0}; B_{0}; B_{1}; •; w; A_{1}; B_{0}; A_{0}; A_{1}; •; v_{1}; A_{0}; B_{0}; f_{0}; α]

which we will denote as α : v_{n}, v_{n−1}, …, v_{1} [figure] w or, using vector notation, α : v [figure] w. Horizontal arrows form a category but there is no composition of the vertical ones. We have a composition of multicells in the style of functions of several variables. Given a cell

β : w_{m}, …, w_{1} [figure] x

and compatible cells α_{i} : v_{i} [figure] w_{i} we are given

β(α_{m}, …, α_{1}) : v_{m}, v_{m−1}, …, v_{1} [figure] x.

This composite is required to be associative and unitary (i.e. for each v, 1_{v} : v [figure] v is given, and 1_{w}α = α = α(1_{v_{m}}, …, 1_{v_{1}})).

1.2.1. Definition. Let A_{0} [figure: •; v_{1}] A_{1} [figure: •; v_{2}] ⋯ [figure: •; v_{n}] A_{n} be a path of vertical arrows in a virtual double category 𝔸. We say it has a strongly representable composite if there is an arrow v : A_{0} [figure: •] A_{n} and a special multicell

ι : v_{n}, v_{n−1}, …, v_{1} ⇒ v

such that for all compatible paths x, y and multicells

α : x, v, y [figure] z

there is a unique multicell ᾱ : x, v, y [figure] z such that

[figure: x, v, y; x, v, y; 1_{x},ι,1_{y}; x, v, y; z; α; x, v, y; z; ᾱ]

1.2.2. Remark. Mere representability, where the universal property is only required for empty x and y, is of course enough to determine the composite up to special isomorphism, but strong representability is needed to get associativity of the composite. If v has a composite we use [v] to denote a chosen one.

Thus in order to properly state the problem of the composition of modules it will be sufficient to define a virtual double category structure on 𝕃ax(𝔸, 𝕏). We gave a definition of multimodulation in [15] which we reproduce here. Our definition was an adaptation of the multimodulations of [5].

1.2.3. Definition. Let F_{0}, F_{1}, …, F_{n}, G_{0}, G_{1} be lax functors 𝔸 [figure] 𝕏, m_{1} : F_{0} [figure: •] F_{1}, m_{2} : F_{1} [figure: •] F_{2}, …, m_{n} : F_{n−1} [figure: •] F_{n}, p : G_{0} [figure: •] G_{1} modules, and t : F_{0} [figure] G_{0}, s : F_{n} [figure] G_{1} natural transformations. A multimodulation

μ : m [figure] p

[figure: ⋮; G_{1}; ⋮; F_{n}; •; m_{n}; G_{1}; F_{n}; s; ⋮; G_{1}; F_{1}; ⋮; •; m_{2}; F_{1}; G_{0}; G_{0}; G_{1}; •; p; F_{1}; G_{0}; F_{0}; F_{1}; •; m_{1}; F_{0}; G_{0}; t; μ]

consists of the following data: (mm1) For every path A_{0} [figure: •; v_{1}] A_{1} [figure: •; v_{2}] … [figure: •; v_{n}] A_{n} a cell

μ(v_{n}, …, v_{1}) : m_{n}v_{n} · m_{n−1}v_{n−1} · . . . · m_{1}v_{1} [figure] p(v_{n} · . . . · v_{1}), μ(v) : [mv] [figure] p[v] These must satisfy the following conditions:

(mm2) (Horizontal naturality) For any n-path of cells α : v [figure] v′,

[figure: p[v]; p[v′]; p[α]; [mv]; p[v]; μ(v); [mv]; [mv′]; [mα]; [mv′]; p[v′]; μ(v′)]

commutes. (mm3) (Inner equivariance) For any path of length n + 1

y_{n}, …, y_{i+1}, v, x_{i}, …, x_{1} (0 < i < n)

y, v, x

we have that

[figure: [m(y · v)] · [mx]; p[y, vx]; μ(y·v,x); [my] · F_{i}v · [mx]; [m(y · v)] · [mx]; 1·ρ_{i+1}·1; [my] · F_{i}v · [mx]; [my] · [m(v · x)]; 1·λ_{i}·1; [my] · [m(v · x)]; p[y, vx]; μ(y,v·x)]

commutes.

(mm3_{l}) (Left equivariance)

[figure: G_{1}v · p[x]; p[v, x]; λ_{p}·1; F_{n}v · [mx]; G_{1}v · p[x]; sv·μ(x); F_{n}v · [mx]; [m(v · x)]; λ_{n}·1; [m(v · x)]; p[v, x]; μ(v·x)]

commutes.

(mm3_{r}) (Right equivariance)

[figure: p[y] · G_{o}v; p[y, v]; ρ_{p}; [my] · F_{o}v; p[y] · G_{o}v; μ(y)·tv; [my] · F_{o}v; [m(y · v)]; 1·ρ_{0}; [m(y · v)]; p[y, v]; μ(y·v)]

commutes.

1.2.4. Notation. In this definition, we have introduced some notational conventions, without which the formulas would quickly become incomprehensible. We set them down here for clarity.

As mentioned before the definition, we use vector notation for paths

v = (v_{n}, …, v_{1}) = A_{0} [figure: •; v_{1}] A_{1} [figure: •; v_{2}] … [figure: •; v_{n}] A_{n}

and square brackets for a chosen composite

[v] = v_{n} · v_{n−1} · . . . · v_{1} = ((v_{n} · v_{n−1}) · . . .) · v_{1}.

If m = (m_{n}, …, m_{1}) : F_{0} [figure: •; m_{1}] F_{1} [figure: •; m_{2}] … [figure: •; m_{n}] F_{n} is a path of modules, then

mv = m(v) = F_{0}A_{0} [figure: •; m_{1}v_{1}] F_{1}A_{1} [figure: •; m_{2}v_{2}] … [figure: •; m_{n}v_{n}] F_{n}A_{n}

is the path obtained by evaluating m at the corresponding v. When the paths are not of the same length we evaluate at the corresponding ones that make sense, so

my = F_{i}A_{i} [figure: •; m_{i+1}y_{i+1}] F_{i+1}A_{i+1} [figure: •; m_{i+2}y_{i+2}] … [figure: •; m_{n}y_{n}] F_{n}A_{n}.

The following is now easily proved.

1.2.5. Theorem. Equipped with multimodulations, 𝕃ax(𝔸, 𝕏) is a virtual double category.

With this result, the question of whether the composite of modules exists is well-posed. Just by considering V-profunctors, we see that certain cocompleteness conditions on 𝕏 will be required. Under such hypotheses, [5] give a simple formula for the composite of two modules in the bicategory case. For m_{1} : F [figure: •] G and m_{2} : G [figure: •] H modules, and v : A [figure: •] Ā they define m(v) as the coequalizer

∑_{J} m_{2}(v_{3}) · G(v_{2}) · m_{1}(v_{1}) [figure]∑_{I} m_{2}(v_{2}) · m_{1}(v_{1}) [figure] m(v)

in the hom category 𝕏[F A, HĀ] whose objects are vertical arrows x : F A [figure: •] HĀ and whose morphisms are (special) cells. I is the set of “lax factorizations” of v

[figure: Ā; Ā; A_{1}; Ā; •; v_{2}; A_{1}; Ā; A_{1}; A; A_{1}; •; v_{1}; A; A; A; Ā; Ā; A; Ā; A; A; A; Ā; •; v; α]

and J is the set of quadruples (α_{1}, α_{2}, β_{1}, β_{2}) such that

[figure: Ā; Ā; A_{2}; Ā; •; v_{3}; A_{2}; A_{2}; A_{2}; Ā; •; v_{3}; A_{2}; A_{2}; A_{1}; A_{2}; •; v_{2}; A_{1}; A_{2}; A_{1}; A; A_{1}; •; v_{1}; A; A; A; A_{2}; A_{2}; A; A_{2}; A; A; A; A_{2}; •; v′_{1}; β_{1}; 1_{v_{3}}; Ā; Ā; A_{2}; Ā; A_{2}; Ā; A_{2}; A; A_{2}; A; A; A; Ā; Ā; A; Ā; A; A; A; Ā; •; v; α_{1}; =; Ā; Ā; A_{2}; Ā; •; v_{3}; A_{2}; Ā; A_{2}; A_{1}; A_{2}; •; v_{2}; A_{1}; A_{1}; A_{1}; Ā; Ā; A_{1}; Ā; A_{1}; A_{1}; A_{1}; Ā; •; v′_{2}; A_{1}; A_{1}; A; A_{1}; •; v_{1}; A; A; A; A_{1}; •; v_{1}; Ā; Ā; A; Ā; A; A; A; Ā; •; v; 1_{v_{1}}; β_{2}; α_{2}]

This is a nice intuitive formula but it has several drawbacks. The main one for us is that it doesn’t work for double categories. The m, thus defined, is not horizontally functorial. If

[figure: Ā; B̄; f̄; A; Ā; •; v; A; B; f; B; B̄; •; w; σ]

is an arbitrary cell, there is no way of defining m(σ). To solve this, it is tempting to enlarge I to all diagrams

[figure: A_{2}; Ā; A_{1}; A_{2}; •; v_{2}; A_{1}; Ā; A_{1}; A_{0}; A_{1}; •; v_{1}; A_{0}; A; A; A_{2}; Ā; f̄; A_{0}; A_{2}; A_{0}; A; f; A; Ā; •; v; α]

But now the arrows m_{2}(v_{2}) · m_{1}(v_{1}) do not all lie in the same hom category. One could require some stronger cocompleteness properties of 𝕏 or, more or less equivalently, that all horizontal arrows of 𝕏 have companions and conjoints. But this doesn’t work either. There is no obvious way of defining left and right actions for m. These problems will be solved in the next two sections.

2. The Construction

2.1. Local Colimits It is clear from the examples, V-profunctors e.g., that we will need some cocompleteness for 𝕏. For objects X, Y in 𝕏 we let 𝕏[X, Y] denote the “vertical hom category”. Its objects are vertical arrows x : X [figure: •] Y, and its morphisms ξ : x ⇒ x′, are special cells

[figure: Y; Y; X; Y; •; x; X; X; X; Y; •; x′; ξ]

2.1.1. Definition. We say that 𝕏 has local I colimits if

(LC1) Each category 𝕏[X, Y] has I colimits;

(LC2) For every w : W [figure: •] X and y : Y [figure: •] Z the functor 𝕏[w, y] : 𝕏[X, Y] [figure] 𝕏[W, Z] which takes x to y · x · w preserves I colimits;

(LC3) The I colimits have a further universal property. Let Γ : I [figure] 𝕏[X, Y] be an I diagram. Given f : X [figure] X′ and g : Y [figure] Y′ horizontal morphisms, x′ : X′ [figure: •] Y′ a vertical morphism of 𝕏 and a cocone of cells

[figure: Y; Y′; g; X; Y; •; ΓI; X; X′; f; X′; Y′; •; x′; ξ(I)]

then there exists a unique cell

[figure: Y; Y′; s; X; Y; •; ⟶^{lim}Γ; X; X′; f; X′; Y′; •; x′; ξ]

such that ξγ(I) = ξ(I) (γ(I) is the Ith colimit injection).

2.1.2. Remarks. (1) (LC3) is not saying that \underrightarrow{lim}Γ is a colimit in the category X_{1}, of all vertical arrows and all cells, because the f and g are fixed. If I is connected however, the two concepts agree.

(2) If in 𝕏, horizontal arrows have companions and conjoints, then (LC3) is automatic because a cell

[figure: Y; Y′; g; X; Y; x; X; X′; f; X′; Y′; x′; ξ]

is equivalent to a special cell

[figure: Y; Y; Y; Y′; Y′; Y; •; g^{∗}; Y′; X′; X′; Y′; •; x′; X′; X; X; X; X; X′; •; f_{∗}; Y; Y; X; Y; •; x; X; X; X; Y; ξ̄]

(3) (LC3) is less mysterious in the context of category theory over a base B. The 2category CAT /B is cotensored over Cat. Given an object P : X [figure] B and a small category I then

X^{(I)} [figure: P^{(I)}] B

is the pullback

[figure: B; B^{I}; Δ; X^{(I)}; B; P^{(I)}; X^{(I)}; X^{(I)}; X^{(I)}; B^{I}; P^{I}]

So an object of X^{(I)} is a pair (B, Γ : I [figure] X_{B}) and a morphism (b, t) : (B, Γ) [figure] (B′, Γ′) is a morphism b : B [figure] B′ and a natural transformation over b, t : Γ [figure] Γ′, i.e. a natural family

tI : ΓI [figure] Γ′I s.t. P (tI) = b.

There is an obvious diagonal functor

[figure: X; B; X; X^{(I)}; Δ; X^{(I)}; B]

If Δ has a left adjoint over B (i.e. in CAT /B) it gives I colimits in the fibres X_{B} but with a further universal property with respect to cocones over b : B [figure] B′.

Then 𝕏 has local I colimits if

[figure: X_{0} × X_{0}; X_{1}; X_{0} × X_{0}; (δ_{0},δ_{1}); X_{1}]

has I colimits (in CAT /X_{0} × X_{0}) and composition X_{1} ×_{X_{0}} X_{1} [figure: •] X_{1} distributes over them.

Many large double categories are locally cocomplete. For example 𝕊et and ℂat are, and V-𝕊et is, provided V has colimits and ⊗ distributes over them (e.g. if V is closed).

2.2. The Construction Let F, G, H : 𝔸 [figure] 𝕏 be lax functors with 𝔸 small and 𝕏 locally cocomplete. Let m : F [figure: •] G and n : G [figure: •] H be modules which we wish to compose. Our colimit formula is a reworking of the coequalizer formula of [5], adapted to the double category context. We will discuss how the two are related in §5.2.

Given v : A [figure: •] Ā we define a diagram Γ_{v} : I_{v} [figure] 𝕏[F A, HĀ] as follows. I_{v} is a bipartite category with two kinds of objects: lax factorizations of v

[figure: Ā; Ā; B; Ā; •; v_{2}; B; Ā; B; A; B; •; v_{1}; A; A; A; Ā; Ā; A; Ā; A; A; A; Ā; •; v; β]

and triple lax factorizations of v

[figure: Ā; Ā; C_{2}; Ā; •; w_{3}; C_{2}; Ā; C_{2}; C_{1}; C_{2}; •; w_{2}; C_{1}; C_{1}; A; C_{1}; •; w_{1}; A; A; A; Ā; Ā; A; Ā; A; A; A; Ā; •; v; γ]

The (non-identity) morphisms go from triple lax factorizations, γ, to double ones β, and there are two kinds of these:

(i) for each horizontal morphism C_{2} [figure] B and cells ϕ_{1}, ϕ_{2} for which β(ϕ_{2} · ϕ_{1}) = γ as in

[figure: Ā; Ā; C_{2}; Ā; •; w_{3}; C_{2}; B; B; Ā; •; v_{2}; C_{2}; B; C_{1}; C_{2}; •; w_{2}; C_{1}; B; C_{1}; A; C_{1}; •; w_{1}; A; A; A; C_{2}; B; A; C_{2}; A; A; A; B; •; v_{1}; ϕ_{1}; ϕ_{2}; Ā; Ā; B; Ā; B; Ā; B; A; B; A; A; A; Ā; Ā; A; Ā; A; A; A; Ā; •; v; β; =; Ā; Ā; C_{2}; Ā; •; w_{3}; C_{2}; Ā; C_{2}; C_{1}; C_{2}; •; w_{2}; C_{1}; C_{1}; A; C_{1}; •; w_{1}; A; A; A; Ā; Ā; A; Ā; A; A; A; Ā; •; v; γ]

we give a morphism

l_{ϕ_{2}ϕ_{1}} : (γ) [figure] (β)

and (ii) for each horizontal arrow C_{1} [figure] B and cells ψ_{1}, ψ_{2} for which β(ψ_{2} · ψ_{1}) = γ as in

[figure: Ā; Ā; C_{2}; Ā; •; w_{2}; C_{2}; Ā; C_{2}; C_{1}; C_{2}; •; w_{2}; C_{1}; B; B; C_{1}; B; A; C_{1}; •; w_{1}; A; A; A; B; •; v_{1}; Ā; Ā; C_{1}; Ā; C_{1}; B; B; Ā; •; v_{2}; ψ_{2}; ψ_{1}; Ā; Ā; A; Ā; A; A; A; Ā; •; v; β; =; Ā; Ā; C_{2}; Ā; •; w_{3}; C_{2}; Ā; C_{2}; C_{1}; C_{2}; •; w_{2}; C_{1}; C_{1}; A; C_{1}; •; w_{1}; A; A; A; Ā; Ā; A; Ā; A; A; A; Ā; •; v; γ]

we give a morphism

r_{ψ_{2}ψ_{1}} : (γ) [figure] (β).

There are no non-trivial composites.

Γ_{v} : I [figure] 𝕏[F A, HĀ] is defined by

Γ_{v}(β) = nv_{2} · mv_{1}
Γ_{v}(γ) = nw_{3} · Gw_{2} · mw_{1}

Γ_{v}(l_{ϕ_{2}ϕ_{1}}) = nw_{3} · Gw_{2} · mw_{1} [figure: •; nw_{3}·λ] nw_{3} · m(w_{2} · w_{1}) [figure: •; nϕ_{2}·mϕ_{1}] nv_{2} · mv_{1}

Γ_{v}(r_{ψ_{2}ψ_{1}}) = nw_{3} · Gw_{2} · mw_{1} [figure: •; ρ·mw_{1}] n(w_{3} · w_{2}) · mw_{1} [figure: •; nψ_{2}·mψ_{1}] nv_{2} · mv_{1}.

In this, λ is the left action of G on m and ρ the right action of G on n.

2.2.1. Proposition. Giving a cocone κ for Γ_{v} is equivalent to giving a family of cells

κ(β) : nv_{2} · mv_{1} [figure] x

indexed by lax factorizations β of v, satisfying

(a) (transfer of scalars) for every triple lax factorization γ as above,

[figure: nw_{3} · Gw_{2} · mw_{1}; nw_{3} · m(w_{2} · w_{1}); nw_{3}·λ; n(w_{3} · w_{2}) · mw_{1}; nw_{3} · Gw_{2} · mw_{1}; ρ·mw_{1}; n(w_{3} · w_{2}) · mw_{1}; nw_{3} · m(w_{2} · w_{1}); x; nw_{3} · m(w_{2} · w_{1}); κ(γ); n(w_{3} · w_{2}) · mw_{1}; x; κ(γ); n(w_{3} · w_{2}) · mw_{1}; nw_{3} · m(w_{2} · w_{1})]

commutes,

(b) (naturality) for any two lax factorizations β and β′ related by

[figure: Ā; Ā; B; Ā; v_{2}; B; B′; B′; Ā; v′_{2}; B; B′; A; B; v_{1}; A; A; A; B′; v′_{1}; θ_{1}; θ_{2}]

β′(θ_{2} · θ_{1}) = β,

[figure: x; nv′_{2} · mv′_{1}; κ(β′); nv_{2} · mv_{1}; x; κ(β); nv_{2} · mv_{1}; nv′_{2} · mv′_{1}; nθ_{2}·mθ_{1}]

commutes.

Proof. First, let κ : Γ_{v} [figure] x be a cocone. Note that both arrows denoted by κ(γ) in (a) are different as is clear from their domains. A more precise notation would be κ(w_{3} · w_{2}, w_{1}, γ) and κ(w_{3}, w_{2} · w_{1}, γ). Then each of the composites in the transfer of scalars diagram is equal to

κ(w_{3}, w_{2}, w_{1}, γ) : nw_{3} · Gw_{2} · mw_{1} [figure] x

by the cocone property for the morphisms r_{1_{w_{3}·w_{2}},1_{w_{1}}} and l_{1_{w_{3}},1_{w_{2}·w_{1}}}.

For naturality, let β, β′, θ_{1}, θ_{2} be as in (b). Consider the triple lax factorization of v

[figure: Ā; Ā; B; Ā; •; v_{2}; B; Ā; B; B; B; •; ^{id^{B}}; B; B; A; B; •; v_{1}; A; A; A; Ā; Ā; A; Ā; A; A; A; Ā; •; v; β̄]

where β̄ is β composed with the canonical isomorphism v_{2} · id_{B} · v_{1} [figure: ≅] v_{2} · v_{1}. We have morphisms in I_{v}

l_{1_{v_{2}}, ¯ 1_{v_{1}}} : (β̄) [figure] (β)
r_{θ̄_{2},θ_{1}} : (β̄) [figure] (β′)

which give a commutative diagram

[figure: nv_{2} · Gid_{B} · mv_{1}; n(v_{2} · id_{B}) · mv_{1}; ρ·mv_{1}; nv_{2} · m(id_{B} · v_{1}); nv_{2} · Gid_{B} · mv_{1}; nv_{2}·λ; nv_{2} · m(id_{B} · v_{1}); n(v_{2} · id_{B}) · mv_{1}; n(v_{2} · id_{B}) · mv_{1}; nv′_{2} · mv′_{1}; n(θ̄_{2})·m(θ_{1}); nv_{2} · m(id_{B} · v_{1}); n(v_{2} · id_{B}) · mv_{1}; nv_{2} · m(id_{B} · v_{1}); nv_{2} · mv_{1}; n1_{v_{2}}·m(𝔩_{v_{1}}); nv_{2} · mv_{1}; nv′_{2} · mv′_{1}; x; nv′_{2} · mv′_{1}; κ(β′); nv_{2} · mv_{1}; x; κ(β); nv_{2} · mv_{1}; nv′_{2} · mv′_{1}; nv_{2} · Gid_{B} · mv_{1}; x; κ(β̄)]

Precede this by the canonical

nv_{2} · mv_{1} [figure: ≅] nv_{2} · id_{GB} · mv_{1} [figure: nv_{2}·γ_{B}·mv_{1}] nv_{2} · Gid_{B} · mv_{1}

and the top path will be equal to κ(β) whereas the bottom will be κ(β′)(nθ_{2} · mθ_{1}).

Conversely, let ⟨κ(β) : nv_{2} ·mv_{1} [figure] x⟩ be a family of cells satisfying (a) and (b). Given a triple lax factorization (γ) as above, define

κ(γ) : nw_{3} · Gw_{2} · mw_{1} [figure] x

to be the common composite given by (a). Then for a morphism l_{ϕ_{2},ϕ_{1}} : (γ) [figure] (β) in I_{v} we have κ(β)Γ_{v}(l_{ϕ_{2},ϕ_{1}}) as the top composite in

[figure: nw_{3} · Gw_{2} · mw_{1}; nw_{3} · Gw_{2} · mw_{1}; x; κ(γ); x; nw_{3} · m(w_{2} · w_{1}); x; nw_{3} · m(w_{2} · w_{1}); nv_{2} · mv_{1}; nϕ_{2}·mϕ_{1}; nv_{2} · mv_{1}; x; κ(β); nw_{3} · Gw_{2} · mw_{1}; nw_{3} · m(w_{2} · w_{1}); nw_{3}·λ; (b); def; κ(γ)]

which is the cocone property for l_{ϕ_{2},ϕ_{1}}. The one for r_{ψ_{2},ψ_{1}} is similar.

Actually we need a stronger form of this proposition; we need it not just for cocones on Γ_{v} but on ΦΓ_{v}, where Φ : 𝕏[F A, HĀ] [figure] X is an arbitrary functor. In the applications that follow, X will be one of the vertical homs of 𝕏, 𝕏[X_{1}, X_{2}], and Φ will come from vertical composition.

2.2.2. Proposition. Giving a cocone κ : ΦΓ_{v} [figure] x is equivalent to giving a family

κ(β) : Φ(nv_{1} · mv_{2}) [figure] x

indexed by lax factorizations β of v, satisfying:

(a) (transfer of scalars)

[figure: Φ(nw_{3} · Gw_{2} · mw_{1}); Φ(nw_{3} · m(w_{2} · w_{1})); Φ(nw_{3}·λ); Φ(n(w_{3} · w_{2}) · mw_{1}); Φ(nw_{3} · Gw_{2} · mw_{1}); Φ(ρ·mw_{1}); Φ(n(w_{3} · w_{2}) · mw_{1}); Φ(nw_{3} · m(w_{2} · w_{1})); x; Φ(nw_{3} · m(w_{2} · w_{1})); κ(γ); Φ(n(w_{3} · w_{2}) · mw_{1}); x; κ(γ); Φ(n(w_{3} · w_{2}) · mw_{1}); Φ(nw_{3} · m(w_{2} · w_{1}))]

commutes,

(b) (naturality)

[figure: x; Φ(nv′_{2} · mv′_{1}); κ(β′); Φ(nv_{2} · mv_{1}); x; κ(β); Φ(nv_{2} · mv_{1}); Φ(nv′_{2} · mv′_{1}); Φ(nθ_{2}·mθ_{1})]

commutes.

Proof. Put a Φ before all objects and arrows in 𝕏[F A, HĀ] in the previous proof, except x and the κ’s.

2.2.3. Definition. (n · m)(v) = \underrightarrow{lim}Γ_{v}.

Let j_{β} : n(v_{2}) · m(v_{1}) [figure] (n · m)(v) denote the colimit injection corresponding to the lax factorization (β) of v. Note that the family ⟨j_{β}⟩ is jointly epic. This is also true for the families ⟨y · j_{β}⟩, ⟨j_{β} · z⟩, ⟨y · j_{β} · z⟩ as composition with vertical arrows preserves colimits. This fact will be used repeatedly below.

2.3. The Actions Given A′ [figure: •; v′] A [figure: •; v] Ā [figure: •; v̄] Ã we wish to define the actions λ_{n·m}(v̄, v) and ρ_{n·m}(v, v′).

2.3.1. Proposition. There are unique cells λ_{n·m}(v̄, v) and ρ_{n·m}(v, v′) satisfying:

[figure: Hv̄ · nv_{2} · mv_{1}; n(v̄ · v_{2}) · mv_{1}; λ_{n}(v̄,v_{2})·mv_{1}; Hv̄ · (n · m)(v); Hv̄ · nv_{2} · mv_{1}; Hv̄·j_{β}; Hv̄ · (n · m)(v); (n · m)(v̄ · v); λ_{n·m}(v̄,v); (n · m)(v̄ · v); n(v̄ · v_{2}) · mv_{1}; j_{v̄·β}]

and

[figure: nv_{2} · mv_{1} · F v′; nv_{2} · m(v_{1} · v′); nv_{2}·ρ_{m}(v_{1}·v′); (n · m)(v) · F v′; nv_{2} · mv_{1} · F v′; j_{β}·F v′; (n · m)(v) · F v′; (n · m)(v · v′); ρ_{n·m}(v,v′); (n · m)(v · v′); nv_{2} · m(v_{1} · v′); j_{β·v′}]

commute for every lax factorization of v

[figure: Ā; Ā; A_{1}; Ā; v_{2}; A_{1}; Ā; A_{1}; A; A_{1}; v_{1}; A; A; A; Ā; Ā; A; Ā; A; A; A; Ā; v; β]

Proof. We will only discuss the left action, the right one being similar. Hv̄·( ) preserves colimits so Hv̄ · (n · m)(v) is \underrightarrow{lim}Hv̄ · Γ_{v} and Hv̄ · j_{β} are colimit injections. So we must show that ⟨j_{v̄·β}(λ_{n}(v̄, v_{2}) · mv_{1})⟩_{β} determines a cocone. By proposition 2.2.2 it is sufficient to check conditions (a) and (b).

Let (γ) = (w_{3}, w_{2}, w_{1}, γ) be a triple lax factorization of v. Condition (a) is commutativity of the outside of the diagram

[figure: Hv̄ · nw_{3} · Gw_{2} · mw_{1}; Hv̄ · nw_{3} · m(w_{2} · w_{1}); H(v̄)·nw_{3}·λ_{m}; Hv̄ · n(w_{3} · w_{2}) · mw_{1}; Hv̄ · nw_{3} · Gw_{2} · mw_{1}; Hv̄·ρ_{n}·mw_{1}; Hv̄ · n(w_{3} · w_{2}) · mw_{1}; Hv̄ · nw_{3} · m(w_{2} · w_{1}); n(v̄ · w_{3}) · Gw_{2} · mw_{1}; n(v̄ · w_{3}) · m(w_{2} · w_{1}); n(v̄·w_{3})·λ_{m}; n(v̄ · w_{3} · w_{2}) · mw_{1}; n(v̄ · w_{3}) · Gw_{2} · mw_{1}; ρ_{n}·mw_{1}; n(v̄ · w_{3} · w_{2}) · mw_{1}; n(v̄ · w_{3}) · m(w_{2} · w_{1}); Hv̄ · nw_{3} · Gw_{2} · mw_{1}; n(v̄ · w_{3}) · Gw_{2} · mw_{1}; λ_{n}·Gw_{2}·mw_{1}; Hv̄ · n(w_{3} · w_{2}) · mw_{1}; n(v̄ · w_{3} · w_{2}) · mw_{1}; λ_{n}·mw_{1}; (n · m)(v̄ · v); n(v̄ · w_{3}) · m(w_{2} · w_{1}); j_{v̄·γ}; n(v̄ · w_{3} · w_{2}) · mw_{1}; (n · m)(v̄ · v); j_{v̄·γ}; n(v̄ · w_{3} · w_{2}) · mw_{1}; n(v̄ · w_{3}) · m(w_{2} · w_{1}); Hv̄ · nw_{3} · m(w_{2} · w_{1}); n(v̄ · w_{3}) · m(w_{2} · w_{1}); λ_{n}·m(w_{2}·w_{1}); (2); (1); (3)]

Mixed associativity for n gives commutativity of (1), functoriality of vertical composition gives (2), and (3) is condition (a) for the lax factorization v̄ · γ = (v̄ · w_{3}, w_{2}, w_{1}, v̄ · γ) of v̄ · v.

Let β = β′(θ_{2} · θ_{1}) as in condition (b). We have to show that the outside of the following diagram commutes.

[figure: Hv̄ · nv′_{2} · mv′_{1}; n(v̄ · v′_{2}) · mv′_{1}; λ_{n}·mv′_{1}; Hv̄ · nv_{2} · mv_{1}; Hv̄ · nv′_{2} · mv′_{1}; Hv̄·nθ_{2}·mθ_{1}; Hv̄ · nv_{2} · mv_{1}; n(v̄ · v_{2}) · mv_{1}; λ_{n}·mv_{1}; n(v̄ · v_{2}) · mv_{1}; n(v̄ · v′_{2}) · mv′_{1}; (n · m)(v̄ · v); n(v̄ · v′_{2}) · mv′_{1}; j_{v̄·β′}; n(v̄ · v_{2}) · mv_{1}; (n · m)(v̄ · v); j_{v̄·β}; n(v̄ · v_{2}) · mv_{1}; n(v̄ · v′_{2}) · mv′_{1}; n(v̄·θ_{2})·mθ_{1}; (1); (2)]

Naturality of λ_{n} gives (1), and (2) is condition (b) for v̄ · v.

3. A Factorization Property

It remains to define n · m on cells.

In order to do this, we need an extra condition on 𝔸, a factorization of cells which holds vacuously for bicategories. This is where the theory for double categories diverges from that of [5]. Double cells or multicells, being two dimensional, can be factored in a variety of ways of which the one given below is but one. We envision many other such factorizations. It is the isolation of this property that we consider the main contribution of this work.

3.1. The Condition AFP 3.1.1. Definition. We say that 𝔸 satisfies AFP if every cell of the form

[figure: A_{2}; B_{2}; g; A_{1}; A_{2}; •; v_{2}; A_{1}; B_{2}; A_{1}; A_{0}; A_{1}; •; v_{1}; A_{0}; B_{0}; f; B_{0}; A_{2}; B_{2}; g; A_{0}; A_{2}; A_{0}; B_{0}; f; B_{0}; B_{2}; •; w; α]

factors as

[figure: A_{2}; B_{2}; g; A_{1}; A_{2}; •; v_{2}; A_{1}; B_{1}; B_{1}; B_{2}; •; w_{2}; A_{1}; B_{1}; A_{0}; A_{1}; •; v_{1}; A_{0}; B_{0}; f; B_{0}; B_{1}; •; w_{1}; α_{2}; α_{1}; B_{2}; B_{2}; B_{0}; B_{2}; B_{0}; B_{0}; B_{0}; B_{2}; •; w; α_{3}]

α = α_{3}(α_{2} · α_{1}), and any two such factorizations are equivalent under the equivalence relation generated by identifying two factorizations

[figure: A_{2}; B_{2}; g; A_{1}; A_{2}; •; v_{2}; A_{1}; C; C; B_{2}; •; u_{2}; A_{1}; C; A_{0}; A_{1}; •; v_{1}; A_{0}; B_{0}; f; B_{0}; C; •; u_{1}; γ_{2}; γ_{1}; B_{2}; B_{2}; B_{0}; B_{2}; B_{0}; B_{0}; B_{0}; B_{2}; •; w; γ_{3}; =; A_{2}; B_{2}; g; A_{1}; A_{2}; •; v_{2}; A_{1}; D; D; B_{2}; •; x_{2}; A_{1}; D; A_{0}; A_{1}; •; v_{1}; A_{0}; B_{0}; f; B_{0}; D; •; x_{1}; δ_{2}; δ_{1}; B_{2}; B_{2}; B_{0}; B_{2}; B_{0}; B_{0}; B_{0}; B_{2}; •; w; δ_{3}]

if there is either

(1) a horizontal reduction (γ_{1}, γ_{2}, γ_{3}) [figure: (ϕ_{1}ϕ_{2})] (δ_{1}, δ_{2}, δ_{3}): there exist

[figure: B_{2}; B_{2}; C; B_{2}; •; u_{2}; C; D; D; B_{2}; •; x_{2}; C; D; B_{0}; C; •; u_{1}; B_{0}; B_{0}; B_{0}; D; •; x_{1}; ϕ_{2}; ϕ_{1}]

such that

(a) ϕ_{1}γ_{1} = δ_{1} (b) ϕ_{2}γ_{2} = δ_{2}

(c) δ_{3}(ϕ_{2} · ϕ_{1}) = γ_{3} or

(2) a vertical reduction (γ_{1}, γ_{2}, γ_{3}) [figure: (y,θ)] (δ_{1}, δ_{2}, δ_{3}): there exists

[figure: A_{1}; D; C; A_{1}; C; D; •; y; θ]

such that

(a) θ · γ_{1} = δ_{1},

(b) δ_{2} · θ = γ_{2},

(c) γ_{3} = δ_{3}.

3.1.2. Note. The intent of the conditions in (2) is clear but because we are working with weak double categories we can’t help certain canonical isomorphisms creeping in. More specifically, we need to require special isomorphisms ξ_{1} : y · u_{1} ⇒ x and ξ_{2} : x_{2} · y ⇒ u_{2} such that (a)

[figure: A_{1}; D; A_{1}; A_{1}; •; id; A_{1}; C; C; D; •; y; A_{1}; C; A_{0}; A_{1}; •; v_{1}; A_{0}; B_{0}; B_{0}; C; •; u_{1}; θ; γ_{1}; D; D; B_{0}; D; B_{0}; B_{0}; B_{0}; D; •; x_{1}; ξ_{1}; =; A_{1}; A_{1}; A_{1}; A_{1}; •; id; A_{1}; A_{1}; A_{1}; A_{0}; A_{1}; •; v_{1}; A_{0}; A_{0}; A_{0}; A_{1}; A_{1}; A_{0}; A_{1}; A_{0}; A_{0}; A_{0}; A_{1}; •; v_{1}; A_{1}; D; A_{0}; A_{1}; A_{0}; B_{0}; B_{0}; D; •; x_{1}; 𝔩_{A_{1}}; δ_{1}]

(b)

[figure: A_{2}; B_{2}; A_{1}; A_{2}; •; v_{2}; A_{1}; D; D; B_{2}; •; x_{2}; A_{1}; D; A_{1}; A_{1}; •; id; A_{1}; C; C; D; •; y; B_{2}; B_{2}; C; B_{2}; C; C_{0}; C_{0}; B_{2}; •; u_{2}; δ_{2}; θ; ξ_{2}; =; A_{2}; A_{2}; A_{1}; A_{2}; •; v_{2}; A_{1}; A_{2}; A_{1}; A_{1}; A_{1}; •; id; A_{1}; A_{1}; A_{1}; A_{2}; A_{2}; A_{1}; A_{2}; A_{1}; A_{1}; A_{1}; A_{2}; •; v_{2}; A_{2}; B_{2}; A_{1}; A_{2}; A_{1}; C; C; B_{2}; •; u_{2}; 𝔯_{A_{1}}; γ_{2}]

[figure: B_{2}; B_{2}; D; B_{2}; •; x_{2}; D; B_{2}; D; C; D; •; y; C; C; C; B_{2}; B_{2}; C; B_{2}; C; C; C; B_{2}; •; u_{2}; C; C; B_{0}; C; •; u_{1}; B_{0}; B_{0}; B_{0}; C; •; u_{1}; B_{2}; B_{2}; B_{0}; B_{2}; B_{0}; B_{0}; B_{0}; B_{2}; •; w; ξ_{2}; 1; γ_{3}; =; B_{2}; B_{2}; D; B_{2}; •; x_{2}; D; D; D; B_{2}; •; x_{2}; D; D; C; D; •; y; C; D; C; B_{0}; C; •; u_{1}; B_{0}; B_{0}; B_{0}; D; D; B_{0}; D; B_{0}; B_{0}; B_{0}; D; •; x_{1}; B_{2}; B_{2}; B_{0}; B_{2}; B_{0}; B_{0}; B_{0}; B_{2}; •; w; 1; ξ_{1}; δ_{2}]

3.1.3. Examples. Bicategories, considered as vertical double categories, satisfy AFP, but more can be said.

3.1.4. Proposition. If every horizontal arrow of 𝔸 admits a companion and a conjoint, then 𝔸 satisfies AFP.

Proof. Any cell

[figure: A_{2}; B_{2}; g; A_{1}; A_{2}; •; v_{2}; A_{1}; B_{2}; A_{1}; A_{0}; A_{1}; •; v_{1}; A_{0}; B_{0}; f; B_{0}; A_{2}; B_{2}; g; A_{0}; A_{2}; A_{0}; B_{0}; f; B_{0}; B_{2}; •; w; α]

factors as

[figure: A_{2}; B_{2}; g; A_{1}; A_{2}; •; v_{2}; A_{1}; A_{1}; A_{1}; B_{2}; •; g_{∗}·v_{2}; A_{1}; A_{1}; A_{0}; A_{1}; •; v_{1}; A_{0}; B_{0}; f; B_{0}; A_{1}; •; v_{1}·f^{∗}; α_{2}; α_{1}; B_{2}; B_{2}; B_{0}; B_{2}; B_{0}; B_{0}; B_{0}; B_{2}; •; w; α_{3}]

where α_{1}, α_{2} and α_{3} are respectively

[figure: A_{1}; A_{1}; A_{0}; A_{1}; •; v_{1}; A_{0}; A_{0}; A_{0}; A_{1}; A_{1}; A_{‘}; A_{0}; A_{1}; •; v_{1}; A_{0}; A_{0}; A_{0}; A_{‘}; •; v_{1}; A_{0}; A_{0}; A_{0}; A_{0}; •; ^{id^{A_{0}}}; A_{0}; B_{0}; f; B_{0}; A_{0}; •; f^{∗}; ≅; 1_{v_{1}}; ⌞; A_{2}; A_{2}; A_{1}; A_{2}; •; v_{2}; A_{1}; A_{1}; A_{1}; A_{2}; ≅; A_{2}; B_{2}; g; A_{2}; A_{2}; •; ^{id^{A_{2}}}; A_{2}; A_{2}; A_{2}; B_{2}; •; g_{∗}; A_{2}; A_{2}; A_{1}; A_{2}; •; v_{2}; A_{1}; A_{1}; A_{1}; A_{2}; •; v_{2}; ⌜; 1_{v_{2}}]

and

[figure: B_{2}; B_{2}; A_{2}; B_{2}; •; g_{∗}; A_{2}; B_{2}; B_{2}; B_{2}; •; ^{id^{B2}}; A_{2}; B_{2}; g; A_{1}; A_{2}; •; v_{2}; A_{1}; B_{2}; A_{1}; A_{0}; A_{1}; •; v_{1}; A_{0}; B_{0}; f; B_{0}; A_{0}; B_{0}; B_{0}; A_{0}; •; f^{∗}; B_{0}; B_{0}; B_{0}; B_{0}; •; ^{id^{B0}}; A_{2}; B_{2}; g; A_{0}; A_{2}; A_{0}; B_{0}; f; B_{0}; B_{2}; •; w; B_{2}; B_{2}; B_{0}; B_{2}; B_{0}; B_{0}; B_{0}; B_{2}; •; w; ⌟; α; ⌝; ≅]

where the corner brackets represent binding cells, and ≅ are canonical (structural) isomorphisms. Any other factorization of α

[figure: A_{2}; B_{2}; g; A_{1}; A_{2}; •; v_{2}; A_{1}; C; C; B_{2}; •; u_{2}; A_{1}; C; A_{0}; A_{1}; •; v_{1}; A_{0}; B_{0}; f; B_{0}; C; •; u_{1}; γ_{2}; γ_{1}; B_{2}; B_{2}; B_{0}; B_{2}; B_{0}; B_{0}; B_{0}; B_{2}; •; w; γ_{3}]

is a horizontal reduct of (α_{1}, α_{2}, α_{3}) via the cells

[figure: B_{2}; B_{2}; A_{1}; B_{2}; •; g_{∗}·v_{2}; A_{1}; C; C; B_{2}; •; u_{2}; A_{1}; C; B_{0}; A_{1}; •; v_{1}·f^{∗}; B_{0}; B_{0}; B_{0}; C; •; u_{1}; ϕ_{2}; ϕ_{1}]

where ϕ_{1} and ϕ_{2} are respectively

[figure: A_{1}; C; A_{0}; A_{1}; •; v_{1}; A_{0}; B_{0}; B_{0}; C; •; u_{1}; A_{0}; B_{0}; f; B_{0}; A_{0}; •; f^{∗}; B_{0}; B_{0}; B_{0}; B_{0}; •; ^{id^{B_{0}}}; C; C; B_{0}; C; B_{0}; B_{0}; B_{0}; C; •; u_{1}; γ_{1}; ≅; ⌝; and; B_{2}; B_{2}; A_{2}; B_{2}; •; g_{∗}; A_{2}; B_{2}; B_{2}; B_{2}; •; ^{id^{B_{2}}}; A_{2}; B_{2}; g; A_{1}; A_{2}; •; v_{2}; A_{1}; C; C; B_{2}; •; u_{2}; B_{2}; B_{2}; C; B_{2}; C; C; C; B_{2}; •; u_{2}; ⌟; γ_{2}; ≅]

3.1.5. Corollary. Any bicategory considered as a vertical double category satisfies AFP.

Whereas, in the proof of proposition 3.1.4, only horizontal reduction (condition (1) of AFP) was needed, the proof of the next result requires vertical reduction (condition (2)) as well.

3.1.6. Proposition. Let 𝔸 be a double category in which every vertical arrow is a companion of some horizontal arrow. Then 𝔸 satisfies AFP.

Proof. Consider a cell

[figure: A_{2}; B_{2}; g; A_{1}; A_{2}; •; v_{2}; A_{1}; B_{2}; A_{1}; A_{0}; A_{1}; •; v_{1}; A_{0}; B_{0}; f; B_{0}; A_{2}; B_{2}; g; A_{0}; A_{2}; A_{0}; B_{0}; f; B_{0}; B_{2}; •; w; α]

and suppose v_{2} ≅ h_{∗} for h : A_{1} [figure] A_{2}. Then α factors as

[figure: A_{2}; B_{2}; g; A_{1}; A_{2}; •; v_{2}; A_{1}; B_{2}; gh; B_{2}; B_{2}; •; ^{id^{B_{2}}}; A_{1}; B_{2}; A_{0}; A_{1}; •; v_{1}; A_{0}; B_{0}; f; B_{0}; B_{2}; •; w; α_{2}; α_{1}; B_{2}; B_{2}; B_{0}; B_{2}; B_{0}; B_{0}; B_{0}; B_{2}; •; w; α_{3}]

where α_{1} , α_{2} are respectively

[figure: A_{1}; A_{1}; A_{0}; A_{1}; •; v_{1}; A_{0}; A_{0}; A_{0}; A_{1}; A_{1}; A_{2}; h; A_{1}; A_{1}; •; ^{id^{A_{1}}}; A_{1}; A_{1}; A_{1}; A_{2}; •; v_{2}; A_{1}; A_{1}; A_{0}; A_{1}; •; v_{1}; A_{0}; A_{0}; A_{0}; A_{1}; •; v_{1}; A_{2}; B_{0}; g; A_{0}; A_{2}; A_{0}; B_{0}; f; B_{0}; B_{0}; •; w; ≅; 1_{v_{1}}; ⌜; and; α; A_{2}; A_{2}; A_{1}; A_{2}; •; v_{2}; A_{1}; A_{2}; h; A_{2}; A_{2}; •; ^{id^{A_{2}}}; A_{2}; B_{2}; g; A_{2}; A_{2}; A_{2}; B_{2}; g; B_{2}; B_{2}; •; ^{id^{B_{2}}}; ⌟; ^{id^{g}}]

and α_{3} is the canonical isomorphism.

Now let

[figure: A_{2}; B_{2}; g; A_{1}; A_{2}; •; v_{2}; A_{1}; B_{1}; B_{1}; B_{2}; •; w_{2}; A_{1}; B_{1}; A_{0}; A_{1}; •; v_{1}; A_{0}; B_{0}; f; B_{0}; B_{1}; •; w_{1}; β_{2}; β_{1}; B_{2}; B_{2}; B_{0}; B_{2}; B_{0}; B_{0}; B_{0}; B_{2}; •; w; β_{3}]

be an arbitrary factorization of α. Use the same procedure as above to factor β_{3} as

[figure: B_{2}; B_{2}; B_{1}; B_{2}; •; w_{2}; B_{1}; B_{2}; B_{2}; B_{2}; •; ^{id^{B2}}; B_{1}; B_{2}; B_{0}; B_{1}; •; w_{1}; B_{0}; B_{0}; B_{0}; B_{2}; •; w; θ_{2}; θ_{1}; B_{2}; B_{2}; B_{0}; B_{2}; B_{0}; B_{0}; B_{0}; B_{2}; •; w; α_{3}]

which gives a horizontal reduction of the β_{3}(β_{2} · β_{1}) factorization to

[figure: A_{2}; B_{2}; A_{1}; A_{2}; •; v_{2}; A_{1}; B_{2}; B_{2}; B_{2}; •; ^{id^{B2}}; A_{1}; B_{2}; A_{0}; A_{1}; •; v_{1}; A_{0}; B_{0}; B_{0}; B_{2}; •; w; γ_{2}; γ_{1}; B_{2}; B_{2}; B_{0}; B_{2}; B_{0}; B_{0}; B_{0}; B_{2}; •; w; α_{3}]

where γ_{i} = θ_{i} · β_{i}. Now let θ be

[figure: A_{1}; A_{2}; h; A_{1}; A_{1}; •; id; A_{1}; A_{1}; A_{1}; A_{2}; •; v_{2}; A_{2}; B_{2}; A_{1}; A_{2}; A_{1}; B_{2}; B_{2}; B_{2}; •; id; γ_{2}; ⌜]

Then an easy calculation shows that θ · γ_{1} = α_{1} and α_{2} · θ = γ_{2}. Thus θ gives a vertical reduction of the α_{3}(γ_{2} · γ_{1}) factorization to the α_{3}(α_{2} · α_{1}) one.

3.1.7. Corollary. Any 2-category considered as a horizontal double category satisfies AFP.

3.1.8. Corollary. The double category of quintets in a 2-category satisfies AFP.

3.1.9. Corollary. If every vertical arrow of 𝔸 is a conjoint, then 𝔸 satisfies AFP.

3.2. Functoriality (defined) We are now in a position to define the action of n · m on cells.

3.2.1. Proposition. Assume that 𝔸 satisfies AFP and let

[figure: Ā; B̄; g; A; Ā; •; v; A; B; f; B; B̄; •; w; σ]

be a cell in 𝔸. Then there exists a unique cell (n · m)(σ) : (n · m)(v) [figure] (n · m)(w) such that

[figure: nv_{2} · mv_{1}; nw_{2} · mw_{1}; nβ_{2}·mβ_{1}; (n · m)(v); nv_{2} · mv_{1}; j_{α}; (n · m)(v); (n · m)(w); (n·m)(σ); (n · m)(w); nw_{2} · mw_{1}; j_{β_{3}}]

commutes for every α and factorization of σα

[figure: A_{3}; Ā; A_{2}; A_{3}; •; v_{2}; A_{2}; Ā; A_{2}; A_{1}; A_{2}; •; v_{1}; A_{1}; A; A; Ā; B̄; g; A; Ā; •; v; A; B; f; B; B̄; •; w; α; σ; =; A_{3}; B_{3}; g; A_{2}; A_{3}; •; v_{2}; A_{2}; B_{2}; B_{2}; B_{3}; •; w_{2}; A_{2}; B_{2}; A_{1}; A_{2}; •; v_{1}; A_{1}; B_{1}; f; B_{1}; B_{2}; •; w_{1}; β_{2}; β_{1}; B_{3}; B̄; B_{1}; B_{3}; B_{1}; B; B; B̄; •; w; β_{3}]

Proof. We first show that j_{β_{3}}(nβ_{2} · mβ_{1}) is independent of the factorization.

(1) Suppose we have a horizontal reduction of (β_{1}, β_{2}, β_{3}) to (β′_{1}, β′_{2}, β′_{3}) by (ϕ_{1}, ϕ_{2}). Then

[figure: nv_{2} · mv_{1}; nw′_{2} · mw′_{1}; nβ′_{2}·mβ′_{1}; nw_{2} · mw_{1}; nv_{2} · mv_{1}; nβ_{2}·mβ_{1}; nw_{2} · mw_{1}; nw′_{2} · mw′_{1}; nϕ_{2}·mϕ_{1}; (n · m)(w); nw′_{2} · mw′_{1}; j_{β′_{3}}; nw_{2} · mw_{1}; (n · m)(w); j_{β_{3}}; nw_{2} · mw_{1}; nw′_{2} · mw′_{1}]

commutes, the left triangle by functoriality of n and m and the right triangle by the cocone property for j (proposition 2.2.2).

(2) Suppose we have a vertical reduction of (β_{1}, β_{2}, β_{3}) to (β′_{1}, β′_{2}, β′_{3}) via θ. Then we have a commutative diagram

[figure: nv_{2} · Gid_{A_{2}} · mv_{1}; nv_{2} · m(id_{A_{2}} · v_{1}); nv_{2}·λ; n(v_{2} · id_{A_{2}}) · mv_{1}; nv_{2} · Gid_{A_{2}} · mv_{1}; ρ·mv_{1}; n(v_{2} · id_{A_{2}}) · mv_{1}; nv_{2} · m(id_{A_{2}} · v_{1}); nw′_{2} · Gx · mw_{1}; nw′_{2} · m(x · w_{1}); nw′_{2}·λ; n(w′_{2} · x) · mw_{1}; nw′_{2} · Gx · mw_{1}; ρ·mw_{1}; n(w′_{2} · x) · mw_{1}; nw′_{2} · m(x · w_{1}); nv_{2} · Gid_{A_{2}} · mv_{1}; nw′_{2} · Gx · mw_{1}; nβ′_{2}·Gθ·mβ_{1}; n(v_{2} · id_{A_{2}}) · mv_{1}; n(w′_{2} · x) · mw_{1}; n(β′_{2}·θ)·mβ_{1}; (n · m)(w); nw′_{2} · mw′_{1}; j_{_{β′}_{3}}; nw_{2} · mw_{1}; (n · m)(w); j_{β_{3}}; nw_{2} · mw_{1}; nw′_{2} · mw′_{1}; nv_{2} · m(id_{A_{2}} · v_{1}); nw′_{2} · m(x · w_{1}); nβ′_{2}·m(θ·β_{1}); (2); (1); (3); ≅; ≅]

where (1) and (2) commute by naturality of ρ and λ and (3) by the cocone property for j (proposition 2.2.2). Note that the top and bottom arrows of this diagram are nβ_{2} · mβ_{1} and nβ′_{2} · mβ′_{1} preceded by canonical isomorphisms, so if we precompose the diagram by

nv_{2} · mv_{1} [figure: ≅] nv_{2} · id_{GA_{2}} · mv_{1} [figure: nv_{2}·γ_{G}·mv_{1}] nv_{2} · G(id_{A_{2}}) · mv_{1}

we get j_{β_{3}}(nβ_{2} · mβ_{1}) = j_{β′_{3}}(nβ′_{2} · mβ′_{1}).

This shows that j_{β_{3}}(nβ_{2} · mβ_{1}) is independent of the factorization of σα. We denote the common value by k_{α}.

Now we show that ⟨k_{α}⟩ determines a cocone. We use proposition 2.2.2.

(a) (Transfer of scalars) Let α : v_{3} · v_{2} · v_{2} ⇒ v be a triple lax factorization of v. Then we can factor σα as

[figure: Ā; Ā; A_{2}; Ā; •; v_{3}; A_{2}; Ā; A_{2}; A_{1}; A_{2}; •; v_{2}; A_{1}; A_{1}; A; A_{1}; •; v_{1}; A; A; A; Ā; Ā; A; Ā; A; A; A; Ā; •; v; Ā; B̄; A; Ā; A; B; B; B̄; •; w; α; σ; =; Ā; B̄; A_{2}; Ā; •; v_{3}; A_{2}; B_{2}; B_{2}; B̄; •; w_{3}; A_{2}; B_{2}; A_{1}; A_{2}; •; v_{2}; A_{1}; B_{1}; B_{1}; B_{2}; •; w_{2}; A_{1}; B_{1}; A; A_{1}; •; v_{1}; A; B; B; B_{1}; •; w_{1}; β_{3}; β_{2}; β_{1}; B̄; B̄; B; B̄; B; B; B; B̄; •; w; β]

by first factoring σα considered as a cell (v_{3} · v_{2}) · v_{1} [figure] w and then factoring the cell with domain v_{3} · v_{2}. Then the following diagram commutes

[figure: nv_{3} · Gv_{2} · mv_{1}; nv_{3} · m(v_{2} · v_{1}); nv_{3}·λ; n(v_{3} · v_{2}) · mv_{1}; nv_{3} · Gv_{2} · mv_{1}; ρ·mv_{1}; n(v_{3} · v_{2}) · mv_{1}; nv_{3} · m(v_{2} · v_{1}); nw_{3} · Gw_{2} · mw_{1}; nw_{3} · m(w_{2} · w_{1}); nw_{1}·λ; n(w_{3} · w_{2}) · mw_{1}; nw_{3} · Gw_{2} · mw_{1}; ρ·mw_{1}; n(w_{3} · w_{2}) · mw_{1}; nw_{3} · m(w_{2} · w_{1}); nv_{3} · Gv_{2} · mv_{1}; nw_{3} · Gw_{2} · mw_{1}; nβ_{3}·Gβ_{2}·mβ_{1}; n(v_{3} · v_{2}) · mv_{1}; n(w_{3} · w_{2}) · mw_{1}; n(β_{3}·β_{2})·mβ_{1}; (n · m)(w); nw_{3} · m(w_{2} · w_{1}); j_{β}; n(w_{3} · w_{2}) · mw_{1}; (n · m)(w); j_{β}; n(w_{3} · w_{2}) · mw_{1}; nw_{3} · m(w_{2} · w_{1}); nv_{3} · m(v_{2} · v_{1}); nw_{3} · m(w_{2} · w_{1}); nβ_{3}·m(β_{2}·β_{1}); (2); (1); (3)]

(1) and (2) by naturality of ρ and λ and (3) by the cocone property for j. The top composite is k_{α}(ρ · mv_{1}) and the bottom is k_{α}(nv_{3} · λ). Thus ⟨k_{α}⟩ determines a cocone.

Now the cocone determined by the k_{α} is of the type required for the “further universal property” (LC3) of definition 2.1.1. Each component has the same vertical domain, F (f), and the same vertical codomain H(g). Then by (LC3) there exists a unique cell (n·m)(σ) : (n · m)(v) [figure] (n · m)(w) satisfying the stated conditions.

4. Proof of Main Theorem

In this section we prove the following theorem.

4.0.1. Theorem. If 𝔸 is a small double category satisfying AFT and 𝕏 is a locally cocomplete double category, then composites of modules between lax functors 𝔸 [figure] 𝕏 are strongly representable.

Now that the hard work has been done and everything properly set up, it is relatively straightforward to check that everything works. We set down the calculations here in the interest of completeness.

We first check that n · m is indeed a module F [figure: •] H. The data (M1) and (M2) from definition 1.1.6 have already been specified. We use the fact that the definition of k_{α} in proposition 3.2.1 is independent of the factorization of σα and make judicious choices in our proofs.

4.1. Functoriality

4.1.1. Proposition. n · m satisfies condition (M3) “horizontal functoriality”.

Proof. For σ = 1_{v} we can factor σα as

[figure: Ā; Ā; A_{1}; Ā; •; v_{2}; A_{1}; Ā; A_{1}; A; A_{1}; •; v_{1}; A; A; A; Ā; Ā; A; Ā; •; v; A; A; A; Ā; •; v; α; 1; =; Ā; Ā; A_{1}; Ā; •; v_{2}; A_{1}; A_{1}; A_{1}; Ā; •; v_{2}; A_{1}; A_{1}; A; A_{1}; •; v_{1}; A; A; A; A_{1}; •; v_{1}; Ā; Ā; A; Ā; A; A; A; Ā; •; v; 1; 1; α]

422  ROBERT PARÉ

so that k_{α} = j_{α}. Thus (n · m)(1_{v}) = 1_{(n·m)(v)}.

Now consider two cells

[figure: Ā; B̄; A; Ā; •; v; A; B; B; B̄; •; w; B̄; C̄; B; B̄; B; C; C; C̄; •; x; σ; τ]

We first factor σα = β_{3}(β_{2} · β_{1}) and then τβ_{3} = γ(γ_{2} · γ_{1})

[figure: Ā; Ā; A_{1}; Ā; •; v_{2}; A_{1}; Ā; A_{1}; A; A_{1}; •; v_{1}; A; A; A; Ā; B̄; A; Ā; •; v; A; B; B; B̄; •; w; B̄; C̄; B; B̄; •; B; C; C; C̄; •; x; α; σ; τ; =; Ā; B̄; A_{1}; Ā; •; v_{2}; A_{1}; B_{1}; B_{1}; B̄; •; w_{2}; A_{1}; B_{1}; A; A_{1}; •; v_{1}; A; B; B; B_{1}; •; w_{1}; B̄; B̄; B; B̄; B; B; B; B̄; •; w; B̄; C̄; B; B̄; •; B; C; C; C̄; •; x; β_{2}; β_{1}; β_{3}; τ]

[figure: =; Ā; B̄; A_{1}; Ā; •; v_{2}; A_{1}; B_{1}; B_{1}; B̄; •; w_{2}; A_{1}; B_{1}; A; A_{1}; •; v_{1}; A; B; B; B_{1}; •; w_{1}; B̄; C̄; B_{1}; B̄; •; B_{1}; C_{1}; C_{1}; C̄; •; x_{2}; B_{1}; C_{1}; B; B_{1}; •; B; C; C; C_{1}; •; x_{1}; C̄; C̄; C; C̄; C; C; C; C̄; •; x; β_{2}; β_{1}; γ_{2}; γ_{1}; γ_{3}; =; Ā; C̄; A_{1}; Ā; •; v_{2}; A_{1}; C_{1}; C_{1}; C̄; •; x_{2}; A_{1}; C_{1}; A; A_{1}; •; v_{1}; A; C; C; C_{1}; •; x_{1}; C̄; C̄; C; C̄; C; C; C; C̄; •; x; γ_{2}β_{2}; γ_{1}β_{1}; γ_{3}]

which gives the commutative diagram

[figure: nv_{2} · mv_{1}; nw_{2} · mw_{1}; nβ_{2}·mβ_{1}; (n · m)(v); nv_{2} · mv_{1}; j_{α}; (n · m)(v); (n · m)(w); (n·m)(σ); (n · m)(w); nw_{2} · mw_{1}; j_{β_{3}}; nw_{2} · mw_{1}; nx_{2} · mx_{1}; nγ_{2}·mγ_{1}; (n · m)(w); nw_{2} · mw_{1}; (n · m)(w); (n · m)(x); (n·m)(τ); (n · m)(x); nx_{2} · mx_{1}; j_{γ_{3}}; nv_{2} · mv_{1}; nx_{2} · mx_{1}; n(γ_{2}β_{2})·m(γ_{1}β_{1})]

so ((n · m)(τ))((n · m)(σ)) = (n · m)(τσ).

4.2. Naturality 4.2.1. Proposition. The left and right actions for n · m are natural (M4). Proof. We give the proof for the left action λ_{n·m}. The right action is the same.

COMPOSITION OF MODULES FOR LAX FUNCTORS  423

For compatible cells, σ : v [figure] w and σ̄ : v̄ [figure] w̄ we must establish the commutativity of

[figure: Hw̄ · (n · m)(w); (n · m)(w̄ · w); λ_{n·m}(w̄,w); Hv̄ · (n · m)(v); Hw̄ · (n · m)(w); Hσ̄·(n·m)(σ); Hv̄ · (n · m)(v); (n · m)(v̄ · v); λ_{n·m}(v̄,v); (n · m)(v̄ · v); (n · m)(w̄ · w); (n·m)(σ̄·σ)]

Given a lax factorization of v, α : v_{2} · v_{1} ⇒ v, we factor σα as

[figure: Ā; Ā; A_{1}; Ā; •; v_{2}; A_{1}; Ā; A_{1}; A; A_{1}; •; v_{1}; A; A; A; Ā; B̄; g; A; Ā; •; v; A; B; f; B; B̄; •; w; α; σ; =; Ā; B̄; g; A_{1}; Ā; •; v_{2}; A_{1}; B_{1}; B_{1}; B̄; •; w_{2}; A_{1}; B_{1}; A; A_{1}; •; v_{1}; A; B; f; B; B_{1}; •; w_{1}; β_{2}; β_{1}; B̄; B̄; B; B̄; B; B; B; B̄; •; w; β_{3}]

which gives us a factorization of (σ̄ · σ)(v̄ · α)

[figure: Ã; Ã; Ā; Ã; •; v̄; Ā; Ā; Ā; Ã; •; v̄; Ā; Ā; A_{1}; Ā; •; v_{2}; A_{1}; Ā; A_{1}; A; A_{1}; •; v_{1}; A; A; A; Ā; Ā; A; Ā; A; A; A; Ā; •; v; 1; α; Ã; B̃; Ā; Ã; •; Ā; B̄; B̄; B̃; •; w̄; Ā; B̄; A; Ā; A; B; B; B̄; •; w; σ̄; σ; =; Ã; B̃; Ā; Ã; •; v̄; Ā; B̄; B̄; B̃; •; w̄; Ā; B̄; A_{1}; Ā; •; v_{2}; A_{1}; B_{1}; B_{1}; B̄; •; w_{2}; A_{1}; B_{1}; A; A_{1}; •; v_{1}; A; B; B; B_{1}; •; w_{1}; B̃; B̃; B̄; B̃; B̄; B̄; B̄; B̃; •; w̄; B̄; B̄; B; B̄; B; B; B; B̄; •; w; σ̄; β_{2}; β_{1}; 1; β_{2}]

Then we have commutative diagrams

[figure: Hv̄ · nv_{2} · mv_{1}; n(v̄ · v_{2}) · mv_{1}; λ_{n}(v̄,v_{2})·mv_{1}; Hv̄ · (n · m)(v); Hv̄ · nv_{2} · mv_{1}; Hv̄·j_{α}; Hv̄ · (n · m)(v); (n · m)(v̄ · v); λ_{n·m}(v̄,v); (n · m)(v̄ · v); n(v̄ · v_{2}) · mv_{1}; j_{v̄·α}; n(v̄ · v_{2}) · mv_{1}; n(w̄ · w_{2}) · mw_{1}; n(σ̄·β_{2})·mβ_{1}; (n · m)(v̄ · v); n(v̄ · v_{2}) · mv_{1}; (n · m)(v̄ · v); (n · m)(w̄ · w); (n·m)(σ̄·σ); (n · m)(w̄ · w); n(w̄ · w_{2}) · mw_{1}; j_{w̄·β_{3}}; n(v̄ · v_{2}) · mv_{1}; (n · m)(w̄ · w); k_{v̄·α}]

and

[figure: Hv̄ · nv_{2} · mv_{1}; Hw̄ · nw_{2} · mw_{1}; Hσ̄·nβ_{2}·mβ_{1}; Hv̄ · (n · m)(v); Hv̄ · nv_{2} · mv_{1}; Hv̄·j_{α}; Hv̄ · (n · m)(v); Hw̄ · (n · m)(w); Hσ̄·(n·m)(σ); Hw̄ · (n · m)(w); Hw̄ · nw_{2} · mw_{1}; Hw̄·j_{β_{3}}; Hw̄ · nw_{2} · mw_{1}; n(w̄ · w_{2}) · mw; λ_{n}(w̄,w_{2})·mw_{1}; Hw̄ · (n · m)(w); Hw̄ · nw_{2} · mw_{1}; Hw̄ · (n · m)(w); (n · m)(w̄ · w); λ_{n·m}(w̄,w); (n · m)(w̄ · w); n(w̄ · w_{2}) · mw; j_{w̄·β_{3}}; Hv̄ · nv_{2} · mv_{1}; Hw̄ · (n · m)(w); Hσ̄·k_{α}]

424  ROBERT PARÉ

in which the bottom rows are equal by naturality of λ_{n}. As the Hv̄ · j_{α} are jointly epic, we get the required commutativity.

4.3. Unit Laws

4.3.1. Proposition. The left and right actions for n · m satisfy condition (M5), “unit laws”.

Proof. Again we just check the unit law for λ_{n·m}. We must show commutativity of

[figure: id_{HĀ} · (n · m)(v); H(id_{A}) · (n · m)(v); ηĀ·(n·m)(v); id_{HĀ} · (n · m)(v); (n · m)(id_{A} · v); ≅; H(id_{A}) · (n · m)(v); (n · m)(id_{A} · v); λ_{n·m}(idĀ,v)]

For any α : v_{2} · v_{1} ⇒ v we have a commutative diagram

[figure: id_{HĀ} · nv_{2} · mv_{1}; H(idĀ) · nv_{2} · mv_{1}; ηĀ·nv_{2}·mv_{1}; id_{HĀ} · (n · m)(v); id_{HĀ} · nv_{2} · mv_{1}; id_{HĀ}·j_{α}; id_{HĀ} · (n · m)(v); H(idĀ) · (n · m)(v); ηĀ·(n·m)(v); H(idĀ) · (n · m)(v); H(idĀ) · nv_{2} · mv_{1}; H(idĀ)·j_{α}; H(idĀ) · nv_{2} · mv_{1}; n(idĀ · v_{2}) · mv_{1}; λ_{n}(idĀ,v_{2})·mv_{1}; H(idĀ) · (n · m)(v); H(idĀ) · nv_{2} · mv_{1}; H(idĀ) · (n · m)(v); (n · m)(idĀ · v); λ_{n,m}(idĀ,v); (n · m)(idĀ · v); n(idĀ · v_{2}) · mv_{1}; j_{idĀ·α}]

The canonical isomorphism represented by ≅ in the triangle above is in fact the top row of the commutative diagram

[figure: id_{HĀ} · nv_{2} · mv_{1}; nv_{2} · mv_{1}; 𝔩_{HĀ}·mv_{1}; id_{HĀ} · (n · m)(v); id_{HĀ} · nv_{2} · mv_{1}; id_{HĀ}·j_{α}; id_{HĀ} · (n · m)(v); (n · m)(v); 𝔩_{HĀ}; (n · m)(v); nv_{2} · mv_{1}; j_{α}; nv_{2} · mv_{1}; n(idĀ · v_{2}) · mv_{1}; n(𝔩_{A}^{−1})·mv_{1}; (n · m)(v); nv_{2} · mv_{1}; (n · m)(v); (n · m)(idĀ · v); (n·m)(𝔩−1 ; Ā); (n · m)(idĀ · v); n(idĀ · v_{2}) · mv_{1}; j_{idĀ·α}; nv_{2} · mv_{1}; (n · m)(id_{A} · v); k_{α}]

where the calculation of k_{α} was made using the factorization

[figure: A_{2}; Ā; A_{1}; A_{2}; •; v_{2}; A_{1}; Ā; A_{1}; A_{0}; A_{1}; •; v_{1}; A_{0}; A; A; A_{2}; Ā; A_{0}; A_{2}; A_{0}; A; A; Ā; •; v; α; Ā; Ā; Ā; Ā; Ā; Ā; •; ^{idĀ}; Ā; A; A; A; A; Ā; •; v; 𝔩_{A}^{−1}; =; A_{2}; A_{2}; A_{2}; A_{2}; A_{2}; A_{2}; •; ^{id^{A2}}; A_{2}; A_{1}; A_{1}; A_{1}; A_{1}; A_{2}; •; v_{2}; A_{1}; A_{1}; A_{0}; A_{1}; •; v_{1}; A_{0}; A_{0}; A_{0}; A_{1}; •; v_{1}; A_{2}; A_{2}; A_{1}; A_{2}; •; v_{2}; A_{1}; A_{1}; A_{1}; A_{2}; A_{2}; Ā; A_{2}; A_{2}; A_{2}; Ā; Ā; Ā; •; ^{idĀ}; A_{2}; Ā; A_{1}; A_{2}; A_{1}; Ā; A_{2}; Ā; A_{0}; A_{2}; A_{0}; A; A; Ā; •; v; 𝔩_{A2}^{−1}; α; 1; 1]

The bottom lines of the two rectangles are equal by the unit law for n.

4.4. Associativity

4.4.1. Proposition. The left and right actions for n · m satisfy condition (M6), “associativity”.

Proof. First we check left associativity. This means that the top composites of the two following diagrams must be equal for any composable triple of vertical arrows v, v̄, ṽ. Any lax factorization of v, α : v_{2} · v_{1} ⇒ v gives lax factorizations v̄ · α : (v̄ · v_{2}) · v_{1} ⇒ v̄ · v and ṽ · v̄ · α : (ṽ · v̄ · v_{2}) · v_{1} ⇒ ṽ · v̄ · v of v̄ · v and ṽ · v̄ · v respectively. Thus we have the following commutative diagrams.

[figure: Hṽ · Hv̄ · nv_{2} · mv_{1}; Hṽ · n(v̄ · v_{2}) · mv_{1}; Hṽ·λ(v̄,v_{2})·mv_{1}; Hṽ · Hv̄ · (n · m)(v); Hṽ · Hv̄ · nv_{2} · mv_{1}; Hṽ·Hv̄·j_{α}; Hṽ · Hv̄ · (n · m)(v); Hṽ · (n · m)(v̄ · v); Hṽ·λ(v̄,v); Hṽ · (n · m)(v̄ · v); Hṽ · n(v̄ · v_{2}) · mv_{1}; Hṽ·j_{v̄·α}; Hṽ · n(v̄ · v_{2}) · mv_{1}; n(ṽ · v̄ · v_{2}) · mv_{1}; λ(ṽ,v̄·v_{2})·mv_{1}; Hṽ · (n · m)(v̄ · v); Hṽ · n(v̄ · v_{2}) · mv_{1}; Hṽ · (n · m)(v̄ · v); (n · m)(ṽ · v̄ · v); λ(ṽ,v̄·v); (n · m)(ṽ · v̄ · v); n(ṽ · v̄ · v_{2}) · mv_{1}; j_{ṽ·v̄·α}]

and

[figure: Hṽ · Hv̄ · nv_{2} · mv_{1}; H(ṽ · v̄) · nv_{2} · mv_{1}; η(ṽ,v̄)·nv_{2}·mv_{1}; Hṽ · Hv̄ · (n · m)(v); Hṽ · Hv̄ · nv_{2} · mv_{1}; Hṽ·Hv̄·j_{α}; Hṽ · Hv̄ · (n · m)(v); H(ṽ · v̄) · (n · m)(v); η(ṽ,v̄)·(n·m)(v); H(ṽ · v̄) · (n · m)(v); H(ṽ · v̄) · nv_{2} · mv_{1}; H(ṽ·v̄)·j_{α}; H(ṽ · v̄) · nv_{2} · mv_{1}; n(ṽ · v̄ · v_{2}) · mv_{1}; λ(ṽ·v̄,v_{2})·mv_{1}; H(ṽ · v̄) · (n · m)(v); H(ṽ · v̄) · nv_{2} · mv_{1}; H(ṽ · v̄) · (n · m)(v); (n · m)(ṽ · v̄ · v); λ(ṽ·v̄,v); (n · m)(ṽ · v̄ · v); n(ṽ · v̄ · v_{2}) · mv_{1}; j_{ṽ·v̄·α}]

That the composites of the bottom rows are equal is left associativity for n, giving left associativity for n · m.

Right associativity follows in the same way from that of m. Middle associativity is a bit different so we set it down here. Now, we take a lax

factorization of v̄, α : v_{2} · v_{1} ⇒ v̄, and the corresponding ones for v̄ · v, ṽ · v̄ and ṽ · v̄ · v, α · v : v_{2} · (v_{1} · v) ⇒ v̄ · v, ṽ · α : (ṽ · v_{2}) · v_{1} ⇒ ṽ · v̄, and ṽ · α · v : (ṽ · v_{2}) · (v_{1} · v) ⇒ ṽ · v̄ · v. With this we get the following commutative diagrams.

[figure: Hṽ · nv_{2} · mv_{1} · F v; n(ṽ · v_{2}) · mv_{1} · F v; λ(ṽ,v_{2})·mv_{1}·F v; Hṽ · (n · m)(v̄) · F v; Hṽ · nv_{2} · mv_{1} · F v; Hṽ·j_{α}F v; Hṽ · (n · m)(v̄) · F v; (n · m)(ṽ · v̄) · F v; λ(ṽ,v̄)·F v; (n · m)(ṽ · v̄) · F v; n(ṽ · v_{2}) · mv_{1} · F v; j_{ṽ·α}·F v; n(ṽ · v_{2}) · mv_{1} · F v; n(ṽ · v_{2}) · m(v_{1} · v); n(ṽ·v_{2})·ρ(v_{1},v); (n · m)(ṽ · v̄) · F v; n(ṽ · v_{2}) · mv_{1} · F v; (n · m)(ṽ · v̄) · F v; (n · n)(ṽ · v̄ · v); ρ(ṽ·v̄,v); (n · n)(ṽ · v̄ · v); n(ṽ · v_{2}) · m(v_{1} · v); j_{ṽα·v}]

and

[figure: Hṽ · nv_{2} · mv_{1} · F v; Hṽ · nv_{2} · m(v_{1} · v); Hṽ·nv_{2}·ρ(v_{1},v); Hṽ · (n · m)(v̄) · F v; Hṽ · nv_{2} · mv_{1} · F v; Hṽ·j_{α}·F v; Hṽ · (n · m)(v̄) · F v; Hṽ · (n · m)(v̄ · v); Hṽ·ρ(v̄,v); Hṽ · (n · m)(v̄ · v); Hṽ · nv_{2} · m(v_{1} · v); Hṽ·j_{α·v}; Hṽ · nv_{2} · m(v_{1} · v); n(ṽ · v_{2}) · m(v_{1} · v); λ(ṽ,v_{2})·m(v_{1}·v); Hṽ · (n · m)(v̄ · v); Hṽ · nv_{2} · m(v_{1} · v); Hṽ · (n · m)(v̄ · v); (n · m)(ṽ · v̄ · v); λ(ṽ,v̄,v); (n · m)(ṽ · v̄ · v); n(ṽ · v_{2}) · m(v_{1} · v); j_{ṽ·α·v}]

The bottom rows are equal simply by functoriality of vertical composition, so the top rows will be equal as well, which is middle associativity.

Thus we have proved that n · m is a module. It remains to see that it has the strong representability property, which we do in the next two sections.

4.5. The Canonical Bimodulation In this section we define the bimodulation

[figure: H; H; G; H; •; n; G; H; G; F; G; •; m; F; F; F; H; H; F; H; F; F; F; H; •; n·m; ι]

Given two vertical arrows A_{0} [figure: •; v_{1}] A_{1} [figure: •; v_{2}] A_{2}, v_{2} · v_{1} has a canonical lax factorization into v_{1} and v_{2}

1_{v_{2}·v_{1}} : v_{2} · v_{1} ⇒ v_{2} · v_{1}.

Define ι(v_{2}, v_{1}) = j_{1_{v_{2}·v_{1}}} : n(v_{2}) · m(v_{1}) [figure] (n · m)(v_{2} · v_{1}).

4.5.1. Proposition. ι is a bimodulation.

Proof. First, ι satisfies (mm2), “horizontal naturality”. Let

[figure: A_{2}; B_{2}; A_{1}; A_{2}; •; v_{2}; A_{1}; B_{1}; B_{1}; B_{2}; •; w_{2}; A_{1}; B_{1}; A_{0}; A_{1}; •; v_{1}; A_{0}; B_{0}; B_{0}; B_{1}; •; w_{1}; α_{2}; α_{1}]

be cells. The composite (α_{2} · α_{1})1_{v_{2}·v_{1}} has the factorization 1_{w_{2}·w_{1}}(α_{2} · α_{1})

[figure: A_{2}; A_{2}; A_{1}; A_{2}; •; v_{2}; A_{1}; A_{2}; A_{1}; A_{0}; A_{1}; •; v_{1}; A_{0}; A_{0}; A_{0}; A_{2}; B_{2}; A_{0}; A_{2}; •; v_{2}·v_{1}; A_{0}; B_{0}; B_{0}; B_{2}; •; w_{2}·w_{1}; α_{2}·α_{1}; =; A_{2}; B_{2}; A_{1}; A_{2}; •; v_{2}; A_{1}; B_{1}; B_{1}; B_{2}; •; w_{2}; A_{1}; B_{1}; A_{0}; A_{1}; •; v_{1}; A_{0}; B_{0}; B_{0}; B_{1}; •; w_{1}; B_{2}; B_{2}; B_{0}; B_{2}; B_{0}; B_{0}; B_{0}; B_{2}; •; w_{2}·w_{1}; α_{2}; α_{1}; 1]

so by proposition 3.2.1, we have that commutes, which is naturality of n · m.

[figure: nv_{2} · mv_{1}; nw_{2} · mw_{1}; nα_{2}·mα_{1}; (n · m)(v_{2} · v_{1}); nv_{2} · mv_{1}; j_{1v_{2}·v_{1}}; (n · m)(v_{2} · v_{1}); (n · m)(w_{2} · w_{1}); (n·m)(α_{2}·α_{1}); (n · m)(w_{2} · w_{1}); nw_{2} · mw_{1}; j_{1w_{2}·w_{1}}]

Next we check equivariance, (mm3). This says that for any three composable vertical arrows v_{1}, v_{2}, v_{3} we must have commutativity of

[figure: n(v_{3} · v_{2}) · mv_{1}; (n · m)(v_{3} · v_{2} · v_{1}); j_{1}; nv_{3} · Gv_{2} · mv_{1}; n(v_{3} · v_{2}) · mv_{1}; ρ(v_{3},v_{2})·mv_{1}; nv_{3} · Gv_{2} · mv_{1}; nv_{3} · m(v_{2} · v_{1}); nv_{3}·λ(v_{2},v_{1}); nv_{3} · m(v_{2} · v_{1}); (n · m)(v_{3} · v_{2} · v_{1}); j_{1}]

This follows from proposition 2.2.1, part (a), because j is a cocone.

Left equivariance (mm3_{l}) says that

[figure: Hv_{3} · (n · m)(v_{2} · v_{1}); (n · m)(v_{3} · v_{2} · v_{1}); λ(v_{3},v_{2}·v_{1}); Hv_{3} · nv_{2} · mv_{1}; Hv_{3} · (n · m)(v_{2} · v_{1}); Hv_{3}·j_{1v_{2}·v_{1}}; Hv_{3} · nv_{2} · mv_{1}; n(v_{3} · v_{2}) · mv_{1}; λ(v_{3},v_{3})·mv_{1}; n(v_{3} · v_{2}) · mv_{1}; (n · m)(v_{3} · v_{2} · v_{1}); j_{1v_{3}·v_{2}·v_{1}}]

commutes, which it does by the definition of the left action for n · m (proposition 2.3.1). Right equivariance, (mm3_{r}), is similar.

4.6. The Universal Property

4.6.1. Proposition. The bimodulation ι : n, m [figure] n·m satisfies the strong representability property.

Proof. Let

p = (F_{k} [figure: •; p_{k}] F_{k−1} [figure: •; p_{k−1}] … [figure: •; p_{1}] F_{0} = F)
q = (H = H_{0} [figure: •; q_{1}] H_{1} [figure: •; q_{2}] … [figure: •; q_{l}] H_{l})

be paths of modules and let

μ : q, n, m, p [figure] r

be a multimodulation. We will show that there is a unique multimodulation μ̄ such that

[figure: q, n, m, p; r; μ; q, n, m, p; q, n · m, p; q,ι,p; q, n · m, p; r; μ̄]

commutes. Thus for vertical arrows

x = (A_{k} [figure: •; x_{k}] A_{k−1} [figure: •; x_{k−1}] … [figure: •; x_{1}] A_{0} = A)
w = (C = C_{0} [figure: •; w_{1}] C_{1} [figure: •; w_{2}] … [figure: •; w_{l}] C_{l})

A [figure: •; v_{1}] B [figure: •; v_{2}] C

we must have commutativity of

[figure: [qw] · nv_{2} · mv_{1} · [px]; r[w, v_{2}, v_{1}, x]; μ(w,v_{2},v_{1},x); [qw] · nv_{2} · mv_{1} · [px]; [qw] · (n · m)(v_{2} · v_{1}) · [px]; [qw]·j_{1v_{2}·v_{1}} ·[px]; [qw] · (n · m)(v_{2} · v_{1}) · [px]; r[w, v_{2}, v_{1}, x]; μ̄(w,v_{2}·v_{1},x); (1)]

Let v : A [figure: •] C be an arbitrary vertical arrow and

[figure: C; C; B; C; •; v_{2}; B; C; B; A; B; •; v_{1}; A; A; A; C; C; A; C; A; A; A; C; •; v; α]

a lax factorization of v. Then for x and w as above, naturality of μ̄ would give the commutative square

[figure: r[w, v_{2}, v_{1}, x]; r[w, v, x]; r[w,α,x]; [qw] · (n · m)(v_{2} · v_{1}) · [px]; r[w, v_{2}, v_{1}, x]; μ̄(w,v_{2}·v_{1},x); [qw] · (n · m)(v_{2} · v_{1}) · [px]; [qw] · (n · m)v · [px]; [qw]·(n·m)α·[px]; [qw] · (n · m)v · [px]; r[w, v, x]; μ̄(w,v,x)]

which, if pasted onto the right side of (1), gives the commuting

[figure: r[w, v_{2}, v_{1}, x]; r[w, v, x]; r[w,α,x]; [qw] · nv_{2} · mv_{1} · [px]; r[w, v_{2}, v_{1}, x]; μ(w,v_{2},v_{1},x); [qw] · nv_{2} · mv_{1} · [px]; [qw] · (n · m)v · [px]; [qw]·j_{α}·[px]; [qw] · (n · m)v · [px]; r[w, v, x]; μ̄(w,v,x); (2)]

because ((n · m)α)(j_{1}) = j_{α}. Now the family ⟨[qw] · j_{α} · [px]⟩_{α} is jointly epic so, if μ̄ exists, it is unique.

The next step is to show r[w, α, x]μ(w, v_{2}, v_{1}, x) determines a cocone as in proposition 2.2.1, which will show that μ̄(w, v, x) does exist. Condition (a) says that for any triple lax factorization γ : v_{3} · v_{2} · v_{1} [figure] v the diagram

[figure: [qw] · nv_{3} · Gv_{2} · mv_{1} · [px]; [qw] · nv_{3} · m(v_{2} · v_{1})[px]; 1·λ_{m}·1; [qw] · n(v_{3} · v_{2}) · mv_{1} · [px]; [qw] · nv_{3} · Gv_{2} · mv_{1} · [px]; 1·ρ_{n}·1; [qw] · n(v_{3} · v_{2}) · mv_{1} · [px]; [qw] · nv_{3} · m(v_{2} · v_{1})[px]; r[w, v_{3}, v_{2}, v_{1}, x]; [qw] · nv_{3} · m(v_{2} · v_{1})[px]; μ(w,v_{3},v_{2}·v_{1},x); [qw] · n(v_{3} · v_{2}) · mv_{1} · [px]; r[w, v_{3}, v_{2}, v_{1}, x]; μ(w,v_{3}·v_{2},v_{1},x); [qw] · n(v_{3} · v_{2}) · mv_{1} · [px]; [qw] · nv_{3} · m(v_{2} · v_{1})[px]]

must commute when followed by

r[w, γ, x] : r[w, v_{3}, v_{2}, v_{1}, x] [figure] r[w, v, x].

But it commutes even before that by associativity of μ.

For condition (b) consider two lax factorizations of v, β : v_{2} · v_{1} ⇒ v, β′ : v′_{2} · v′_{1} ⇒ v related by β′(θ_{2} · θ_{1}) = β for

[figure: C; C; B; C; •; v_{2}; B; B′; B′; C; •; v′_{2}; B; B′; A; B; •; v_{1}; A; A; A; B′; •; v′_{1}; θ_{2}; θ_{1}]

We have to show that

[figure: [qw] · nv′_{2} · mv′_{1} · [px]; r[wv′_{2}, v′_{1}, x]; μ(w,v′_{2},v′_{1},x); [qw] · nv_{2} · mv_{1} · [px]; [qw] · nv′_{2} · mv′_{1} · [px]; 1·nθ_{2}·mθ_{1}·1; [qw] · nv_{2} · mv_{1} · [px]; r[wv_{2}, v_{1}, x]; μ(w,v_{2},v_{1},x); r[wv_{2}, v_{1}, x]; r[wv′_{2}, v′_{1}, x]; r[w, v, x]; r[wv′_{2}, v′_{1}, x]; r[w,β′,x]; r[wv_{2}, v_{1}, x]; r[w, v, x]; r[w,β,x]; r[wv_{2}, v_{1}, x]; r[wv′_{2}, v′_{1}, x]; r[w,θ_{2},θ_{1},x]]

commutes, which it does, the square by naturality of μ and the triangle by functoriality of r. This shows that the μ̄(w, v, x) exist (and are unique) satisfying (2).

It remains to show that this definition makes μ̄ into a multimodulation. There are a number of things to check but the method of proof is the same for all of them. The condition is expressed as the commutativity of a diagram involving μ̄ which we reduce to a similar diagram for μ by precomposing with an arbitrary 1·j_{α} ·1 (for suitable identities).

To check naturality of μ̄ we take a path of cells

[figure: C_{k}; C_{k}; C; C_{k}; •; w; C; C′; C′; C_{k}; •; w′; ω; C; C′; A; C; •; v; A; A′; A′; C′; •; v′; σ; A; A′; A_{l}; A; •; x; A_{l}; A′_{l}; A′_{l}; A′; •; x′; ξ]

and must show that

[figure: [qw′] · (n · m)v′ · [px′]; r[w′, v′, x′]; μ̄(w′,v′,x′); [qw] · (n · m)v · [px]; [qw′] · (n · m)v′ · [px′]; [qω]·(n·m)σ·[pξ]; [qw] · (n · m)v · [px]; r[w, v, x]; μ̄(w,v,x); r[w, v, x]; r[w′, v′, x′]; r[ω,σ,ξ]; (∗)]

commutes. For this it will be sufficient to show that it does when preceded by [qw]·j_{α}·[px] for α : v_{2} · v_{1} ⇒ v, an arbitrary lax factorization of v. Factor σα as

[figure: C; C; B; C; v_{2}; B; C; B; A; B; v_{1}; A; A; A; C; C; A; C; A; A; A; C; v; C; C′; A; C; A; A′; A′; C′; v′; α; σ; =; C; C′; B; C; v_{1}; B; B′; B′; C′; v′_{2}; B; B′; A; B; v_{1}; A; A′; A′; B′; v′_{1}; C′; C′; A′; C′; A′; A′; A′; C′; v′; β_{2}; β_{1}; β]

Then by definition of (n · m)σ and functoriality of vertical composition, we get the commutative square

[figure: [qw′] · nv′_{2} · mv′_{1} · [px′]; [qw′] · (n · m)v′ · [px′]; 1·j_{β}·1; [qw] · nv_{2} · mv_{1} · [px]; [qw′] · nv′_{2} · mv′_{1} · [px′]; [qω]·nβ_{2}·mβ_{1}[pξ]; [qw] · nv_{2} · mv_{1} · [px]; [qw] · (n · m)v · [px]; 1·j_{α}·1; [qw] · (n · m)v · [px]; [qw′] · (n · m)v′ · [px′]; [qω]·(n·m)σ·[pξ]]

If we paste this onto (∗) and use the definition of μ̄ we get

[figure: [qw′] · nv′_{2} · mv′_{1} · [px′]; r[w′, v′_{2}, v′_{1}, x]; μ(w′,v′_{2},v′_{1},x′); [qw] · nv_{2} · mv_{1} · [px]; [qw′] · nv′_{2} · mv′_{1} · [px′]; [qω]·nβ_{2}·mβ_{1}·[pξ]; [qw] · nv_{2} · mv_{1} · [px]; r[w, v_{2}, v_{1}, x]; μ(w,v_{2},v_{1},x); r[w, v_{2}, v_{1}, x]; r[w′, v′_{2}, v′_{1}, x]; r[ω,β_{2},β_{1},ξ]; r[w′, v′_{2}, v′_{1}, x]; r[w′, v′, x′]; r[w′,β,x′]; r[w, v_{2}, v_{1}, x]; r[w′, v′_{2}, v′_{1}, x]; r[w, v_{2}, v_{1}, x]; r[w, v, x]; r[w,α,x]; r[w, v, x]; r[w′, v′, x′]; r[ω,σ,ξ]]

which commutes by naturality of μ and functoriality of r. This establishes naturality of μ̄.

Checking the equivariance of μ̄ involves evaluating one of the F ’s or one of the H’s at a vertical arrow. There are eight cases to consider:

(1) F_{k}, k > 0 (right equivariance),

(2) F_{i}, 0 < i < k (doesn’t involve n · m),

(3) F_{0}, k > 0 (involves n · m),

(4) F_{0}, k = 0 (involves n · m), and four dual ones for the H’s.

For (1), let x, w, α be as before, and x′ : A′_{k} [figure: •] A_{k}. We must show that

[figure: [qw] · (n · m)v · [p(x · x′)]; r[w, v, x · x′]; μ̄(w,v,x·x′); [qw] · (n · m)v · [px] · F_{k}x′; [qw] · (n · m)v · [p(x · x′)]; 1·ρ_{p_{k}}; [qw] · (n · m)v · [px] · F_{k}x′; r[w, v, x] · F_{k}x′; μ̄(w,v,x)·F_{k}x′; r[w, v, x] · F_{k}x′; r[w, v, x · x′]; ρ_{r}]

commutes. Paste onto this the commutative diagram

[figure: [qw] · nv_{2} · mv′_{1}[p(x · x′)]; [qw] · (n · m)v · [p(x · x′)]; 1·j_{α}·1; [qw] · nv_{2} · mv_{1} · [px] · F_{k}x′; [qw] · nv_{2} · mv′_{1}[p(x · x′)]; 1·ρ_{p_{k}}; [qw] · nv_{2} · mv_{1} · [px] · F_{k}x′; [qw] · (n · m)v · [px] · F_{k}x′; 1·j_{α}·1; [qw] · (n · m)v · [px] · F_{k}x′; [qw] · (n · m)v · [p(x · x′)]; 1·ρ_{p_{k}}]

and use the definition of μ̄ to get

[figure: [qw] · nv_{2} · mv_{1} · [p(x · x′)]; r[w, v_{2}, v_{1}, x · x′]; μ(w,v_{2},v_{1},x·x′); [qw] · nv_{2} · mv_{1} · [px] · F_{k}x′; [qw] · nv_{2} · mv_{1} · [p(x · x′)]; 1·ρ_{p_{k}}; [qw] · nv_{2} · mv_{1} · [px] · F_{k}x′; r[w, v_{2}, v_{1}, x] · F_{k}x′; μ(w,v_{2},v_{1},x)·F_{k}x′; r[w, v_{2}, v_{1}, x] · F_{k}x′; r[w, v_{2}, v_{1}, x · x′]; ρ_{r}; r[w, v_{2}, v_{1}, x · x′]; r[w, v, x · x′]; r[w,α,x·x′]; r[w, v_{2}, v_{1}, x] · F_{k}x′; r[w, v_{2}, v_{1}, x · x′]; r[w, v_{2}, v_{1}, x] · F_{k}x′; r[w, v, x] · F_{k}x′; r[w,α,x]·F_{k}x′; r[w, v, x] · F_{k}x′; r[w, v, x · x′]; ρ_{r}]

which commutes, the left square by right equivariance of μ and the right square by naturality of ρ_{r}.

To prove equivariance for case (2) we replace the path x by a path (x, y, z) where x and z are paths of lengths i and k − i and y a single arrow. We must show that the following diagram commutes

[figure: [qw] · (n · m)v · [px] · [p(y · z)]; [qw] · (n · m)v · [p(x · y)] · [pz]; [qw] · (n · m)v · [px] · F_{i}y · [pz]; [qw] · (n · m)v · [px] · [p(y · z)]; 1·λ_{p_{i+1}}·1; [qw] · (n · m)v · [px] · F_{i}y · [pz]; [qw] · (n · m)v · [p(x · y)] · [pz]; 1·ρ_{p_{i}}·1; [qw] · (n · m)v · [px] · [p(y · z)]; r[w, v, x, y, z]; μ̄(w,v,x,y·z); [qw] · (n · m)v · [px] · [p(y · z)]; [qw] · (n · m)v · [p(x · y)] · [pz]; [qw] · (n · m)v · [p(x · y)] · [pz]; r[w, v, x, y, z]; μ̄(w,v,x·y,z)]

If we precede this by [qw] · j_{α} · [px] · F_{i}y · [pz] we get the corresponding diagram for μ followed by r[w, α, x, y, z]. This uses the definition of μ̄ and the fact that j_{α} and ρ_{p_{i}} (resp. λ_{p_{i+1}}) act on different factors and so can be permuted.

For case (3) we must show that

[figure: [qw] · (n · m)v · [p(x′ · x)]; r[w, v, x′, x]; μ̄(w,v,x′·x); [qw] · (n · m)v · F x′ · [px]; [qw] · (n · m)v · [p(x′ · x)]; 1·λ_{p_{1}}·1; [qw] · (n · m)v · F x′ · [px]; [qw] · (n · m)(v · x′) · F x′ · [px]; 1·ρ_{n·m}·1; [qw] · (n · m)(v · x′) · F x′ · [px]; r[w, v, x′, x]; μ̄(w,v·x′,x)]

commutes. Now we must use the definition of ρ_{n·m} (proposition 2.3.1), which gives the commutative

[figure: [qw] · (n · m)v · F x′ · [px]; [qw] · (n · m)(v · x′) · [px]; 1·ρ_{n·m}·1; [qw] · nv_{2} · mv_{1} · F x′ · [px]; [qw] · (n · m)v · F x′ · [px]; 1·j_{α}·1; [qw] · nv_{2} · mv_{1} · F x′ · [px]; [qw] · nv_{2} · m(v_{1} · x′) · [px]; 1·ρ_{m}·1; [qw] · nv_{2} · m(v_{1} · x′) · [px]; [qw] · (n · m)(v · x′) · [px]; 1·j_{α·x′}·1]

that we paste on top of the diagram we want to commute. We use the definition of μ̄ and the fact that 1 · j_{α} · 1 and 1 · λ_{p_{1}} · 1 act on different factors to permute them, to get

[figure: [qw] · (n · m)v · [p(x′ · x)]; r[w, v, x′, x]; μ̄(w,v,x′·x); [qw] · nv_{2} · mv_{1} · [p(x′ · x)]; [qw] · (n · m)v · [p(x′ · x)]; 1·j_{α}1; [qw] · nv_{2} · mv_{1} · [p(x′ · x)]; r[w, v_{2}, v_{1}, x′, x]; r[w, v_{2}, v_{1}, x′, x]; r[w, v, x′, x]; r[w,α,x′,x]; [qw] · nv_{2} · mv_{1} · [p(x′ · x)]; r[w, v_{2}, v_{1}, x′, x]; μ(w,v_{2},v_{1},x′·x); [qw] · nv_{2} · mv_{1} · F x′ · [px]; [qw] · nv_{2} · mv_{1} · [p(x′ · x)]; 1·λ_{p_{1}}·1; [qw] · nv_{2} · mv_{1} · F x′ · [px]; [qw] · nv_{2} · m(v_{1} · x′) · [px]; 1·ρ_{n}·1; [qw] · nv_{2} · m(v_{1} · x′) · [px]; r[w, v_{2}, v_{1}, x′, x]; μ(w,v_{2},v_{1}·x′,x)]

The top square commutes by equivariance of μ and the bottom by definition of μ̄.

Case (4) is somewhere between cases (1) and (3) and so is its proof. We must establish the commutativity of

[figure: [qw] · (n · m)(v · x); r[w, v · x]; μ̄(w,v·x); [qw] · (n · m)v · F_{0}x; [qw] · (n · m)(v · x); 1·ρ_{n·m}; [qw] · (n · m)v · F_{0}x; r[w, v] · F_{0}x; μ̄(w,v)·F_{0}x; r[w, v] · F_{0}x; r[w, v · x]; ρ_{r}]

Paste onto this the commutative diagram (proposition 2.3.1)

[figure: [qw] · nv_{1} · m(v_{2} · x); [qw] · (n · m)(v · x); 1·j_{α·x}; [qw] · nv_{1} · mv_{2} · F_{0}x; [qw] · nv_{1} · m(v_{2} · x); 1·ρ_{m}; [qw] · nv_{1} · mv_{2} · F_{0}x; [qw] · (n · m)v · F_{0}x; 1·j_{α}1; [qw] · (n · m)v · F_{0}x; [qw] · (n · m)(v · x); 1·ρ_{n·m}]

and use the definition of μ̄ to get

[figure: [qw] · nv_{1} · m(v_{2} · x); r[w, v_{1}, v_{2} · x]; μ(w,v_{1},v_{2}·x); [qw] · nv_{1} · mv_{2} · F_{0}x; [qw] · nv_{1} · m(v_{2} · x); 1·ρ_{m}; [qw] · nv_{1} · mv_{2} · F_{0}x; r[w, v_{1}, v_{2}] · F_{0}x; μ(w,v_{1},v_{2})·F_{0}x; r[w, v_{1}, v_{2}] · F_{0}x; r[w, v_{1}, v_{2} · x]; ρ_{r}; r[w, v_{1}, v_{2} · x]; r[w, v · x]; r[w,α·x]; r[w, v_{1}, v_{2}] · F_{0}x; r[w, v_{1}, v_{2} · x]; r[w, v_{1}, v_{2}] · F_{0}x; r[w, v] · F_{0}x; r[w,α]·F_{0}x; r[w, v] · F_{0}x; r[w, v · x]; ρ_{r}]

which commutes, the left square by right equivariance of μ and the right square by naturality of ρ_{r}.

The other four cases are dual.

5. Complements

5.1. Identities In this section we show that for arbitrary 𝔸 and 𝕏, identities are strongly representable in 𝕃ax(𝔸, 𝕏). This justifies our claim in [15], theorem 4.3. It is also necessary in order to see that, under the hypotheses of theorem 4.0.1, 𝕃ax(𝔸, 𝕏) is a double category.

We have to check this separately because, for one thing, nullary modulations are not exactly the specialization of multimodulations to the nullary case, although a more global definition of multimodulation than the one given above would indeed show it in that light. Another reason is that, as Peter Lumsdaine has pointed out, our AFP is a binary condition and those usually come with a corresponding nullary one. But if we generalize our AFP to n-ary factorizations, which is easily enough done, and then specialize to n = 0, we get a ridiculously strong condition, which says (in part) that every cell

[figure: A; C; g; B; A; f; B; C; •; v; α]

factors as

A [figure: f][figure: B; C; B; B; B; C; •; v; ᾱ]

which implies that B = C and g = f.

We recall the definition of the module we called id_{F} (in corollary 3.19 of [15]) and Id_{G} (in theorem 4.3 of [15]).

5.1.1. Definition. For any lax functor F : 𝔸 [figure] 𝕏 there is a canonical module id_{F} : F [figure: •] F defined by the formulas

id_{F} (v) = F (v) : F A [figure: •] F Ā
id_{F} (σ) = F (σ) : F v [figure] F w
λ_{id_{F}} (v̄, v) = ϕ_{F} (v̄, v) : F v̄ · F v [figure] F (v̄ · v)
ρ_{id_{F}} (v̄, v) = ϕ_{F} (v̄, v) : F v̄ · F v [figure] F (v̄ · v).

5.1.2. Proposition. The above definitions make id_{F} into a module F [figure: •] F.

Proof. Condition (M3) follows immediately from (LF3), (M4) from (LF4), (M5) and (M6) from (LF5).

5.1.3. Definition. If t : F [figure] G is a natural transformation between the lax functors F and G, there is a canonical modulation id_{t} : id_{F} [figure] id_{G} defined by

id_{t}(v) = t(v) : F v [figure] Gv.

5.1.4. Proposition. The above definition makes id_{t} into a modulation.

Proof. Condition (m2) follows immediately from (NT2) and condition (m3) from (NT3).

We also recall the definition of null modulation. Conditions (nm1) and (nm2) below are just a specialization of (mm1) and (mm2) from section 1 above, but (mm3), (mm3_{l}) and (mm3_{r}) don’t make sense when n = 0 and must be replaced by (nm3).

5.1.5. Definition. Let F, G_{0}, G_{1} be lax functors 𝔸 [figure] 𝕏 and p : G_{0} [figure: •] G_{1} a module, t : F [figure] G, s : F [figure] H natural transformations. A null modulation

μ : F [figure] p

[figure: F; H; s; G; F; t; G; H; •; p; μ]

consists of the following data:

(nm1) For every object A, a cell

μA : id_{F A} [figure] p(id_{A}).

These must satisfy

(nm2) (Horizontal naturality) For any horizontal arrow f : A [figure] A′,

[figure: p(id_{A}); p(id_{A′}); p(id_{f}); ^{id^{F A}}; p(id_{A}); μA; ^{id^{F A}}; ^{id^{F A′}}; ^{id^{F f}}; ^{id^{F A′}}; p(id_{A′}); μA′]

commutes.

(nm3) (Equivariance) For every vertical arrow v : A [figure: •] Ā,

[figure: Hv · p(id_{A}); p(v · id_{A}); λ_{p}; F v · id_{F A}; Hv · p(id_{A}); sv·μA; F v · id_{F A}; id_{F Ā} · F v; ≅; id_{F Ā} · F v; p(v · id_{A}); p(v · id_{A}); p(idĀ · v); ≅; id_{F Ā} · F v; p(v · id_{A}); id_{F Ā} · F v; p(idĀ) · Gv; μĀ·tv; p(idĀ) · Gv; p(idĀ · v); ρ_{p}]

commutes.

We can now define the null modulation ι which will turn out to be the universal one.

5.1.6. Definition. For any lax functor F we let

ιA = ϕA : id_{F A} [figure] F (id_{A}).

5.1.7. Proposition. ι is a null modulation from F into id_{F}.

Proof. Conditions (nm2) and (nm3) follow immediately from (LF4) and (LF5) respectively.

There are two bimodulations associated with an arbitrary module m : F [figure: •] G which will be useful in the proof below.

5.1.8. Definition. For a module m : F [figure: •] G we have bimodulations

λ : id_{G}, m [figure] m
ρ : m, id_{F} [figure] m

defined by

λ(v_{2}, v_{1}) = λ_{m}(v_{2}, v_{1}) : Gv_{2} · mv_{1} [figure] m(v_{2} · v_{1})
ρ(v_{2}, v_{1}) = ρ_{m}(v_{2}, v_{1}) : mv_{2} · F v_{1} [figure] m(v_{2} · v_{1})

i.e. λ and ρ are the left and right actions for m.

5.1.9. Proposition. λ and ρ are bimodulations and satisfy

[figure: G; G; G; G; G; G; •; ^{id^{G}}; G; G; F; G; F; G; •; m; F; G; F; F; F; G; •; m; G; G; G; G; G; G; •; G; G; F; G; F; G; •; m; F; G; F; F; F; G; •; ι; 1_{m}; λ; =; 1_{m}; =; G; G; F; G; F; G; •; m; F; G; F; F; F; G; •; m; F; F; F; F; F; F; •; ^{id^{F}}; G; G; F; G; F; G; •; F; G; F; F; F; G; •; m; F; F; F; F; F; F; •; ι; 1_{m}; ρ]

Proof. The conditions for λ and ρ to be bimodulations correspond to those for m to be a module. For λ, e.g., (mm2) is (M4), (mm3) and (mm3_{l}) are the first condition of (M6), and (mm3_{r}) is the second condition of (M6).

Evaluating λ(ι, 1_{m}) at v : A [figure: •] Ā gives the commutative

[figure: id_{GĀ} · mv; G(idĀ) · mv; γĀ·mv; id_{GĀ} · mv; m(idĀ · v); G(idĀ) · mv; m(idĀ · v); λ_{m}(idĀ,v); mv; id_{GĀ} · mv; ≅; mv; m(idĀ · v); ≅]

by (M5), and this is the first equation above.

The argument for ρ is dual.

5.1.10. Theorem. Identities in 𝕃ax(𝔸, 𝕏) are strongly represented by id_{F} with universal null modulation ι.

Proof. We first prove weak representability. Given a null modulation μ : F [figure] r we want to show that there is a unique modulation μ̄ : id_{F} [figure] r such that

[figure: F; F; F; F; F; F; •; ^{id^{F}}; F; L; t; F; F; •; F; K; s; K; L; •; r; =; F; L; t; K; F; s; K; L; •; r; ι; μ̄; μ]

i.e. for every A

[figure: ^{id^{F A}}; r(id_{A}); μA; F (id_{A}); ^{id^{F A}}; ϕA; F (id_{A}); r(id_{A}); μ̄(id_{A})]

commutes. If μ̄ exists, its left associativity gives commutativity of the middle part of the diagram

[figure: F v · id_{F A}; Lv · r(id_{A}); tv·μA; F v · F (id_{A}); F v · id_{F A}; F v·ϕA; F v · F (id_{A}); Lv · r(id_{A}); tv·μ̄(id_{A}); Lv · r(id_{A}); r(v · id_{A}); λ_{r}(v,id_{A}); F v · F (id_{A}); Lv · r(id_{A}); F v · F (id_{A}); F (v · id_{A}); ϕ(v,id_{A}); F (v · id_{A}); r(v · id_{A}); μ̄(v·id_{A}); r(v · id_{A}); r(v); ≅; F (v · id_{A}); r(v · id_{A}); F (v · id_{A}); F (v); ≅; F (v); r(v); μ̄v]

The right square commutes by naturality of μ̄ and the triangle by functoriality of vertical composition and the defining property of μ̄ above. The right unit law for F says that the top composite is a canonical isomorphism, so μ̄v is uniquely determined.

In fact μ̄v is the composite

F v [figure: ≅] F v · id_{F A} [figure: tv·μA] Lv · r(id_{A}) [figure: λ_{r}(v,id_{A})] r(v · id_{A}) [figure: ≅] rv

which is the composite modulation

[figure: F; L; L; F; L; L; •; ^{id^{L}}; L; F; F; L; F; F; •; ^{id^{F}}; F; L; K; F; K; L; •; r; L; L; L; L; L; L; •; L; L; K; L; K; L; •; r; K; L; K; K; K; L; •; μ; ^{id^{t}}; λ]

at v. So μ̄ is a modulation. That it satisfies the required commutativity condition follows from the equalities

[figure: F; F; F; F; F; F; •; ^{id^{F}}; F; L; t; L; F; L; L; •; ^{id^{L}}; L; F; F; L; F; F; •; F; L; t; K; F; s; K; L; •; r; L; L; L; L; L; L; •; L; L; K; L; K; L; •; r; K; L; K; K; K; L; •; ι; ^{id^{t}}; μ; λ; =]

[figure: F; L; t; K; F; s; K; L; •; r; L; L; L; L; L; L; •; ^{id^{L}}; L; L; K; L; K; L; •; K; L; K; K; K; L; •; r; L; L; L; L; L; L; •; L; L; K; L; K; L; •; r; K; L; K; K; K; L; •; μ; ι; 1_{r}; λ; =; F; L; t; K; F; s; K; L; •; r; μ]

The validity of these equations is checked by evaluating at A to get

[figure: r(id_{A}); id_{LA} · r(id_{A}); ≅; r(id_{A}); r(id_{A}); id_{LA} · r(id_{A}); r(id_{A}); ≅; r(id_{A}); r(id_{A} · id_{A}); ≅; id_{LA} · r(id_{A}); r(id_{A}); id_{LA} · r(id_{A}); L(id_{A}) · r(id_{A}); L(id_{A}) · r(id_{A}); r(id_{A} · id_{A}); λ_{r}(id_{A},id_{A}); r(id_{A}); id_{LA} · r(id_{A}); ^{id^{F A}}; r(id_{A}); μA; ^{id^{F A}}; id_{F A} · id_{F A}; ≅; id_{F A} · id_{F A}; id_{LA} · r(id_{A}); id_{tA}·μA; id_{LA} · r(id_{A}); L(id_{A}) · r(id_{A}); lA·1; id_{F A} · id_{F A}; id_{LA} · r(id_{A}); id_{F A} · id_{F A}; F (id_{A}) · id_{F A}; ϕA·1; F (id_{A}) · id_{F A}; L(id_{A}) · r(id_{A}); t(id_{A})·μa]

where lA is the structure morphism for L and the top right square commutes by the unit law for t (NT3). The bottom square is the unit law for ι. The top diagram above corresponds to the path top, right, bottom, and the second diagram to the path right, down, right, down, left.

To prove strong representability, we adopt the notation of 4.6. Thus we start with paths of modules

p = F_{k} [figure: •; p_{k}] F_{k−1} [figure: •; p_{k−1}] … [figure: •; p_{1}] F_{0}
q = H_{0} [figure: •; q_{1}] H_{1} [figure: •; q_{2}] … [figure: •; q_{l}] H_{l}

with F_{0} = F = H_{0}. We have to show that for any multimodulation μ : q, p [figure] r, there is a unique multimodulation μ̄ : q, id_{F} , p [figure] r such that

[figure: q, p; r; μ; q, p; q, id_{F} , p; q,ι,p; q, id_{F} , p; r; μ̄]

commutes.

Thus for paths of vertical arrows

x = A_{k} [figure: •; x_{k}] A_{k−1} [figure: •; x_{k−1}] … [figure: •; x_{1}] A_{0}
w = C_{0} [figure: •; w_{1}] C_{1} [figure: •; w_{2}] … [figure: •; w_{l}] C_{l}

with A_{0} = A = C_{0}, we must have commutativity of

[figure: [qw] · id_{F A} · [px]; r[w, id_{A}, x]; [qw] · id_{F A} · [px]; [qw] · F (id_{A}) · [px]; 1·ϕA·1; [qw] · F (id_{A}) · [px]; r[w, id_{A}, x]; μ̄(w,id_{A},x); [qw] · [px]; [qw] · id_{F A} · [px]; ≅; r[w, id_{A}, x]; r[w, x]; ≅; [qw] · [px]; r[w, x]; μ(w,x)]

We’ve already considered the case where both x and w are empty, so we can assume that one of them is not, say x (the other case being dual).

Now, take x and w as above but with y : A_{0} [figure: •] C_{0}. Then if μ̄ does exist, inner equivariance says that

[figure: [qw] · F (id_{A_{0}} · y) · [px]; r[w, id_{A_{0}}, y, x]; μ̄(w,id_{A_{0}}·y,x); [qw] · F (id_{A_{0}}) · F (y) · [px]; [qw] · F (id_{A_{0}} · y) · [px]; 1·ϕ(id_{A_{0}},y)·1; [qw] · F (id_{A_{0}}) · F (y) · [px]; [qw] · F (id_{A_{0}}) · [p(y · x]; 1·λ_{p_{1}}·1; [qw] · F (id_{A_{0}}) · [p(y · x]; r[w, id_{A_{0}}, y, x]; μ̄(w,id_{A_{0}},y·x)]

commutes. If we precede this square by 1 · ϕA_{0} · 1, the bottom composite gives the commutative

[figure: r[w, y, x]; r[w, id_{A_{0}}, y, x]; ≅; [qw] · F y · [px]; r[w, y, x]; μ̄(w,y,x); [qw] · F y · [px]; [qw] · F (id_{A_{0}} · y) · [px]; ≅; [qw] · F (id_{A_{0}} · y) · [px]; r[w, id_{A_{0}}, y, x]; μ̄(w,id_{A_{0}}·y,x); [qw] · F y · [px]; [qw] · F (id_{A_{0}} · y) · [px]; [qw] · id_{A_{0}} · F y · [px]; [qw] · F y · [px]; ≅; [qw] · id_{A_{0}} · F y · [px]; [qw] · F (id_{A_{0}}) · F y · [px]; 1·ϕA_{0}·1; [qw] · F (id_{A_{0}}) · F y · [px]; [qw] · F (id_{A_{0}} · y) · [px]; 1·ϕ(id_{A},y)·1]

The top composite gives the commutative

[figure: r[w, y, x]; r[w, id_{A_{0}}, y, x]; ≅; [qw] · [p(y · x)]; r[w, y, x]; μ(w,y·x); [qw] · [p(y · x)]; r[w, id_{A_{0}}, y, x]; [qw] · [p(y · x)]; [qw] · id_{F A_{0}} · [p(y · x)]; [qw] · [p(y · x)]; ≅; [qw] · id_{F A_{0}} · [p(y · x)]; [qw] · F (id_{A_{0}}) · [p(y · x)]; 1·ϕA_{0}·1; [qw] · F (id_{A_{0}}) · [p(y · x)]; [qw] · id_{F A_{0}} · [p(y · x)]; [qw] · F (id_{A_{0}}) · [p(y · x)]; [qw] · F y · [px]; [qw] · id_{F A_{0}} · [p(y · x)]; 1·λ_{p_{1}}·1; [qw] · F y · [px]; [qw] · F (id_{A_{0}} · y) · [px]; 1·ϕA_{0}·1; [qw] · F (id_{A_{0}} · y) · [px]; [qw] · F (id_{A_{0}}) · [p(y · x)]; 1·λ_{p_{1}}·1; [qw] · F (id_{A_{0}}) · [p(y · x)]; r[w, id_{A_{0}}, y, x]; μ̄(w,id_{A_{0}},y·x)]

where the unlabeled isomorphisms are canonical. This shows that μ̄, if it exists, is unique. In fact we can solve for μ̄(w, y, x). It is the composite

[qw] · F y · [px] [figure: 1·λ_{p_{1}}·1] [qw] · [p(y · x)] [figure: μ(w,y·x)] r[w, y, x].

If we write p as p_{1}, p′ we see that this means that μ̄ is the composite of multimodulations μ(1, λ, 1)

[figure: H_{l}; H_{l}; F; H_{l}; •; q; F; F; F; H_{l}; •; q; F; F; F; F; •; ^{id^{F}}; F; F; F; F_{1}; F; •; p_{1}; F_{1}; F_{1}; F_{1}; F_{1}; F_{1}; F_{k}; F_{1}; •; p′; F_{k}; F_{k}; F_{k}; F_{1}; •; p′; H_{l}; L; F_{k}; H_{l}; F_{k}; K; K; L; •; r; F_{1}; F; •; p_{1}; 1; λ; 1; μ]

where λ is the bimodulation of proposition 5.1.9. It follows immediately that μ̄ is a multimodulation. By the same proposition it also follows that μ̄(1, ι, 1) = μ. This completes the proof.

5.2. Reduction to [5] In this section we show that if 𝔸 and 𝕏 are bicategories, i.e. all horizontal arrows are identities, our colimit formula for m·n (definition 2.2.3) is equivalent to the one given in [5], §2.4. By proposition 2.2.1, a cocone κ on Γ_{v} is given by a family of cells

κ(β) : nv_{2} · mv_{1} [figure] x

indexed by lax factorizations of v satisfying two conditions: (a) transfer of scalars and (b) naturality. A cocone on their diagram is also a family κ(β) : nv_{2} · m_{1} [figure] x as above satisfying just one condition (c): For all β, γ_{1}, β_{2}, γ_{2}, β_{1}(1 · γ_{1}) = β_{2}(γ_{2} · 1) as in

[figure: Ā; Ā; A_{2}; Ā; •; w_{3}; A_{2}; A_{2}; A_{2}; Ā; •; w_{3}; A_{2}; A_{2}; A_{1}; A_{2}; •; w_{2}; A_{1}; A_{2}; A_{1}; A; A_{1}; •; w_{1}; A; A; A; A_{2}; A_{2}; A; A_{2}; A; A; A; A_{2}; •; v_{1}; 1; γ_{1}; Ā; Ā; A_{2}; Ā; •; A_{2}; Ā; A_{2}; A; A_{2}; •; v_{1}; A; A; A; Ā; Ā; A; Ā; A; A; A; Ā; •; v; β_{1}; =; Ā; Ā; A_{2}; Ā; •; w_{1}; A_{2}; Ā; A_{2}; A_{1}; A_{2}; •; w_{2}; A_{1}; A_{1}; A_{1}; Ā; Ā; A_{1}; Ā; A_{1}; A_{1}; A_{1}; Ā; •; v_{2}; A_{1}; A_{1}; A; A_{1}; •; w_{1}; A; A; A; A_{1}; •; w_{1}; γ_{2}; 1; Ā; Ā; A; Ā; A; A; A; Ā; •; v; β_{2}]

we have the commutative hexagon

[figure: nw_{3} · Gw_{2} · mw_{1}; nw_{3} · m(w_{2} · w_{1}); 1·λ_{m}; n(w_{3} · w_{2}) · mw_{1}; nw_{3} · Gw_{2} · mw_{1}; ρ_{n}·1; n(w_{3} · w_{2}) · mw_{1}; nw_{3} · m(w_{2} · w_{1}); nw_{3} · m(w_{2} · w_{1}); nw_{3} · mv_{1}; 1·mγ_{1}; n(w_{3} · w_{2}) · mw_{1}; nw_{3} · m(w_{2} · w_{1}); n(w_{3} · w_{2}) · mw_{1}; nv_{2} · mw_{1}; nγ_{2}·1; nv_{2} · mw_{1}; nw_{3} · mv_{1}; x; nw_{3} · mv_{1}; κβ_{1}; nv_{2} · mw_{1}; x; κβ_{2}; nv_{2} · mw_{1}; nw_{3} · mv_{1}]

If κ satisfies (a) and (b) then it satisfies (c) as can be seen from

[figure: nw_{3} · Gw_{2} · mw_{1}; nw_{3} · m(w_{2} · w_{1}); 1·λ_{m}; n(w_{3} · w_{2}) · mw_{1}; nw_{3} · Gw_{2} · mw_{1}; ρ_{n}·1; n(w_{3} · w_{2}) · mw_{1}; nw_{3} · m(w_{2} · w_{1}); nw_{3} · m(w_{2} · w_{1}); nw_{3} · mv_{1}; 1·mγ_{1}; n(w_{3} · w_{2}) · mw_{1}; nw_{3} · m(w_{2} · w_{1}); n(w_{3} · w_{2}) · mw_{1}; nv_{2} · mw_{1}; nγ_{2}·1; nv_{2} · mw_{1}; nw_{3} · mv_{1}; x; nw_{3} · mv_{1}; κβ_{1}; nv_{2} · mw_{1}; x; κβ_{2}; nv_{2} · mw_{1}; nw_{3} · mv_{1}; n(w_{3} · w_{2}) · mw_{1}; x; κ(β_{2}(γ_{2}·1)); nw_{3} · m(w_{2} · w_{1}); x; κ(β_{1}(1·γ_{1})); (a); (b); (b)]

On the other hand, (a) is a special case of (c) where γ_{1} and γ_{2} are identities. Showing that naturality (condition (b)) follows from (c) is a bit trickier. Let β : v_{2} · v_{1} [figure] v and β′ : v′_{2} · v′_{1} [figure] v be lax factorizations of v such that β′(θ_{2} · θ_{1}) = β for θ_{i} : v_{i} [figure] v′_{i}. We have to show that

[figure: x; nv′_{2} · mv′_{1}; κβ′; nv_{2} · mv_{1}; x; κβ; nv_{2} · mv_{1}; nv′_{2} · mv′_{1}; nθ_{2}·mθ_{1}]

commutes. A consequence of (c) is the following. Let γ_{1} : w_{1}  [figure] v_{1} and γ_{2} : w_{2}  [figure] v_{2},
β_{1} : w_{2} · v_{1}  [figure] v, β_{2} : v_{2} · w_{1}  [figure] v be such that β_{1}(1 · γ_{1}) = β_{2}(γ_{2} · 1). Then the pentagon

of condition (c) when applied to the situation

[figure: Ā; Ā; A_{1}; Ā; •; w_{2}; A_{1}; A_{1}; A_{1}; Ā; •; w_{2}; A_{1}; A_{1}; A_{1}; A_{1}; •; ^{id^{A1}}; A_{1}; A_{1}; A_{1}; A; A_{1}; •; w_{1}; A; A; A; A_{1}; A_{1}; A; A_{1}; A; A; A; A_{1}; •; v_{1}; 1; γ̄_{1}; Ā; Ā; A_{1}; Ā; A_{1}; Ā; A_{1}; A; A_{1}; •; A; A; A; Ā; Ā; A; Ā; A; A; A; Ā; •; v; β_{1}; =; Ā; Ā; A_{1}; Ā; •; w_{2}; A_{1}; Ā; A_{1}; A_{1}; A_{1}; •; ^{id^{A1}}; A_{1}; A_{1}; A_{1}; A_{1}; A_{1}; A; A_{1}; •; w_{1}; A; A; A; A_{1}; w_{1}; Ā; Ā; A_{1}; Ā; A_{1}; A_{1}; A_{1}; Ā; •; v_{2}; γ̄_{2}; 1; Ā; Ā; A_{1}; Ā; A_{1}; Ā; A_{1}; A; A_{1}; A; A; A; Ā; Ā; A; Ā; A; A; A; Ā; •; v; β_{2}]

and preceded by

nw_{2} · mw_{1} [figure: •; ≅] nw_{2} · id_{GA_{1}} · mw_{1} [figure: •; 1·γA_{1}·1] nw_{2} · G(id_{A_{1}}) · mw_{1}

reduces to

[figure: nw_{2} · mw_{1}; nw_{2} · mv_{1}; 1·mγ_{1}; nv_{2} · mw_{1}; nw_{2} · mw_{1}; nγ_{2}·1; nv_{2} · mw_{1}; nw_{2} · mv_{1}; x; nw_{2} · mv_{1}; κβ_{1}; nv_{2} · mw_{1}; x; κβ_{2}; nv_{2} · mw_{1}; nw_{2} · mv_{1}]

being commutative. Now specialize this to

γ_{1} = θ_{1}, β_{1} = β′

and

γ_{2} = 1_{v′}_{2}, β_{2} = β′(1 · θ_{1})

to get commutativity of

[figure: nv′_{2} · mv_{1}; nv′_{2} · mv′_{1}; 1·mθ_{1}; nv′_{2} · mv_{1}; x; κ(β′(1·θ_{1})); x; nv′_{2} · mv′_{1}; κβ′]

Then let

γ_{1} = 1_{v_{1}}, β_{1} = β

and

γ_{2} = θ_{2}, β_{2} = β′(1 · θ_{1})

COMPOSITION OF MODULES FOR LAX FUNCTORS  443

to get commutativity of

[figure: nv_{2} · mv_{1}; x; κβ; nv′_{2} · mv_{1}; nv_{2} · mv_{1}; nθ_{2}·1; nv′_{2} · mv_{1}; x; κ(β′(1·θ_{1}))]

Pasting these two diagrams along κ(β′(1 · θ_{1}) gives the required commutativity (b).

Thus we see that, when 𝔸 and 𝕏 are bicategories (i.e., double categories whose horizontal arrows are all identities) our construction is equivalent to that of [5]. It follows that composition of modules is associative up to coherent isomorphism as claimed in loc. cit.

References

[1] J. Bénabou, Introduction to Bicategories, Springer Lect. Notes in Math. (Reports of the Midwest Category Seminar) 47, 1967, 1-77

[2] A. Burroni, T -catégories (catégories dans un triple), Cahiers de Topologie et Géométrie Différentielle XII-3, 1971, 215-321

[3] M. Clementino, D. Hofmann, W. Tholen, One setting for all: metric, topology, uniformity, approach structure, Applied Categorical Structures 12, 2004, 127-154

[4] J.R.B. Cockett, J. Koslowski, R.A.G. Seely, Morphisms and Modules for Poly-bicategories, Theory and Applications of Categories 11(2), 2003, 15-74

[5] J.R.B. Cockett, J. Koslowski, R.A.G. Seely, R.J. Wood, Modules, Theory and Applications of Categories 11(17), 2003, 375-396

[6] G.S.H. Cruttwell, M. Shulman, A Unified Framework for Generalized Multicategories, Theory and Applications of Categories 24(21), 2010, 580-655

[7] R.J.M. Dawson, R. Paré, D.A. Pronk, Universal properties of Span, Theory and Applications of Categories (The Carboni Festschrift) 13(4), 2005, 61-85

[8] M. Grandis and R. Paré, Limits in double categories, Cahiers de Topologie et Géométrie Différentielle Catégorique XL-3, 1999, 162-220

[9] M. Grandis and R. Paré, Adjoint for double categories, Cahiers de Topologie et Géométrie Différentielle Catégorique XLV-3, 2004, 193-240

[10] C. Hermida, Representable multicategories, Adv. Math. 151, 2000, 164-225

[11] C. Hermida, From coherent structure to universal properties, J. of Pure and Applied Algebra 165, 2001, 7-61

[12] S. Lack, Icons, Applied Categorical Structures 18, 2010, 289-307

[13] T. Leinster, Higher Operads, Higher Categories, London Math. Soc. Lecture Note Ser. 298, 2004, Cambridge University Press

[14] R. Paré, First Order Theories as Double Lawvere Theories, CT 2009 (Cape Town, South Africa), unpublished

[15] R. Paré, Yoneda theory for double categories, Theory and Applications of Categories 25(17), 2011, 436-489 [16] M. Shulman, Framed bicategories and monoidal fibrations, Theory and Applications of Categories

20(18), 2008, 650-738

[17] R.F.C. Walters, Sheaves and Cauchy-Complete Categories, Cahiers de Topologie et Géométrie Différentielle Catégorique XXII-3, 1981, 283-286

Department of Mathematics and Statistics, Dalhousie University Halifax, NS, Canada, B3H 3J5

Email: pare@mathstat.dal.ca

This article may be accessed at http://www.tac.mta.ca/tac/ or by anonymous ftp at

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/27/16/27-16.{dvi,ps,pdf}

THEORY AND APPLICATIONS OF CATEGORIES (ISSN 1201-561X) will disseminate articles that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. The scope of the journal includes: all areas of pure category theory, including higher dimensional categories; applications of category theory to algebra, geometry and topology and other areas of mathematics; applications of category theory to computer science, physics and other mathematical sciences; contributions to scientific knowledge that make use of categorical methods. Articles appearing in the journal have been carefully and critically refereed under the responsibility of members of the Editorial Board. Only papers judged to be both significant and excellent are accepted for publication. Full text of the journal is freely available in .dvi, Postscript and PDF from the journal’s server at http://www.tac.mta.ca/tac/ and by ftp. It is archived electronically and in printed paper format.

Subscription information Individual subscribers receive abstracts of articles by e-mail as they are published. To subscribe, send e-mail to tac@mta.ca including a full name and postal address. For institutional subscription, send enquiries to the Managing Editor, Robert Rosebrugh, rrosebrugh@mta.ca.

Information for authors The typesetting language of the journal is TEX, and L^{A}TEX2e strongly encouraged. Articles should be submitted by e-mail directly to a Transmitting Editor. Please obtain detailed information on submission format and style files at http://www.tac.mta.ca/tac/.

Managing editor Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca

TEXnical editor Michael Barr, McGill University: barr@math.mcgill.ca

Assistant TEX editor Gavin Seal, Ecole Polytechnique Fédérale de Lausanne:

gavin seal@fastmail.fm

Transmitting editors

Clemens Berger, Université de Nice-Sophia Antipolis, cberger@math.unice.fr Richard Blute, Université d’ Ottawa: rblute@uottawa.ca Lawrence Breen, Université de Paris 13: breen@math.univ-paris13.fr Ronald Brown, University of North Wales: ronnie.profbrown(at)btinternet.com

Valeria de Paiva: valeria.depaiva@gmail.com

Ezra Getzler, Northwestern University: getzler(at)northwestern(dot)edu Kathryn Hess, Ecole Polytechnique Fédérale de Lausanne : kathryn.hess@epfl.ch Martin Hyland, University of Cambridge: M.Hyland@dpmms.cam.ac.uk Anders Kock, University of Aarhus: kock@imf.au.dk Stephen Lack, Macquarie University: steve.lack@mq.edu.au F. William Lawvere, State University of New York at Buffalo: wlawvere@buffalo.edu Tom Leinster, University of Edinburgh, Tom.Leinster@ed.ac.uk Ieke Moerdijk, University of Utrecht: moerdijk@math.uu.nl Susan Niefield, Union College: niefiels@union.edu Robert Paré, Dalhousie University: pare@mathstat.dal.ca Jiri Rosicky, Masaryk University: rosicky@math.muni.cz Giuseppe Rosolini, Università di Genova: rosolini@disi.unige.it Alex Simpson, University of Edinburgh: Alex.Simpson@ed.ac.uk James Stasheff, University of North Carolina: jds@math.upenn.edu Ross Street, Macquarie University: street@math.mq.edu.au Walter Tholen, York University: tholen@mathstat.yorku.ca Myles Tierney, Rutgers University: tierney@math.rutgers.edu Robert F. C. Walters, University of Insubria: robert.walters@uninsubria.it R. J. Wood, Dalhousie University: rjwood@mathstat.dal.ca