Theory and Applications of Categories, Vol. 25, No. 17, 2011, pp. 436–489.

YONEDA THEORY FOR DOUBLE CATEGORIES

ROBERT PARÉ

Abstract. Representables for double categories are defined to be lax morphisms into a certain double category of sets. We show that horizontal transformations from representables into lax morphisms correspond to elements of that lax morphism. Vertical arrows give rise to modules between representables. We establish that the Yoneda embedding is a strong morphism of lax double categories which is horizontally full and faithful and dense.

Introduction

There is no question about the importance of the Yoneda lemma in category theory. It is the basis for categorical universal algebra and, more generally, for categorical model theory. There are enriched versions [14] which specialize to Yoneda embeddings for 2categories which are then easily generalized to bicategories. This was used by Joyal and Street [12] to give an elegant treatment of coherence for bicategories. In another (related) direction is the fundamental work of Street and Walters [20] on abstract Yoneda structures.

Although (weak) double categories may seem a minor generalization of bicategories, Yoneda theory is very different. A straightforward generalization of the 2-categorical case presents some difficulties. If we take the “hom functor” to consist of horizontal arrows, it is not clear what to do with the vertical ones, and vice versa. In fact it is not immediately apparent where representables are to take their values or, for that matter, what sort of morphisms they are.

A careful study of the structure of representables leads to the most basic double category, the double category 𝕊et, of sets, functions and spans. This, we claim, is the natural recipient for representables, which then turn out to be lax morphisms of double categories.

This paper exposes the Yoneda theory for double categories, from the basic lemma characterizing transformations defined on representables (Theorem 2.3) to the Yoneda embedding (Theorem 4.8) and its density (Theorem 4.10).

There are several ways we could have chosen to present the theory.

Research supported by an NSERC grant.

Received by the editors 2011-05-02 and, in revised form, 2011-11-10.

Transmitted by Stephen Lack. Published on 2011-11-17.

2000 Mathematics Subject Classification: 18D05, 18A23, 18A25, 18A40, 18B15.

Key words and phrases: Double category, lax functor, module, modulation, representable, Yoneda lemma.

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

One way, as suggested by the referee, is via the theory of pseudo and lax algebras for 2monads [19]. The free category monad, fc, on the category of graphs is cartesian so lifts to a 2-monad on Cat(Graph), the 2-category of category objects in graphs. Then a pseudo algebra for this monad is an unbiased version of (weak) double category. Lax morphisms of algebras are exactly lax functors, and algebra 2-cells are our natural transformations. Lax algebras correspond to (unbiased) lax double categories. Not only does this provide a more succinct presentation of the basic definitions but it explains why they work so well. Following this line, if we want to capture virtual double categories, we must pass to the double category ℂat(Graph) of categories, functors and profunctors, in Graph, and the extension of fc to a double monad.

A related approach is to consider monoids in a Kleisli double category as explained in [5] and [16], developing the original ideas of Burroni [3]. In this context, it would be interesting to understand why certain natural constructions performed on double categories merely produce virtual double categories in general.

Although [19] deals with a 2-categorical version of the Yoneda lemma, it is too general to be immediately applicable in the present situation. We have chosen a more basic, follow-your-nose, approach. We can look at a (weak) double category in two ways, either as a (horizontal) 2-category in which we carry along its “logic” in the form of some extra vertical arrows (think of sets with functions and relations), or as a (vertical) bicategory in which we specify some rigidifying arrows (the point of view of [18]). Both the theories of 2-categories and the theory of bicategories are well developed, and the basic concepts and results are easily generalized to double categories. Things become interesting when the results don’t generalize straightforwardly, as in the case of the Yoneda lemma. We have followed these ideas and concluded the inevitability of the double category 𝕊et as the basis of double category theory. Along the way, virtual double categories and modules are concepts that also impose themselves. We believe that our process has uncovered interesting concepts which can now be transported back to the more abstract setup.

As the referee pointed out, (weak) double categories are nothing other than Batanin’s monoidal 1-globular categories [1] and 𝕊et is the result of the span construction in this context. He also considered higher dimensional analogues of this notion, and it is hoped that our “nuts and bolts” study will work its way up the dimension chain and yield useful intuitions.

Weber’s work [21] provides further evidence that 𝕊et is a fundamental object of study in 2-dimensional category theory, leading us out of the realm of mere bicategories. It is a colimit completion in his setting. We believe that this will translate back to ours but have not worked through the details yet. His work also views it as a 2-dimensional replacement for the Ω of topos theory, with “true” replaced by the universal opfibration of pointed sets. These are interesting ideas which should be pursued further in relation to the present work.

Finally we mention a related work which has recently appeared on arXiv, that of Fiore, Gambino and Kock [8]. In the course of their work on double adjunctions and monads in double categories, they develop representables (Example 3.4 = our Section 2.1) and a Yoneda theorem (Proposition 3.10 = our Theorem 2.3). Because the Yoneda embedding is not full on vertical arrows, adjointness cannot be characterized as an objectwise representability property as in the case of ordinary adjoints. To remedy this, they introduce presheaves with parameters and parametric representability, which is a useful replacement for something we take for granted in our daily work in categories. Our Theorem 3.18 is in some sense an alternative approach to the same problem. More work is needed to reconcile the two.

A more detailed description of the paper follows.

In section 1, we recall the notions of double category, lax functor, and natural transformation (a.k.a. lax transformation), with illustrative examples chosen to set the scene for later use.

In section 2, we establish, for lax double functors, the familiar version of the Yoneda lemma, giving a bijection between natural transformations defined on representables and elements of the codomain. We illustrate this circle of ideas by giving an application to adjoint double functors.

In section 3, we introduce the appropriate notion of vertical transformation of lax functor in order to study how the representables depend on the vertical structure. This is the double category version of the modules of [4] which are a multiobject version of profunctor. Following [4], we call the cells introduced modulations. This will lead, at the end of the section, to a Yoneda lemma for modules which has as a corollary, a characterization of elements of a lax functor at a vertical arrow in terms of modulations. This, together with the Yoneda lemma of section 2, gives complete information about a lax functor in terms of representables, which will be formalized as the density theorem of section 4. An application to the calculation of tabulators illustrates well the power of these results.

As a computational tool we introduce the double category of elements of a lax functor into 𝕊et. Of course it is much more than a notational convenience. It is central to all of categorical model theory and its use in the proof of Theorem 4.10 is just one aspect of this. We work out in detail the example of a horizontally discrete double category. That is, our domain is just a category A considered as a vertical double category and then everything reduces to category theory in the slice Cat/A. In particular, modules give the “right” definition of profunctor over A.

Finally, in the short section 4, we tie everything together. We define the Yoneda embedding and explain in what sense it is full and faithful, and we show that every lax functor into 𝕊et is a colimit of representables. For this we need to introduce multimodulations, making 𝕃ax(𝔸^{op}, 𝕊et) into a virtual double category. We leave the question of representability of composition of modules to a future paper [17].

1. The Basic Structures

1.1. Double categories

Double categories go back to Ehresmann [7]. They have objects, two kinds of arrows, horizontal and vertical, and cells whose boundaries are squares, horizontal and vertical composition of arrows and cells giving category structures and satisfying middle four interchange on cells. There is a perfect duality between horizontal and vertical.

The double categories we encounter in practice, and certainly in this work, are a weakened version where one of the composites is only associative and unitary up to coherent isomorphism. These weak double categories (also called pseudo double categories) have come up in recent work [9], [6], [18], with different conventions for the weak direction. Our convention is that vertical is the weak direction, as will become evident below. We shall also call them simply double categories and use the term strict double category for the classical notion.

Our basic example is the double category of sets, 𝕊et. Its objects are sets and its horizontal arrows are functions. A vertical arrow from A to B is a span, i.e. a diagram of sets

[figure: A; B; S; A; ( )_{0}; S; B; ( )_{1}]

with composition given by pullback

[figure: A; B; S; A; S; B; B; C; T; B; T; C; S; T; T ⊗ S; S; T ⊗ S; T; Pb]

and vertical identities Id_{A} by

[figure: A; A; A; A; 1_{A}; A; A; 1_{A}]

A cell

[figure: B; B′; g; A; B; •; S; A; A′; f; A′; B′; •; S′; s]

is a commutative diagram

[figure: B; B′; g; S; B; S; S′; s; S′; B′; S; S′; A; S; A; A′; f; A′; S′]

Cells can be composed horizontally giving a category. They can also be composed vertically using the universal property of pullback.

Vertical composition of spans is of course neither strictly associative nor unitary but it is up to canonical special isomorphisms,

α : U ⊗ (T ⊗ S) [figure: ≅] (U ⊗ T) ⊗ S, ρ : S ⊗ Id_{A} [figure: ≅] S, λ : Id_{B} ⊗ S [figure: ≅] S

In general, a special isomorphism is a cell of the form

[figure: B; B; A; B; •; v; A; A; A; B; •; v′]

which has a horizontal inverse. Vertical composition of cells is as strictly associative and unitary as the constraints of domain and codomain permit

[figure: D; D′; C; D; •; U; C; C′; C′; D′; •; U′; C; C′; A; C; •; T ⊗S; A; A′; A′; C′; •; T′⊗S′; D′; D′; D′; B′; B′; D′; •; U′⊗T′; B′; A′; A′; A′; A′; B′; •; S; υ; τ⊗σ; α′; D; D; C; D; •; U; C; D; C; A; C; •; T ⊗S; A; A; A; D; D′; B; D; •; U⊗T; B; B′; B′; D′; •; U′⊗T′; B; B′; A; B; •; S; A; A′; A′; B′; •; S′; α; υ⊗τ; σ; =]

The interchange law, asserting the equality of the two different ways of evaluating

[figure: C; C′; B; C; •; B; B′; B′; C′; •; C′; C′′; B′; C′; •; B′; B′′; B′′; C′′; •; B; B′; A; B; •; A; A′; A′; B′; •; B′; B′′; A′; B′; •; A′; A′′; A′′; B′′; •; τ; τ′; σ; σ′]

holds without qualification.

Similar considerations hold for identities: there are special isomorphisms, λ_{B} : Id_{B} ⊗ S [figure] S, ρ_{A} : S ⊗ Id_{A} [figure] S, and suitably interpreted equalities Id_{g} ⊗ σ = σ, σ ⊗ Id_{f} = σ and Id_{1_{A}} = 1_{Id_{A}}.

For a general (weak) double category the notation is this: the horizontal direction is the dominant one and notation is simpler; multiplication is strict and denoted by juxtaposition and identities are 1_{A}, 1_{f}. The vertical direction is in a sense complementary and provides the two-dimensional structure. It is associative and unitary up to coherent special isomorphism, and the notation is more “fancy”; multiplication is denoted with a dot or a tensor, and identities by id_{A}, id_{f} or Id_{A}, Id_{f}. Vertical arrows are distinguished with a dot.

A closely related example is V-𝕊et. Let V be a monoidal category with coproducts over which ⊗ distributes, i.e. V ⊗ ( ) and ( ) ⊗ V preserve these coproducts. Then V-𝕊et has sets as objects and functions as horizontal arrows. A vertical arrow A [figure: •] B in V-𝕊et is an A × B matrix [V_{ab}] of objects of V, and a cell

[figure: B; B′; g; A; B; •; [V_{ab}]; A; A′; f; A′; B′; •; [W′_{a′b′}]; [x_{ab}]]

is a matrix of morphisms x_{ab} : V_{ab} [figure] W_{fa,gb} of V. Vertical composition is matrix multiplication: for [W_{bc}] : B [figure: •] C, [W_{bc}] ⊗ [V_{ab}] = [∑_{b∈B} W_{bc} ⊗ V_{ab}]. That V-𝕊et is a double category is a straightforward calculation.

A close contender for the most basic double category is ℂat, the double category of small categories, whose objects are small categories and whose horizontal morphisms are functors. A vertical morphism P : A [figure: •] B is a profunctor, i.e. a functor P : A^{op} × B [figure] Set thought of as providing arrows from objects of A to objects of B. Thus an element x ∈ P (A, B) is often denoted by x : A [figure: •; P] B. Functoriality of P allows composition of these arrows by morphisms of A and B. Vertical composition is profunctor composition. Thus if Q : B [figure: •] C, then an element of Q ⊗ P (A, C) is an equivalence class of pairs A [figure: •; x; P] B [figure: •; y; Q] C, denoted y ⊗_{B} x. The equivalence relation

is generated by (yb) ⊗ x = y ⊗ (bx). The identity Id_{A} is, as usual, the hom functor A^{op} × A [figure] Set.

A cell

[figure: B; B′; G; A; B; •; P; A; A′; F; A′; B′; •; P′; t]

is a natural transformation t : P [figure] P′(F −, G−). Thus t is a way of assigning arrows t(x) : F A [figure: •; P′] GB to arrows x : A [figure: •; P] B in a natural way, i.e. t(xa) = t(x)F (a) and

t(bx) = G(b)t(x).

A certain amount of calculation is coded in the statement that ℂat is a double category. There are various reasons for orienting our vertical arrows as we did. One is that a

cell

[figure: A; A′; G; A; A; •; ^{Id^{A}}; A; A′; F; A′; A′; •; ^{Id^{A′}}; t]

is a natural transformation F [figure] G so that the 2-category Cat lies comfortably inside ℂat. Another reason, more relevant to the present paper, is that these correspond to the vertical transformations of lax morphisms which arise as values of our “hom-functor”.

Inevitably, when dealing with profunctors, something gets switched around but in the present context our convention minimizes this. Many people following Bénabou use the word distributor or, following the Australian school, bimodule from A to B for a functor B^{op} × A [figure] Set. Bénabou actually introduced the word “profunctor” with the above convention (A^{op} × B [figure] Set) then changed the convention and later the name. One of the objections to the word “profunctor” was that they are not projective limits of functors, but a functor P : A^{op} × B [figure] Set can be viewed as functor A [figure] (Set^{B})^{op} and then its values are indeed projective limits of representables.

In a similar vein, we also have the double category V-ℂat for V a monoidal category with colimits over which ⊗ distributes. The objects are (small) V-categories, the horizontal arrows V-functors, the vertical arrows V-profunctors, and cells

[figure: B; D; G; A; B; •; P; A; C; F; C; D; •; Q; α]

families of morphisms α(A, B) : P (A, B) [figure] Q(F A, GB) respecting the profunctor actions.

A double category in which the horizontal arrows are all identities is essentially a bicategory and much of the general theory of double categories is a straightforward generalization of bicategory theory. A notable exception is the Yoneda theory presented below. When we wish to consider a bicategory B as the vertical structure of a double category in this way we denote it by 𝕍B.

A 2-category A can be made into a double category in a variety of ways. It can be considered as a bicategory and made into a double category 𝕍A or it can be considered the horizontal part of a double category whose only vertical arrows are identities. This is denoted ℍA. There is also Ehresmann’s double category ℚA of quintets in A. It has the same objects as A, the horizontal arrows and vertical arrows are the same: the 1-cells of A. A cell in ℚA

[figure: B; D; g; A; B; •; h; A; C; f; C; D; •; k; α]

is a 2-cell α : kf [figure] gh.

1.2. Lax functors

It has been known for a long time [2] that the morphisms of bicategories which occur in practice come in various forms, more general than what one might suspect in the first instance. The same is true for double categories.

Recall from [9] that a lax functor of double categories F : 𝔸 [figure] 𝔹 assigns to objects, horizontal arrows, vertical arrows and cells of 𝔸 like ones in 𝔹, respecting boundaries and preserving horizontal composition of arrows and cells but not necessarily vertical composition. Instead, comparison special cells are given: for every A in 𝔸,

[figure: F A; F A; F A; F A; •; ^{id^{F A}}; F A; F A; F A; F A; •; F (id_{A}); ϕ_{A}]

and for every A [figure: •; v] Ā [figure: •; v̄] Ã,

[figure: F Ã; F Ã; F Ā; F Ã; •; F v̄; F Ā; F Ã; F Ā; F A; F Ā; •; F v; F A; F A; F A; F Ã; F Ã; F A; F Ã; F A; F A; F A; F Ã; •; F (v̄·v); ϕ_{v̄,v}]

satisfying unit and associativity laws that look very much like those for a monad, so much so in fact, that a lax functor 1 [figure] 𝔹 is a monad in 𝔹.

An oplax functor is the same sort of thing with the direction of the ϕ_{A} and ϕ_{v̄,v} reversed. A lax (or oplax) functor is normal if the ϕ_{A} are isomorphisms. If the ϕ_{v̄,v} are isomorphisms as well, we say that F is a pseudo functor. If the ϕ_{A} and ϕ_{v̄,v} are identities, we say that F is a (strict) functor. As will become evident later, strict functors are important, even when 𝔸 and 𝔹 are weak.

The discrete category functor Set [figure] Cat extends to a pseudo functor D : 𝕊et [figure] ℂat. In fact, a profunctor between discrete categories is very nearly the same thing as a span between their sets of objects, each being a representation of a matrix of sets. D is a doubly full embedding: it induces a bijection between horizontal arrows A [figure] A′ and horizontal arrows DA [figure] DA′; a bijection between cells v [figure] v′ and cells Dv [figure] Dv′; an equivalence of categories between vertical arrows A [figure: •] Ā and vertical arrows DA [figure: •] DĀ, with special cells as morphisms; and an equivalence of categories between cells f [figure: •] f̄ and cells Df [figure: •] Df̄, with commuting squares of special cells as morphisms.

The object functor Ob : Cat [figure] Set extends to a lax functor ℂat [figure] 𝕊et. On categories and functors it’s the usual thing. For a vertical arrow P : A [figure: •] B, i.e. a functor P : A^{op} × B [figure] Set, we construct the span Ob(P) : Ob(A) [figure: •] Ob(B)

[figure: ObA; ObB; ∑_{A,B} P (A, B); ObA; ∑_{A,B} P (A, B); ObB]

The composite Ob(Q) ⊗ Ob(P) is

[figure: Ob(A); Ob(B); ∑_{A,B,C} Q(B, C) × P (A, B); Ob(A); ∑_{A,B,C} Q(B, C) × P (A, B); Ob(B)]

and Ob(Q ⊗ P) is a quotient of this, giving

(ObQ) ⊗ Ob(P) [figure] Ob(Q ⊗ P)

which is generally not an isomorphism. Ob is not normal either. The identity Id_{A} : A [figure: •] A is the hom functor so Ob(Id_{A}) is the span

[figure: Ob(A); Ob(A); Arr(A); Ob(A); dom; Arr(A); Ob(A); cod]

and the comparison Id_{Ob(A)} [figure] Ob(Id_{A}) is the function Ob(A) [figure] Arr(A) which picks out the identities. Thus Ob : ℂat [figure] 𝕊et is a genuine lax functor.

On the other hand, the connected components functor π_{0} : Cat [figure] Set extends to an oplax normal functor ℂat [figure] 𝕊et. On categories and functors it’s the usual thing. A vertical morphism P : A [figure: •] B has associated to it a category of elements with projection functors giving a span in Cat

[figure: A; B; El(P); A; El(P); B]

to which we can apply π_{0} to get a span in Set. This is π_{0}P : π_{0}A [figure: •] π_{0}B. Thus an element of π_{0}P is an equivalence class of elements of P, x : A [figure: •; P] B, where the equivalence relation is generated by x ∼ x′ if there are a and b such that

[figure: B; B; b; A; B; •; x; A; A; a; A; B; •; x′]

“commutes”.

An element of π_{0}(Q⊗P) is an equivalence class of elements y⊗_{B}x which are themselves equivalence classes. We can combine the two equivalence relations to get a more direct description of π_{0}(Q ⊗ P), namely as the set of equivalence classes of pairs (x, y) as below, where (x, y) ∼ (x′, y′) if there exist a, b, c such that

[figure: B; B′; A; B; •; x; A; A′; a; A′; B′; •; x′; C; C′; c; B; C; •; y; B; B′; b; B′; C′; •; y′]

On the other hand an element of π_{0}Q ⊗ π_{0}P is a pair, ([A [figure: •; x] B], [B′ [figure: •; y] C]), of equivalence classes with B connected to B′. There is a canonical function π_{0}(Q⊗P) [figure] π_{0}Q⊗π_{0}P which takes [A [figure: •; x] B [figure: •; y] C] to ([A [figure: •; x] B], [B [figure: •; y] C]) which is manifestly not a bijection. The identity Id_{A} : A [figure: •] A is the hom functor so π_{0}(Id_{A}) is the span

[figure: π_{0}A; π_{0}A; π_{0}(A^{2}); π_{0}A; π_{0}dom; π_{0}(A^{2}); π_{0}A; π_{0}cod]

which is isomorphic to the identity via π_{0}(id_{A}) : π_{0}A [figure] π_{0}(A^{2}). This is because cod ⊣ id ⊣ dom and π_{0} takes adjoints to isomorphisms. This makes π_{0} : ℂat [figure] 𝕊et an oplax normal functor.

1.3. Remark. The object functor Ob : ℂat [figure] 𝕊et can also be viewed as taking P : A [figure: •] B to

[figure: ObA; ObB; Ob(El(P)); ObA; Ob(El(P)); ObB]

1.4. Remark. The chaotic functor K : Set [figure] Cat can also be made into an oplax normal functor K : 𝕊et [figure] ℂat although it is less interesting. This is because any non empty chaotic category is equivalent to 1 and any profunctor, which can’t distinguish equivalent categories, is constant. But for the record, K(S) : KA^{op} × KB [figure] Set is the constant functor 1 if S ≠ ∅ and the constant functor ∅ if S = ∅.

A lax functor 1 [figure] 𝕊et is easily seen to be a small category. Indeed, as is well-known, a small category is the same as a monad in 𝕊pan, the bicategory of sets and spans, and a lax morphism with domain 1 is a vertical monad.

Similarly, a lax functor 1 [figure] V-𝕊et is a small V-category.

For B and B′ bicategories, a lax functor F : 𝕍B [figure] 𝕍B′ is nothing but a (lax) morphism of bicategories. On the other hand, for 2-categories A and A′, a lax functor F : ℍA [figure] ℍA′ corresponds to a 2-functor.

1.5. Natural Transformations

1.6. Definition. Let 𝔸 and 𝔹 be double categories and F, G : 𝔸 [figure] 𝔹 lax functors. A natural transformation t : F [figure] G assigns to each object A in 𝔸 a horizontal arrow tA : F A [figure] GA in 𝔹 and to each vertical arrow v : A [figure: •] Ā of 𝔸 a cell

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

of 𝔹 satisfying the following conditions: (Horizontal naturality) for every f : A [figure] A′

[figure: F A′; GA′; tĀ; F A; F A′; F f; F A; GA; tA; GA; GA′; Gf]

commutes, and for every cell

[figure: Ā; Ā′; f̄; A; Ā; •; v; A; A′; f; A′; Ā′; •; v′; α]

[figure: F Ā; GĀ; tĀ; F A; F Ā; •; F v; F A; GA; tA; GA; GĀ; •; Gv; tv; GĀ; GĀ′; Gf̄; GA; GĀ; •; GA; GA′; Gf; GA′; GĀ′; •; Gv′; Gα; =; F Ā; F Ā′; F f̄; F A; F Ā; •; F v; F A; F A′; F f; F A′; F Ā′; •; F v′; F α; F Ā′; GĀ′; tĀ′; F A′; F Ā′; •; F A′; GA′; tA′; GA′; GĀ′; •; Gv′; tv′]

(Vertical functoriality) for every A

[figure: F A; F A; F A; F A; •; ^{id^{F A}}; F A; F A; F A; F A; •; ϕA; F A; GA; tA; F A; F A; •; F (id_{A}); F A; GA; tA; GA; GA; •; G(id_{A}); t(id_{A}); =; F A; GA; tA; F A; F A; •; ^{id^{F A}}; F A; GA; tA; GA; GA; •; ^{id^{GA}}; ^{id^{tA}}; GA; GA; GA; GA; •; GA; GA; GA; GA; •; G(id_{A}); γA]

for all v : A [figure: •] Ā, v̄ : Ā [figure: •] Ã

[figure: F Ã; F Ã; F Ā; F Ã; •; F v̄; F Ā; F Ã; F Ā; F A; F Ā; •; F v; F A; F A; F A; F Ã; F Ã; F A; F Ã; F A; F A; F A; F Ã; •; F (v̄·v); ϕ(v̄,v); F Ã; GÃ; tÃ; F A; F Ã; •; F A; GA; tA; GA; GÃ; •; G(v̄·v); t(v̄·v); =; F Ã; GÃ; tÃ; F Ā; F Ã; •; F v̄; F Ā; GĀ; tĀ; GĀ; GÃ; •; Gv̄; tv̄; F Ā; GĀ; F A; F Ā; •; F v; F A; GA; tA; GA; GĀ; •; Gv; tv; GÃ; GÃ; GA; GÃ; GA; GA; GA; GÃ; •; G(v̄·v); γ(v̄,v)]

Natural transformations compose horizontally and vertically giving a 2-category of double categories, lax functors and natural transformations. This may seem a bit paradoxical because, as is well-known, bicategories with lax morphisms and any of the usual 2-cells don’t form a 2-category or bicategory. What makes it work for natural transformations is that they are defined using horizontal arrows and these are well-behaved. Actually this 2-category is part of a larger strict double category 𝔻oub introduced in [9] and about which we will have more to say in the next section.

Returning to our examples of the previous section where we saw that a lax functor 1 [figure] 𝕊et corresponds to a small category, a natural transformation now corresponds to a functor. More generally, a natural transformation between lax functors 1 [figure] V-𝕊et is a V-functor.

For lax morphisms of bicategories F, G : B [figure] B′, natural transformation between the corresponding lax functors 𝕍B [figure] 𝕍B′ are precisely the ICONs of [15]. That’s because all horizontal arrows in 𝕍B′ are identities.

Finally, for 2-functors F, G : A [figure] A′, a natural transformation ℍF [figure] ℍG is the same as a 2-natural transformation.

2. The Yoneda Lemma Part I

2.1. The Hom Functor

Let 𝔸 be a double category and 𝔸^{op} the horizontal dual of 𝔸. Hom will be the lax functor 𝔸^{op} × 𝔸 [figure] 𝕊et defined as follows: (H1) for objects A, B of 𝔸, Hom(A, B) is the set of horizontal arrows f : A [figure] B in 𝔸; (H2) for horizontal morphisms a : A′ [figure] A and b : B [figure] B′, Hom(a, b) is the function taking f to bfa (as usual); (H3) for vertical arrows v : A [figure: •] Ā and w : B [figure: •] B̄, Hom(v, w) is the span

[figure: Hom(A, B); Hom(Ā, B̄); Hom(v, w); Hom(A, B); ∂_{0}; Hom(v, w); Hom(Ā, B̄); ∂_{1}]

where Hom(v, w) is the set of cells

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

and where ∂_{0} and ∂_{1} are vertical domain and codomain, i.e. ∂_{0}ϕ = f, ∂_{1}ϕ = f̄; (H4) for cells

[figure: Ā′; Ā; ā; A′; Ā′; •; v′; A′; A; a; A; Ā; •; v; α; B̄; B̄′; b̄′; B; B̄; •; w; B; B′; b; B′; B̄′; •; w′; β; and]

Hom(α, β) is the function Hom(v, w) [figure] Hom(v′, w′) which takes ϕ to βϕα, which is in fact a morphism of spans, i.e. ∂_{0}, ∂_{1} are preserved; (H5) for every pair of objects, the structural unit

[figure: Hom(A, B); Hom(A, B); Hom(A, B); Hom(A, B); •; ^{Id^{Hom(A,B)}}; Hom(A, B); Hom(A, B); Hom(A, B); Hom(A, B); •; Hom(id_{A},id_{B})]

is given by the function

h(A, B) : Hom(A, B) [figure] Hom(id_{A}, id_{B})
f ⟼ id_{f};

(H6) for composable pairs \xymatrix{A \ar[r]|{•}^{v} & Ā \ar[r]|{•}^{v̄} & Ã} and \xymatrix{B \ar[r]|{•}^{w} & B̄ \ar[r]|{•}^{w̄} & B̃} the structural multiplication for Hom

[figure: Hom(A, B); Hom(v,w); •; h((v̄,w̄),(v,w)); Hom(A, B); Hom(v̄·v,w̄·w); •; Hom(Ā, B̄); Hom(v̄,w̄); •; Hom(Ã, B̃); Hom(Ã, B̃)]

is the function

Hom(v̄, w̄) ⊗ Hom(v, w) [figure] Hom(v̄ · v, w̄ · w)

[figure: Ã; B̃; f̃; Ā; Ã; •; v̄; Ā; B̄; B̄; B̃; •; w̄; ϕ̄; Ā; B̄; f̄; A; Ā; •; v; A; B; f; B; B̄; •; w; ϕ; ⟼; Ã; B̃; f̃; A; Ã; •; v̄·v; A; B; f; B; B̃; •; w̄·w; ϕ̄·ϕ]

which is a morphism of spans.

That Hom is horizontally functorial is obvious, it being instances of the ordinary hom functor. The associativity and unit laws for Hom are easily seen to be just the corresponding ones for 𝔸.

Notice that all of the structure of 𝔸 is used in the definition of Hom. The double category 𝕊et was originally conceived as the recipient of the hom functor.

Of course there could be other ways of defining Hom, for example it could take its values in ℂat. It would then be lax normal. It is hoped that the unity of concepts developed below will convince even the most skeptical reader of the advantages of our choice.

We more often use the notation 𝔸(−, −) instead of Hom, especially when more than one double category is considered.

2.2. The Yoneda Lemma I

Given an object B of 𝔸 we get a lax functor 𝔸(−, B) : 𝔸^{op} [figure] 𝕊et by substituting the pseudo functor 1 [figure] 𝔸 determined by B into the second variable of the hom functor. So in particular 𝔸(v, B) = 𝔸(v, id_{B}).

2.3. Theorem. [Yoneda Lemma I] Let F : 𝔸^{op} [figure] 𝕊et be a lax functor. Then there is a bijection between natural transformations t : 𝔸(−, B) [figure] F and elements x ∈ F B given by x = t(B)(1_{B}).

Proof. Given x ∈ F B we want to construct a natural transformation t_{x} : 𝔸(−, B) [figure] F such that t_{x}(B)(1_{B}) = x. It follows by naturality on horizontal arrows that

t_{x}(A) : 𝔸(A, B) [figure] F A

must be given by

t_{x}(A)(f) = F (f)(x).

In order to determine

[figure: 𝔸(Ā, B); F Ā; t_{x}Ā; 𝔸(A, B); 𝔸(Ā, B); •; 𝔸(v,B); 𝔸(A, B); F A; t_{x}A; F A; F Ā; •; F_{v}; t_{x}v]

450  ROBERT PARÉ

take an element

[figure: Ā; B; f̄; A; Ā; •; v; A; B; f; B; B; •; ^{id^{B}}; ψ]

of 𝔸(v, B). Then

[figure: 𝔸(B, B); 𝔸(B, B); 𝔸(B, B); 𝔸(B, B); •; ^{Id^{𝔸(B,B)}}; 𝔸(B, B); 𝔸(B, B); 𝔸(B, B); 𝔸(B, B); •; 𝔸(id_{B},B); h(B); 𝔸(B, B); 𝔸(Ā, B); 𝔸(f̄,B); 𝔸(B, B); 𝔸(B, B); •; 𝔸(B, B); 𝔸(A, B); 𝔸(f,B); 𝔸(A, B); 𝔸(Ā, B); •; 𝔸(v,B); 𝔸(ψ,B); 𝔸(Ā, B); F Ā; t_{x}Ā; 𝔸(A, B); 𝔸(Ā, B); •; 𝔸(A, B); F A; t_{x}A; F A; F Ā; •; F v; t_{x}v]

is equal to

[figure: 𝔸(B, B); 𝔸(B, B); 𝔸(B, B); 𝔸(B, B); •; ^{Id^{𝔸(B,B)}}; 𝔸(B, B); 𝔸(B, B); 𝔸(B, B); 𝔸(B, B); •; 𝔸(id_{B},B); hB; 𝔸(B, B); F B; t_{x}B; 𝔸(B, B); 𝔸(B, B); •; 𝔸(B, B); F B; t_{x}B; F B; F B; •; F id_{B}; t_{x}id_{B}; F B; F Ā; F f̄; F B; F B; •; F B; F A; F f; F A; F Ā; •; F v; F ψ]

by horizontal naturality, which is then equal to

[figure: 𝔸(B, B); F B; t_{x}B; 𝔸(B, B); 𝔸(B, B); •; ^{Id^{𝔸(B,B)}}; 𝔸(B, B); F B; t_{x}B; F B; F B; •; ^{id^{F B}}; ^{id^{txB}}; F B; F B; F B; F B; •; F B; F B; F B; F B; •; F id_{B}; ϕB; F B; F Ā; F f̄; F B; F B; •; F B; F A; F f; F A; F Ā; •; F v; F ψ]

by the unit law. Take 1_{B} ∈ Id_{𝔸(B,B)}. The top cell

1_{B} ⟼ id_{1_{B}} = 1_{id_{B}} ⟼ 1_{id_{B}}ψ = ψ ⟼ t_{k}(v)(ψ)

and the bottom cell

1_{B} ⟼ x ⟼ ϕ(B)(x) ⟼ F (ψ)ϕ(B)(x)

so we must have

t_{x}(v)(ψ) = F (ψ)ϕ(B)(x).

Obviously t_{x}(B)(1_{B}) = x, so all that remains to be done is to check that t_{x} is indeed a natural transformation, which is an easy calculation.

Specializing to F = 𝔸(−, B′), we see that a natural transformation 𝔸(−, B) [figure] 𝔸(−, B′) corresponds to a horizontal arrow b : B [figure] B′. To be more precise, b defines a natural transformation 𝔸(−, b) : 𝔸(−, B) [figure] 𝔸(−, B′) given by

𝔸(A, b) = 𝔸(1_{A}, b) : 𝔸(A, B) [figure] 𝔸(A, B′)
(f : A [figure] B) ⟼ (bf : A [figure] B′)
𝔸(v, b) = 𝔸(v, id_{b}) : 𝔸(v, id_{B}) [figure] 𝔸(v, id_{B′})

[figure: Ā; B; A; Ā; •; v; A; B; B; B; •; ^{id^{B}}; ψ; Ā; B′; A; Ā; •; v; A; B′; B′; B′; •; ^{id^{B′}}; (id_{b})(ψ); ⟼]

We can now state the following.

2.4. Corollary. Every natural transformation t : 𝔸(−, B) [figure] 𝔸(−, B′) is of the form 𝔸(−, b) for a unique horizontal arrow b : B [figure] B′.

2.5. Adjoints

In this section and the next, we give an application of the Hom functor and Yoneda lemma to adjoints for double categories. Here we sketch the relevant ideas from [10].

The theory of adjoints for double categories was developed in [10] where it was made clear that adjointness is a relation between lax functors for the right and oplax ones for the left. This is a well-known feature of adjunctions between morphisms of bicategories and, in fact goes back to adjoints between monoidal categories (see e.g. [13]).

In order to formulate adjointness in general terms, a strict double category, 𝔻oub, of double categories with lax functors as horizontal arrows and oplax functors as vertical ones was introduced. This is perhaps the main point of [10]. A cell

[figure: ℂ; 𝔻; G; 𝔸; ℂ; •; R; 𝔸; 𝔹; F; 𝔹; 𝔻; •; S; t]

assigns to each object A in 𝔸 a horizontal arrow

tA : SF A [figure] GRA

and to each vertical arrow v : A [figure: •] Ā, a cell

[figure: SF Ā; GRĀ; tĀ; SF A; SF Ā; •; SF v; SF A; GRA; tA; GRA; GRĀ; •; GRv; tv]

satisfying the following conditions. (Horizontal naturality 1) For every f : A [figure] A′

[figure: SF A′; GRA′; tA′; SF A; SF A′; SF f; SF A; GRA; tA; GRA; GRA′; GRf]

commutes. (Horizontal naturality 2) For every cell

[figure: Ā; Ā′; f̄; A; Ā; •; v; A; A′; f; A′; Ā′; •; v′; α]

[figure: SF Ā; GRĀ; tA; SF A; SF Ā; •; SF v; SF A; GRA; tA; GRA; GRĀ; •; GRv; tv; GRĀ; GRĀ′; GRf̄; GRA; GRĀ; •; GRA; GRA′; GRf; GRA′; GRĀ′; •; GRv′; GRα; =; SF Ā; SF Ā′; SF f̄; SF A; SF Ā; •; SF v; SF A; SF A′; SF f; SF A′; SF Ā′; •; SF v′; SF α; SF Ā′; GRĀ′; tĀ′; SF A′; SF Ā′; •; SF A′; GRA′; tA′; GRA′; GRĀ′; •; GRv′; tv′]

(Vertical functoriality 1)

[figure: =; SF A; SF A; SF A; SF A; •; S(id_{F A}); SF A; SF A; SF A; SF A; •; SF id_{A}; SϕA; SF A; GRA; tA; SF A; SF A; •; SF A; GRA; tA; GRA; GRA; •; GRid_{A}; tid_{A}; GRA; GRA; GRA; GRA; •; GRA; GRA; GRA; GRA; •; G(id_{RA}); GρA]

[figure: SF A; SF A; SF A; SF A; •; S(id_{F A}); SF A; SF A; SF A; SF A; •; ^{id^{SF A}}; σF A; SF A; GRA; tA; SF A; SF A; •; SF A; GRA; tA; GRA; GRA; •; ^{id^{GRA}}; ^{id^{tA}}; GRA; GRA; GRA; GRA; •; GRA; GRA; GRA; GRA; •; G(id_{RA}); γRA]

(Vertical functoriality 2)

[figure: =; SF Ã; SF Ã; SF A; SF Ã; •; S(F v̄·F v); SF A; SF A; SF A; SF Ã; •; SF (v̄·v); Sϕ(v̄,v); SF Ã; GRÃ; tÃ; SF A; SF Ã; •; SF A; GRA; tA; GRA; GRÃ; •; GR(v̄·v); t(v̄·v); GRÃ; GRÃ; GRA; GRÃ; •; GRA; GRA; GRA; GRÃ; •; G(Rv̄·Rv); Gρ(v̄,v)]

YONEDA THEORY FOR DOUBLE CATEGORIES  453

[figure: SF Ã; SF Ã; SF A; SF Ã; •; SF v̄·F v); SF A; SF A; SF A; SF Ã; σ(F v̄,F v); SF Ã; GRÃ; tÃ; SF Ā; SF Ã; •; SF v̄; SF Ā; GRĀ; tĀ; GRĀ; GRÃ; •; GRv̄; tv̄; SF Ā; GRĀ; SF A; SF Ā; •; SF v; SF A; GRA; tA; GRA; GRĀ; •; GRv; tv; GRÃ; GRÃ; GRA; GRÃ; GRA; GRA; GRA; GRÃ; •; G(Rv̄·v); γ(Rv̄,Rv)]

Horizontal composition

[figure: ℂ; 𝔻; G; 𝔸; ℂ; •; R; 𝔸; 𝔹; F; 𝔹; 𝔻; •; t; 𝔻; 𝔻′; G′; 𝔹; 𝔻; •; S; 𝔹; 𝔹′; F′; 𝔹′; 𝔻′; •; S′; t′]

is given by

t′tA = (S′F′F A [figure: t′F A] G′SF A [figure: G′tA] G′GRA)

and

[figure: t′t(v); =; S′F′F Ā; G′SF Ā; t′F Ā; S′F′F A; S′F′F Ā; •; S′F′F v; S′F′F A; G′SF A; t′F A; G′SF A; G′SF Ā; •; G′SF v; t′F v; G′SF Ā; G′GRĀ; G′tĀ; G′SF A; G′SF Ā; •; G′SF A; G′GRA; G′tA; G′GRA; G′GRĀ; •; G′GRv; G′tv]

And vertical composition

[figure: ℂ̄; 𝔻̄; Ḡ; ℂ; ℂ̄; •; R̄; ℂ; 𝔻; 𝔻; 𝔻̄; •; S̄; t̄; ℂ; 𝔻; G; 𝔸; ℂ; •; R; 𝔸; 𝔹; F; 𝔹; 𝔻; •; S; t]

is given by

t̄· t(A) = (S̄SF A [figure: S̄tA] S̄GRA [figure: t̄RA] ḠR̄RA)

and

[figure: t̄· t(v); =; S̄SF Ā; S̄GRĀ; S̄tĀ; S̄SF A; S̄SF Ā; S̄SF v; S̄SF A; S̄GRA; S̄tA; S̄GRA; S̄GRĀ; S̄GRv; S̄tv; S̄GRĀ; ḠR̄RĀ; t̄RA; S̄GRA; S̄GRĀ; S̄GRA; ḠR̄RA; t̄RA; ḠR̄RA; ḠR̄RĀ; ḠR̄R(v); t̄Rv]

One might be suspicious of this construction because, although we are dealing with weak double categories, 𝔻oub is a strict double category. The reason is that both horizontal and vertical composition are defined in terms of horizontal composition in the codomain double category.

Another cause for suspicion might be that bicategories can be considered as double categories with identity horizontal arrows and neither lax, oplax, or pseudo natural transformations make lax functors into the 1-cells of a 2-category of bicategories. Again, because cells are defined in terms of the horizontal structure, the components of t on the objects are identities so if R and S are identity functors, a cell t is exactly an ICON as defined in [15].

We remark in passing that when R and S are identities and 𝔸 and 𝔹 are arbitrary double categories, the cells we have just defined are exactly the natural transformations of §1.5.

In [10], an oplax functor F : 𝔸 [figure] 𝔹 is said to be left adjoint to the lax functor U : 𝔹 [figure] 𝔸 if they form a conjoint pair in 𝔻oub. This means that there are cells

[figure: 𝔹; 𝔸; U; 𝔸; 𝔹; •; F; 𝔸; 𝔸; 1_{𝔸}; 𝔸; 𝔸; •; ^{Id^{𝔸}}; η; 𝔹; 𝔹; 1_{𝔹}; 𝔹; 𝔹; •; ^{Id^{𝔹}}; 𝔹; 𝔸; U; 𝔸; 𝔹; •; F; ϵ; and]

satisfying the “triangle” identities

[figure: 𝔹; 𝔹; 1_{𝔹}; 𝔹; 𝔹; •; ^{Id^{𝔹}}; 𝔹; 𝔸; 𝔸; 𝔹; •; F; ϵ; 𝔹; 𝔸; U; 𝔸; 𝔹; •; F; 𝔸; 𝔸; 1_{𝔸}; 𝔸; 𝔸; •; ^{Id^{𝔸}}; η; =; 𝔹; 𝔹; 1_{𝔹}; 𝔸; 𝔹; •; F; 𝔸; 𝔸; 1_{𝔸}; 𝔸; 𝔹; •; F; 1_{F}]

and

[figure: 𝔹; 𝔹; 1_{𝔹}; 𝔹; 𝔹; •; ^{Id^{𝔹}}; 𝔹; 𝔸; U; 𝔸; 𝔹; •; F; ϵ; 𝔹; 𝔸; U; 𝔸; 𝔹; •; 𝔸; 𝔸; 1_{𝔸}; 𝔸; 𝔸; •; ^{Id^{𝔹}}; η; =; 𝔹; 𝔸; U; 𝔹; 𝔹; •; ^{Id^{𝔹}}; 𝔹; 𝔸; U; 𝔸; 𝔸; •; ^{Id^{𝔸}}; ^{id^{U}}]

The usual properties of uniqueness and composability of adjoints follow from general properties of conjoints. All the details can be found in [10].

2.6. Example. π_{0} : ℂat [figure] 𝕊et which is oplax (normal) is left adjoint to the discrete category functor D : 𝕊et [figure] ℂat, and Ob : ℂat [figure] 𝕊et which is lax is right adjoint to D.

2.7. The Hom Version of Adjoints

Let U : 𝔹 [figure] 𝔸 be a lax functor. It can be substituted into the second variable of the Hom functor for 𝔸 to get a lax functor

𝔸(−, U−) : 𝔸^{op} × 𝔹 [figure] 𝕊et.

If F : 𝔸 [figure] 𝔹 is an oplax functor, F^{op} : 𝔸^{op} [figure] 𝔹^{op} is lax and it can be substituted into the first variable of the Hom functor for 𝔹 to get a lax

𝔹(F −, −) : 𝔸^{op} × 𝔹 [figure] 𝕊et.

2.8. Theorem. F is left adjoint to U if and only if 𝔹(F −, −) is isomorphic to 𝔸(−, U−).

Proof. Suppose F is left adjoint to U with unit η and counit ϵ as above. Define

t : 𝔹(F −, −) [figure] 𝔸(−, U−)

by the usual formulas

t(A, B) : 𝔹(F A, B) [figure] 𝔸(A, UB)
(b : F A [figure] B) ⟼ (A [figure: ηA] UF A [figure: Ub] UB)

and

t(v, w) : 𝔹(F v, w) [figure] 𝔸(v, Uw)

[figure: F Ā; B̄; b̄; F A; F Ā; •; F v; F A; B; b; B; B̄; •; w; β; ⟼; Ā; UF Ā; ηĀ; A; Ā; •; v; A; UF A; ηA; UF A; UF Ā; •; UF v; ηv; UF Ā; UB̄; Ub̄; UF A; UF Ā; •; UF A; UB; Ub; UB; UB̄; •; Uv; Uβ]

It is clear that t is horizontally natural at both the object and vertical arrow level. Vertical functoriality requires, first of all that

be equal to the first takes an element b : F A [figure] B of id_{𝔹(F A,B)} to

[figure: 𝔹(F A, B); 𝔹(F A, B); 𝔹(F A, B); 𝔹(F A, B); •; ^{Id^{𝔹(F A,B)}}; 𝔹(F A, B); 𝔹(F A, B); 𝔹(F A, B); 𝔹(F A, B); •; 𝔹(F id_{A},id_{B}); h(F A,B); 𝔹(F A, B); 𝔸(A, UB); t(A,B); 𝔹(F A, B); 𝔹(F A, B); •; 𝔹(F A, B); 𝔸(A, UB); t(A,B); 𝔸(A, UB); 𝔸(A, UB); •; 𝔸(id_{A},Uid_{B}); t(id_{A},id_{B})] [figure: 𝔹(F A, B); 𝔸(A, UB); t(A,B); 𝔹(F A, B); 𝔹(F A, B); •; ^{Id^{𝔹(F A,B)}}; 𝔹(F A, B); 𝔸(A, UB); t(A,B); 𝔸(A, UB); 𝔸(A, UB); •; ^{Id^{𝔸(A,UB)}}; ^{Id^{t(A,B)}}; 𝔸(A, UB); 𝔸(A, UB); 𝔸(A, UB); 𝔸(A, UB); •; 𝔸(A, UB); 𝔸(A, UB); 𝔸(A, UB); 𝔸(A, UB); •; 𝔸(id_{A},Uid_{B}); h′(A,UB)]

[figure: A; UF A; ηA; A; A; •; ^{id^{A}}; A; UF A; ηA; UF A; UF A; •; UF id_{A}; ηid_{A}; UF A; UF A; UF A; UF A; •; UF A; UF A; UF A; UF A; •; Uid_{F A}; UϕA; UF A; UB; Ub; UF A; UF A; •; UF A; UB; Ub; UB; UB; •; Uid_{B}; Uid_{B}]

whereas the second takes it to

[figure: A; UF A; ηA; A; A; •; ^{id^{A}}; A; UF A; ηA; UF A; UF A; •; ^{id^{UF A}}; ^{id^{ηA}}; UF A; UB; Ub; UF A; UF A; •; UF A; UB; Ub; UB; UB; •; ^{id^{UB}}; ^{id^{Ub}}; UB; UB; UB; UB; •; UB; UB; UB; UB; •; Uid_{B}; ψB]

This last rectangle is equal to

[figure: A; UF A; ηA; A; A; •; ^{id^{A}}; A; UF A; ηA; UF A; UF A; •; ^{id^{UF A}}; ^{id^{ηA}}; UF A; UF A; Ub; UF A; UF A; •; UF A; UF A; UF A; UF A; •; Uid_{F A}; ψF A; UF A; UB; Ub; UF A; UF A; •; UF A; UB; Ub; UB; UB; •; Uid_{B}; Uid_{B}]

by naturality of ψ, and this in turn is equal to the above because η respects vertical identities (1).

t must also respect vertical composition. This means that

[figure: 𝔹(F Ã, B̃); 𝔹(F Ã, B̃); 𝔹(F A, B); 𝔹(F Ã, B̃); 𝔹(F A, B); 𝔹(F A, B); 𝔹(F A, B); 𝔹(F Ã, B̃); •; 𝔹(F (v̄·v),w̄·w); h; 𝔹(F Ã, B̃); 𝔹(F Ã, B̃); 𝔹(F Ā, B̄); 𝔹(F Ã, B̃); •; 𝔹(F v̄,w̄); 𝔹(F Ā, B̄); 𝔹(F Ã, B̃); 𝔹(F Ā, B̄); 𝔹(F A, B); 𝔹(F Ā, B̄); •; 𝔹(F v,w); 𝔹(F A, B); 𝔹(F A, B); 𝔹(F A, B); 𝔹(F Ã, B̃); 𝔸(Ã, B̃); t(Ã,B̃); 𝔹(F A, B); 𝔹(F Ã, B̃); •; 𝔹(F A, B); 𝔸(A, UB); t(A,B); 𝔸(A, UB); 𝔸(Ã, B̃); •; 𝔸(v̄·v,U(w̄·w)); t(v̄·v,w̄·w)]

must equal

[figure: 𝔹(F Ã, B̃; 𝔸(Ã, UB̃); t(Ã,B̃); 𝔹(F Ā, B̄); 𝔹(F Ã, B̃; •; 𝔹(F v̄,w); 𝔹(F Ā, B̄); 𝔸(Ā, UB̄); t(Ā,B̄); 𝔸(Ā, UB̄); 𝔸(Ã, UB̃); •; 𝔸(v̄,Uw̄); t(v̄,w̄); 𝔹(F Ā, B̄); 𝔸(Ā, UB̄); 𝔹(F A, B); 𝔹(F Ā, B̄); •; 𝔹(F v,w); 𝔹(F A, B); 𝔸(A, UB); t(A,B); 𝔸(A, UB); 𝔸(Ā, UB̄); •; 𝔸(v,Uw)); t(v,w); 𝔸(Ã, UB̃); 𝔸(Ã, B̃); 𝔸(A, UB); 𝔸(Ã, UB̃); 𝔸(A, UB); 𝔸(A, UB); 𝔸(A, UB); 𝔸(Ã, B̃); •; 𝔸(v̄·v,U(w̄·w)); h′]

The first takes a pair of cells, β, β̄,

[figure: F Ã; B̃; b̄; F Ā; F Ã; •; F v̄; F Ā; B̄; b̄; B̄; B̃; •; w̄; β̄; F Ā; B̄; F A; F Ā; •; F v; F A; B; b; B; B̄; •; w; β]

to

[figure: Ã; UF Ã; ηÃ; A; Ã; A; UF A; ηA; UF A; UF Ã; •; UF (v̄·v); η(v̄·v); Ã; UF Ã; Ā; Ã; •; v̄; Ā; UF Ã; Ā; A; Ā; •; v; A; UF A; UF A; UF Ã; UF Ã; UF A; UF Ã; UF A; UF A; UF A; UF Ã; •; U(F v̄·F v); Uϕv̄,v; UF Ã; UB̃; Ub̃; UF A; UF Ã; UF A; UB; Ub; UB; UB̃; •; U(w̄·w); U(β̄·β)]

whereas the second takes β, β̄ to

[figure: Ã; UF Ã; ηÃ; Ā; Ã; •; v̄; Ā; UF Ā; ηĀ; UF Ā; UF Ã; •; UF v̄; ηv̄; Ā; UF Ā; A; Ā; •; v; A; UF A; ηA; UF A; UF Ā; •; UF v; ηv; UF Ã; UB̃; Ub̃; UF Ā; UF Ã; UF Ā; UB̄; Ub̄; UB̄; UB̃; •; Uw̄; Uβ̄; UF Ā; UB̄; UF A; UF Ā; •; UF A; UB; Ub; UB; UB̄; •; Uw; Uβ; UB̃; UB̃; UB; UB̃; UB; UB; UB; UB̃; •; U(w̄·w); ψ_{w̄,w}]

Again, naturality of ψ allows us to transform this last rectangle into

[figure: Ã; UF Ã; ηĀ; Ā; Ã; •; v̄; Ā; UF Ā; ηĀ; UF Ā; UF Ã; •; UF v̄; ηv̄; Ā; UF Ā; A; Ā; •; v; A; UF A; ηA; UF A; UF Ā; •; UF v; ηv; UF Ã; UF Ã; UF A; UF Ã; UF A; UF A; UF A; UF Ã; •; U(F v̄·F v); ψ_{F v̄,F v}; UF Ã; UB̃; Ub̃; UF A; UF Ã; UF A; UB; Ub; UB; UB̃; •; U(w̄·w); U(β̄·β)]

which is equal to the one above because η respects vertical composition (2). This shows that t is a natural transformation of lax morphisms

𝔹(F −, −) [figure] 𝔸(−, U−).

Similarly, using ϵ and F we get a transformation

𝔸(−, U−) [figure] 𝔹(F −, −)

which is inverse to t, by virtue of the triangle identities just like for ordinary adjoints.

Conversely, suppose we have a natural transformation t : 𝔹(F −, −) [figure] 𝔸(−, U−). Let ηA : A [figure] UF A be t(A, F A)(1_{F A}) and

[figure: Ā; UF Ā; ηĀ; A; Ā; •; v; A; UF A; ηA; UF A; UF Ā; •; UF v; ηv]

be t(v, F v)(1_{F v}). It follows from horizontal naturality of t that

t(A, B)(f) = (Uf)(ηA)

and

[figure: t(v, w)(ψ) =; Ā; UF Ā; ηĀ; A; Ā; •; v; A; UF A; ηA; UF A; UF Ā; •; UF v; ηv; UF Ā; UB̄; Uf̄; UF A; UF Ā; •; UF A; UB; Uf; UB; UB̄; •; Uw; Uψ]

Note that the vertical domain and codomain of ηv are ηA and ηĀ because t(v, F v) is a morphism of spans. The horizontal naturality of η in A and v is straightforward. It’s just the usual Yoneda calculus.

Should there be any lingering doubts about the definition of cells in 𝔻oub, we check the vertical functoriality condition for η. It is a direct consequence of vertical functoriality for the natural transformation t. This says that for A [figure: •; v] Ā [figure: •; v̄] Ã and B [figure: •; w] B̄ [figure: •; w̄] B̃ we have that

[figure: 𝔹(F Ã, B̃); 𝔸(Ã, UB̃); 𝔹(F Ā, B̄); 𝔹(F Ã, B̃); •; 𝔹(F v̄,w̄); 𝔹(F Ā, B̄); 𝔸(Ā, UB̄); 𝔸(Ā, UB̄); 𝔸(Ã, UB̃); •; 𝔸(v̄,Uw̄); t(v̄,w̄); 𝔹(F Ā, B̄); 𝔸(Ā, UB̄); 𝔹(F A, B); 𝔹(F Ā, B̄); •; 𝔹(F v,w); 𝔹(F A, B); 𝔸(A, UB); 𝔸(A, UB); 𝔸(Ā, UB̄); •; 𝔸(v,Uw); t(v,w); 𝔸(Ã, UB̃); 𝔸(Ã, UB̃); 𝔸(A, UB); 𝔸(Ã, UB̃); 𝔸(A, UB); 𝔸(A, UB); 𝔸(A, UB); 𝔸(Ã, UB̃); •; 𝔸(v̄·v,U(w̄·w)); ξ]

equals

[figure: 𝔹(F Ã, B̃); 𝔹(F Ã, B̃); 𝔹(F Ā, B̄); 𝔹(F Ã, B̃); •; 𝔹(F v̄,w̄); 𝔹(F Ā, B̄); 𝔹(F Ã, B̃); 𝔹(F Ā, B̄); 𝔹(F A, B); 𝔹(F Ā, B̄); •; 𝔹(F v,w); 𝔹(F A, B); 𝔹(F A, B); 𝔹(F A, B); ξ; 𝔹(F Ã, B̃); 𝔹(F Ã, B̃); 𝔹(F A, B); 𝔹(F Ã, B̃); 𝔹(F A, B); 𝔹(F A, B); 𝔹(F A, B); 𝔹(F Ã, B̃); •; 𝔹(F (v̄·v),w̄·w); 𝔹(F Ã, B̃); 𝔸(Ã, UB̃); 𝔹(F A, B); 𝔹(F Ã, B̃); 𝔹(F A, B); 𝔸(A, UB); 𝔸(A, UB); 𝔸(Ã, UB̃); •; 𝔸(v̄·v,U(w̄·w)); t(v̄·v,w̄·w)]

Here ξ combines the laxity of 𝔸(−, −) and that of U

ξ : (ψ̄, ψ) ⟼ ψ(w̄ · w)(ψ̄ · ψ)

[figure: Ã; UB̃; Ā; Ã; •; v̄; Ā; UB̄; UB̄; UB̃; •; Uw̄; ψ̄; Ā; UB̄; A; Ā; •; v; A; UB; UB; UB̄; •; Uw; ψ; UB̃; UB̃; UB; UB̃; UB; UB; UB; UB̃; U(w̄·w); ψ(w̄·w)]

Likewise ξ uses the oplaxity of F

ξ : (θ̄, θ) ⟼ (θ̄ · θ)ϕ(v̄, v)

[figure: F Ã; F Ã; F A; F Ã; •; F (v̄·v); F A; F A; F A; F Ã; ϕ(v̄,v); F Ã; B̃; F Ā; F Ã; •; F v̄; F Ā; B̄; B̄; B̃; •; w̄; θ̄; F Ā; B̄; F A; F Ā; •; F v; F A; B; B; B̄; •; w; θ]

Now we specialize this by letting B, B̄, B̃, w, w̄ be F A, F Ā, F Ã, F v, and F v̄ respectively, and evaluate at the element (1_{F v̄}, 1_{F v}). The cell in (1) first applies t componentwise to get (ηv̄, ηv) and then ξ to get

[figure: Ã; UF Ã; Ā; Ã; •; v̄; Ā; UF Ā; UF Ā; UF Ã; •; UF v̄; ηv̄; Ā; UF Ā; A; Ā; •; v; A; UF A; UF A; UF Ā; •; UF v; ηv; UF Ã; UF Ã; UF A; UF Ã; UF A; UF A; UF A; UF Ã; •; U(F v̄·F v); U(F v̄,F v)]

To evaluate (2) at (1_{F v̄}, 1_{F v}) we first apply ξ. Thus, multiply 1_{F v̄} · 1_{F v} = 1_{F v̄·F v} and then multiply horizontally by ϕ(v̄, v), so

[figure: ξ(1_{F v̄}, 1_{F v}); =; F Ã; F Ã; F Ã; F Ā; F Ā; F Ã; •; F v̄; F Ā; F A; F A; F A; F A; F Ā; •; F v; F Ã; F Ã; F A; F Ã; •; F (v̄·v); F A; F A; F A; F Ã; ϕ(F,v)]

Then we apply t

[figure: t(v̄ · v, F v̄ · F v)(ϕ(v̄, v)) =; Ã; UF Ã; ηÃ; A; Ã; •; v̄·v; A; UF A; ηA; UF A; UF Ã; •; UF (v̄·v); η(v̄·v); UF Ã; UF Ã; UF A; UF Ã; •; UF A; UF A; UF A; UF Ã; •; U(F v̄·F v); Uϕ(v̄,v)]

The equality of (3) and (4) is vertical functoriality (2) of η. It is a bit simpler than the general formulation because the domain of η is a composite of two identities.

We leave the verification that η respects identities, which is similar, as a salutary exercise for the suspicious reader.

It is thus seen that η is a cell

[figure: 𝔹; 𝔸; U; 𝔸; 𝔹; •; F; 𝔸; 𝔸; 1_{𝔸}; 𝔸; 𝔸; •; ^{Id^{𝔸}}; η]

When t is invertible, a similar argument applied to t^{−1} will produce a cell

[figure: 𝔹; 𝔹; 1_{𝔹}; 𝔹; 𝔹; •; ^{Id^{𝔹}}; 𝔹; 𝔸; U; 𝔸; 𝔹; •; F; ϵ]

For w : B [figure: •] B̄,

[figure: F UB̄; B̄; ϵB̄; F UB; F UB̄; •; F Uw; F UB; B; ϵB; B; B̄; •; w; ϵw; = t^{−1}(Uw, w)(1_{Uw})]

and then

[figure: t^{−1}(v, w)(θ) =; F Ā; F UB; F A; F Ā; •; F v; F A; F UB; F UB; F UB; •; F Uw; F θ; F UB; B̄; F UB; F UB; •; F UB; B; B; B̄; •; w; ϵw]

Now the composite

[figure: 𝔹(F Ā, F Ā); 𝔸(Ā, UF Ā); 𝔹(F A, F A); 𝔹(F Ā, F Ā); •; 𝔹(F v,F v); 𝔹(F A, F A); 𝔸(A, UF A); 𝔸(A, UF A); 𝔸(Ā, UF Ā); •; 𝔸(v,UF v); t(v,F v); 𝔸(Ā, UF Ā); 𝔹(F Ā, F Ā); 𝔸(A, UF A); 𝔸(Ā, UF Ā); •; 𝔸(A, UF A); 𝔹(F A, F A); 𝔹(F A, F A); 𝔹(F Ā, F Ā); •; 𝔹(F v,F v); t^{−1}(v,F v)]

is the identity, so it sends 1_{F v} to itself but

t^{−1}(v, F v)t(v, F v)(1_{F v}) = t^{−1}(v, F v)(ηv) = (ϵF v)(F ηv).

So

[figure: F Ā; F UF Ā; F A; F Ā; •; F v; F A; F UF A; F UF A; F UF Ā; •; F UF v; F ηv; F UF Ā; F Ā; F UF A; F UF Ā; •; F UF A; F A; F A; F Ā; •; F v; ϵF v; = 1_{F v}]

Similarly we get

[figure: UB̄; UF UB̄; UB; UB̄; •; Uw; UB; UF UB; UF UB; UF UB̄; •; ηUw; UF UB̄; UB̄; UF UB; UF UB̄; •; UF UB; UB; UB; UB̄; •; Uw; Uϵw; = 1_{Uw}]

Note that, although both of these express an equality of horizontal composites with horizontal identities, the first one is the identity

[figure: 𝔹; 𝔹; 𝔹; 𝔹; •; Id; 𝔹; 𝔸; U; 𝔸; 𝔹; •; F; ϵ; 𝔹; 𝔸; 𝔸; 𝔹; •; F; 𝔸; 𝔸; 1; 𝔸; 𝔸; •; Id; η; = 1_{F}]

and the second

[figure: 𝔹; 𝔹; 1; 𝔹; 𝔹; •; Id; 𝔹; 𝔸; U; 𝔸; 𝔹; •; F; ϵ; 𝔹; 𝔸; U; 𝔸; 𝔹; •; 𝔸; 𝔸; 1; 𝔸; 𝔸; •; Id; η; = Id_{U}]

3. The Yoneda Lemma Part II

3.1. Modules

The first part of the Yoneda lemma given in §2.2 tells us what the elements of F B are in terms of transformations. In order to determine a lax functor F : 𝔸^{op} [figure] 𝕊et we must also know what the elements of F (v) are, for a vertical arrow v. This requires an understanding of how the lax functors 𝔸(−, A) depend on A. We have already seen in Corollary 2.4 that a horizontal arrow f : A [figure] B gives, by composition, a natural transformation 𝔸(−, f) : 𝔸(−, A) [figure] 𝔸(−, B) and what we study in this section is what kind of morphism 𝔸(−, A) [figure: •] 𝔸(−, Ā) a vertical morphism v : A [figure: •] Ā gives. Thus the natural transformations will be the horizontal arrows of a (lax) double category 𝕃ax(𝔸^{op}, 𝕊et) for which we will be defining the vertical arrows and cells. This prepares the scene for the Yoneda embedding of §4.

There are several reasonable candidates for the notion of vertical transformation of lax functors. Our choice is guided by the structure created by vertical arrows on representables. In fact the source of this concept goes deeper than that. A lax functor of two variables Φ : 𝔸 × 𝔹 [figure] ℂ produces, by fixing the second variable, a lax functor Φ(−, B) : 𝔸 [figure] ℂ and a vertical arrow w : B [figure: •] B̄ will give the doulbe category version of what was called a module Φ(−, w) : Φ(−, B) [figure: •] Φ(−, B̄) in [4]. This is a kind of multiobject version of profunctor.

We give the essentials here formulated in the language of double categories. An indepth study, adapting and extending that of [4], will appear elsewhere.

3.2. Definition. Let F, G : 𝔸 [figure] 𝔹 be lax functors. A module m : F [figure: •] G consists of: (M1) for every vertical arrow v : A [figure: •] Ā, a vertical arrow m(v) : F A [figure: •] GĀ; (M2) for every cell

[figure: Ā; Ā′; f̄; A; Ā; •; v; A; A′; f; A′; Ā′; •; v′; α; a cell; GA; GA′; Gf̄; F A; GA; •; m(v); F A; F A′; F f; F A′; GA′; •; m(v′); m(α)]

(M3) for every pair of vertical arrows A [figure: •; v] Ā [figure: •; v̄] Ã, special cells

[figure: GÃ; GÃ; GĀ; GÃ; •; G(v̄); GĀ; GÃ; GĀ; F A; GĀ; •; m(v); F A; F A; F A; GÃ; GÃ; F A; GÃ; F A; F A; F A; GÃ; •; m(v̄·v); λ(v̄,v); and; GÃ; GÃ; F Ā; GÃ; •; m(v̄); F Ā; GÃ; F Ā; F A; F Ā; •; F v; F A; F A; F A; GÃ; GÃ; F A; GÃ; F A; F A; F A; GÃ; •; m(v̄·v); ρ(v̄,v)]

These are required to satisfy the following conditions: (M4) (Horizontal functoriality) for cells

[figure: Ā; Ā′; A; Ā; •; A; A′; A′; Ā′; •; α; Ā′; Ā′′; A′; Ā′; •; A′; A′′; A′′; Ā′′; •; α′]

we have

[figure: GĀ; GĀ′′; F A; GĀ; •; F A; F A′′; F A′′; GĀ′′; •; m(α′α); =; GĀ; GĀ′; F A; GĀ; •; F A; F A′; F A′; GĀ′; •; m(α); GĀ′; GĀ′′; F A′; GĀ′; •; F A′; F A′′; F A′′; GĀ′′; •; m(α′)]

and for any v : A [figure: •] Ā

[figure: GĀ; GĀ; F A; GĀ; •; F A; F A; F A; GĀ; •; m(1_{v}); =; GĀ; GĀ; F A; GĀ; •; F A; F A; F A; GĀ; •; 1_{m(v)}]

(M5) (Naturality of λ and ρ) for cells

[figure: Ã; Ã′; Ā; Ã; •; Ā; Ā′; Ā′; Ã′; •; ᾱ; Ā; Ā′; A; Ā; •; A; A′; A′; Ā′; •; α]

we have

[figure: GÃ; GÃ; F Ā; GÃ; •; F Ā; GÃ; F Ā; F A; F Ā; •; F A; F A; F A; GÃ; GÃ′; F A; GÃ; •; F A; F A′; F A′; GÃ′; •; ρ; m(ᾱ·α); =; GÃ; GÃ′; F Ā; GÃ; •; F Ā; F Ā′; F Ā′; GÃ′; •; F Ā; F Ā′; F A; F Ā; •; F A; F A′; F A′; F Ā′; •; GÃ′; GÃ′; F A′; GÃ′; F A′; F A′; F A′; GÃ′; •; m(ᾱ); F (α); ρ]

and

[figure: GÃ; GÃ; GĀ; GÃ; •; GĀ; GÃ; GĀ; F A; GĀ; •; F A; F A; F A; GÃ; GÃ′; F A; GÃ; •; F A; F A′; F A′; GÃ′; •; λ; m(ᾱ·α); =; GÃ; GÃ′; GĀ; GÃ; •; GĀ; GĀ′; GĀ′; GÃ′; •; GĀ; GĀ′; F A; GĀ; •; F A; F A′; F A′; GĀ′; •; GÃ′; GÃ′; F A′; GÃ′; F A′; F A′; F A′; GÃ′; •; G(ᾱ); m(α); λ]

(M6) (Associativity) for A [figure: •; v] Ā [figure: •; v̄] Ã [figure: •; ṽ] Â

[figure: GÂ; GÂ; F Ã; GÂ; •; F Ã; GÂ; F Ã; F Ā; F Ã; •; F Ā; F Ā; F Ā; F Ā; F Ā; F A; F Ā; •; F A; F A; F A; F Ā; •; GÂ; GÂ; F Ā; GÂ; •; F Ā; GÂ; GÂ; GÂ; F A; GÂ; F A; F A; F A; GÂ; •; 1; ρ; ρ; =; GÂ; GÂ; F Ã; GÂ; •; F Ã; F Ã; F Ã; GÂ; •; F Ã; F Ã; F Ā; F Ã; •; F Ā; F Ã; F Ā; F A; F Ā; •; F A; F A; F A; F Ã; F Ã; F A; F Ã; F A; F A; F A; F Ã; •; GÂ; GÂ; F A; GÂ; F A; F A; F A; GÂ; •; 1; ϕ; ρ]

[figure: GÂ; GÂ; GÃ; GÂ; •; GÃ; GÂ; GÃ; F Ā; GÃ; •; F Ā; F Ā; F Ā; F Ā; F Ā; F A; F Ā; •; F A; F A; F A; F Ā; •; 1; GÂ; GÂ; F Ā; GÂ; F Ā; F Ā; F Ā; GÂ; •; λ; GÂ; GÂ; F A; GÂ; F A; F A; F A; GÂ; •; ρ; =; GÂ; GÂ; GÃ; GÂ; •; GÃ; GÃ; GÃ; GÂ; •; 1; GÃ; GÃ; F Ā; GÃ; •; F Ā; GÃ; F Ā; F A; F Ā; •; F A; F A; F A; GÃ; GÃ; F A; GÃ; F A; F A; F A; GÃ; •; ρ; GÂ; GÂ; GÃ; GÂ; •; GÃ; GÂ; GÃ; F A; GÃ; •; F A; F A; F A; GÂ; GÂ; F A; GÂ; F A; F A; F A; GÂ; •; λ]

[figure: GÂ; GÂ; GÃ; GÂ; •; GÃ; GÃ; GÃ; GÂ; •; 1; GÃ; GÃ; GA; GÃ; •; GA; GÃ; GA; F A; GA; •; F A; F A; F A; GÃ; GÃ; F A; GÃ; F A; F A; F A; GÃ; •; GÂ; GÂ; GÃ; GÂ; •; GÃ; GÂ; GÃ; F A; GÃ; •; F A; F A; F A; GÂ; GÂ; F A; GÂ; F A; F A; F A; GÂ; •; λ; λ; =; GÂ; GÂ; GÃ; GÂ; •; GÃ; GÂ; GÃ; GĀ; GÃ; •; GĀ; GĀ; GĀ; GÂ; GÂ; GĀ; GÂ; GĀ; GĀ; GĀ; GÂ; •; γ; GĀ; GĀ; F A; GĀ; •; F A; F A; F A; GĀ; •; GÂ; GÂ; F A; GÂ; F A; F A; F A; GÂ; •; λ; 1]

(M7) (Unit) for v : A [figure: •] Ā

[figure: GĀ; GĀ; F A; GĀ; •; m(v); F A; F A; F A; GĀ; •; m(v); 1_{m(v)}; F A; F A; F A; F A; •; ^{id^{F A}}; F A; F A; F A; F A; •; F id_{A}; ϕA; GĀ; GĀ; F A; GĀ; F A; F A; F A; GĀ; •; m(v); ρ; =; GĀ; GĀ; F A; GĀ; •; m(v); F A; GĀ; F A; F A; F A; •; ^{id^{F A}}; F A; F A; F A; GĀ; GĀ; F A; GĀ; F A; F A; F A; GĀ; •; m(v); ≅]

and

[figure: GĀ; GĀ; GĀ; GĀ; •; ^{id^{GĀ}}; GĀ; GĀ; GĀ; GĀ; •; GidĀ; γĀ; GĀ; GĀ; F A; GĀ; •; m(v); F A; F A; F A; GĀ; •; m(v); 1_{m(v)}; GĀ; GĀ; GĀ; GĀ; •; GĀ; GĀ; GĀ; F A; GĀ; •; F A; F A; F A; GĀ; GĀ; F A; GĀ; F A; F A; F A; GĀ; •; m(v); λ; =; GĀ; GĀ; GĀ; GĀ; •; ^{id^{GĀ}}; GĀ; GĀ; GĀ; F A; GĀ; •; m(v); F A; F A; F A; GĀ; GĀ; F A; GĀ; F A; F A; F A; GĀ; •; m(v); ≅]

where ≅ represents the canonical unit isomorphism in 𝔹.

The data given in (M1) and (M2) as well as condition (M4) are coded in the functors M_{w,x} of [4]. Our left and right actions, λ, ρ of (M3), are both called M̃ there, and (M5) is its naturality. The five familiar unit and associative laws they refer to are our (M6) and (M7).

The name “module” comes from successive generalizations of the classical notion. If we consider the monoidal category (Ab, ⊗, ℤ) as a one object bicategory and make it into a double category vertically, 𝕍(Ab), then a lax functor 1 [figure] 𝕍(Ab) corresponds to a ring and a module between two such lax functors to a bimodule in the classical sense. The “bi” was dropped early on as redundant, in favour of “module” from one ring to another to emphasize that we were dealing with a kind of morphism that could be composed and to avoid potential clashes with other bicategorical notation.

Still following [4] we will call our cells, modulations.

3.3. Definition. Given lax functors F, F′, G, G′ : 𝔸 [figure] 𝔹, natural transformations t : F [figure] F′, s : G [figure] G′, and modules m : F [figure: •] G, m′ : F′ [figure: •] G′, a modulation

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

consists of: (m1) for every vertical arrow v : A [figure: •] Ā of 𝔸, a cell

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

satisfying (m2) (Horizontal naturality) for every cell

[figure: Ā; Ā′; f̄; A; Ā; •; v; A; A′; f; A′; Ā′; •; v′; α]

[figure: GĀ; G′Ā; sĀ; F A; GĀ; •; m(v); F A; F′A; tA; F′A; G′Ā; •; m′(v); μ(v); G′Ā; G′Ā′; Gf̄; F′A; G′Ā; •; F′A; F′A′; F f; F′A′; G′Ā′; •; m′(v′); m′(α); =; GĀ; GĀ′; Gf̄; F A; GĀ; •; m(v); F A; F A′; F f; F A′; GĀ′; •; m(v′); m(α); GĀ′; G′Ā′; sĀ′; F A′; GĀ′; •; F A′; F′A′; tA′; F′A′; G′Ā′; •; m′(v′); μ(v′)]

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

[figure: GÃ; G′Ã′; GĀ; GÃ; •; GĀ; G′Ā; G′Ā; G′Ã′; •; GĀ; G′Ā; F A; GĀ; •; F A; F′A; F′A; G′Ā; •; G′Ã′; G′Ã′; F′A; G′Ã′; F′A; F′A; F′A; G′Ã′; •; s(v̄); μ(v); λ′; =; GÃ; GÃ; GĀ; GÃ; •; GĀ; GÃ; GĀ; F A; GĀ; •; F A; F A; F A; GÃ; G′Ã; F A; GÃ; •; F A; F′A; F′A; G′Ã; •; λ; μ(v̄·v)]

and

[figure: GÃ; G′Ã; F Ā; GÃ; •; F Ā; F′Ā; F′Ā; G′Ã; •; F Ā; F′Ā; F A; F Ā; •; F A; F′A; F′A; F′Ā; •; G′Ã; G′Ã; F′A; G′Ã; F′A; F′A; F′A; G′Ã; •; μ(v̄); t(v); ρ′; =; GÃ; GÃ; F Ā; GÃ; •; F Ā; GÃ; F Ā; F A; F Ā; •; F A; F A; F A; GÃ; G′Ã; F A; GÃ; •; F A; F′A; F′A; G′Ã; •; ρ; μ(v̄·v)]

To make the connection with [4], the data (m1) and condition (m2) are coded in their natural transformations t_{w,x} and (m3) is also called “equivariance” there.

3.4. Proposition. Let K : 𝔸 × 𝕏 [figure] 𝔹 be a lax functor. Then, every vertical arrow x : X [figure: •] X̄ gives a module K(−, x) : K(−, X) [figure: •] K(−, X̄) and every cell

[figure: X̄; Ȳ; X; X̄; •; x; X; Y; Y; Ȳ; •; y; ξ]

gives a modulation

[figure: K(−, X̄); K(−, Ȳ); K(−, X); K(−, X̄); •; K(−,x); K(−, X); K(−, Y); K(−, Y); K(−, Ȳ); •; K(−,y); K(−,ξ)]

Proof. We indicate the, pretty well obvious, formulas and will provide a detailed proof elsewhere. (M1) K(−, x)(v) = K(v, x) (M2) K(−, x)(α) = K(α, 1_{x})

(M3)

[figure: K(−, Y)(Ã); K(−, Y)(Ã); K(−, Y)(Ā); K(−, Y)(Ã); •; K(−,Y)(v̄); K(−, Y)(Ā); K(−, Y)(Ã); K(−, Y)(Ā); K(−, X)(A); K(−, Y)(Ā); •; K(−,x)(v); K(−, X)(A); K(−, X)(A); K(−, X)(A); K(−, Y)(Ã); K(−, Y)(Ã); K(−, X)(A); K(−, Y)(Ã); K(−, X)(A); K(−, X)(A); K(−, X)(A); K(−, Y)(Ã); •; K(−,x)(v̄·v); λ(v̄,v); =; K(Ã, Y); K(Ã, Y); K(Ā, Y); K(Ã, Y); •; K(v̄,id_{y}); K(Ā, Y); K(Ã, Y); K(Ā, Y); K(A, X); K(Ā, Y); •; K(v,x); K(A, X); K(A, X); K(A, X); K(Ã, Y); K(Ã, Y); K(A, X); K(Ã, Y); K(A, X); K(A, X); K(A, X); K(Ã, Y); •; K(v̄·v,x); κ((v̄,id_{y}),(v,x))]

and ρ is similarly obtained from the laxity of K, ρ(v̄, v) = κ((v̄, x), (v, id_{x})). (m1) K(−, ξ)(v) = K(1_{v}, ξ).

3.5. Remark. If we let 𝕏 = 𝕍2, the double category with two objects 0, 1, one vertical arrow 0 [figure: •] 1, and nothing else except identities, then not only does a lax functor K : 𝔸 × 𝕍2 [figure] 𝔹 give a module K(−, 0) [figure: •] K(−, 1) but every module m : F [figure: •] G arises in this way from a unique K.

3.6. Corollary. A vertical arrow v : A [figure: •] Ā in 𝔸 produces a module 𝔸(−, v) : 𝔸(−, A) [figure: •] 𝔸(−, Ā). A cell

[figure: Ā; Ā′; f̄; A; Ā; •; v; A; A′; f; A′; Ā′; •; v′; α]

produces a modulation

[figure: 𝔸(−, A); 𝔸(−, A′); 𝔸(−,f̄); 𝔸(−, A); 𝔸(−, A); •; 𝔸(−,v); 𝔸(−, A); 𝔸(−, A′); 𝔸(−,f); 𝔸(−, A′); 𝔸(−, A′); •; 𝔸(−,v′); 𝔸(−,α)]

3.7. Elements

We will be working with lax functors 𝔸^{op} [figure] 𝕊et and their morphisms (natural transformations, modules, modulations). To do any serious calculation, we will need good notation.

We use the same symbol for a span S : A [figure: •] B and its apex:

[figure: A; B; S; A; ( )_{0}; S; B; ( )_{1}]

We write s : a [figure: •; S] b or just s : a [figure: •] b to indicate that s is an element of S such that s_{0} = a and s_{1} = b. For another span T : B [figure: •] C, an element of the composite T ⊗ S is a pair

a [figure: •; s; S] b [figure: •; t; T] c

also denoted t ⊗_{b} s : a [figure: •] c, or simply t ⊗ s. The unique element a [figure: •] a in the identity span Id_{A} : A [figure: •] A is denoted id_{a} : a [figure: •] a. A cell

[figure: B; B′; g; A; B; •; S; A; A′; f; A′; B′; •; S′; σ]

is a function assigning to a [figure: •; s] b an element fa [figure: •; σ(s)] sb.

We extend this notation to lax functors F : 𝔸^{op} [figure] 𝕊et. F has elements of different sorts indexed by the objects of 𝔸, x ∈ F A, which we denoted by (A, x). For v : A [figure: •] Ā in 𝔸, F (v) : F A [figure: •] F Ā is a span. We denote a typical element r ∈ F (v) by (v, r) : (A, x) [figure: •] (Ā, x̄), where x = r_{0} and x̄ = r_{1}. The laxity morphism

[figure: F Ã; F Ã; F Ā; F Ã; •; F v̄; F Ā; F Ã; F Ā; F A; F Ā; •; F v; F A; F A; F A; F Ã; F Ã; F A; F Ã; F A; F A; F A; F Ã; •; F (v̄·v); Q(v̄,v)]

takes an element (A, x) [figure: •; (v,r)] (Ā, x̄) [figure: •; (v̄,r̄)] (Ã, x̃) of F v̄ · F v to an element of F (v̄ · v), which we denote by (v̄ · v, r̄ · r) : (A, x) [figure: •] (Ã, x̃). The cell

[figure: F A; F A; F A; F A; •; ^{Id^{F A}}; F A; F A; F A; F A; •; F (id_{A}); QA]

takes the element id_{(A,x)} : (A, x) [figure: •] (A, x) of Id_{F A} to an element of F (id_{A}) denoted (id_{A}, id_{x}) : (A, x) [figure: •] (A, x).

This is more than just notation, it is the vertical part of a double category, 𝔼l(F), the double category of elements of F.

An object of 𝔼l(F) is a pair (A, x), for A an object of 𝔸 and x ∈ F A. A horizontal arrow (A, x) [figure] (B, y) is a pair (f, y) such that f : A [figure] B is a horizontal arrow of 𝔸 and x = F (f)(y). A vertical arrow (A, x) [figure: •] (Ā, x̄) is a pair (v, r) as above. A cell

[figure: (Ā, x̄); (B̄, ȳ); (f̄,ȳ); (A, x); (Ā, x̄); •; (v,r); (A, x); (B, y); (f,y); (B, y); (B̄, ȳ); •; (w,s); (α,s)]

is a pair (α, s) for α a cell

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

such that F (α)(s) = r. Horizontal composition is given by

(g, z)(f, y) = (gf, z),
(β, t)(α, s) = (βα, t),

and vertical composition by

(v̄, r̄) · (v, r) = (v̄ · v, r̄ · r),
(ᾱ, s̄) · (α, s) = (ᾱ · α, s̄ · s).

Much of the computational flexibility presented by this notation is summarized in the following.

3.8. Theorem. 𝔼l(F) is a double category and projection onto the first factor is a strict double functor.

Note that if 𝔸 is not a strict double category neither is 𝔼l(F), but it is as strict as 𝔸 is. That the canonical projection 𝔼l(F) [figure] 𝔸 is strict is a precise way of saying this.

A natural transformation t : F [figure] G induces a functor over 𝔸

[figure: 𝔼l(F); 𝔸; 𝔼l(F); 𝔼l(G); T; 𝔼l(G); 𝔸]

given by the formulas T (A, x) = (A, t(A)(x)), T (f, y) = (f, t(B)(y)), T (v, r) = (v, t(v)(r)), T (α, s) = (α, t(w)(s)).

T is not strict but as strict as 𝔸. This is formally that T commutes strictly with the projection functor. We summarize this in the following.

3.9. Proposition. Natural transformations t : F [figure] G correspond bijectively to pseudo functors over 𝔸

[figure: 𝔼l(F); 𝔸; 𝔼l(F); 𝔼l(G); T; 𝔼l(G); 𝔸]

The correspondence preserves composition.

3.10. Remark. We could have stated the above proposition for T lax. It is automatically pseudo. Also if 𝔸 is strict, then so will T be. This is because 𝔼l(G) [figure] 𝔸 is a horizontal discrete fibration, a fact we will not use in this paper.

As is well known, the arrow notation for elements of a span can also be used to simplify calculations with profunctors. If P : A [figure: •] B is a profunctor, i.e. a functor P : A^{op} × B [figure] Set, we write x : A [figure: •; P] B to indicate that x ∈ P (A, B). The action of P on arrows

A′ [figure: a] A and B [figure: b] B′ is denoted P (a, B)(x) = xa and P (A, b)(x) = bx. Functoriality of P says that these actions are unitary and associative. If Q : B [figure] C is another profunctor, then an element of the composite Q⊗P is an equivalence class of “composable pairs” A [figure: •; x; P] B [figure: •; y; Q] C, denoted [A [figure: •; x; P] B [figure: •; y; Q] C] = y ⊗_{B} x. The equivalence relation is

generated by (y′b) ⊗_{B} x = y′ ⊗_{B′} bx

[figure: A; B′; •; x′; A; A; A; B; •; x; B; B′; b; B′; C; •; y′; B; B′; B; C; •; y; C; C]

A cell in ℂat

[figure: B; B′; G; A; B; •; P; A; A′; F; A′; B′; •; P′; t]

is a function which assigns equivariantly an element F A [figure: •; tx; P′] GB to each element A [figure: •; x; P] B.

This notation can be usefully extended to modules m : F [figure: •] G for F, G : 𝔸^{op} [figure] 𝕊et lax functors. When 𝔸 = 1, modules are profunctors. As with elements of lax functors the notation is more than that, it’s a double category, and this is the best way to organize its properties.

We write (v, z) : (A, x) [figure: •; m] (B, y) to indicate that x ∈ F A, y ∈ GB, v : A [figure: •] B, z ∈ m(v) such that z_{0} = x and z_{1} = y,

[figure: y∈; GB; z∈; y∈; z∈; mv; mv; GB; ( )_{1}; z∈; mv; x∈; z∈; x∈; F A; F A; mv; ( )_{0}]

The (v, z) are vertical arrows in a double category which we denote 𝔼l(F) +_{m} 𝔼l(G). It is the disjoint union of 𝔼l(F) with 𝔼l(G) with extra vertical arrows from 𝔼l(F) to 𝔼l(G), viz. the (v, z) above. Along with these vertical arrows are extra cells

[figure: (B, y); (B′, y′); (g,y′); (A, x); (B, y); •; (v,z); (A, x); (A′, x′); (f,x′); (A′, x′); (B′, y′); •; (v′,z′); (α,z′)]

when α is a cell in 𝔸

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

such that m(α)(z′) = z. There are no vertical arrows from 𝔼l(G) to 𝔼l(F) and no horizontal arrows in either direction. Composition of arrows (v, z) : (A, x) [figure: •; m] (B, y) with vertical arrows of 𝔼l(G), (w, s) : (B, y) [figure: •; G] (B̄, ȳ), is given by the left action of m

(w, s) · (v, z) = (w · v, s · z),
s · z = λ(w, v)(s, z).

Similarly, the right action of m produces a composition with vertical arrows of 𝔼l(F), (v̄, r) : (Ā, x̄) [figure: •] (A, x),

(v, z)(v̄, r) = (v · v̄, z · r),
z · r = ρ(v, v̄)(z, r).

Both horizontal and vertical composition of cells come straight from 𝔸. The module conditions (M4)-(M7) are summarized in the following.

3.11. Theorem. 𝔼l(F)+_{m} 𝔼l(G) is a double category and projecting onto the first factor is a strict double functor into 𝔸.

3.12. Remark. If K : 𝔸^{op} × 𝕍2 [figure] 𝕊et is the unique lax functor such that K(−, 0) = F, K(−, 1) = G and K(−, 01) = m, then 𝔼l(F) +_{m} 𝔼l(G) is exactly 𝔼l(K).

3.13. Example: Cat/A

Although the previous section shows a different aspect of the profunctor nature of modules we are still in unfamiliar territory. A more tractable example is when 𝔸 is horizontally discrete, i.e. it is just a category made into a vertical double category. We start with the simplest and most familiar case.

If 1 is the terminal double category, then as pointed out at the end of sections 2.2 and 2.3, a lax functor F : 1 [figure] 𝕊et “is” a small category and a natural transformation t : F [figure] G “is” a functor. If F and G correspond to categories X and Y, then a module m : F [figure: •] G is a span

[figure: F (∗); G(∗); m(1_{∗}); F (∗); m(1_{∗}); G(∗)]

with a right action of F (1_{∗}) and a left action of G(1_{∗}), so that m corresponds to a functor

M : X^{op} × Y [figure] Set

i.e. a profunctor M : X [figure: •] Y. It is easily seen that a modulation corresponds to a morphism of profunctors, so that lax functors, natural transformations, modules and modulations with domain 1 make up the double category ℂat. We can’t make this precise because we haven’t yet discussed composition of modules and modulations. There is no problem with horizontal composition of modulations, but vertical composition of modules does present some difficulties. This will be discussed in [17].

Nevertheless we can generalize this example. For a category A, the double category 𝕍A has the same objects as A, the arrows of A as its vertical arrows, and only identity horizontal arrows and cells. A lax functor F : 𝕍A [figure] 𝕊et is “the same as” a category over A. To be more precise, if Lax(𝕍A, 𝕊et) is the category of lax functors 𝕍A [figure] 𝕊et and natural transformations, we have an equivalence of categories

Lax(𝕍A, 𝕊et) ≃ Cat/A.

This is a reformulation of the observation due to Bénabou that Grothendieck’s construction of an opfibration from a pseudo functor A [figure] Cat can be generalized to give an equivalence between categories over A and lax normal functors from A into the bicategory of profunctors.

If F : 𝕍A [figure] 𝕊et is a lax functor, then 𝔼l(F) is horizontally discrete, i.e. all horizontal arrows are identities and all cells are horizontal identities. It is thus of the form 𝕍El(F) for an ordinary category El(F). The projection 𝕍El(F) [figure] 𝕍A is just a functor El(F) [figure] A. Conversely, any functor Φ : X [figure] A gives a lax functor F : 𝕍A [figure] 𝕊et by defining

F A = {X ∈ Ob(X)|ΦX = A}

F f = {x : X [figure] Y ∈ X|Φx = f}

with span projections “domain” and “codomain”.

By Proposition 3.9, a natural transformation t : F [figure] G corresponds to a pseudo functor over 𝕍A which, in the present situation, is simply a functor over A.

[figure: El(F); A; El(F); El(G); T; El(G); A]

The above equivalence now tells us what a profunctor over A should be. It should correspond to a module between the corresponding lax functors 𝕍A [figure] 𝕊et.

3.14. Theorem. Let F, G : 𝕍A [figure] 𝕊et be lax functors and Φ : B [figure] A, Ψ : C [figure] A the corresponding categories over A. Then there is a canonical correspondence between modules m : F [figure: •] G and paris (P, π) of a profunctor P : B [figure: •] C and a natural transformation π

[figure: C; A; Ψ; B; C; •; P; B; A; Φ; A; A; •; ^{Id^{A}}; π]

Modulations

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

correspond canonically to natural transformations

[figure: C; C′; s; B; C; •; P; B; B′; T; B′; C′; •; P′; ⇒^{τ}]

such that

[figure: C; C′; S; B; C; •; P; B; B′; T; B′; C′; •; P′; C′; A; Φ′; B′; C′; •; B′; A; Φ′; A; A; •; ^{Id^{A}}; =; C; A; Ψ; B; C; •; P; B; A; Φ; A; A; •; ^{Id^{A}}; ⇒^{τ}; ⇒^{π′}; ⇒^{π}]

These correspondences set up an equivalence between the category of modules and modulations with horizontal composition and the category whose objects are pairs (P, π) and whose morphisms are τ as above, with horizontal composition.

Proof. This is merely a matter of rearranging the data for modules into that for profunctor over A and vice versa.

3.15. Remark. The categories Cat/A are rarely cartesian closed so any hopes that 𝕃ax(𝔸^{op}, 𝕊et), being a kind of presheaf double category, be cartesian closed, are immediately dashed.

Recall from [10] the notion of comma double category. Given a lax functor Φ : 𝕏 [figure] ℤ and an oplax one 𝕐 [figure: •] ℤ, there is a double category (Ψ ⇓ Φ) and a cell in 𝔻oub

[figure: 𝕏; ℤ; Φ; (Ψ ⇓ Φ); 𝕏; •; (Ψ ⇓ Φ); 𝕐; 𝕐; ℤ; •; Ψ̄; κ]

satisfying some universal property. An object of (Ψ ⇓ Φ) is a triple (Y, ΨY [figure: z] ΦX, X), X an object of 𝕏, Y an object of 𝕐 and z a horizontal arrow of ℤ. A horizontal arrow is a pair of horizontal arrows x : X [figure] X′ and y : Y [figure] Y′ such that

[figure: ΨY′; ΦX′; z′; ΨY; ΨY′; Ψy; ΨY; ΦX; z; ΦX; ΦX′; Φx]

commutes. A vertical arrow is a triple (w, ξ, v)

[figure: Ȳ; Ψ̄Ȳ; Y; Ȳ; •; w; Y; ΨY; ΨY; Ψ̄Ȳ; •; Ψ̄Ȳ; ΦX̄; z̄; ΨY; Ψ̄Ȳ; •; Ψw; ΨY; ΦX; z; ΦX; ΦX̄; •; Φv; ΦX̄; X̄; ΦX; ΦX̄; •; ΦX; X; X; X̄; •; v; ξ̄]

with v, w vertical arrows and ξ a cell. Finally a cell is a pair of cells, one in 𝕏 and one in 𝕐 forming a commutative cube. It is the vertical composition that is interesting and involves the laxity and oplaxity cells. The composite (w̄, ξ̄, v̄) · (w, ξ, v) is

[figure: Ỹ; Ψ̄Ỹ; Ȳ; Ỹ; •; w̄; Ȳ; Ψ̄Ỹ; Ȳ; Y; Ȳ; •; w; Y; Ψ̄Y; Ψ̄Y; Ψ̄Ỹ; Ψ̄Ỹ; Ψ̄Ỹ; ^{Ψ̄Ȳ}; ^{Ψ̄Ȳ}; Ψ̄Ỹ; •; ^{Ψ̄w̄}; ^{Ψ̄Ȳ}; Ψ̄Y; Ψ̄Y; Ψ̄Y; Ψ̄Y; ^{Ψ̄Ȳ}; •; Ψ̄w; Ψ̄Ỹ; Ψ̄Ỹ; Ψ̄Y; Ψ̄Ỹ; •; Ψ̄(w̄·w); Ψ̄Y; Ψ̄Y; Ψ̄Y; Ψ̄Ỹ; ψ_{w̄,w}; Ψ̄Ỹ; ΦX̃; ^{Ψ̄Ȳ}; Ψ̄Ỹ; •; ^{Ψ̄Ȳ}; ΦX̄; ΦX̄; ΦX̃; •; Φv̄; ^{Ψ̄Ȳ}; ΦX̄; Ψ̄Y; ^{Ψ̄Ȳ}; Ψ̄Y; ΦX; ΦX; ΦX̄; •; Φv; ξ; ξ; ΦX̃; ΦX̃; ΦX̄; ΦX̃; ΦX̄; ΦX̃; ΦX̄; ΦX; ΦX̄; ΦX; ΦX; ΦX; ΦX̃; ΦX̃; ΦX; ΦX̃; ΦX; ΦX; ΦX; ΦX̃; •; Φ(v̄·v); ϕ_{v̄,v}; ΦX̃; X̃; ΦX̃; X̄; X̄; X̃; •; v̄; X̄; ΦX; ΦX; X; X; X̄; •; v]

The identity id_{(Y,z,X)} is

[figure: Y; ΨY; Y; Y; •; ^{id^{Y}}; Y; ΨY; ΨY; ΨY; •; ΨY; ΨY; ΨY; ΨY; •; Ψ(id_{Y} ); ΨY; ΨY; ΨY; ΨY; •; ^{id^{ΨY}}; ψ_{Y}; ΨY; ΦX; z; ΨY; ΨY; •; ΨY; ΦX; z; ΦX; ΦX; •; ^{id^{ΦX}}; ^{id^{z}}; ΦX; ΦX; ΦX; ΦX; •; ΦX; ΦX; ΦX; ΦX; •; Φid_{x}; ϕ_{X}; ΦX; X; ΦX; ΦX; •; ΦX; X; X; X; •; ^{id^{X}}]

It all works! See [10] for details, where it is shown, among other things, that an oplax F : 𝔸 [figure] 𝔹 is left adjoint to a lax U : 𝔹 [figure] 𝔸 if and only if there is an isomorphism of double categories over 𝔸 × 𝔹

[figure: (F ⇓ 1_{𝔹}); 𝔸 × 𝔹; (F ⇓ 1_{𝔹}); (1_{𝔸} ⇓ U); ≅; (1_{𝔸} ⇓ U); 𝔸 × 𝔹]

If Z is an object of ℤ and we take the comma double category

[figure: 1; ℤ; Z; (1_{ℤ}, Z); 1; (1_{ℤ}, Z); ℤ; ℤ; ℤ; 1_{ℤ}]

and get the (horizontal) slice double category ℤ//Z whose objects are horizontal arrows Z′ [figure] Z, horizontal arrows are commutative triangles, vertical arrows are cells

[figure: Z̄′; Z; Z′; Z̄′; •; Z′; Z; Z; Z; •; ^{id^{Z}}; ξ]

and cells are commutative prisms of cells

[figure: Z̄′; Z; Z̄′; Z̄′′; Z̄′′; Z; Z̄′; Z̄′′; Z′; Z̄′; •; Z′; Z′′; Z′′; Z̄′′; •; Z; Z; •; ^{id^{z}}; Z̄′; Z̄′′; Z′; Z; Z′; Z′′; Z′′; Z]

The patient reader will have realized by now that the point of this discussion is the following reformulation of Theorem 3.14.

3.16. Theorem. 𝕃ax(𝕍A, 𝕊et) ≃ ℂat//A.

Actually, the proof of this theorem is incomplete as we haven’t yet defined vertical composition in 𝕃ax(𝔸, 𝕊et), which we will do in the next section. For now we simply remark that, not only does a functor over A

[figure: B; A; F; B; C; K; C; A; G]

produce vertical morphisms

[figure: C; A; G; B; C; •; K_{∗}; B; A; F; A; A; •; ^{Id^{A}}; κ_{∗}; and; B; A; F; C; B; •; K^{∗}; C; A; G; A; A; •; ^{Id^{A}}; κ^{∗}]

which are, in fact, companion and conjoint to K in ℂat//A, but that upon examining the definitions of κ_{∗} and κ^{∗}, we see that an oplax triangle

[figure: B; A; F; B; C; K; C; A; G; ⇒^{κ}]

also gives a vertical morphism (K_{∗}, κ_{∗}), and a lax triangle

[figure: B; A; F; B; C; K; C; A; G; ⇐^{κ}]

gives one like (K^{∗}, κ^{∗}) above.

3.17. The Yoneda Lemma Part II

3.18. Theorem. (Yoneda Lemma II) Let F, G : 𝔸^{op} [figure] 𝕊et be lax functors and m : F [figure: •] G a module. Then for every v : A [figure: •] Ā, there is a bijection between elements r ∈ m(v) and modulations

[figure: 𝔸(−, Ā); G; t_{1}; 𝔸(−, A); 𝔸(−, Ā); •; 𝔸(−,v); 𝔸(−, A); F; t_{0}; F; G; •; m; μ]

given by r = μ(v)(1v).

Proof. Suppose we are given r ∈ m(v) and we wish to construct a modulation μ as in the statement. We will have a commutative diagram

[figure: 𝔸(Ā, Ā); GĀ; t_{1}Ā; 𝔸(v, v); 𝔸(Ā, Ā); ∂_{1}; 𝔸(v, v); m(v); μ(v); m(v); GĀ; ( )_{0}; 𝔸(v, v); m(v); 𝔸(A, A); 𝔸(v, v); ∂_{0}; 𝔸(A, A); F A; t_{0}A; F A; m(v); ( )_{0}]

Thus t_{0}A(1_{A}) = r_{0} and t_{1}Ā(1Ā) = r_{1}, which completely determine t_{0} and t_{1} (by Theorem 2.3). For a cell

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

horizontal naturality of μ (m2) requires

[figure: 𝔸(Ā, Ā); 𝔸(B̄, Ā); 𝔸(A, A); 𝔸(Ā, Ā); •; 𝔸(v,v); 𝔸(A, A); 𝔸(B, A); 𝔸(B, A); 𝔸(B̄, Ā); •; 𝔸(B̄, Ā); GB̄; 𝔸(B, A); 𝔸(B̄, Ā); •; 𝔸(w,v); 𝔸(B, A); F B; F B; GB̄; •; m(w); 𝔸(α,v); μ(w); =; 𝔸(Ā, Ā); GĀ; 𝔸(A, A); 𝔸(Ā, Ā); •; 𝔸(v,v); 𝔸(A, A); F A; F A; GĀ; •; m(v); GĀ; GB̄; F A; GĀ; •; F A; F B; F B; GB̄; •; m(w); m(α)]

If we apply both sides to 1_{v} we see that we must have

μ(w)(α) = m(α)(r).

Thus if there is a modulation μ it is unique and given by this formula. It is now simply a matter of checking that it does indeed define a modulation, and this is straightforward.

3.19. Corollary. There is a bijection between elements r ∈ F (v) and modulations

[figure: 𝔸(−, Ā); F; 𝔸(−, A); 𝔸(−, Ā); •; 𝔸(−,v); 𝔸(−, A); F; F; F; •; ^{id^{F}}; μ]

given by r = μ(v)(1_{v}).

3.20. Corollary. (Fullness on modulations) Every modulation

[figure: 𝔸(−, Ā); 𝔸(−, B̄); 𝔸(−, A); 𝔸(−, Ā); •; 𝔸(−,v); 𝔸(−, A); 𝔸(−, B); 𝔸(−, B); 𝔸(−, B̄); •; 𝔸(−,w); μ]

is of the form 𝔸(−, α) for a unique cell

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

We give a simple application of the Yoneda theorems we have so far, to the construction of tabulators for modules. Recall from [9] that a tabulator for a vertical arrow v : A [figure: •] Ā in a double category is an object T and a cell

[figure: T; Ā; A; T; A; Ā; •; v; τ]

with universal properties: (T1) For every cell

[figure: X; Ā; A; X; A; Ā; •; v; ξ]

there is a unique horizontal arrow x : X [figure] T such that τx = ξ; (T2) For every commutative tetrahedron of cells

[figure: X; Ā; X̄; A; X̄; Ā; X; X̄; •; x; X; A; A; Ā; •; v]

there is a unique cell ξ such that

[figure: T; X̄; X; T; X; X̄; •; x; T; Ā; A; T; A; Ā; •; v; ξ; τ]

gives the tetrahedron in the “obvious” way. (T2′) We state the “obvious”: given cells α_{0}, α_{1}, ξ_{0}, ξ_{1} such that

[figure: X̄; Ā; X; X̄; •; x; X; Ā; Ā; Ā; •; id; ξ_{1}; X; Ā; X; X; •; id; X; A; A; Ā; •; v; α_{0}; =; X̄; Ā; X̄; X̄; •; id; X̄; A; A; Ā; •; v; α_{1}; X̄; A; X; X̄; •; x; X; A; A; A; •; ^{id^{A}}; ξ_{0}]

there is a unique ξ such that

[figure: X̄; T; X; X̄; •; x; X; T; T; T; •; ^{id^{T}}; ξ; T; A; t_{0}; T; T; •; T; A; t_{0}; A; A; •; ^{id^{A}}; ^{id^{t_{0}}}; =; X̄; A; X; X̄; •; x; X; A; A; A; •; ^{id^{A}}; ξ_{0}]

[figure: X̄; T; X; X̄; •; x; X; T; T; T; •; ξ; T; Ā; t_{1}; T; T; •; T; Ā; t_{1}; Ā; Ā; •; ^{idĀ}; ^{id^{t_{1}}}; =; X̄; Ā; X; X̄; •; x; X; Ā; Ā; Ā; •; ^{id^{A}}; ξ_{1}]

[figure: X; T; X; X; •; ^{id^{X}}; X; T; T; T; •; ^{id^{T}}; id; T; Ā; t_{1}; T; T; •; T; A; t_{0}; A; Ā; •; v; τ; =; X; Ā; X; X; ^{id^{x}}; X; A; A; Ā; •; v; α_{0}]

[figure: X̄; T; X̄; X̄; •; ^{idX̄}; X̄; T; T; T; •; ^{id^{T}}; id; T; Ā; t_{1}; T; T; •; T; A; t_{0}; A; Ā; •; v; τ; =; X̄; Ā; X̄; X̄; •; X̄; A; A; Ā; •; v; α_{1}]

Now let m : F [figure: •] G be a module. If it has a tabulator, T, we can use 2.3 and 3.18 to discover what it is. Elements of T A are in bijection with natural transformations t : 𝔸(−, A) [figure] T which by (T1) are in bijection with modulations

[figure: 𝔸(−, A); G; 𝔸(−, A); 𝔸(−, A); •; ^{Id^{𝔸(−,A)}}; 𝔸(−, A); F; F; G; •; m; μ]

and as Id_{𝔸(−,A)} = 𝔸(−, id_{A}), such μ are in bijection with elements r ∈ m(id_{A}). So we take T (A) = m(id_{A}). It’s clear how T is horizontally functorial. In a similar way, elements of T (v) are in bijection with modulations

[figure: 𝔸(−, Ā); T; 𝔸(−, A); 𝔸(−, Ā); •; 𝔸(−,v); 𝔸(−, A); T; T; T; •; ^{id^{T}}; μ]

and these correspond to modulations α_{0}, α_{1}, ξ_{0}, ξ_{1} such that ξ_{1} · α_{0} = α_{1} · ξ_{0},

[figure: 𝔸(−, Ā); G; 𝔸(−, A); 𝔸(−, Ā); •; 𝔸(−,v); 𝔸(−, A); G; G; G; •; ^{id^{G}}; ξ_{1}; 𝔸(−, A); G; 𝔸(−, A); 𝔸(−, A); •; ^{Id^{𝔸(−,A)}}; 𝔸(−, A); F; F; G; •; m; α_{0}; =; 𝔸(−, Ā); G; 𝔸(−, Ā); 𝔸(−, Ā); •; ^{Id^{𝔸(−,Ā)}}; 𝔸(−, Ā); F; F; G; •; m; α_{1}; 𝔸(−, Ā); F; 𝔸(−, A); 𝔸(−, Ā); •; 𝔸(−,v); 𝔸(−, A); F; F; F; •; ^{id^{F}}; ξ_{0}]

and these correspond to elements r_{0} ∈ m(id_{A}), r_{1} ∈ m(idĀ), x_{0} ∈ F (v) and x_{1} ∈ G(v) such that x_{1} · r_{0} = r_{1} · x_{0} in the notation of §3.7. That is, T (v) is defined by the pullback diagram

[figure: m(idĀ) ⊗ F (v); m(v); T (v); m(idĀ) ⊗ F (v); T (v); G(v) ⊗ m(id_{A}); G(v) ⊗ m(id_{A}); m(v)]

Now, everything falls into place. The projections of T (v) onto T (A) and T (Ā) are (r_{0}, r_{1}, x_{0}, x_{1})_{0} = r_{0} and (r_{0}, r_{1}, x_{0}, x_{1}) = r_{1}. The multiplication for T is given by

(r_{1}, r_{2}, x̄_{0}, ȳ_{0}) · (r_{0}, r_{1}, x_{0}, y_{0}) = (r_{0}, r_{2}, x̄_{0} · x_{0}, ȳ_{0} · y_{0})

and the unit

id_{T} (r) = (r, r_{1}, id_{r}, id_{r}).

The natural transformation t_{0} : T [figure]F is given by t_{0}(A)(r) = r_{0} ∈ F A, and t_{0}(v)(r_{0}, r_{1}, x_{0}, x_{1}) = x_{0} ∈ F v. t_{1} : T [figure] G is similar. The modulation

[figure: T; G; T; T; •; ^{id^{T}}; T; F; F; G; •; m; τ]

is given by

τ(v)(r_{0}, r_{1}, x_{0}, x_{1}) = x_{0} · r_{0} = r_{1} · x_{0}.

Checking the universal property is equally straightforward.

4. The Yoneda Lemma Parts III and IV

In this section we will define the Yoneda embedding and discuss to what extent it is full and faithful. Then we show that it is dense, i.e. every lax functor 𝔸^{op} [figure] 𝕊et is a colimit of representables. We also show that every module is a colimit of representable modules.

We have almost all of the ingredients of the Yoneda embedding except for one crucial thing: 𝕃ax(𝔸^{op}, 𝕊et) is not yet a double category.

Composition of modules is problematic. In fact it doesn’t exist in general. Even composition of V-profunctors requires certain well-behaved colimits in V. It is straightforward, however, to define a rich enough structure to encode all of the information regarding composition so that the existence of composites is just a question of representability. We are referring of course to what we called “lax double categories” in [6]. This name is not ideal. It should be reserved for the case where all n-fold composites are given but unit laws and associativity only hold up to comparison cells. We adopt the “virtual double category” nomenclature of [5]. Other names in the literature are “T-catégories” [3], “fcmulticategories” [16], “multicategories with several objects” [11], and “multibicategories” [4]. In any case, it is precisely the structure preserved by lax functors. It is thus not surprising that it ends up playing a central role here.

As a matter of fact, composites of modules in 𝕃ax(𝔸^{op}, 𝕊et) are representable, although we don’t know if they are strongly representable. They certainly are in many important cases. These questions will be discussed in [17]. But the composites are complicated and in many cases it is best to work directly with the virtual double category, a position also put forward in [4]. We refer the reader to [6] for complete definitions.

4.1. Multimodulations

Let 𝔸 and 𝔹 be double categories, F_{0}, F_{1}, G_{0}, G_{1}, …, G_{k} lax functors from 𝔸 to 𝔹, t_{0}, t_{1} natural transformations and m, n_{1}, …, n_{k} modules as in the diagram

[figure: ⋮; F_{1}; ⋮; G_{k}; •; n_{k}; F_{1}; G_{k}; t_{1}; G_{1}; F_{0}; G_{0}; G_{1}; •; n_{1}; G_{0}; F_{0}; t_{0}; ⋮; F_{1}; G_{1}; ⋮; •; n_{2}; G_{1}; F_{0}; F_{0}; F_{1}; •; m]

4.2. Definition. A multimodulation μ with domains and codomains as in the above diagram is an assignment (mm1) for each A_{0} [figure: •; v_{1}] A_{1} [figure: •; v_{2}] ⋯ [figure: •; v_{k}] A_{k} in 𝔸 a cell in 𝔹

[figure: ⋮; F_{1}A_{k}; ⋮; G_{k}A_{k}; •; n_{k}(v_{k}); F_{1}A_{k}; G_{k}A_{k}; t_{1}A_{k}; G_{1}A_{1}; F_{0}A_{0}; G_{0}A_{0}; G_{1}A_{1}; •; n_{1}(v_{1}); G_{0}A_{0}; F_{0}A_{0}; t_{0}A_{0}; ⋮; F_{1}A_{k}; G_{1}A_{1}; ⋮; •; n_{2}(v_{2}); G_{1}A_{1}; F_{0}A_{0}; F_{0}A_{0}; F_{1}A_{k}; •; m(v_{k}·...·v_{1}); μ(v_{k},...,v_{1})]

satisfying (mm2) (horizontal naturality) for all vertically composable cells α_{1}, …, α_{k}

[figure: G_{k}A_{k}; G_{k}A′_{k}; ⋮; G_{k}A_{k}; •; n_{k}v_{k}; ⋮; ⋮; ⋮; G_{k}A′_{k}; •; ⋮; ⋮; G_{1}A_{1}; ⋮; •; n_{2}v_{2}; G_{1}A_{1}; G_{1}A′_{1}; G_{1}A′_{1}; ⋮; •; G_{1}A_{1}; G_{1}A′_{1}; G_{0}A_{0}; G_{1}A_{1}; •; n_{1}v_{1}; G_{0}A_{0}; G_{0}A′_{0}; G_{0}A′_{0}; G_{1}A′_{1}; •; ⋮; F_{1}A′_{k}; ⋮; G_{k}A′_{k}; •; F_{1}A′_{k}; G_{k}A′_{k}; ⋮; F_{1}A′_{k}; G_{1}A′_{1}; ⋮; •; G_{1}A′_{1}; F_{0}A′_{0}; F_{0}A′_{0}; F_{1}A′_{k}; •; m(v′_{n}·...·v′_{1}); G_{1}A′_{1}; F_{0}A′_{0}; G_{0}A′_{0}; G_{1}A′_{1}; •; G_{0}A′_{0}; F_{0}A′_{0}; n_{k}α_{k}; ⋮; n_{2}α_{2}; n_{1}α_{1}; μ; =; ⋮; F_{1}A_{k}; ⋮; G_{k}A_{k}; •; n_{k}v_{k}; F_{1}A_{k}; G_{k}A_{k}; F_{1}A_{k}; F_{1}A′_{k}; F_{0}A_{0}; F_{1}A_{k}; •; F_{0}A_{0}; F_{0}A′_{0}; F_{0}A′_{0}; F_{1}A′_{k}; •; ⋮; F_{1}A_{k}; G_{1}A_{1}; ⋮; •; n_{2}v_{2}; G_{1}A_{1}; F_{0}A_{0}; F_{0}A_{0}; F_{1}A_{k}; •; G_{1}A_{1}; F_{0}A_{0}; G_{0}A_{0}; G_{1}A_{1}; •; n_{1}v_{1}; G_{0}A_{0}; F_{0}A_{0}; μ; m(α_{k}·...·α_{1})]

(mm3_{l}) (left equivariance)

[figure: t_{1}v_{k+1}; μ; λ; G_{k}A_{k}; F_{1}A_{k+1}; G_{k}A_{k}; G_{k}A_{k+1}; •; G_{k}v_{k+1}; F_{1}A_{k+1}; G_{k}A_{k+1}; G_{k}A_{k}; F_{1}A_{k+1}; F_{1}A_{k}; G_{k}A_{k}; F_{1}A_{k}; F_{1}A_{k+1}; •; F v_{k+1}; ⋮; F_{1}A_{k}; ⋮; G_{k}A_{k}; •; n_{k}V_{k}; F_{1}A_{k}; G_{k}A_{k}; ⋮; F_{1}A_{k}; G_{1}A_{1}; ⋮; •; n_{2}v_{2}; G_{1}A_{1}; F_{0}A_{0}; F_{0}A_{0}; F_{1}A_{k}; •; m(···); G_{1}A_{1}; F_{0}A_{0}; G_{0}A_{0}; G_{1}A_{1}; •; n_{1}v_{1}; G_{0}A_{0}; F_{0}A_{0}; F_{1}A_{k+1}; F_{1}A_{k+1}; F_{1}A_{k}; F_{1}A_{k+1}; F_{1}A_{k}; F_{1}A_{k+1}; •; F_{0}A_{0}; F_{1}A_{k}; F_{0}A_{0}; F_{0}A_{0}; F_{0}A_{0}; F_{1}A_{k}; •; F_{0}A_{0}; F_{1}A_{k+1}; •; m(v_{k+1}·····v_{1}); λ_{k}; μ; G_{k}A_{k+1}; G_{k}A_{k+1}; G_{k}A_{k}; G_{k}A_{k+1}; G_{k}A_{k}; G_{k}A_{k+1}; •; G_{k}v_{k+1}; G_{k−1}A_{k−1}; G_{k}A_{k}; G_{k−1}A_{k−1}; G_{k−1}A_{k−1}; G_{k−1}A_{k−1}; G_{k}A_{k}; •; n_{k}v_{k}; G_{k}A_{k}; G_{k}A_{k+1}; G_{k−1}A_{k−1}; G_{k}A_{k}; G_{k−1}A_{k−1}; G_{k}A_{k+1}; •; n(v_{k+1}·v_{k}); G_{k−1}A_{k−1}; G_{k−1}A_{k−1}; ⋮; G_{k−1}A_{k−1}; ⋮; G_{k−1}A_{k−1}; •; ⋮; G_{k−1}A_{k−1}; ⋮; ⋮; ⋮; G_{k−1}A_{k−1}; •; ⋮; ⋮; G_{1}A_{1}; ⋮; G_{1}A_{1}; ⋮; •; G_{1}A_{1}; ⋮; G_{1}A_{1}; G_{1}A_{1}; G_{1}A_{1}; ⋮; n_{2}V_{2}; G_{1}A_{1}; G_{1}A_{1}; G_{0}A_{0}; G_{1}A_{1}; G_{0}A_{0}; G_{1}A_{1}; •; G_{0}A_{0}; G_{1}A_{1}; G_{0}A_{0}; G_{0}A_{0}; G_{0}A_{0}; G_{1}A_{1}; •; n_{1}v_{1}; F_{1}A_{k+1}; G_{k}A_{k+1}; G_{k−1}A_{k−1}; F_{1}A_{k+1}; G_{k−1}A_{k−1}; G_{k}A_{k+1}; •; F_{0}A_{0}; G_{1}A_{1}; G_{0}A_{0}; F_{0}A_{0}; G_{0}A_{0}; G_{1}A_{1}; •; F_{0}A_{0}; F_{1}A_{k+1}; •; =]

(mm3_{r}) (right equivariance)

[figure: ⋮; G_{k}A_{k}; •; n_{k}v_{k}; G_{1}A_{1}; ⋮; •; n_{2}v_{2}; G_{0}A_{0}; G_{1}A_{1}; •; n_{1}v_{1}; G_{0}A_{−1}; G_{0}A_{0}; •; G_{0}v_{0}; F_{0}A_{0}; F_{1}A_{k}; •; F_{0}A_{−1}; F_{0}A_{0}; •; F_{0}A_{−1}; F_{1}A_{k}; •; G_{k}A_{k}; F_{1}A_{k}; G_{0}A_{0}; F_{0}A_{0}; G_{0}A_{−1}; F_{0}A_{−1}; F_{1}A_{k}; F_{1}A_{k}; F_{0}A_{−1}; F_{0}A_{−1}; ⋮; G_{k}A_{k}; •; n_{k}v_{k}; G_{1}A_{1}; ⋮; •; n_{2}v_{2}; G_{0}A_{0}; G_{1}A_{1}; •; n_{1}v_{1}; G_{0}A_{−1}; G_{0}A_{0}; •; G_{0}v_{0}; ⋮; G_{k}A_{k}; •; G_{1}A_{1}; ⋮; •; G_{0}A_{−1}; G_{1}A_{1}; •; F_{0}A_{−1}; F_{1}A_{k}; •; G_{k}A_{k}; G_{k}A_{k}; G_{1}A_{1}; G_{1}A_{1}; G_{0}A_{−1}; G_{0}A_{−1}; G_{k}A_{k}; F_{1}A_{k}; G_{0}A_{−1}; F_{0}A_{−1}; μ; t_{0}v_{0}; ρ; ρ_{0}; μ; =]

(mm3_{i}) (inner equivariance) for every 1 ≤ i < k

[figure: ⋮; G_{k}A_{k}; •; G_{i+1}A_{i+1}; ⋮; •; G_{i}Ā_{i}; G_{i+1}A_{i+1}; •; n_{i+1}v_{i+1}; G_{1}A_{i}; G_{i}Ā_{i}; •; G_{i}v̄_{i}; G_{i−1}A_{i−1}; G_{1}A_{i}; •; n_{i}v_{i}; ⋮; G_{i−1}A_{i−1}; •; G_{0}A_{0}; ⋮; •; ⋮; G_{k}A_{k}; •; G_{i+1}A_{i+1}; ⋮; •; G_{i}Ā_{i}; G_{i+1}A_{i+1}; •; G_{i−1}A_{i−1}; G_{i}Ā_{i}; •; ⋮; G_{i−1}A_{i−1}; •; G_{0}A_{0}; ⋮; •; G_{k}A_{k}; G_{k}A_{k}; G_{i+1}A_{i+1}; G_{i+1}A_{i+1}; G_{i}Ā_{i}; G_{i}Ā_{i}; G_{i−1}A_{i−1}; G_{i−1}A_{i−1}; G_{0}A_{0}; G_{0}A_{0}; F_{0}A_{0}; F_{1}A_{k}; •; G_{k}A_{k}; F_{1}A_{k}; G_{0}A_{0}; F_{0}A_{0}; ⋮; G_{k}A_{k}; •; G_{i+1}A_{i+1}; ⋮; •; G_{i}Ā_{i}; G_{i+1}A_{i+1}; •; n_{i+1}v_{i+1}; G_{1}A_{i}; G_{i}Ā_{i}; •; G_{i}v̄_{i}; G_{i−1}A_{i−1}; G_{1}A_{i}; •; n_{i}v_{i}; ⋮; G_{i−1}A_{i−1}; •; G_{0}A_{0}; ⋮; •; ⋮; G_{k}A_{k}; •; G_{i+1}A_{i+1}; ⋮; •; G_{i}Ā_{i}; G_{i+1}A_{i+1}; •; G_{i−1}A_{i−1}; G_{i}Ā_{i}; •; ⋮; G_{i−1}A_{i−1}; •; G_{0}A_{0}; ⋮; •; G_{k}A_{k}; G_{k}A_{k}; G_{i+1}A_{i+1}; G_{i+1}A_{i+1}; G_{1}A_{i}; G_{i}Ā_{i}; G_{i−1}A_{i−1}; G_{i−1}A_{i−1}; G_{0}A_{0}; G_{0}A_{0}; F_{0}A_{0}; F_{1}A_{k}; •; G_{k}A_{k}; F_{1}A_{k}; G_{0}A_{0}; F_{0}A_{0}; λ_{i}; μ; ρ_{i+1}; μ; =]

It is understood that an empty composite is an identity and when k = 0 (mm1) and (mm2) still make sense but none of (mm3_{r}), (mm3_{l}) or (mm3_{i}) do. We, instead, require the condition (mm3_{0})

[figure: G_{0}A_{1}; G_{0}A_{1}; G_{0}A_{0}; G_{0}A_{1}; •; G_{0}v; G_{0}A_{0}; G_{0}A_{0}; G_{0}A_{0}; G_{0}A_{1}; ≅; G_{0}A_{1}; F_{1}A_{1}; G_{0}A_{0}; G_{0}A_{1}; •; G_{0}v; G_{0}A_{0}; F_{1}A_{0}; F_{1}A_{0}; F_{1}A_{1}; •; F_{1}v; t_{1}v; G_{0}A_{0}; F_{1}A_{0}; G_{0}A_{0}; G_{0}A_{0}; •; ^{id^{G_{0}A_{0}}}; G_{0}A_{0}; F_{0}A_{0}; F_{0}A_{0}; F_{1}A_{0}; •; m(id_{A_{0}}); μA_{0}; F_{1}A_{1}; F_{1}A_{1}; F_{0}A_{0}; F_{1}A_{1}; F_{0}A_{0}; F_{0}A_{0}; F_{0}A_{0}; F_{1}A_{1}; •; m(v); λ; =; G_{0}A_{1}; G_{0}A_{1}; G_{0}A_{0}; G_{0}A_{1}; •; G_{0}v; G_{0}A_{0}; G_{0}A_{0}; G_{0}A_{0}; G_{0}A_{1}; ≅; G_{0}A_{1}; F_{1}A_{1}; G_{0}A_{1}; G_{0}A_{1}; •; id^{^{G_{0}}^{A_{1}}}; G_{0}A_{1}; F_{0}A_{1}; F_{0}A_{1}; F_{1}A_{1}; •; m(id_{A_{1}}); μA_{1}; G_{0}A_{1}; F_{0}A_{1}; G_{0}A_{0}; G_{0}A_{1}; •; G_{0}v; G_{0}A_{0}; F_{0}A_{0}; F_{0}A_{0}; F_{0}A_{1}; •; F_{0}v; t_{0}v; F_{1}A_{1}; F_{1}A_{1}; F_{0}A_{0}; F_{1}A_{1}; F_{0}A_{0}; F_{0}A_{0}; F_{0}A_{0}; F_{1}A_{1}; •; m(v); ρ]

Although this last condition is certainly reasonable, it may raise some suspicions in the cautious reader. The following theorem should allay these concerns.

4.3. Theorem. With these definitions, 𝕃ax(𝔸, 𝔹) is a virtual double category. Identities are strongly representable.

Proof. We refer the reader to [17] for a complete proof. We simply mention that the identity on G is indeed the module we have been referring to as Id_{G} : G [figure: •] G, viz. Id_{G}(v) = G(v). Given a multimodulation

[figure: G; F_{1}; F_{0}; G; F_{0}; F_{1}; •; m; μ]

it extends to a modulation

[figure: G; F_{1}; G; G; •; ^{Id^{G}}; G; F_{0}; F_{0}; F_{1}; •; m; μ̄]

by defining μ̄(v) to be either side of the equation (mm3_{0}).

Now that we understand 𝕃ax(𝔸^{op}, 𝕊et) as a virtual double category, it will be useful to upgrade our Theorem 3.18 to the following.

4.4. Theorem. [Yoneda Lemma II ^{+}] Let m : F [figure: •] G be a module between lax functors F, G : 𝔸^{op} [figure] 𝕊et, and A_{0} [figure: •; v_{1}] A_{1} [figure: •; v_{2}] A_{2} ⋯ [figure: •; v_{k}] A_{k} vertical morphisms. Then there is a bijection between multimodulations

[figure: ⋮; G; ⋮; 𝔸(−, A_{k}); •; 𝔸(−,v_{k}); G; 𝔸(−, A_{k}); ⋮; G; 𝔸(−, A_{1}); ⋮; •; 𝔸(−,v_{2}); 𝔸(−, A_{1}); F; F; G; •; m; 𝔸(−, A_{1}); F; 𝔸(−, A_{0}); 𝔸(−, A_{1}); •; 𝔸(−,v_{1}); 𝔸(−, A_{0}); F; μ]

and elements x ∈ m(v_{k} · . . . · v_{1}) given by

x = μ(v_{k}, …, v_{1})(1_{v_{k}}, …, 1_{v_{1}}).

Proof. μ is an assignment taking vertically composable cells α_{1}, …, α_{k} to elements μ(α_{k}, … α_{1}) ∈ m(v_{k} · . . . · v_{1}), satisfying certain conditions, one of which is naturality

μ(α′_{k}α_{k}, …, α′_{1}α_{1}) = m(α_{k} · . . . · α_{1})μ(α′_{e}, …, α′_{1}).

It follows that

μ(α_{k}, …, α_{1}) = m(α_{k} · . . . · α_{1})μ(1_{v_{k}}, …, 1_{v_{1}}),

so that μ is uniquely determined by this formula. It is now just a matter of calculation to check that μ defined by

μ(α_{k}, …, α_{1}) = m(α_{k} · . . . · α_{1})(x)

does indeed define a multimodulation.

4.5. Corollary. The composite of 𝔸(−, v_{k}), 𝔸(−, v_{k−1}), ⋯, 𝔸(−, v_{1}) exists and is represented by 𝔸(−, v_{k} · . . . · v_{1}).

4.6. Corollary. Every multimodulation

[figure: ⋮; 𝔸(−, A′_{1}); ⋮; 𝔸(−, A_{k}); •; 𝔸(−,v_{k}); 𝔸(−, A′_{1}); 𝔸(−, A_{k}); ⋮; 𝔸(−, A′_{1}); 𝔸(−, A_{1}); ⋮; •; 𝔸(−,v_{2}); 𝔸(−, A_{1}); 𝔸(−, A′_{0}); 𝔸(−, A′_{0}); 𝔸(−, A′_{1}); •; 𝔸(−,v′); 𝔸(−, A_{1}); 𝔸(−, A′_{0}); 𝔸(−, A_{0}); 𝔸(−, A_{1}); •; 𝔸(−,v_{1}); 𝔸(−, A_{0}); 𝔸(−, A′_{0}); μ]

is of the form 𝔸(−, α) for a unique cell

[figure: ⋮; ^{A′^{1}}; ⋮; A_{k}; •; v_{k}; ^{A′^{1}}; A_{k}; ⋮; ^{A′^{1}}; A_{1}; ⋮; •; v_{2}; A_{1}; ^{A′^{0}}; ^{A′^{0}}; ^{A′^{1}}; •; v′; A_{1}; ^{A′^{0}}; A_{0}; A_{1}; •; v_{1}; A_{0}; ^{A′^{0}}; α]

where 𝔸(−, α)(v_{k}, …, v_{1})(α_{k}, …, α_{1}) = α(α_{k}, …, α_{1}).

4.7. The Yoneda Embedding

We now have all the ingredients to define the Yoneda functor Y : 𝔸 [figure] 𝕃ax(𝔸^{op}, 𝕊et). As we are considering 𝕃ax(𝔸^{op}, 𝕊et) to be a virtual double category, we will also consider 𝔸 to be one in the canonical way, viz. a multicell with horizontal domain

A_{0} [figure: •; v_{1}] A_{1} [figure: •; v_{2}] ⋯ [figure: •; v_{k}] A_{k}

is the corresponding cell with horizontal domain v_{k} · . . . · v_{1} : A_{0} [figure: •] A_{k}.

4.8. Theorem. [Yoneda Lemma III] Y : 𝔸 [figure] 𝕃ax(𝔸^{op}, 𝕊et) defined by Y A = 𝔸(−, A), Y f = 𝔸(−, f), Y v = 𝔸(−, v), Y α = 𝔸(−, A), is a strong functor (vertical composition is preserved up to special isomorphism) which is full and faithful on horizontal arrows and multicells.

Y is called the Yoneda embedding. It is not full on vertical arrows as we can see by taking 𝔸 = 1. Then Y becomes the double functor 1 [figure] ℂat whose value is the category 1. Modules 1 [figure: •] 1 are profunctors and so are in bijection with sets.

However it is straightforward to give the “correct” definition of a fully faithful functor between category objects in an arbitrary category with pullbacks, viz. F : 𝔸 [figure] 𝔹 is fully faithful if

[figure: A_{0} × A_{0}; B_{0} × B_{0}; F_{0}×F_{0}; A_{1}; A_{0} × A_{0}; (∂_{0},∂_{1}); A_{1}; B_{1}; F_{1}; B_{1}; B_{0} × B_{0}; (∂_{0}∂_{1})]

is a pullback diagram. When we apply this definition to a category object in Cat, we get the definition of a full and faithful double functor as one which is full and faithful on horizontal arrows and cells, with no mention of vertical arrows. This we call horizontally full and faithful. It’s a small step to define horizontal full and faithfulness for virtual double categories, and that is exactly what Y is.

Although Y is far from full on vertical arrows, it is “locally faithful”: if 𝔸(−, v) ≅ 𝔸(−, v′) (special isomorphism) then v ≅ v′. This is an immediate consequence of it being full and faithful on multicells.

4.9. Density

4.10. Theorem. [Yoneda Lemma IV] Any lax functor F : 𝔸^{op} [figure] 𝕊et is a colimit of representables, namely the colimit of 𝔼l(F) [figure: P] 𝔸 [figure: Y] 𝕃ax(𝔸^{op}, 𝕊et).

Proof. 𝔼l(F) is the double category of elements of F introduced in §3.7; and we are dealing of course with horizontal double colimits.

We first construct a colimiting cocone λ : Y P [figure] F. For (A, x) in 𝔼l(F),

λ(A, x) : 𝔸(−, A) [figure] F

is the unique natural transformation for which λ(A, x)(A)(1_{A}) = x guaranteed by 2.3. For a vertical arrow (v, r) : (A, κ) [figure: •] (Ā, x̄) in 𝔼l(F), we define

[figure: 𝔸(−, Ā); F; λ(Ā,x̄); 𝔸(−, A); 𝔸(−, Ā); •; 𝔸(−,v); 𝔸(−, A); F; λ(A,x); F; F; •; ^{id^{P}}]

to be the unique modulation for which λ(v, r)(v)(1_{v}) = r guaranteed by 3.18. It is straightforward to check horizontal naturality and vertical functoriality of λ. A useful technique in this regard is to use the fact that two natural transformations (or modulations) whose domain is a representable, are equal if they have the same value at the identity. The same technique can be used in checking the details of the next step.

If κ : Y P [figure] G is another cocone, we would like to show that there is a unique natural transformation t : F [figure] G such that tλ = κ. For any x ∈ F A we must have

[figure: 𝔸(−, A); G; κ(A,x); F; 𝔸(−, A); λ(A,x); F; G; t]

and following 1_{A} in the diagram

[figure: 𝔸(A, A); GA; κ(A,x)(A); F A; 𝔸(A, A); λ(A,x)(A); F A; GA; tA]

we see that t(A)(x) must be κ(A, x)(A)(1_{A}). For any (v, r) : (A, x) [figure: •] (Ā, x̄) we must have

[figure: 𝔸(−, Ā); F; λ(Ā,x̄); 𝔸(−, A); 𝔸(−, Ā); •; 𝔸(−,v); 𝔸(−, A); F; λ(A,x); F; F; •; ^{id^{F}}; λ(v,r); F; G; t; F; F; •; F; G; t; G; G; •; ^{id^{G}}; ^{id^{t}}; =; 𝔸(−, Ā); G; κ(Ā,x̄); 𝔸(−, A); 𝔸(−, Ā); •; 𝔸(−,v); 𝔸(−, A); G; κ(A,x); G; G; •; ^{id^{G}}; κ(v,r)]

which, when evaluated at 1_{v} gives

t(v)(r) = κ(v, r)(v)(1_{v}).

Thus t is uniquely determined by tλ = κ. Checking that t is a natural transformation poses no problem.

We omit the details of the two-dimensional universal property which is straightforward but long and uninformative.

We end with a simple example, 𝔸 = 1. 𝕃ax(1, 𝕊et) is equivalent to ℂat and there is only one representable and this corresponds to the category 1. If F : 1 [figure] 𝕊et is a lax functor corresponding to the category A, then 𝔼l(F) = 𝕍A, the vertical double category determined by A. The diagram P Y from the above theorem is the constant functor Δ1 : 𝕍A [figure] 𝕊et with value 1. If G : 1 [figure] 𝕊et is another lax functor, corresponding to a category B, then a cocone Δ1 [figure] G corresponds to a functor A [figure] B. The universal such functor is 1_{A} : A [figure] A. Thus we see how every category is a double colimit of copies of 1.

References

[1] Batanin, M., Monoidal globular categories as a natural environment for the theory of weak ncategories, Adv. Math. 136, 39-103 (1998).

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

[3] Burroni, A., T -catégories (catégories dans un triple), Cahiers Topologie Géom. Différentielle, Vol. XII (1971), No. 3, pp. 215-321.

[4] Cockett, J.R.B., Koslowski, J., Seely, R.A.G., Wood, R.J., Modules, Theory Appl. Categ. 11 (2003), No. 17, pp. 375-396.

[5] Cruttwell, G.S.H., Shulman, M., A Unified Framework for Generalized Multicategories, Theory Appl. Categ., Vol. 24, No. 21, 2010, pp. 580-655.

[6] Dawson, R.J.M., Paré, R., Pronk, D.A., Universal properties of Span, in The Carboni Festschrift, Theory Appl. Categ. 13 (2005), pp. 61-85.

[7] Ehresmann, C., Catégories et structures, Dunod, Paris, 1965.

[8] Fiore, T., Gambino, N., Kock, J., Double Adjunctions and Free Monads, arXiv:1105.620, 31 May

YONEDA THEORY FOR DOUBLE CATEGORIES  489

[9] Grandis, M., Paré, R., Limits in double categories, Cahiers Topologie Géom. Différentielle Catég. 40 (1999), 162-220.

[10] Grandis, M., Paré, R., Adjoint for double categories, Cahiers Topologie Géom. Différentielle Catég. 45 (2004), 193-240.

[11] Hermida, C., Representable multicategories, Adv. Math. 151 (2000), pp. 164-225.

[12] Joyal, A., Street, R., Braided Tensor Categories, Adv. Math. 102, 20-78 (1993).

[13] Kelly, G.M., Doctrinal Adjunction, in Category Seminar, Lecture Notes in Math., (1974), Vol. 420, 257-280.

[14] Kelly, G.M., Basic concepts of enriched category theory, London Math. Soc. Lecture Note Ser., No. 64, Cambridge Univ. Press, New York 1982.

[15] Lack, S., Icons, Appl. Categ. Structures, (2010) 18: 289-307.

[16] Leinster, T., Higher Operads, Higher Categories, London Math. Soc. Lecture Note Ser., No. 298, Cambridge Univ. Press, 2004.

[17] Paré, R., The Double Category of Lax Presheaves, in preparation.

[18] Shulman, M., Framed bicategories and monoidal fibrations, Theory Appl. Categ. 20:650-738, 2008.

[19] Street, R., Fibrations and Yoneda’s Lemma in a 2-category, in Category Seminar, Sydney 1972/73, Lecture Notes in Math., no. 420 (1974), 104-133, Springer Verlag.

[20] Street, R., Walters, R.F.C., Yoneda structures on 2-categories, J. Algebra 50 (1978), 350-379.

[21] Weber, M., Yoneda structures from 2-toposes, Appl. Categ. Structures, (2007) 15: 259-323.

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/25/17/25-17.{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 Martin Hyland, University of Cambridge: M.Hyland@dpmms.cam.ac.uk P. T. Johnstone, University of Cambridge: ptj@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 Glasgow, Tom.Leinster@glasgow.ac.uk Jean-Louis Loday, Université de Strasbourg: loday@math.u-strasbg.fr 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 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