Theory and Applications of Categories, Vol. 16, No. 18, 2006, pp. 460–521.

PATHS IN DOUBLE CATEGORIES

R. J. MACG. DAWSON, R. PARÉ, AND D. A. PRONK

Abstract. Two constructions of paths in double categories are studied, providing algebraic versions of the homotopy groupoid of a space. Universal properties of these constructions are presented. The first is seen as the codomain of the universal oplax morphism of double categories and the second, which is a quotient of the first, gives the universal normal oplax morphism. Normality forces an equivalence relation on cells, a special case of which was seen before in the free adjoint construction. These constructions are the object part of 2-comonads which are shown to be oplax idempotent. The coalgebras for these comonads turn out to be Leinster’s fc-multicategories, with representable identities in the second case.

Introduction

In [DPP1] and [DPP2] we studied the 2-category Π_{2}A obtained by freely adjoining right adjoints to each arrow of a category A considered as a locally discrete 2-category. The 2-category Π_{2}A was conceived as a more informative 2-dimensional version of Π_{1}A, which is obtained from A by freely inverting all arrows, and indeed, Π_{1}A can be obtained by applying Π_{0} locally in Π_{2}A. Morphisms of Π_{2}A are zig-zag paths of arrows of A which may be thought of as paths of spans in A. The cells of Π_{2}A are a bit more complicated, being equivalence classes of certain diagrams, which we call fences and which formally look like directed homotopies between the paths.

In [DPP3] we studied several universal properties of the Span construction applied to categories with pullbacks, each expressing the sense in which Span (A) is the result of adjoining right adjoints for the arrows of A.

It should be instructive to break the construction of Π_{2}A into two steps, first applying the span construction and then taking paths. Each construction is interesting in its own right. In the sequel to this paper [DPP4] we generalise the span construction to apply to categories without pullbacks and even 2-categories. We give there its universal properties and relate it to the Π_{2} construction. In that paper we will also see the advantages of using double categories and even Leinster’s fc-multicategories rather than bicategories.

This paper is concerned with the “pathology” of double categories. After a prologue in which we review two path constructions for mere categories we begin our study of paths in double categories. The first, simpler, construction gives the universal oplax morphism of double categories. (The universal oplax morphism for 2-categories will be derived from this in [DPP4].) The resulting comonad in double categories is in fact an oplax idempotent comonad (also known as KZ-comonad). The Kleisli morphisms are the oplax morphisms of double categories, which is not surprising. What is perhaps more surprising is that the Eilenberg-Moore coalgebras turn out to be exactly Leinster’s fc-multicategories, so that these are precisely the structures corresponding to oplax morphisms and we call them oplax double categories.

All three authors are supported by NSERC grants.

Received by the editors 2006-03-30 and, in revised form, 2006-08-16.

Transmitted by R. Brown. Published on 2006-08-28.

2000 Mathematics Subject Classification: 18A40, 18C20, 18D05.

Key words and phrases: double categories, oplax double categories, paths, localisation.

\begin{matrix}c \\ ◯ \end{matrix} R. J. MacG. Dawson, R. Paré, and D. A. Pronk, 2006. Permission to copy for private use granted.

Working with oplax morphisms, we rapidly find ourselves wanting more structure, and in order to get any significant results we need the morphisms to be at least normal. Accordingly, our second path construction gives the universal oplax normal morphism of double categories. Here is where the equivalence relation on fences in the Π_{2} construction comes in. The Kleisli morphisms for this second path construction are, not surprisingly, the oplax normal morphisms of double categories. We identify an interesting class of fc-multicategories that constitute the Eilenberg-Moore coalgebras for this comonad.

Both of these constructions are like the fundamental groupoid of a topological space. Further study of this analogy should prove fruitful.

0. Prologue

Let Cat be the category of small categories and Gph the category of directed multigraphs. The forgetful functor U: Cat → Gph has a left adjoint F which takes a graph to the category whose objects are nodes and whose morphisms are compatible paths of edges

• ⟶^{f_{1}} • ⟶^{f_{2}} • ⟶^{f_{3}} ⋯ ⟶^{f_{n}} •

for n ⩾ 0. Composition is given by concatenation and identities are paths of length zero. Thus we get a monad ( )^{∗} on Gph whose Eilenberg-Moore algebras are small categories; i.e., U is monadic. This of course is well known. What is perhaps less well known is that, in the spirit of Barr’s paper [Ba], F is comonadic. Thus, a graph may be considered as a category equipped with a costructure.

It will be instructive for us to work out in detail how this works. The triple (F U, ε, F ηU) is a comonad on Cat which we shall denote by (Path, E, D). Thus, for a category A, Path (A) is the category with the same objects as A but whose morphisms are paths

A_{0} ⟶^{f_{1}} A_{1} ⟶^{f_{2}} ⋯ ⟶^{f_{n}} A_{n}

of composable morphisms of A, denoted by ⟨f_{i}⟩_{i∈{1,...,n}}. Both E and D are the identity on objects. The counit E: Path (A) → A is given by E(⟨f_{i}⟩) = f_{n} ∘ f_{n−1} ∘ ⋯ ∘ f_{1}, which we will also denote by ∏_{i=1}^{n} f_{i}. The comultiplication D: Path (A) → Path Path (A) takes a path ⟨f_{i}⟩_{i∈{1,...,n}} to the path ⟨⟨f_{i}⟩⟩_{i∈{1,...,n}}, i.e., the path of paths of length n where each inside path has length one.

A coalgebra, then, is a category A with a comultiplication (coaction) G: A → Path (A). The counit law

[figure: A; G; Path (A); E; A]

says that G is the identity on objects and factorises every morphism into a string of compatible morphisms. While this may appear to require rather arbitrary choices, in fact the coassociativity law removes the arbitrariness.

The coassociativity law of a coalgebra requires the following diagram to commute:

\xymatrix{A \ar[r]^{G} \ar[d]_{G} & Path(A) \ar[d]^{Path (G)} \\ Path (A) \ar[r]_{D} & Path Path(A).}

In detail, this says that for every f: A → B, factored by G into ⟨f_{i}⟩, the path of paths

⟨⟨f_{ij}⟩_{j∈{1,...,m_{i}}}⟩_{i∈{1,...,n}}

obtained by applying G to each of the f_{i} is equal to ⟨⟨f_{i}⟩⟩_{i∈{1,...,n}}. Thus, each path ⟨f_{ij}⟩_{j∈{1,...,m_{i}}} has length one and f_{ij} = f_{i}; and G applied to f_{i} returns f_{i} itself. Now, these f_{i} cannot be identity arrows because, as a functor, G takes an identity arrow to a path of length zero. Moreover, the f_{i} cannot be factored non-trivially into two arrows, since if f_{i} = gh with both g and h non-identity arrows then G(f_{i}) = G(g)G(h) would have length greater than one. We will call an arrow f ≠ 1 prime if it cannot be factored in a non-trivial way, i.e., f = gh implies g = 1 or h = 1. The factorisation G is thus a prime factorisation, and it is unique because Gg = ⟨g⟩ for any prime g. Indeed, if f = f_{n} ∘ f_{n−1} ∘ ⋯ ∘ f_{1} = g_{m} ∘ g_{m−1} ∘ ⋯ ∘ g_{1} where all the f_{i} and g_{j} are prime, then

⟨f_{i}⟩_{i∈{1,...,n}} = ⟨f_{n}⟩ ∘ ⟨f_{n−1}⟩ ∘ ⋯ ∘ ⟨f_{1}⟩
= G(f_{n}) ∘ G(f_{n−1}) ∘ ⋯ ∘ G(f_{1})
= G(g_{m}) ∘ G(g_{m−1}) ∘ ⋯ ∘ G(g_{1})
= ⟨g_{m}⟩ ∘ ⟨g_{m−1}⟩ ∘ ⋯ ∘ ⟨g_{1}⟩
= ⟨g_{j}⟩_{j∈{1,...,m}},

so m = n and f_{i} = g_{i} for all i ∈ {1, …, n}. It follows that A is the free category on the graph whose nodes are the objects of A and whose edges are the prime arrows of A.

Given two coalgebras (A, G) and (B, H), for any homomorphism

Φ: (A, G) → (B, H)

the following square commutes

\xymatrix{A \ar[d]_{G} \ar[r]^{Φ} & B \ar[d]^{H} \\ Path (A) \ar[r]_{Path (Φ)} & Path (B).}

So, for any f: A → B, with G-factorisation f = f_{n} ∘ f_{n−1} ∘ ⋯ ∘ f_{1}, the H-factorisation of Φ(f) is given by Φ(f_{n}) ∘ Φ(f_{n−1}) ∘ ⋯ ∘ Φ(f_{1}). As primes are those arrows whose factorisation has length one, Φ preserves primes and so restricts to the prime graphs. That is to say, every coalgebra morphism comes from a morphism of graphs. We have thus established an equivalence of categories

Gph ≃ Cat_{Path}.  (1)

0.1. Remarks.

1. Although Path is a natural comonad on Cat, it does not preserve natural transformations, so it is not a 2-functor. Given a natural transformation t: Φ → Φ′, one might be tempted to define Path (t): Path (Φ) → Path (Φ′) at A to be the path of length one, ⟨t(A)⟩: ΦA → Φ′A, but the naturality squares won’t commute, except in the most trivial cases, because in Path (A) nothing commutes non-trivially.

2. For any category A there is at most one coalgebra structure on it, a rather strong property usually associated with idempotent (co)monads. We will be able to explain better why this is the case once we have introduced the double category version ℙath of this construction.

3. The Kleisli category of Path has small categories as its objects but its morphisms are ‘functors’ which preserve neither composition nor identities, pretty poor morphisms indeed.

4. We could have used the comonadicity theorem to get the above equivalence (1). Indeed, Gph has all equalisers and F reflects isomorphisms and preserves equalisers, as is easily checked.

We wish to examine a similar construction over the category Rgph of reflexive graphs. A reflexive graph is a graph as above with the specification of a distinguished loop 1_{A}: A →

A for each vertex A. It is thus determined by a diagram of the form \xymatrix{E \ar[r]^{s} \ar[r]_{t} & V \ar[l]|{i}} in Set

with si = ti = 1_{V}. Again there is a forgetful functor U: Cat → Rgph which has a left adjoint F. For a reflexive graph G, F (G) is the category whose objects are the nodes of G and whose morphisms are equivalence classes of directed paths of edges, two paths being equivalent if one can be obtained from the other by inserting and/or deleting identity loops. Each equivalence class has a canonical representative, namely the path without any identities. Equivalently, F (G) could have been defined as having morphisms which are paths without identities. This result is useful for some computations, but should be treated with some caution as it does not generalise for graphs in an arbitrary topos.

Once again, it is well-known that Cat is monadic over Rgph. Indeed, an algebra structure UF G → G on a reflexive graph G equips it with a family of n-fold composition operations defined on compatible paths of non-identity arrows. As this is a morphism of reflexive graphs, the empty path at A is sent to 1_{A}. Moreover, the unit law says that paths of length one compose to themselves, and the associative law says that for a path of paths, we have

(f_{k_{n}} ∘ f_{k_{n}−1} ∘ ⋯ ∘ f_{l_{n}}) ∘ ⋯ ∘ (f_{k_{1}} ∘ ⋯ ∘ f_{2} ∘ f_{1}) = f_{k_{n}} ∘ ⋯ ∘ f_{2} ∘ f_{1}.

Clearly, such a family of composition operations is determined by an associative binary composition operation, and we know how to compose with identities.

However, it is the comonad induced on Cat we are interested in. We denote it by (Path_{∗}, E_{∗}, D_{∗}) with counit E_{∗} and comultiplication D_{∗}. For a category A, Path_{∗}(A) has the same objects as A and has as morphisms compatible paths of non-identity morphisms. For a functor Φ: A → B, Path_{∗}(Φ) is the same as Φ on objects; on paths Φ is applied to each component and identities are deleted, so that the length of Φ(⟨f_{i}⟩) might be less than the length of ⟨f_{i}⟩, even zero. Just as for Path, E_{∗} takes a path to its composite in A, and D_{∗} takes a path to the path of paths whose components are paths of length one (for example, D_{∗}(⟨f_{1}, f_{2}, f_{3}⟩) = ⟨⟨f_{1}⟩, ⟨f_{2}⟩, ⟨f_{3}⟩⟩).

As before, a coalgebra structure G: A → Path_{∗}(A) is the identity on objects and gives a factorisation of each morphism into n non-identity morphisms, each of which G does not factor further. We now construct the reflexive graph Prime_{∗}(A) consisting of those arrows of A such that length (G(f)) ⩽ 1. Note that any functor Φ: A → B restricts to a reflexive graph morphism

Prime_{∗}(Φ): Prime_{∗}(A) → Prime_{∗}(B).

Thus we get a functor

Prime_{∗}: Cat_{Path_{∗}} → Rgph.

Of course, the free functor F: Rgph → Cat factors through Cat_{Path_{∗}} which gives a weak inverse for Prime_{∗}, thus demonstrating the equivalence

Rgph ≃ Cat_{Path_{∗}}.  (2)

0.2. Remarks. Here, Kleisli morphisms are ‘functors’ which don’t preserve composition but do preserve identities; Path_{∗} is still not a 2-functor; and coalgebra structures relative to UF are again unique.

1. ℙath

1.1. The Construction. We now wish to examine similar constructions for double categories. Rather than starting from graphs and studying the monad generated by the free category construction, we instead concentrate on the comonad of paths and then determine what the corresponding notion of ‘graph’ is by considering the Eilenberg-Moore coalgebras. There are several possible definitions for the notion of 2-cells of paths. Some are not very interesting, whereas others are dual forms of the notion we will introduce in this section. We have been guided in our definition by our desire for a deeper understanding of the Π_{2} construction and its relationship to spans. The main results of this section, Theorems 1.17 and 1.21 below, justify our choices.

Let 𝔸 be a double category (see, for example, [E] or [DP1]). We construct a new double category ℙath 𝔸 with the same objects and vertical arrows as in 𝔸. A horizontal arrow in ℙath 𝔸 is a path

A_{0} ⟶^{f_{1}} A_{1} ⟶^{f_{2}} A_{2} ⟶ ⋯ ⟶ A_{m−1} ⟶^{f_{m}} A_{m}  (3)

of horizontal arrows in 𝔸, with m ⩾ 0. Let

B_{0} ⟶^{g_{1}} B_{1} ⟶^{g_{2}} B_{2} ⟶ ⋯ ⟶ B_{n−1} ⟶^{g_{n}} B_{n}

be another path. For i ⩽ j, define g_{j}^{i}: B_{i} → B_{j} by

g_{j}^{i} = \{ \begin{matrix}g_{j}g_{j−1} ⋯ g_{i+1} & if & i < j \\ 1_{B_{i}} & if & i = j. \end{matrix}

Then a double cell from ⟨f_{i}⟩ to ⟨g_{j}⟩ is a triple (φ, ⟨v_{i}⟩, ⟨α_{i}⟩) where

φ: {0, 1, …, m} → {0, 1, …, n}

is an order preserving function with φ(0) = 0 and φ(m) = n, the \xymatrix{v_{i}: A_{i} \ar[r]|{•} & B_{φ(i)}} are vertical arrows, and

[figure: A_{i−1}; f_{i}; v_{i−1}; •; α_{i}; A_{i}; v_{i}; •; B_{φ(i)}; g_{φ(i)}^{φ(i−1)}; B_{φ(i)}]

are cells of 𝔸. A typical cell might look like

[figure: A_{0}; •; v_{0}; f_{1}; A_{1}; α_{1}; •; v_{1}; f_{2}; α_{2}; A_{2}; •; v_{2}; f_{3}; α_{3}; A_{3}; •; v_{3}; B_{0}; g_{1}; B_{1}; g_{2}; B_{2}; g_{3}; B_{3}; g_{4}; B_{4}.]  (4)

Horizontal composition of both arrows and cells is by concatenation. Vertical composition of arrows is as in 𝔸. To define vertical composition of cells, extend the notation as follows, for i ⩽ j,

α_{j}^{i} = \{ \begin{matrix}α_{j}α_{j−1} ⋯ α_{i+1} & if & i < j \\ 1_{v_{i}} & if & i = j , \end{matrix}

466  R. J. MACG. DAWSON, R. PARÉ, AND D. A. PRONK

so

\xymatrix{A_{i} \ar[r]^{f_{j}^{i}} \ar[d]^{α_{j}^{i}}|{•}_{v_{i}} & A_{i} \ar[d]|{•}^{v_{j}} \\ B_{φ(i)} \ar[r]_{g_{φ(j)}^{φ(i)}} & B_{φ(j)}.}

If (ψ, ⟨w_{j}⟩, ⟨β_{j}⟩) is a cell ⟨g_{j}⟩ → ⟨h_{k}⟩, then the vertical composition is defined by

(ψ, ⟨w_{j}⟩, ⟨β_{j}⟩) · (φ, ⟨v_{i}⟩, ⟨α_{i}⟩) = (ψφ, ⟨w_{φ(i)} · v_{i}⟩, ⟨β_{φ(i)}^{φ(i−1)} · α_{i}⟩).

An example will make this transparent. The composition of

[figure: B_{0}; g_{1}; •; w_{0}; β_{1}; B_{1}; •; w_{1}; g_{2}; β_{2}; B_{2}; •; w_{2}; g_{3}; B_{3}; β_{3}; •; w_{3}; g_{4}; β_{4}; B_{4}; •; w_{4}; C_{0}; h_{1}; C_{1}; h_{2}; C_{2}; h_{3}; C_{3}]

with the cell in (4) is

[figure: A_{0}; •; w_{0}·v_{0}; f_{1}; γ_{1}; A_{1}; f_{2}; γ_{2}; •; w_{1}·v_{1}; A_{2}; •; w_{1}·v_{2}; γ_{3}; f_{3}; A_{3}; •; w_{4}·v_{3}; C_{0}; h_{1}; C_{1}; h_{2}; C_{2}; h_{3}; C_{3}; ,]

where γ_{3} is, e.g., the pasting of

[figure: A_{2}; •; v_{2}; f_{3}; α_{3}; A_{3}; •; v_{3}; B_{1}; •; w_{1}; β_{2}; g_{2}; B_{2}; •; w_{2}; g_{3}; B_{3}; β_{3}; g_{4}; •; w_{3}; B_{4}; β_{4}; •; w_{4}; C_{0}; h_{1}; C_{1}; h_{2}; C_{2}; h_{3}; C_{3}; .]

It is straightforward to check that ℙath 𝔸 is a (strict) double category.

1.2. Example. Let 1 be the terminal double category. Then ℙath 1 has just one object ∗ and one vertical arrow, 1_{∗}. Horizontal arrows are in bijective correspondence with non-empty ordinals, [m] = {0, 1, …, m} and cells

[figure: ∗; [m]; φ; ∗; ∗; [n]; ∗]

with order preserving functions φ: [m] → [n] such that φ(0) = 0 and φ(m) = n. Horizontal composition is given by [m′]⊗[m] = [m′ +m], the ordinal sum with merged endpoints; this extends to functions in the obvious way:

(φ′ ⊗ φ)(i) = \{ \begin{matrix}φ′(i) & if i ⩽ m′ \\ m′ + φ(i) & otherwise. \end{matrix}

1.3. Remark. ℙath 1 is really a 2-category, since all vertical arrows are identities. It is even a strict monoidal category since there is only one object. As such it is equivalent to Δ^{op} where Δ is the category of finite ordinals including zero, with ordinal sum as ⊗. The equivalence Δ^{op} → ℙath 1 is as follows: the ordinal m = {0, 1, 2, …, m − 1} is mapped to [m]. An order preserving function f: m → n can be extended to [f]: [m] → [n] by defining [f](m) = n. The function [f] preserves the top element and therefore has a left adjoint f^{∗} which of course preserves 0. But the left adjoint of a morphism g: [m] → [n] preserves the top element if and only if g(i) = n precisely when i = m. So f^{∗} also preserves the top. The equivalence Δ^{op} → ℙath 1 is given by sending f to f^{∗}.

1.4. Definition.

1. A 2-cell (φ, ⟨v_{i}⟩, ⟨α_{i}⟩) is called neat if φ is an identity, for example

[figure: A_{0}; f_{1}; •; v_{0}; α_{1}; A_{1}; f_{2}; •; v_{1}; α_{2}; A_{2}; f_{3}; •; v_{2}; α_{3}; A_{3}; •; v_{3}; B_{0}; g_{1}; B_{1}; g_{2}; B_{2}; g_{3}; B_{3}; .]

2. A 2-cell (φ, ⟨v_{i}⟩, ⟨α_{i}⟩) is called cartesian if the v_{i} and α_{i} are all vertical identities, for example

[figure: A_{0}; f_{2}f_{1}; •; 1_{A_{0}}; _{id_{f_{2}f_{1}}}; A_{2}; •; 1_{A_{2}}; 1_{A_{2}}; A_{2}; •; 1_{A_{2}}; _{id_{A_{2}}}; A_{0}; f_{1}; A_{2}; f_{2}; A_{2}; .]

3. A factorisation (φ, ⟨v_{i}⟩, ⟨α_{i}⟩) = (φ^{2}, ⟨v_{i}^{2}⟩, ⟨α_{i}^{2}⟩)(φ^{1}, ⟨v_{i}^{1}⟩, ⟨α_{i}^{1}⟩) is called neat-cartesian if (φ^{1}, ⟨v_{i}^{1}⟩, ⟨α_{i}^{1}⟩) is neat and (φ^{2}, ⟨v_{i}^{2}⟩, ⟨α_{i}^{2}⟩) is cartesian.

1.5. Proposition. Every 2-cell (φ, ⟨v_{i}⟩, ⟨α_{i}⟩) has a unique neat-cartesian factorisation.

Proof. One can easily check that

(φ, ⟨id_{B_{i}}⟩, ⟨id_{g_{i+1}^{i}}⟩)(1_{[m]}, ⟨v_{i}⟩, ⟨α_{i}⟩).

is a neat-cartesian factorisation. To prove uniqueness, let

(φ, ⟨v_{i}⟩, ⟨α_{i}⟩) = (ν, ⟨w_{i}⟩, ⟨β_{i}⟩)(ψ, ⟨u_{i}⟩, γ_{i}),

where (ψ, ⟨u_{i}⟩, ⟨γ_{i}⟩) is neat and (ν, ⟨w_{i}⟩, β_{i}) is cartesian. Since (ν, ⟨w_{i}⟩, β_{i}) is cartesian, the w_{i} are identity arrows and the β_{i} are identity cells, so in order to compose to (φ, ⟨v_{i}⟩, ⟨α_{i}⟩), we must have u_{i} = v_{i} and γ_{i} = α_{i} for all i. Since (ψ, ⟨u_{i}⟩, ⟨γ_{i}⟩) is neat, it follows that the horizontal arrows in its codomain must be of the form g_{i+1}^{i}. Since ψ = id, it follows that ν = ϕ, and (ν, ⟨w_{i}⟩, β_{i}) = (φ, ⟨id_{B_{i}}⟩, ⟨id_{g_{i+1}^{i}}⟩) and (ψ, ⟨u_{i}⟩, γ_{i}) = (1_{[m]}, ⟨v_{i}⟩, ⟨α_{i}⟩).

1.6. Example. The 2-cell (φ, ⟨v_{i}⟩, ⟨α_{i}⟩) depicted in (4) above factors as

[figure: A_{0}; •; v_{0}; f_{1}; α_{1}; A_{1}; •; v_{1}; f_{2}; α_{2}; A_{2}; •; v_{2}; f_{3}; α_{3}; A_{3}; •; v_{3}; B_{0}; id; g_{1}; B_{1}; id; 1_{B_{1}}; B_{1}; id; g_{4}g_{3}g_{2}; B_{4}; B_{0}; g_{1}; B_{1}; g_{2}; B_{2}; g_{3}; B_{3}; g_{4}; B_{4}; .]

We recall that a double category 𝔸 can be viewed as a category object

\xymatrix{A_{2} \ar[r] \ar[r]|{Comp} \ar[r] & A_{1} \ar[r]^{∂_{0}} \ar[r]_{∂_{1}} & A_{0} \ar[l]}

in Cat, the category of categories. In this notation, we will assume that A_{0} is the category of objects and vertical arrows, A_{1} is the category with horizontal arrows as objects and double cells as morphisms, and A_{2} is the category with composable pairs of horizontal arrows as objects and composable pairs of double cells as morphisms. The functors ∂_{0} and ∂_{1} give the horizontal domain and codomain of a double cell. So the vertical composition of double cells is defined by the composition in A_{1} whereas the horizontal composition is defined by the functor Comp: A_{2} → A_{1}.

1.7. Definition. A double functor P: 𝔹 → 𝔸 is a vertical fibration if both functors P_{0} : B_{0} → A_{0} and P_{1} : B_{1} → A_{1} are fibrations in the usual sense and the functors ∂_{0}, ∂_{1} : B_{1} → B_{0}, Id: B_{0} → B_{1}, Comp: B_{2} → B_{1}, are cartesian over the corresponding functors for 𝔸. In elementary terms this means:

(VF1) For every object B in 𝔹 and vertical arrow \xymatrix{v: A \ar[r]|{•} & P B} there is a vertical arrow \xymatrix{ṽ: v^{∗}B \ar[r]|{•} & B} such that P (ṽ) = v and for any \xymatrix{w: B′ \ar[r]|{•} & B} and factorisation P (w) = v · v′ there is a unique w′ such that P (w′) = v′ and w = ṽ · w′. In a diagram,

[figure: B′; •; w′; •; w; P B′; •; v′; •; P w; v^{∗}B; •; ṽ; A; •; v; B; P B; .]

(VF2) For every horizontal arrow b: B′ → B in 𝔹 and cell

[figure: A′; a; •; v′; α; A; •; v; P B′; P b; P B]

in 𝔸, there exists a cell

\xymatrix{v^{′∗}B′ \ar[d]|{•}_{ṽ′} \ar[r]_{α̃}^{α^{∗}b} & v^{∗}B \ar[d]|{•}^{ṽ} \\ B′ \ar[r]_{b} & B}

in 𝔹, such that P (α̃) = α, and for any β and factorisation P β = α · α′ there exists a unique β′ such that P β′ = α′ and α̃ · β′ = β, as depicted in

[figure: •; β′; •; β; •; •; •; •; α′; P β; •; •; v^{′∗}B′; •; ṽ′; α̃; α^{∗}b; v^{∗}B; •; ṽ; A′; •; v′; α; a; A; •; v; B′; b; B; P B′; P b; P B; .]

(VF3) For any object B and vertical arrow \xymatrix{v: A \ar[r]|{•} & P B} , the cell

[figure: v^{∗}B; •; ṽ; 1_{v^{∗}B}; 1ṽ; v^{∗}B; •; ṽ; B; 1_{B}; B]

is cartesian over

[figure: A; 1_{A}; •; v; 1_{v}; A; •; v; P B; 1_{P B}; P B,]

i.e., ˜1_{v} = 1ṽ.

(VF4) For any path of horizontal arrows B′′ ⟶^{b′} B′ ⟶^{b} B with a path of cells

[figure: A′′; •; v′′; a′; α′; A′; •; v′; a; α; A; •; v; P B′′; P b′; P B′; P b; P B,]

the composite

\xymatrix{v^{′′∗}B′′ \ar[d]|{•}_{ṽ′′} \ar[r]_{α̃′}^{α^{′∗}b′} & v^{′∗}B′ \ar[d]|{•}^{ṽ′} \ar[r]_{α̃}^{α^{′∗}b} & v^{∗}B′ \ar[d]|{•}^{ṽ} \\ B′′ \ar[r]_{b′} & B′ \ar[r]_{b} & B}

is cartesian over αα′, i.e., (αα′)^{∗}(bb′) = (α^{∗}b)(α^{′∗}b′).

1.8. Proposition. The projection double functor ℙath 𝔸 → ℙath 1 is a vertical fibration.

Proof. The zero dimensional condition (VF1) is trivial as ℙath 1only has identity vertical arrows.

Given a path B_{0} ⟶^{g_{1}} B_{1} ⟶^{g_{2}} ⋯ ⟶^{g_{n}} B_{n} and a function θ: [p] → [n], θ^{∗}⟨g_{i}⟩ is the path ⟨g_{θ(j)}^{θ(j−1)}⟩,

[figure: B_{0} = B_{θ(0)}; g_{θ(1)}^{θ(0)}; B_{θ(1)}; g_{θ(2)}^{θ(1)}; g_{θ(p)}^{θ(p−1)}; B_{θ(p)} = B_{n},]

and the cartesian cell is (θ, ⟨id_{B_{θ(j)}}⟩, ⟨id_{g_{θ(j)}^{θ(j−1)}}⟩),

[figure: B_{θ(j−1)}; g_{θ(j)}^{θ(j−1)}; id; B_{θ(j)}; B_{θ(j−1)}; B_{θ(j−1)+1}; B_{θ(j)}.]

Given another cell

[figure: A_{0}; ⟨f_{i}⟩; •; (φ,⟨v_{i}⟩,⟨α_{i}⟩); A_{m}; •; B_{0}; ⟨g_{j}⟩; B_{n},]

and a factorisation

\xymatrix{[m] \ar[dr]_{ψ} \ar[rr]^{φ} &  & [n] \\  & [p] \ar@{-->}[ur]_{θ}}

there is a unique cell

[figure: A_{0}; ⟨f_{i}⟩; •; (ψ,⟨v̄_{i}⟩,⟨β_{i}⟩); A_{m}; •; B_{θ(0)}; ⟨g_{θ(j)}^{θ(j−1)}⟩; B_{θ(n)}]

such that (ψ, ⟨v̄_{i}⟩, ⟨β_{i}⟩)(θ, ⟨id_{B_{θ(j)}}⟩, ⟨id_{g_{θ(j)}^{θ(j−1)}}⟩) = (φ, ⟨v_{i}⟩, ⟨α_{i}⟩), namely v̄_{i} = v_{i} and β_{i} = α_{i}.

Conditions (VF3) and (VF4) follow from the definition of θ^{∗}.

1.9. Oplax morphisms. In order to express the universal property of ℙath 𝔸 we need the notion of oplax morphism of double categories. Recall [GP] that F: 𝔸 → 𝔹 is an oplax morphism if it assigns to objects, vertical and horizontal arrows, and cells of 𝔸 corresponding elements of 𝔹, preserving domains and codomains

\xymatrix{A_{1} \ar[dd]|{•}_{v_{1}} \ar[r]_{α}^{f_{1}} & A_{2} \ar[dd]|{•}^{v_{2}} &  & F A_{1} \ar[dd]|{•}_{F v_{1}} \ar[r]_{F α}^{F f_{1}} & F A_{2} \ar[dd]|{•}^{F v_{2}} \\  &  & ↦ \\ A_{3} \ar[r]_{f_{3}} & A_{4} &  & F A_{3} \ar[r]_{F f_{3}} & F A_{4},}

and also preserving vertical identities and vertical composition of arrows and cells. The oplax structure of F describes its effect on the horizontal structure of 𝔸. For every object A of 𝔸 there is given a cell

[figure: F A; F 1_{A}; φ_{A}; F A; F A; 1_{F A}; F A,]

and for every composable pair of horizontal arrows A ⟶^{f} A′ ⟶^{f′} A′′ a cell

[figure: F A; F (f′f); φ_{f′,f}; F A′′; F A; F f; F A′; F f′; F A′′.]

These are required to satisfy:

(OL1; vertical naturality) For every vertical arrow \xymatrix{v: A \ar[r]|{•} & B}

[figure: F A; •; F v; F 1_{v}; F 1_{A}; F A; •; F v; F A; φ_{A}; F 1_{A}; F A; F B; φ_{B}; F 1_{B}; F B; =; F A; 1_{F A}; •; F v; 1_{F v}; F A; •; F v; F B; 1_{F B}; F B; F B; 1_{F B}; F B;]

(OL2; horizontal naturality) For every pair of composable cells

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

[figure: F A; F (f′f); F (α′α); •; F v; F A′′; •; F v′′; F A; F (f′f); φ_{f′,f}; F A′′; F B; F (g′g); φ_{g′,g}; F B′′; =; F A; •; F v; F α; F f; F A′; •; F v′; F f′; F α′; F A′′; •; F v′′; F B; F g; F B′; F g′; F B′′; F B; F g; F B′; F g′; F B′′;]

(OL3; unit laws) For every f: A → A′, we require

[figure: F A; F f; φ_{f,1A}; F A′; F A; F f; φ_{1A′ ,f}; F A′; F A; F 1_{A}; φ_{A}; F A; F f; _{id_{F f}}; F A′; =; F A; F f; _{id_{F f}}; F A′; =; F A; F f; _{id_{F f}}; F A′; F 1_{A′}; φ_{A′}; F A′; F A; 1_{F A}; F A; F f; F A′; F A; F f; F A′; F A; F f; F A′; 1_{F A′}; F A′.]

(OL4; associativity) For every composable triple A ⟶^{f} A′ ⟶^{f′} A′′ ⟶^{f′′} A′′′, we require that

[figure: F A; F (f′′f′f); φ_{f′′,f′f}; F A′′′; F A; φ_{f′′f′,f}; F (f′′f′f); F A′′′; F A; F (f′f); φ_{f′,f}; F A′′; id; F (f′′); F A′′′; =; F A; F (f); id; F A′; F (f′′f′); φ_{f′′,f′}; F A′′′; F A; F (f); F A′; F (f′); F A′′; F (f′′); F A′′′; F A; F (f); F A′; F (f′); F A′′; F (f′′); F A′′′.]

For A_{0} ⟶^{f_{1}} A_{1} ⟶^{f_{2}} A_{2} ⟶^{f_{3}} ⋯ ⟶^{f_{n}} A_{n}, we define the n-fold comparison morphism

φ_{f_{n},f_{n−1},...,f_{1}} : F (f_{n}f_{n−1} ⋯ f_{1}) → F (f_{n})F (f_{n−1}) ⋯ F (f_{1})

recursively by

φ  = φ_{A_{0}}  (n = 0)
φ_{f}  = id_{F f}  (n = 1)
φ_{f_{n+1},f_{n},...,f_{1}} = (id_{F f_{n+1}}φ_{f_{n},f_{n−1},...,f_{1}}) · φ_{f_{n+1},f_{n}···f_{1}}

as in the following diagram

[figure: F A_{0}; F (f_{n+1}f_{n}···f_{1}); φ_{fn+1,fnfn−1···f1}; F A_{n+1}; F A_{0}; F (f_{n}···f_{1}); φ_{fn,fn−1,...,f1}; F A_{n}; _{id_{F fn+1}}; F f_{n+1}; F A_{n+1}; F A_{0}; F f_{1}; F A_{1}; F f_{2}; F f_{n}; F A_{n}; F f_{n+1}; F A_{n+1}.]

1.10. Proposition.

1. For any path of cells

[figure: A_{0}; f_{1}; α_{1}; •; v_{0}; A_{1}; f_{2}; α_{2}; •; v_{1}; ···; f_{n}; α_{n}; A_{n}; •; v_{n}; B_{0}; g_{1}; B_{1}; g_{2}; g_{n}; B_{n}]  (n ⩾ 0)

we have general naturality in the sense that

[figure: F A_{0}; •; F v_{0}; F (f_{n}···f_{1}); F (α_{m}···α_{1}); F A_{n}; •; F v_{n}; F A_{0}; F (f_{n}···f_{1}); φ_{fn,...,f_{1}}; F A_{n}; F B_{0}; φ_{gn,...,g_{1}}; F (g_{n}···g_{1}); F B_{n}; =; F A_{0}; F v_{0}; •; F f_{1}; F α_{1}; F A_{1}; F v_{1}; •; F α_{2}; F f_{2}; ···; F f_{n}; F α_{n}; F A_{n}; F v_{n}; •; F B_{0}; F g_{1}; F B_{1}; F g_{2}; F g_{n}; F B_{n}; F B_{0}; F g_{1}; F B_{1}; F g_{2}; F g_{n}; F B_{n}.]

2. For any path of paths ⟨f_{ij}⟩, we have general associativity in the sense that

[figure: F A_{00}; F (∏_{i,j} f_{ij}); φ_{⟨∏_{j} f_{ij} ⟩}; F A_{mn}; =; F A_{00}; F (∏_{i,j} f_{ij}); φ_{⟨f_{ij} ⟩}; F A_{mn}; F A_{00}; φ_{⟨f_{0j} ⟩}; F A_{10}; φ_{⟨f_{mj} ⟩}; F A_{mn}; F A_{00}; F f_{01}; F A_{01}; F f_{02}; F A_{10}; F A_{mn}; F A_{00}; F f_{01}; ⋯; F f_{mn}; F A_{mn}.]

Proof. Straightforward induction.

1.11. Remark. Conditions (OL2) - (OL4) are the same as the coherence conditions for oplax morphisms of bicategories [Bé]. In the case of bicategories, condition (OL1) is vacuous as all vertical arrows are identities and 1_{id_{A}} = id_{1_{A}}. However, when specifying the cells φ_{A} for bicategories one might wonder whether further naturality conditions might be needed. It would not make sense to require commutativity of the diagram

[figure: F A; F f; 1_{F A}; F (1_{A}); ⇓ φ_{A}; F A; F f; F A′; 1_{F A′}; F (1_{A′}); ⇓ φ_{A′}; F A′]

since F f F 1_{A} ≠ F 1_{A′} F f. One might precede these cells by φ_{f,1_{A}} and φ_{1_{A′},f} and get an equality, but this is just the condition (OL3). It turns out that the double category formulation of oplaxity very nicely expresses the naturality of φ_{A} in A.

General naturality for n = 0 is exactly (OL1) as the proof shows. Similarly, general associativity has as a special case the unit conditions when the path of paths is made up of two paths where one is of length one and the other one is of length two.

1.12. Example. Let 𝔸 be any double category and ℙath 𝔸 its double category of paths. Define Ξ: 𝔸 → ℙath 𝔸 as follows. Ξ is the identity on objects and vertical arrows; also, Ξ takes a cell, or a horizontal arrow, to the corresponding singleton path. For an object A in 𝔸, let ξ_{A} be the cell

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

and for a path A ⟶^{f} A′ ⟶^{f′} A′′ of horizontal arrows, let ξ_{f′,f} be the cell

[figure: A; f′f; _{id_{f′f}}; A′′; A; f; A′; f′; A′′; .]

All conditions for Ξ hold trivially, because all cells are identities. (Note however that although ξ_{A} and ξ_{f′,f} are given by identities, neither is invertible as the indexing functions are not. They are only cartesian morphisms.) So Ξ (equipped with the cells ξ) is an oplax morphism of double categories. We shall show that it is in fact the universal one. In order to express properly what this means, we need the notion of vertical transformation of oplax morphisms.

1.13. Definition. Let F, G: 𝔸 → 𝔹 be oplax morphisms of double categories. A vertical transformation t: F → G assigns to each object A in 𝔸 a vertical arrow \xymatrix{tA: F A \ar[r]|{•} & GA} and to each horizontal arrow \xymatrix{f: A \ar[r] & A′} a cell

[figure: F A; •; tA; F f; tf; F A′; tA′; •; GA; Gf; GA′; ,]

satisfying the following four conditions.

(VT1) For every vertical arrow \xymatrix{v: A \ar[r]|{•} & C} in 𝔸, the square

\xymatrix{F A \ar[r]|{•}^{F v} \ar[d]|{•}^{tA} & F C \ar[d]|{•}^{tB} \\ GA \ar[r]|{•}_{Gv} & GC}

commutes.

(VT2) For every cell

[figure: A; f; •; v; α; A′; •; v′; C; h; C′]

in 𝔸,

[figure: F A; •; tA; F f; tf; F A′; •; tA′; F A; •; F v; F f; F α; F A′; •; F v′; GA; •; Gv; Gα; Gf; GA′; •; Gv′; =; F A; •; tC; F h; th; F C′; •; tC′; GC; Gh; GC′; GC; Gh; GC′.]

(VT3) For every A in 𝔸,

[figure: F A; •; tA; t1_{A}; F 1_{A}; F A; •; tA; F A; F 1_{A}; φ_{A}; F A; GA; G1_{A}; γ_{A}; GA; =; F A; •; tA; 1_{tA}; 1_{F A}; F A; •; tA; GA; 1_{GA}; GA; GA; 1_{GA}; GA.]

(VT4) For every pair of composable horizontal arrows

A ⟶^{f} A′ ⟶^{f′} A′′,

[figure: F A; F (f′f); φ_{f′,f}; F A′′; F A; •; F (f′f); t(f′f); F A′′; •; tA′′; F A; •; tA; F f; tf; F A′; •; tA′; tf′; F f′; F A′′; •; tA′′; =; GA; γ_{f′,f}; G(f′f); GA′′; GA; Gf; GA′; Gf′; GA′′; GA; Gf; GA′; Gf′; GA′′.]

1.14. Remark. While condition (VT1) is, strictly speaking, implicit in condition (VT2), it is stated separately for greater clarity. These conditions describe what we will call vertical naturality. Conditions (VT3) and (VT4) describe horizontal functoriality.

1.15. Proposition. (General Horizontal Functoriality) For every path

A_{0} ⟶^{f_{1}} A_{1} ⟶^{f_{2}} A_{2} ⟶ ⋯ ⟶^{f_{n}} A_{n},

we have

[figure: F A_{0}; F (f_{n}···f_{1}); φ_{fn,...,f_{1}}; F A_{n}; F A_{0}; •; tA_{0}; F (f_{n}···f_{1}); t(f_{n}···f_{1}); F A_{n}; •; tA_{n}; F A_{0}; •; tA_{0}; tf_{1}; F A_{1}; •; tf_{2}; F A_{2}; •; tf_{3}; tf_{n}; F A_{n}; •; tA_{n}; =; GA_{0}; γ_{fn,...,f_{1}}; GA_{n}; GA_{0}; Gf_{1}; GA_{1}; Gf_{2}; GA_{2}; Gf_{3}; Gf_{n}; GA_{n}; GA_{0}; Gf_{1}; GA_{1}; Gf_{2}; Gf_{n}; GA_{n}.]

Proof. Easy induction.

1.16. Remarks.

1. The special case when n = 0 is part of (VT3). The case n = 1 is vacuous.

2. Double categories, oplax morphisms and vertical transformations form a 2-category. In fact, as shown in [GP], they are part of a strict double category 𝔻oub whose horizontal arrows are oplax morphisms and whose vertical arrows are lax morphisms. This is remarkable, and another instance where the double category point of view is illuminating. Indeed, it is well-known that we cannot form a 2-category consisting of bicategories, oplax morphisms and any of the obvious choices of 2-cells (lax, oplax, or pseudo). (See for example [Lac].) Indeed, although oplax morphisms do compose in a strictly associative way (so we would obtain a 2-category rather than a bicategory if anything) whiskering does not work for any of these choices. Suppose that we have a transformation t: F → G for oplax morphisms F, G: A → B with components

\xymatrix{F A \ar[d]_{F f} \ar[r]_{⇒^{tf}}^{tA} & GA \ar[d]^{Gf} \\ F B \ar[r]_{tB} & GB}

where tf must be a cell, an isomorphism or an equality. If H: B → C is an oplax morphism then applying H to tf gives us

[figure: HF A; HF f; ⇒^{Htf}; HtA; HGA; HGf; ⇒; ⇐; HF B; HtB; HGB]

so this would not compose.

The correct 2-cells are the specialisations of those we introduced above, the vertical cells. In the case of bicategories, these look overly special, since their onedimensional components are all identities (so there are only 2-cells between morphisms which agree on objects). However, they are not that special, and indeed occur throughout bicategory theory (see for example [CR]).

Let Doub(𝔸, 𝔹) denote the category of double functors from 𝔸 to 𝔹 with vertical natural transformations, and Doub_{Opl}(𝔸, 𝔹) the category of oplax morphisms from 𝔸 to 𝔹 with vertical transformations.

1.17. Theorem. For any double category 𝔸, Ξ: 𝔸 → ℙath 𝔸 is the universal oplax morphism in the sense that composition with Ξ,

Ξ^{∗}: Doub(ℙath 𝔸, 𝔹) → Doub_{Opl}(𝔸, 𝔹)

is an isomorphism of categories.

Proof. Given an oplax morphism F: 𝔸 → 𝔹, define Φ(F): ℙath 𝔸 → 𝔹 to be the same as F on objects and vertical arrows. For a path A_{0} ⟶^{f_{1}} A_{1} ⟶^{f_{2}} ⋯ ⟶^{f_{n}} A_{n}, define Φ(F)(⟨f_{i}⟩) to be the composite

F A_{0} ⟶^{F f_{1}} F A_{1} ⟶^{F f_{2}} ⋯ ⟶^{F f_{n}} F A_{n}

(the empty path goes to 1_{F A_{0}}, of course). For a cell of the form

[figure: A; •; v; f; α; A′; •; v′; B_{0}; g_{1}; B_{1}; g_{2}; g_{n}; B_{n}]

we assign the cell

[figure: F A; •; F v; F f; F α; F A′; •; F v′; F B_{0}; F (g_{n}···g_{1}); φ_{gn,...,g_{1}}; F B_{n}; F B_{0}; F g_{1}; F B_{1}; F g_{2}; F g_{n}; F B_{n},]

and extend Φ(F) to cells with vertical domains of arbitrary length, by horizontal composition.

Now Φ(F) is functorial on vertical arrows because F is, and on horizontal arrows because ℙath 𝔸 is free on these. ℙath 𝔸 is also free for horizontal composition of cells, so Φ(F) is also functorial on these. We must verify that Φ(F) preserves vertical composition of cells (and vertical identities). A typical example will make this clear. Consider the vertical composite

[figure: A; •; f; α; A′; •; B_{0}; •; g_{1}; β_{1}; B_{1}; •; g_{2}; β_{2}; B_{2}; •; β_{3}; g_{3}; B_{3}; •; C_{0}; h_{1}; C_{1}; h_{2}; C_{2}; h_{3}; C_{3}; h_{4}; C_{4}.]

The composite of the images in ℙath 𝔸 is the pasting of

[figure: F A; •; F α; F f; F A′; •; F B_{0}; φ_{g_{3},g_{2},g_{1}}; F (g_{3}g_{2}g_{1}); F B_{3}; F B_{0}; •; F β_{1}; F g_{1}; F B_{1}; •; F β_{2}; F g_{2}; F B_{2}; •; F β_{3}; F g_{3}; F B3; •; F C_{0}; F h_{1}; φ_{h_{1}}; F C_{1}; φ_{C_{1}}; F (1_{C_{1}}); F C_{1}; φ_{h_{4},h_{3},h_{2}}; F (h_{4}h_{3}h_{2}); F C_{4}; F C_{0}; F h_{1}; F C_{1}; F h_{2}; F C_{2}; F h_{3}; F C_{3}; F h_{4}; F C_{4}.]

Now apply general naturality to the two middle rows to get

[figure: F A; •; F α; F f; F A′; •; F B_{0}; •; F (β_{3}β_{2}β_{1}); F (g_{3}g_{2}g_{1}); F B_{3}; •; F C_{0}; φ_{h_{4}h_{3}h_{2},h_{1}}; F (h_{4}h_{3}h_{2}h_{1}); F C_{4}; F C_{0}; F h_{1}; φ_{h_{1}}; F C_{1}; φ_{C_{1}}; F (1_{C_{1}}); F C_{1}; φ_{h_{4},h_{3},h_{2}}; F (h_{4}h_{3}h_{2}); F C_{4}; F C_{0}; F h_{1}; F C_{1}; F h_{2}; F C_{2}; F h_{3}; F C_{3}; F h_{4}; F C_{4}.]

The top two squares compose to F (β_{3}β_{2}β_{1}·α), and the bottom row composes to φ_{h_{4},h_{3},h_{2},h_{1}} by general associativity, so the whole diagram pastes to Φ(F)(β_{3}β_{2}β_{1} · α) as required. (Notwithstanding what we tell our students, sometimes an example is better than a proof.)

Now suppose that we start with a double functor G: ℙath 𝔸 → 𝔹 and consider ΦΞ^{∗}(G) = Φ(G ∘ Ξ). On objects, vertical arrows, and horizontal paths of length one, Φ(G ∘ Ξ) agrees with G, and by freeness, they agree on paths of arbitrary length as well. Also by freeness, we only have to check that they agree on cells of the form

[figure: A; •; f; α; A′; •; B_{0}; g_{1}; B_{1}; g_{2}; g_{n}; B_{n}]

which Φ(G ∘ Ξ) takes to

[figure: GA; •; Gα; Gf; GA′; •; GB_{0}; γ_{gm,...,g_{1}}; G(g_{n}···g_{1}); GB_{n}; GB_{0}; Gg_{1}; GB_{1}; Gg_{2}; Gg_{n}; GB_{n},]

where γ is the generalised “codiagonal” expressing oplaxity of G∘Ξ. The codiagonal for a composite is the composite of the codiagonals in the only sense possible, (G, γ) ∘ (F, φ) = (GF, Gφ · γ), which in this case gives γ_{g_{m},...,g_{1}} = G(id_{g_{n}···g_{1}}), so that Φ(G ∘ Ξ)(α) = G(id)G(α) = g(α). So ΦΞ^{∗}(G) = G.

Starting with F: 𝔸 → 𝔹 an oplax morphism, we have that Ξ^{∗}Φ(F) = Φ(F) ∘ Ξ. Moreover, since Φ(F) agrees with F on objects, vertical arrows, vertical composition, horizontal arrows of length one, and cells whose codomain has length one, we only need to check that Ξ^{∗}Φ(F) and F have the same oplaxity cells. For a path ⟨f_{i}⟩ in 𝔸, the generalised oplaxity cell of Φ(F) ∘ Ξ is Φ(F)(ξ_{f_{n},...,f_{1}}), which by definition of Φ(F) is

[figure: F A_{0}; F (f_{n}···f_{1}); F (id); F A_{n}; F A_{0}; φ_{fn,...,f_{1}}; F (f_{n}···f_{1}); F A_{n}; F A_{0}; F A_{1}; F A_{n},]

i.e., φ_{f_{n},...,f_{1}}. So Φ(F) ∘ Ξ = F. This establishes that Ξ^{∗} is bijective on objects with inverse Φ.

To finish the proof we will show that Ξ^{∗} is full and faithful. Choose double functors G, K: ℙath (𝔸) → 𝔹, and a vertical transformation \xymatrix{t: G ∘ Ξ \ar[r]|{•} & K ∘ Ξ} . Then t is specified on objects and horizontal morphisms of 𝔸, i.e., paths of length one. We wish to show that it extends uniquely to paths of arbitrary length. For any path ⟨f_{i}⟩, an extension of t would have to satisfy general functoriality, i.e.,

[figure: GA_{0}; •; tA_{0}; G⟨f_{i}⟩; t⟨f_{i}⟩; GA_{n}; •; tA_{n}; GA_{0}; G⟨f_{i}⟩; γ_{⟨f_{i}⟩}; GA_{n}; KA_{0}; K⟨f_{i}⟩; γ_{⟨f_{i}⟩}; KA_{n}; =; GA_{0}; •; tA_{0}; tf_{1}; GA_{1}; tf_{2}; •; tf_{n}; GA_{n}; •; tA_{n}; KA_{0}; Kf_{1}; KA_{1}; Kf_{2}; Kf_{n}; KA_{n}; KA_{0}; Kf_{1}; KA_{1}; Kf_{2}; Kf_{n}; KA_{n}.]

As G and K are double functors on ℙath (𝔸), the cells γ_{⟨f_{i}⟩} and κ_{⟨f_{i}⟩} are actually vertical identities, so this completely determines t⟨f_{i}⟩. It is straightforward to check that, thus extended, t is a vertical transformation \xymatrix{G \ar[r]|{•} & K} , thus completing the proof.

1.18. The Comonad. Not surprisingly, ℙath is the functor part of a comonad on the category of double categories. The one-dimensional version, Path, studied in the prologue arose from the underlying graph - free category adjoint pair. Here we work in the reverse direction. First we get the comonad structure and then determine, in Section 3, what the two-dimensional analog of ‘graph’ is.

The universality of ℙath in the previous section expresses an adjointness which is the two dimensional version of the Kleisli category construction of the prologue. The Kleisli morphisms were “pretty poor morphisms”, i.e., ‘functors’ that don’t preserve composition nor identities. In the current context these correspond to oplax morphisms, a much richer notion of morphism which occurs frequently in practice. Once again we see that the two-dimensional structure adds so much more.

Let A be a 2-category and 𝔾 = (G, E, D) a 2-comonad on A. The Kleisli 2-category A𝔾 of 𝔾 has the same objects as A and hom categories defined by

A^{𝔾}(A, B) = A(GA, B).

Vertical composition of cells is as in A and horizontal composition of arrows and cells is the usual Kleisli composition: g ∘ f = g(Gf)D. There is an adjoint pair of 2-functors

\xymatrix{A \ar[r]^{R^{𝔾}} & A^{𝔾} \ar[l]^{U^{𝔾}}}
U^{𝔾} ⊣ R^{𝔾}

inducing the comonad 𝔾; among those A^{𝔾} is characterised up to isomorphism by the mere fact that the right adjoint is bijective on objects.

Theorem 1.17 has as an immediate corollary the following result.

1.19. Proposition. The inclusion, Doub ↪ Doub_{Opl} of the 2-category of double categories, double functors, and vertical transformations into the 2-category of double categories, oplax morphisms, and vertical transformations, has a 2-left adjoint ℙath with unit Ξ. Doub_{Opl} is the Kleisli 2-category for the 2-comonad ℙath induced on Doub.

1.20. Remark. The fact that ℙath is a 2-functor is a double category phenomenon. Of course the ℙath construction would work for 2-categories because 2-categories are special double categories, but vertical transformations look overly special in that setting. In any case, it is the vertical transformations that make things work, so even if we start with 2-categories we must consider them as double categories to get the two dimensional structure of Doub and ℙath. In fact, ℙath is even better than a 2-comonad, it is one in which the structure morphisms are left adjoint to the counits, of the sort studied by Kock [K] and Zöberlein [Z]. Following Kelly and Lack [KL] we call them oplax idempotent comonads. (See also [M].)

Let us recall the definition. A 2-comonad 𝔾 = (G, E, D) on a 2-category A is oplax idempotent if for every object A, there are 2-cells α: DA · GEA → 1_{G^{2}A} and β: 1_{G^{2}A} → DA · EGA which together with the triangle identities 1_{GA} = GEA · DA and EGA · DA = 1_{GA} give an adjoint triple

GEA ⊣ DA ⊣ EGA.

Wood [W] has shown that if ε: UR → 1_{B} and η: 1_{A} → RU are the adjunctions for an

adjoint pair \xymatrix{A \ar[r]_{R} & B \ar[l]_{U}} of 2-functors, then there is a transformation φ: ηR · Rε → 1_{RUR}

which together with the triangle identity Rε · ηR = 1_{R} makes Rε ⊣ ηR, if and only if there is a transformation ψ: Uη · εU → 1_{URU} which makes Uη ⊣ εU with 1_{U} → εU · Uη as unit, and in this case the comonad (UR, ε, UηR) is an oplax idempotent. This is a useful criterion as it avoids having to deal with G^{2} which can be quite complicated.

1.21. Theorem. The comonad ℙath on Doub is an oplax idempotent.

Proof. The comonad structure on ℙath is obtained from the adjoint pair of 2-functors, ℙath: Doub_{Opl} → Doub, left adjoint to the inclusion Doub ↪ Doub_{Opl}. The unit is Ξ: 𝔸 → ℙath 𝔸 and the counit is Γ: ℙath 𝔸 → 𝔸 is composition. So it is sufficient to show that Γ is left adjoint to Ξ in Doub_{Opl}. The composite ΓΞ is the identity on 𝔸, so our unit \xymatrix{η: 1_{𝔸} \ar[r]|{•} & ΓΞ} will be the identity vertical transformation. The counit \xymatrix{ε: ΞΓ \ar[r]|{•} & 1_{ℙath 𝔸}} is the identity on objects, and for every 1-cell in ℙath 𝔸, i.e., a path ⟨f_{i}⟩, ε(⟨f_{i}⟩) is the cell

[figure: A_{0}; •; _{id_{A0}}; _{id_{fn,...,f1}}; f_{n}···f_{1}; A_{n}; •; _{id_{An}}; A_{0}; f_{1}; A_{1}; f_{2}; A_{2}; f_{n}; A_{n}.]

Note that for paths of length 1, this is actually an identity so that εΞ is the identity. This is one of the triangle equalities. Also notice that Γε is the identity, and this is the other triangle equality.

We saw in the prologue that the comonad Path on Cat has as its coalgebras free categories on graphs (the category of coalgebras is equivalent to the category of graphs), and that a category has at most one coalgebra structure, despite the fact that Path is not an idempotent comonad. This surprising phenomenon can now be understood as follows. If a category A is considered as a vertically discrete double category, then a coalgebra structure F: A → ℙath 𝔸 is the same as a coalgebra structure A → PathA, because ℙath A and Path A are the same at the level of horizontal arrows. As ℙath is an oplax idempotent, there can be at most one of these, a (vertical) left adjoint to E: ℙath 𝔸 → 𝔸.

1.22. Remark. ℙath A has a nontrivial double structure even when A is just a category. Indeed, this is already seen for ℙath 1 . The vertical arrows are identities (so it is a 2category), but a cell from a path A_{0} ⟶^{f_{1}} A_{1} ⟶^{f_{2}} ⋯ ⟶^{f_{n}} A_{n} to a path B_{0} ⟶^{g_{1}} B_{1} ⟶^{g_{2}} ⋯ ⟶^{g_{m}} B_{m} is an endpoint and order preserving function φ: [n] → [m] such that for every i = 1, …, n, f_{i} = g_{φ(i)}^{φ(i−1)} (so in particular, B_{φ(i)} = A_{i}). Although the composites that A has are forgotten in Path (A), they are remembered in ℙath (A) and, in fact, applying Π_{0} locally to ℙath (A) gives us back A itself.

As the coalgebras for Path are graphs, and graphs are the building blocks for categories, it will be instructive to determine the Eilenberg-Moore coalgebras for the oplax idempotent comonad ℙath on Doub. They should be to oplax morphisms what graphs are to functors, i.e., the true objects on which oplax morphisms are defined. After all, if morphisms are meant to be structure preserving, what can we make of oplax morphisms, which don’t preserve horizontal composition? We shall see in Section 3 that the coalgebras are precisely Leinster’s fc-multicategories, whose theory we review in the next section.

2. Oplax Double Categories

Oplax morphisms don’t preserve composition in spite of the fact that morphisms should be structure preserving functions. In a situation such as this, it is often the case that what we do not sufficiently understand is the structure. If composition is not preserved, then it shouldn’t be part of the structure. But we do need enough structure to yield oplaxness.

Our main example is the double category 𝕊pan (A) which will be explored in detail in the sequel [DPP4] to the present work. 𝕊pan (A) has the same objects as A, its vertical arrows are the morphisms of A, its horizontal arrows are spans in A, and a typical cell looks like

\xymatrix{A \ar[d]_{f} & S \ar[l]_{p} \ar[r]^{p′} \ar[d]^{s} & A′ \ar[d]^{f′} \\ B & T \ar[l]^{q} \ar[r]_{q′} & B′.}

If A has pullbacks, then 𝕊pan(A) is a (weak) double category. If A fails to have pullbacks, we don’t have horizontal composition; however, we have not only all the rest of the double category structure (vertical composition of arrows and cells), but also the extra structure that would determine the horizontal composition if it existed. Since composition of spans is performed using pullbacks we know what a morphism into it should be; in fact we know this not just for composites of two spans, but for n-fold composites as well. Indeed, if T is the composite of the spans

B = B_{0} ⟵^{q_{1}} T_{1} ⟶^{q′_{1}} B_{1} ⟵^{q_{2}} T_{2} ⟶^{q′_{2}} B_{2} ⟵^{q_{3}} ⋯ ⟵^{q_{n}} T_{n} ⟶^{q′_{n}} B_{n} = B′,

then cells as above are in bijective correspondence with diagrams

[figure: A; f; S; p; p′; s_{1}; s_{2}; ···; s_{n}; A′; f′; B_{0}; T_{1}; B_{1}; T_{2}; T_{n}; B_{n}]

and it is clear from representability theory that a knowledge of such ‘generalised cells’ will determine the composite up to isomorphism, if it exists. We have vertical identities and a generalised composition: given n other generalised cells with domains T_{i}, they can be vertically composed with the above one, and this composition is associative. This is the kind of structure we want. It is simply the vertical dual of Leinster’s fc-multicategories [L1, L2, L3], whose theory we now review. They are the double category version of what Hermida [H1] calls ‘multicategories with several objects’ and what Hermida, Makkai, and Power [HMP] call ‘multitopic categories’. We propose to call them lax double categories for reasons hinted at above and which should become clear shortly. (Actually, we shall study the dual oplax double categories, because of the applications we have in mind.)

2.1. Multicategories. All of these concepts are an outgrowth of the notion of multicategory [Lam] which was inspired by the relationship between tensor products and multilinear maps. A (small) multicategory consists of a set of objects and set of multiarrows with domains finite strings of objects and codomains single objects. Given multiarrows f: ⟨B_{1}, …, B_{n}⟩ → C and g_{i}: ⟨A_{1}, …, A_{m_{i}}⟩ → B_{i}, i = 1, …, n, there is a composite f(g_{1}, …, g_{n}): ⟨A_{i}⟩ → C. This composition is associative and there are identities satisfying 1_{C}f = f = f(1_{B_{1}}, …, 1_{B_{n}}).

We can reformulate this in terms of the free monoid monad (T, η, μ). A multicategory consists of two sets A_{0}, A_{1} (objects and arrows) with functions ∂_{0} : A_{1} → T A_{0}, ∂_{1} : A_{1} → A_{0}, ι: A_{0} → A_{1}, and γ: A_{2} → A_{1} (domain, codomain, identity, and composition). A_{2} is defined by the pullback

[figure: A_{2}; Pb; T A_{1}; T ∂_{1}; A_{1}; ∂_{0}; T A_{0}.]

The associativity and unit laws can easily be expressed diagrammatically. In fact, all of this can be carried out in any category with pullbacks and for any cartesian monad 𝕋, i.e., a monad 𝕋 = (T, η, μ) for which T preserves pullbacks and the naturality squares

\xymatrix{A \ar[dd]_{f} \ar[r]^{ηA} & T A \ar[dd]^{T f} &  & T^{2}A \ar[r]^{μA} \ar[dd]_{T^{2}f} & T A \ar[dd]^{T f} \\  &  & and \\ B \ar[r]_{ηB} & T B &  & T^{2}B \ar[r]_{μB} & T B}

are all pullbacks. This gives Burroni’s notion of 𝕋-multicategory [Bu].

In keeping with the theme of spans, let us introduce the double category 𝕋-𝕊pan(A) for any cartesian monad 𝕋 = (T, η, μ) on a category A with pullbacks. The objects of 𝕋-𝕊pan(A) are those of A. A horizontal arrow \xymatrix{A \ar[r]|{+} & B} is a span

\xymatrix{ & S \ar[dl] \ar[dr] \\ T A &  & B.}

A vertical arrow is just an arrow of A, and a cell is a commutative diagram

\xymatrix{T A \ar[d]_{T a} & S \ar[d]^{s} \ar[l] \ar[r] & B \ar[d]^{b} \\ T A′ & S′ \ar[l] \ar[r] & B′.}

Horizontal composition is given by pullback and composition with μ:

[figure: R ⊗ S; Pb; T S; R; T^{2}A; μA; T B; C; T A]

and identities are

\xymatrix{ & A \ar[dl]_{ηA} \ar[dr]^{1_{A}} \\ T A &  & A.}

Horizontal composition of cells is given by the universal property of pullbacks. Proving the unit laws and associativity of horizontal composition is an easy exercise using the cartesianness of 𝕋. Now, a 𝕋-multicategory is exactly a horizontal monad in 𝕋-𝕊pan(A) and a 𝕋-multifunctor is a vertical morphism of monads in 𝕋-𝕊pan(A).

Note that multifunctors are defined using vertical arrows, and so their construction uses the double structure of 𝕋-𝕊pan(A). When category objects are defined as monads in the bicategory Span(A) none of the various notions of morphism give functors. At best we get profunctors and at worst we get things never before observed in nature. Of course we want functors as our morphisms and the usual way of dealing with this is to define morphisms to be maps in Span(A) with left and right actions. While this does work in the present context, it is certainly ad hoc. There doesn’t seem to be any overriding idea for doing this, except that it gives what we want. Strictly speaking, it doesn’t even do that, the representability of maps being intimately related to Cauchy completeness.

2.2. Lax Double Categories. The following discussion can be found in Chapter 5 of Leinster’s book [L2]. We include it here so as not to interrupt the logical flow of ideas. Consider the category of graphs, Gph, and on it the free category monad, 𝕋 = (T, η, μ), introduced in the Prologue.

2.3. Proposition. 𝕋 is a cartesian monad.

Proof. Let

\xymatrix{G \ar[r]^{P_{1}} \ar[d]_{P_{2}} & G_{1} \ar[d]^{F_{1}} \\ G_{2} \ar[r]_{F_{2}} & G_{0}}

be a pullback of graphs and consider

\xymatrix{T G \ar[r]^{T P_{1}} \ar[d]_{T P_{2}} & T G_{1} \ar[d]^{T F_{1}} \\ T G_{2} \ar[r]_{T F_{2}} & T G_{0} .}

T is the identity on vertices, so there is no problem there. An edge in T G is a path of edges in G and an edge in G is a pair of edges (A_{1} ⟶^{f_{1}} B_{1}, A_{2} ⟶^{f_{2}} B_{2}) in G_{1} × G_{2} such that F_{1}f_{1} = F_{2}f_{2}. A path of these is a pair of paths of the same length (⟨f_{1i}⟩, ⟨f_{2i}⟩) such that F_{1}f_{1i} = F_{2}f_{2i} for all i. Since T F_{1} and T F_{2} preserve length and two paths in T G_{0} are equal if and only if they are identical, such a pair of paths is exactly an edge in the pullback of T F_{1} and T F_{2}. So T preserves pullbacks.

Let F: G → G′ be a morphism of graphs and consider the naturality square

\xymatrix{G \ar[d]_{F} \ar[r]^{ηG} & T G \ar[d]^{T F} \\ G′ \ar[r]_{ηG′} & T G′.}

An edge of the pullback corresponds to an edge g of G′ together with a path ⟨f_{i}⟩ in G such that ⟨F f_{i}⟩ is g, i.e., the path ⟨f_{i}⟩ has length one, and F f_{1} = g. Thus, an element of the pullback is completely determined by an edge of G, i.e., the above square is a pullback.

Also consider the square

\xymatrix{T^{2}G \ar[d]_{T^{2}F} \ar[r]^{μG} & T G \ar[d]^{T F} \\ T^{2}G′ \ar[r]_{μG′} & T G′.}

An edge of the pullback of T^{2}G′ and T G is a path of paths (m, (n_{j}, ⟨g_{ij}⟩)) in G′ and a path (p, ⟨f_{k}⟩) in G such that (∑_{j∈m} n_{j}, ⟨g_{ij}⟩) = (p, ⟨F f_{k}⟩) which is entirely determined by a partition of p into m pieces, and the edges f_{k}, i.e., a path of paths in G or an element of T^{2}G. Thus the μ-naturality square is a pullback.

2.4. Definition. A lax double category is a 𝕋-multicategory in Gph.

In elementary terms, a lax double category has objects, horizontal and vertical arrows, and multicells. The vertical arrows form a category whereas the horizontal arrows don’t. A multicell has domains and codomains as illustrated

[figure: B_{0}; g_{1}; •; v; α; B_{1}; g_{2}; B_{2}; g_{n}; B_{n}; •; v′; A; f; A′.]

Such an α can be composed with n cells

[figure: C_{i0}; β_{i}; •; h_{i1}; C_{i1}; h_{i2}; h_{im_{i}}; C_{im_{i}}; •; B_{i−1}; g_{i}; B_{i}]

to give a cell

[figure: C_{10}; α∘⟨β_{i}⟩; •; h_{11}; C_{11}; h_{12}; C_{12}; h_{nmn}; C_{nm_{n}}; •; A; f; A′.]

There are identity multicells

[figure: A; f; _{id_{f}}; A′; A; f; A′]

and the composition is associative in the only sense it can be.

A lax double category in which all vertical arrows are identities is what Hermida [H1] calls a multicategory with several objects. A lax double category with a single object is the same as a multicategory as defined in [Lam] (see also [L2]).

2.5. Definition. A morphism of lax double categories F: 𝔸 → 𝔹 takes arrows to arrows of the same type and cells to cells respecting domains and codomains, and preserving identities and vertical composition of arrows and cells.

A double category 𝔸 gives a lax double category 𝕃ax 𝔸 if we take multicells

[figure: B_{0}; •; g_{1}; α; B_{1}; g_{2}; g_{n}; B_{n}; •; v′; A; f; A′]

to be double cells

[figure: B_{0}; •; v; (g_{n}g_{n−1})···g_{2})g_{1}; α; B_{n}; •; v′; A; f; A′.]

That we actually get a lax double category follows from the coherence theorem for (weak) double categories which is a minor variation on the coherence theorem for bicategories [DP2], and in fact is equivalent to it. This is one of Hermida’s main points in [H1].

The following theorem is implicitly in [H1] (see 9.4 and 9.5 there).

2.6. Theorem. Let 𝔸 and 𝔹 be double categories. A morphism of lax double categories 𝕃ax 𝔸 → 𝕃ax 𝔹 is the same as a lax morphism of double categories 𝔸 → 𝔹.

Proof. For A_{0} ⟶^{f_{1}} A_{1} ⟶^{f_{2}} A_{2} in 𝔸, we have the multicell

[figure: A_{0}; f_{1}; _{id_{f2,f1}}; A_{1}; f_{2}; A_{2}; A_{0}; f_{2}f_{1}; A_{2}]

and applying F we get

[figure: F A_{0}; F f_{1}; F (id_{f_{2},f_{1}}); F A_{1}; F f_{2}; F A_{2}; F A_{0}; F (f_{2}f_{1}); F A_{2}]

which we take as φ_{f_{2},f_{1}} : (F f_{2})(F f_{1}) → F (f_{1}f_{2}). For φ_{A}: 1_{F A} → F (1_{A}) we take the image under F of

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

The coherence properties that φ must satisfy all follow from the fact that F is a morphism of lax double categories. For example, associativity of φ follows from the identity:

[figure: A_{0}; f_{1}; _{id_{f2,f1}}; A_{1}; f_{2}; A_{2}; f_{3}; _{id_{f3}}; A_{3}; A_{0}; f_{1}; _{id_{f1}}; A_{1}; f_{2}; _{id_{f3,f2}}; A_{2}; f_{3}; A_{3}; A_{0}; _{id_{f3,f2f1}}; f_{2}f_{1}; A_{2}; f_{3}; A_{3}; =; A_{0}; f_{1}; _{id_{f3f2,f1}}; A_{1}; f_{3}f_{2}; A_{3}; A_{0}; f_{3}f_{2}f_{1}; A_{3}; A_{0}; f_{3}f_{2}f_{1}; A_{3}]

(since both are equal to Naturality follows by applying F to both sides of the identity

[figure: A_{0}; _{id_{f3,f2,f1}}; f_{1}; A_{1}; f_{2}; A_{2}; f_{3}; A_{3}; A_{0}; f_{3}f_{2}f_{1}; A_{3} . )]

[figure: A_{0}; •; α; A_{1}; •; β; A_{2}; •; A_{0}; id; A_{1}; A_{2}; B_{0}; id; B_{1}; B_{2}; =; A_{0}; •; βα; A_{2}; •; B_{0}; B_{2}; B_{0}; B_{2}.]

In order to extend the bijection in the previous theorem to an isomorphism of categories we must define what transformations of morphisms of lax double categories are. Let F, G: 𝔸 → 𝔹 be morphisms of lax double categories. A vertical transformation \xymatrix{t: F \ar[r]|{•} & G} consists of the following data:

1. For each object A of 𝔸, a vertical arrow \xymatrix{tA: F A \ar[r]|{•} & GA} ;

2. For each horizontal arrow f: A → A′ in 𝔸, a cell

[figure: F A; •; tA; F f; tf; F A′; •; tA′; GA; Gf; GA′,]

satisfying the following naturality conditions:

1. For each vertical arrow \xymatrix{v: A \ar[r]|{•} & \overline{A}} in 𝔸,

\xymatrix{F A \ar[r]|{•}^{tA} \ar[d]|{•}_{F v} & GA \ar[d]|{•}^{Gv} \\ F \overline{A} \ar[r]|{•}_{t\overline{A}} & G\overline{A}}

commutes;

2. For each multicell

[figure: A_{0}; •; v; α; f_{1}; A_{1}; f_{2}; A_{2}; f_{n}; A_{n}; •; w; B; g; B′]

we have

[figure: F A_{0}; •; v; F α; F f_{1}; F A_{1}; F f_{2}; F A_{2}; F f_{n}; F A_{n}; •; F w; F B; F g; tg; •; tB; F B′; •; tB′; GB; Gg; GB′; F A_{0}; •; tA_{0}; F f_{1}; tf_{1}; F A_{1}; •; tA_{1}; F f_{2}; tf_{2}; F A_{2}; •; tA_{2}; F f_{n−1}; F A_{n−1}; F f_{n}; •; tA_{n−1}; tf_{n}; F A_{n}; •; tA_{n}; =; GA_{0}; •; Gv; Gα; Gf_{1}; GA_{1}; Gf_{2}; GA_{2}; GA_{n−1}; Gf_{n}; GA_{n}; •; Gw; GB; Gg; GB′.]

For double categories 𝔸 and 𝔹 and morphisms F, G: 𝕃ax 𝔸 → 𝕃ax 𝔹, vertical transformations \xymatrix{t: F \ar[r]|{•} & G} correspond to vertical transformations of oplax morphisms of double categories.

We have now defined the correct structure so that the natural morphisms are lax morphisms. In the process we have taken care of coherence as well.

In the notion of lax double category we have enough structure to recover horizontal composition if it is there. Indeed,

[figure: A_{0}; f_{1}; _{id_{f2,f1}}; A_{1}; f_{2}; A_{2}; A_{0}; f_{2}f_{1}; A_{2}]

is a universal cell in the sense that vertical composition with it gives a natural bijection between cells of the form

[figure: A_{0}; f_{2}f_{1}; •; α; A_{2}; •; B_{0}; g; B′]

and cells of the form

[figure: A_{0}; •; f_{1}; α; A_{1}; f_{2}; A_{2}; •; B; g; B′.]

This universal property determines f_{2}f_{1} uniquely up to isomorphism. However, as Hermida makes clear, this condition is not enough in general. If we wish to show that composition defined this way is associative (up to coherent isomorphism) we need what he calls strong representability. Our definition follows the lines in Hermida [H1].

2.7. Definition. Let 𝔸 be a lax double category and

[figure: A_{0}; f_{1}; A_{1}; f_{2}; f_{n}; A_{n}]

a path of arrows of 𝔸. We say that the composite of the path is strongly representable if there is an arrow f: A_{0} → A_{n} and a multicell

[figure: A_{0}; η_{⟨fn,...,f_{1}⟩}; f_{1}; A_{1}; f_{2}; f_{n}; A_{n}; A_{0}; f; A_{n}]

such that for any paths ⟨x_{1}, …, x_{m}⟩, and ⟨y_{p}, …, y_{1}⟩, and cell α as below

[figure: X_{m}; •; v; x_{m}; X_{1}; x_{1}; A_{0}; α; f_{1}; A_{1}; f_{2}; f_{n}; A_{n}; y_{1}; Y_{1}; y_{2}; Y_{p}; •; w; B; g; C]

there is a unique cell \overline{α}

[figure: X_{m}; •; v; x_{m}; X_{1}; x_{1}; A_{0}; \overline{α}; f; A_{n}; y_{1}; Y_{1}; y_{2}; Y_{p}; •; w; B; g; C]

such that

[figure: X_{m}; x_{m}; id; X_{m−1}; x_{m−1}; X_{1}; x_{1}; id; A_{0}; f_{1}; η_{⟨fm,...,f_{1}⟩}; A_{1}; f_{2}; f_{n}; A_{n}; y_{1}; id; Y_{1}; y_{2}; y_{p}; Y_{p}; X_{m}; •; v; x_{m}; X_{m−1}; x_{m−1}; X_{1}; x_{1}; A_{0}; \overline{α}; f; A_{n}; y_{1}; Y_{1}; y_{2}; y_{p}; Y_{p}; •; w; B; g; C]

is equal to α.

We say that the composite of the path ⟨f_{n}, …, f_{1}⟩ is representable if we require the above condition only in the case where m = p = 0, i.e., when there are no x’s or y’s.

We will usually choose one representing f and call it f_{n}f_{n−1} ⋯ f_{1}. When n = 1, the composite is represented by f_{1}. When n = 0, a case we will be particularly interested in, we say that the identity 1_{A_{0}} is (strongly) representable. Aside from the case n = 0, we will be mostly interested in the case n = 2. The following proposition is essentially due to Hermida ([H1], 11.4).

2.8. Proposition. A lax double category is of the form 𝕃ax 𝔸 if and only if all composites are strongly representable.

2.9. Representability of composition. It may appear from the literature so far that strong representability is the only useful condition, and in fact it is the only one we will use in this paper. However, plain representability is also interesting. In fact there is something mysterious about strong representability; after all, representability on its own does determine the composites up to isomorphism. Without strong representability we do not get associativity of composition up to isomorphism. We do get, however, comparison cells fgh → (fg)h and fgh → f(gh). More generally, given a path of paths of morphisms f_{1,1} … f_{1,n_{1}} … f_{m,1} … f_{m,n_{m}} we have comparison morphisms

f_{m,n_{m}} ⋯ f_{1,1} → (f_{m,n_{m}} ⋯ f_{m,1}) ⋯ (f_{1,n_{1}} ⋯ f_{1,1})  (5)

satisfying the obvious associativity conditions. Thus we obtain the double category version of (the dual of) Leinster’s lax bicategories (see [L2], p. 121). Let us call these slack double categories so as to avoid possible confusion with what we call lax double categories and he calls fc-multicategories. The relationship between these two concepts is this. Given a slack double category 𝔸 we can construct a lax one, 𝕃ax 𝔸, as in the paragraph following Definition 2.5. The composition of multicells there only requires the comparison morphisms (5). Then Proposition 2.8 can be modified to say that a lax double category is of the form 𝕃ax 𝔸 for a slack double category 𝔸 if and only if all composites are (weakly) representable.

There are also Grandis’ related notions of lax bicategories which have comparison cells between certain pairs of associations of composites in a preferred direction (which is chosen to model problems in concurrency theory) [G]. These form a special case of Leinster’s lax bicategories where some of the comparison cells are identities.

We believe that our notion of lax double category is the most basic one from which the others can best be understood and so we suggest using this name rather than that of fc-multicategory, since the latter does not reflect the central role of this concept.

2.10. Oplax double categories. The example that motivated this section is that of 𝕊pan A where A is a category which does not necessarily have pullbacks and this yields an oplax double category rather than a lax one. This is simply the vertical dual of the notion of lax double category in which multicells look like

[figure: A; v; •; f; α; A′; •; v′; B_{0}; g_{1}; B_{1}; g_{2}; B_{2}; g_{3}; g_{n}; B_{n}.]

The 𝕊pan construction has been central to our work and has guided us in our choice of orientation for the construction of Π_{2}A ([DPP1]) and consequently ℙath 𝔸. Thus we now switch to oplax double categories.

Given a double category 𝔸 we now have an oplax double category 𝕆plax 𝔸 associated to it where a multicell α as above is a cell

[figure: A; f; •; v; α; A′; •; v′; B_{0}; g_{n}^{0}; B_{n}]

in 𝔸. Morphisms of oplax double categories are the obvious ones (dual to the lax case) as are vertical transformations. It is easy to see that 𝕆plax extends to double functors and vertical transformations of such.

We introduced the 2-categories Doub and Doub_{Opl} in Section 1. We also have the larger 2-category Oplax of oplax double categories, whose objects are oplax double categories, arrows are morphisms of such, and 2-cells are vertical transformations.

2.11. Proposition. 𝕆plax is a locally full and faithful 2-functor Doub → Oplax.

Proof. The only thing that is not completely obvious is the locally full and faithful part, and that is an easy calculation.

Proposition 1.19 of Section 1 showed that ℙath is left adjoint to the inclusion Doub ↪ Doub_{Opl}. We now show that ℙath extends to Oplax and is 2-left adjoint to 𝕆plax. This is the natural setting for ℙath. An oplax double category has all the ingredients for a double category except for the horizontal composition. Generating the free double category from one would necessarily involve paths, ordinary paths of 1-cells and paths of double cells, and perhaps some bookkeeping complications for double cells. Our ℙath construction is exactly the right thing. In fact, it doesn’t use horizontal composition of arrows or cells.

Explicitly, let 𝔸 be our oplax double category. We construct a (strict) double category ℙath 𝔸 with the same objects and vertical arrows as 𝔸. A horizontal arrow is a path of horizontal arrows in 𝔸 and a double cell is a horizontal path of multicells in 𝔸. The vertical domain and codomain of such a path are the path of domains and the concatenation of the paths of the codomains (respectively). For example, a typical cell might look like

[figure: A_{0}; •; v_{0}; f_{1}; α_{1}; A_{1}; •; v_{1}; f_{2}; A_{2}; α_{2}; •; v_{2}; f_{3}; α_{3}; A_{3}; •; v_{3}; B_{0}; g_{1}; B_{1}; g_{2}; B_{2}; g_{3}; B_{3}; g_{4}; B_{4}; g_{5}; B_{5}.]

The domains and codomains are clear. Vertical composition of cells uses the multicell composition of 𝔸, in the obvious way. Both horizontal structures are free categories; vertical composition of arrows also forms a category because it is the same as in 𝔸. It is easy to show that vertical composition of cells also forms a category and to check the middle four interchange law.

A loftier point of view will make this all transparent. For a cartesian monad 𝕋 in a category A, we have not only the double category 𝕋-𝕊pan (A) but also the the double category 𝕊pan(A^{𝕋}) of spans in the Eilenberg-Moore category A^{𝕋} of A, and a double functor T̃: 𝕋-𝕊pan (A) → 𝕊pan(A^{𝕋}). T̃ is defined by T̃(A) = (T A, μA) and T̃(f) = T (f) for an object A and a vertical arrow f of 𝕋-𝕊pan. For a 𝕋-Span, T A ⟵^{p} S ⟶^{g} B, T̃ is defined as

(T A, μA) ⟵^{μA} (T^{2}A, μT A) ⟵^{T p} (T S, μS) ⟶^{T g} (T B, μB)

and for a cell

\xymatrix{A \ar[d]_{f} & T A \ar[d]_{T f} & S \ar[d]_{x} \ar[l]_{p} \ar[r]^{q} & B \ar[d]^{g} \\ A′ & T A′ & S′ \ar[l]^{p′} \ar[r]_{q′} & B′,}

T̃(f, x, g) = (T f, T x, T g).

For the identity span T A ⟵^{ηA} A ⟶^{1_{A}} A we get

\xymatrix{T A & T^{2}A \ar[l]_{μA} & T A \ar[l]_{T ηA} \ar[r]^{T 1_{A}} & T A}

which is the identity in 𝕊pan (A^{𝕋}). A composite

[figure: P; π; π′; Pb; T S; T p; T q; S′; p′; q′; T^{2}A; μA; T B; C; T A]

is transformed into

[figure: T P; T π; T π′; Pb; T^{2}S; T^{2}p; T^{2}q; T S′; T p′; T q′; T^{3}A; T μA; T^{2}B; T C; T^{2}A; μA; T A]

whereas the composite T̃(S′)T̃(S) is given by

[figure: T P; T π; T π′; Pb; T^{2}S; Pb; μS; T^{2}q; T S′; T p′; T q′; T S; T p; T q; T^{2}B; μB; T C; T^{2}A; μA; T B; T A]

where the two squares are pullbacks because 𝕋 is cartesian. Finally, the left legs are equal because

\xymatrix{T^{2}S \ar[d]_{μS} \ar[r]^{T^{2}p} & T^{3}A \ar[d]_{μT A} \ar[r]^{T μA} & T^{2}A \ar[d]^{μA} \\ T S \ar[r]_{T p} & T^{2}A \ar[r]_{μA} & T A}

commutes.

So T̃: 𝕋-𝕊pan (A) → 𝕊pan(A^{𝕋}) is indeed a double functor and as such preserves monads and their morphisms. If A is the category of graphs and 𝕋 is the free category monad on it, then 𝕋-𝕊pan (A) is the double category of lax double categories, A^{𝕋} is the category of categories so a monad in 𝕊pan(A^{𝕋}) is a double category. This is the higher reason why we can apply the ℙath construction to a lax double category, and by duality, to an oplax double category to get a genuine double category, ℙath 𝔸.

2.12. Theorem. ℙath is the object part of a 2-functor Oplax → Doub which is a 2-left adjoint to the inclusion 𝕆plax: Doub → Oplax.

Proof. That ℙath is a 2-functor with the obvious extension to morphisms of oplax double categories and vertical transformations is a straightforward calculation.

Let 𝔸 be an arbitrary oplax double category. Define Ξ: 𝔸 → 𝕆plax ℙath 𝔸 to be the identity on objects and vertical arrows and to take horizontal arrows and cells to singleton paths of the same. This is clearly a morphism of oplax double categories.

Given a double category 𝔹 we will show that

Ξ̃: Doub (ℙath 𝔸, 𝔹) → Oplax (𝔸, 𝕆plax 𝔹)

defined by Ξ̃(F) = 𝕆plax(F) · Ξ is an isomorphism of categories.

The referee has pointed out that the above adjunction can also be seen as part of our previously described “loftier point of view”. Indeed, one can extend the usual forgetful functor A^{𝕋} → A to a lax double functor Ũ, which is right adjoint to T̃ in an appropriate double categorical sense. Then taking monads it will induce the inclusion of categories, and yield the adjunction of Theorem 2.12. See [L2], Section 6.6 for further details.

2.13. Theorem. ℙath : Oplax → Doub is 2-comonadic.

Proof. The 2-comonad on Doub induced by the adjunction

ℙath ⊣ 𝕆plax

is what we called ℙath in Section 1.18 where we showed that it was oplax idempotent.

A coalgebra for the ℙath comonad is a double category 𝔸 with a double functor F: 𝔸 → ℙath 𝔸 satisfying the counit law

[figure: 𝔸; F; ℙath 𝔸; E; 𝔸]

and coassociativity

\xymatrix{𝔸 \ar[d]_{F} \ar[r]^{F} & ℙath 𝔸 \ar[d]^{ℙath F} \\ ℙath 𝔸 \ar[r]_{D} & ℙath^{2} 𝔸.}

The first condition forces F to be the identity on objects and vertical arrows. It also says that F gives a functorial factorisation of horizontal arrows and double cells into n-fold composites. In particular, this assigns a grading to horizontal arrows and double cells. As in the proof of the one-dimensional case from the prologue, this makes the horizontal arrows into a free category on the graph of degree 1 arrows, and similarly for the cells under horizontal composition.

In fact, the grading is given by \xymatrix{𝔸 \ar[r]^{F} & ℙath 𝔸 \ar[r]^{ℙath (!)} & ℙath 1} . It will be recalled from Section 1 that a cell of degree 1 in ℙath 1 has the form

[figure: ∗; 1; ∗; ∗; n; ∗]

which tells us that a cell of degree 1 in 𝔸 has boundary

[figure: A; f; α; •; v; A′; •; v′; B_{0}; g_{1}; B_{1}; g_{2}; g_{n}; B_{n}]

where f and each g_{i} has itself degree 1. It follows that the degree 1 cells form an oplax double category 𝔸(1) and that 𝔸 ≅ ℙath 𝔸(1).

2.14. Remark. We interpret this theorem as validating our claim that oplax double categories are precisely the right structure on which to define oplax morphisms. In particular, Oplax is as cocomplete as Doub which has all 2-colimits, i.e., Oplax is 2-cocomplete. It is also 2-complete because Doub is and the comonad ℙath preserves pullbacks as is easily seen. Note that Doub_{Opl} is neither complete nor cocomplete, a problem that surfaces immediately when working with oplax morphisms. However, we know from monad theory that every coalgebra is an equaliser of two cofree coalgebras, in fact that equaliser is a pullback, even an intersection, so that Oplax is a completion of Doub_{Opl} under binary intersections. Simply adding intersections makes it complete and cocomplete.

It should also be remarked that since the comonad ℙath is oplax idempotent, it is a property of a double category to be ℙath of an oplax one, not extra structure.

3. ℙath_{∗}

The pointed case is more complicated but also more interesting and is at the heart of our Π_{2} construction. Now we are dealing with the case where identities are preserved. Thus we are in the situation analogous to free categories generated by reflexive graphs, the Path_{∗} construction from the Prologue. Already, in the one dimensional case, there were some complications involving the equivalence relation on paths, but the situation was quite simple and equivalence classes had canonical representatives. In the two dimensional case we do not have to worry about equivalent paths of arrows, but the equivalence relation on cells is much more complicated.

3.1. Definition. An oplax morphism of double categories F: 𝔸 → 𝔹 is called normal if for every A the given cell

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

is vertically invertible.

The problem which we shall address is the construction of the universal oplax normal morphism

\xymatrix{𝔸 \ar[r]^{Ξ_{∗}} & ℙath_{∗} 𝔸}

for any double category 𝔸.

Normality is important. Without it we can do almost nothing; and we note in particular that our motivating example, A → 𝕊panA, is normal. This is more or less equivalent to preservation of adjoints. More precisely, a morphism is normal if and only if it preserves adjoints and companions [GP], as will be shown in [DPP4].

3.2. The Necessity of the Equivalence Relation. It is clear that the universal oplax normal morphism, Ξ_{∗}: 𝔸 → ℙath_{∗} 𝔸 exists as it is described by operations and equations. Our problem is to get a concrete workable description of it. We have already constructed the universal oplax morphism, Ξ: 𝔸 → ℙath 𝔸 and this will be our starting point. Universality of Ξ gives a unique morphism of double categories, Φ, such that

\xymatrix{ & ℙath 𝔸 \ar[dd]^{Φ} \\ 𝔸 \ar[ur]^{Ξ} \ar[dr]_{Ξ_{∗}} \\  & ℙath_{∗} 𝔸}

commutes. So ℙath_{∗} 𝔸 will require some inverses that are not present in ℙath 𝔸, and these in turn will require certain elements to be identified. Specifically, we must add an inverse for each canonical morphism

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

in ℙath 𝔸, and then all double categorical consequences of this. Thus the objects and vertical arrows on ℙath_{∗} 𝔸 are those of 𝔸, and the horizontal arrows are paths of arrows of 𝔸, just like the arrows of ℙath 𝔸. However, the double cells are equivalence classes of words in the cells of ℙath 𝔸 and the ι_{A}^{−1}, constructed using horizontal and vertical composition. This, of course, is potentially very complicated. The following proposition hints that the problem may be tractable after all.

There are two simple kinds of words, those that come from single cells in ℙath 𝔸, i.e., fences (φ, ⟨v_{i}⟩, ⟨α_{i}⟩): ⟨f_{i}⟩ → ⟨g_{j}⟩, which we call words of type 1, and those of the form

[figure: A; ι_{A}^{−1}; A; 1_{A}; •; v; λ; A; •; v′; B_{0}; g_{1}; B_{1}; g_{2}; g_{m}; B_{m}]

where λ is a double cell

[figure: A; 1_{A}; •; v; λ; A; •; v′; B_{0}; g_{m}^{1}; B_{m}]

in 𝔸, which we call words of type 2.

3.3. Proposition. Each cell of ℙath_{∗} 𝔸 with vertical domain of length greater than 0 has a representative of type 1; a cell with vertical domain of length 0 has a representative of type 2.

Proof. It is clear that the cells of ℙath_{∗} 𝔸 are generated by equivalence classes of words of type 1 and 2, so it will be sufficient to show that they are closed under horizontal and vertical composition.

Both horizontal and vertical composition of two words of type 1 yield words of type 1 as they come from ℙath 𝔸. Also, a word of type 2 composed vertically with a word of type 1 (where the word of type 2 is above the word of type 1) gives another word of type 2. For a word of type 1 composed vertically with a word of type 2, consider the diagram

[figure: A_{0}; f_{1}; •; v_{0}; A_{1}; f_{2}; •; v_{1}; α_{1}; α_{2}; α_{n}; f_{n}; A_{n}; •; v_{n}; A; ι_{A}^{−1}; A; •; v; λ; 1_{A}; A; •; v′; B_{0}; g_{1}; B_{1}; g_{2}; g_{m}; B_{m}.]

If we write α_{n} = ι_{A} · \overline{α}_{n} for

[figure: A_{n−1}; •; v_{n−1}; f_{n}; _{\overline{α}_{n}}; A_{n}; •; v_{n}; A; 1_{A}; A,]

the above composition can be rewritten as

[figure: A_{0}; •; v·v_{0}; f_{1}; α_{1}; A_{1}; •; α_{2} ···; f_{2}; A_{n−1}; •; v·v_{2}; λ·\overline{α}_{n}; f_{n}; A_{n}; •; v′·v_{n}; B_{0}; g_{1}; B_{1}; g_{2}; g_{m}; B_{m}.]

In a similar way, composing two type 2 words vertically

[figure: X; ι_{X}^{−1}; X; 1_{X}; •; w; ξ; X; •; w′; A; ι_{A}^{−1}; A; 1_{A}; •; v; λ; A; •; v′; B_{0}; g_{1}; B_{1}; g_{2}; g_{m}; B_{m}]

gives

[figure: X; ι_{X}^{−1}; X; 1_{X}; •; v·w; λ·\overline{ξ}; X; •; v′·w′; B_{0}; g_{1}; B_{1}; g_{2}; g_{m}; B_{m}.]

Next, consider the horizontal composite of a word of type 1 with a word of type 2 as above. First note that for any f: A → A′, the vertical composites

[figure: A; f; ι_{A}^{−1}; A′; _{id_{f}}; A; f; “id_{f} ”; A′; A; 1_{A}; ι_{A}; A; f; _{id_{f}}; A′; and; A; 1_{A}; ι_{A}; A; f; _{id_{f}}; A′; A; f; A′; A; f; A′]

are both equal to id_{f} and the bottom cell is invertible, so

[figure: A; f; ι_{A}^{−1}; A′; _{id_{f}}; is equal to; A; f; “id_{f} ”; A′; A; 1_{A}; A; f; A′; A; 1_{A}; A; f; A′.]

Thus, the horizontal composition of a word of type 2 as above with a word of type 1, (φ, ⟨v_{i}⟩, ⟨α_{i}⟩), can be written as

[figure: A; ι_{A}^{−1}; f_{1}; A_{1}; _{id_{f_{1}}}; f_{2}; id; f_{n}; A_{n}; A; 1_{A}; λ; •; v; A; •; v′; f_{1}; A_{1}; f_{2}; (φ,⟨v_{i}⟩,⟨α_{i}⟩); f_{n}; A_{n}; •; B_{0}; g_{1}; B_{1}; g_{2}; g_{m}; B_{m}; g_{m+1}; B_{m+1}; g_{p}; B_{p}]

so that the ι_{A}^{−1} gets absorbed into the id_{f_{1}} and the whole composition is a word of type 1. Dually, a word of type 1 followed by a word of type 2 is another word of type 1.

Finally, the horizontal composite of two type 2 words is another type 2 word. Indeed, the two vertical composites

[figure: A; A; ι_{A}^{−1}; A; 1_{A}; ι_{A}; A; ι_{A}^{−1}; ι_{A}^{−1}; 1_{A}; _{id_{1_{A}}}; A; and; A; 1_{A}; “id_{1_{A}}”; A; A; 1_{A}; A; A; 1_{A}; ι_{A}; A; _{id_{1_{A}}}; 1_{A}; A; A; 1_{A}; A]

both equal ι_{A}^{−1} and as (id_{1_{A}})(ι_{A}) is invertible, we see that

[figure: A; A; ι_{A}^{−1}; A; 1_{A}; A; ι_{A}^{−1}; ι_{A}^{−1}; 1_{A}; A; =; A; 1_{A}; “id_{1_{A}}”; A; A; 1_{A}; A; 1_{A}; A.]

It is now easy to see that the horizontal composite of two type 2 words is again one.

Now that we have an idea of what the equivalence classes are, our next step is to understand the equivalence relation as such. The next result is crucial in this endeavour.

3.4. Proposition. Let (φ, ⟨v_{i}⟩, ⟨α_{i}⟩) and (ψ, ⟨w_{i}⟩, ⟨β_{i}⟩) be two fences (i.e., words of type 1) with common boundary

[figure: A_{0}; •; v; f_{1}; A_{1}; f_{2}; f_{n}; A_{n}; •; v′; B_{0}; g_{0}; B_{1}; g_{2}; g_{m}; B_{m}]

502  R. J. MACG. DAWSON, R. PARÉ, AND D. A. PRONK

such that:

1. φ ⩽ ψ;

2. for each i = 0, 1, …, n, there are cells λ_{i}, as in

[figure: A_{i}; •; v_{i}; λ_{i}; A_{i}; •; w_{i}; B_{φ(i)}; B_{φ(i)+1}; B_{ψ(i)}]

such that

[figure: A_{i−1}; •; v_{i−1}; f_{i}; α_{i}; A_{i}; •; v_{i}; λ_{i}; A_{i}; •; v_{i}; =; A_{i−1}; •; v_{i−1}; λ_{i−1}; A_{i−1}; •; w_{i−1}; f_{i}; β_{i}; A_{i}; •; w_{i}; B_{φ(i)}; g_{φ(i)}^{φ(i−1)}; B_{φ(i)}; g_{ψ(i)}^{φ(i)}; B_{ψ(i)}; B_{φ(i)}; g_{φ(i)}^{φ(i−1)}; B_{φ(i)}; g_{ψ(i)}^{φ(i)}; B_{ψ(i)}]  (6)

3. λ_{0} = 1_{v_{0}} = 1_{w_{0}} and λ_{n} = 1_{v_{n}} = 1_{w_{n}}. Then (φ, ⟨v_{i}⟩, ⟨α_{i}⟩) and (ψ, ⟨w_{i}⟩, ⟨β_{i}⟩) represent the same cell in ℙath_{∗} 𝔸. 3.5. Remark. The intertwining of α, β and λ in (6) is nicely expressed in the double index notation, viz. λ_{i}α_{i}^{j} = β_{i}^{j}λ_{j}.

Proof. Consider α, β, and λ as illustrated in

[figure: A; f; _{id_{f}}; A′; ι_{A}^{−1}; f′; A′′; _{id_{f′}}; A; f; •; α; A′; •; λ; A′; •; β; f′; A′′; •; B_{0}; ⋯; B_{p}; ⋯; B_{q}; ⋯; B_{m}.]

First composing the four cells on the left and the two on the right and then composing the two on the left and the four on the right, we see that the fences

[figure: A; •; f; λα; A′; f′; β; •; A′′; •; and; A; •; f; α; A′; f′; βλ; •; A′′; •; B_{0}; ⋯; B_{q}; ⋯; B_{m}; B_{0}; ⋯; B_{p}; ⋯; B_{m}]

represent the same cell in ℙath_{∗} 𝔸. Thus we get the following:

⟨α_{n}, α_{n−1}, …, α_{1}⟩ = ⟨λ_{n}α_{n}, α_{n−1}, …, α_{1}⟩
= ⟨β_{n}λ_{n−1}, α_{n−1}, …, α_{1}⟩
= ⟨β_{n}, λ_{n−1}α_{n−1}, …, α_{1}⟩
= ⟨β_{n}, β_{n−1}λ_{n−2}, …, α_{1}⟩
= ⟨β_{n}, β_{n−1}, λ_{n−2}α_{n−2}, …, α_{1}⟩
⋯
= ⟨β_{n}, β_{n−1}, …, λ_{1}α_{1}⟩
= ⟨β_{n}, β_{n−1}, …, β_{1}λ_{0}⟩
= ⟨β_{n}, β_{n−1}, …, β_{1}⟩

3.6. Remark. For fences whose vertical domain has length 1, there are no non-trivial such systems of λ-cells. Moreover, since type 2 representatives are vertically isomorphic to type 1 representatives with vertical domains of length 1, there are none for that case either. This implies that the equivalence relation for double cells introduced in the next Proposition is trivial for all representatives of type 2, and for those of type 1 with vertical domains of length 1.

3.7. Proposition. Let ∼ be the equivalence relation on fences generated by

(φ, ⟨v_{i}⟩, ⟨α_{i}⟩) ∼ (ψ, ⟨w_{i}⟩, ⟨β_{i}⟩)

if there exist ⟨λ_{i}⟩ satisfying the conditions of the previous proposition. Then ∼ is a congruence of double categories on ℙath 𝔸.

Proof. It is clear that horizontal composition of fences respects ∼: simply concatenate the λs.

To show that vertical composition respects ∼ it will be sufficient to show that if there are ⟨λ_{i}⟩ directly relating (φ, ⟨v_{i}⟩, ⟨α_{i}⟩) to (ψ, ⟨w_{i}⟩, ⟨β_{i}⟩), then

(φ, ⟨v_{i}⟩, ⟨α_{i}⟩) · (θ, ⟨u_{i}⟩, ⟨γ_{i}⟩) is related to (ψ, ⟨w_{i}⟩, ⟨β_{i}⟩) · (θ, ⟨u_{i}⟩, ⟨γ_{i}⟩)

and

(ξ, ⟨x_{k}⟩, ⟨δ_{k}⟩) · (φ, ⟨v_{i}⟩, ⟨α_{i}⟩) is related to (ξ, ⟨x_{k}⟩, ⟨δ_{k}⟩) · (ψ, ⟨w_{i}⟩, ⟨β_{i}⟩).

Now

(φ, ⟨v_{i}⟩, ⟨α_{i}⟩) · (θ, ⟨u_{i}⟩, ⟨γ_{i}⟩) = (φθ, ⟨v_{θ(j)} · u_{j}⟩, ⟨α_{θ(j)}^{θ(j−1)} · γ_{j}⟩)

and

(ψ, ⟨w_{i}⟩, ⟨β_{i}⟩) · (θ, ⟨u_{i}⟩, ⟨γ_{i}⟩) = (ψθ, ⟨w_{θ(j)} · u_{j}⟩, ⟨β_{θ(j)}^{θ(j−1)} · γ_{j}⟩).

We have

[figure: Y_{j−1}; •; u_{j−1}; γ_{j}; Y_{j}; •; u_{j}; 1_{u_{j}}; Y_{j}; •; u_{j}; Y_{j−1}; •; u_{j−1}; 1_{u_{j−1}}; Y_{j}; •; u_{j}; γ_{j}; Y_{j}; •; u_{j}; A_{θ(j−1)}; •; v_{θ(j−1)}; f_{θ(j)}^{θ(j−1)}; α_{θ(j)}^{θ(j−1)}; A_{θ(j)}; •; v_{θ(j)}; λ_{θ(j)}; A_{θ(j)}; •; w_{θ(j)}; =; A_{θ(j−1)}; •; v_{θ(j−1)}; λ_{θ(j−1)}; A_{θ(j)}; •; v_{θ(j)}; f_{θ(j)}^{θ(j−1)}; β_{θ(j)}^{θ(j−1)}; A_{θ(j)}; •; w_{θ(j)}; B_{φθ(j−1)}; g_{φθ(j)}^{φθ(j−1)}; B_{φθ(j)}; g_{ψθ(j)}^{φθ(j)}; B_{ψθ(j)}; B_{φθ(j−1)}; g_{ψθ(j−1)}^{φθ(j−1)}; B_{ψθ(j−1)}; g_{ψθ(j)}^{ψθ(j−1)}; B_{ψθ(j)}]

so if we take \overline{λ} = λ_{θ(j)} · 1_{u_{j}} we get our relation.

For the equivalence involving (ξ, ⟨x_{k}⟩, ⟨δ_{k}⟩) take \overline{\overline{λ}}_{i} = δ_{ψ(i)}^{φ(i)} · λ_{i}. Then

[figure: A_{i−1}; •; v_{i−1}; f_{i}; α_{i}; A_{i}; •; v_{i}; λ_{i}; A_{i}; •; w_{i}; A_{i−1}; •; v_{i−1}; λ_{i−1}; A_{i−1}; f_{i}; •; w_{i−1}; β_{i}; A_{i}; •; w_{i}; B_{φ(i−1)}; •; x_{φ(i−1)}; g_{φ(i)}^{φ(i−1)}; δ_{φ(i)}^{φ(i−1)}; B_{φ(i)}; •; x_{φ(i)}; g_{ψ(i)}^{φ(i)}; δ_{ψ(i)}^{φ(i)}; B_{ψ(i)}; •; x_{ψ(i)}; =; B_{φ(i−1)}; •; x_{φ(i−1)}; g_{ψ(i−1)}^{φ(i−1)}; δ_{ψ(i−1)}^{φ(i−1)}; B_{ψ(i−1)}; •; x_{ψ(i−1)}; g_{ψ(i)}^{ψ(i−1)}; δ_{ψ(i)}^{ψ(i−1)}; B_{ψ(i)}; •; x_{ψ(i)}; X_{ξφ(i−1)}; X_{ξφ(i)}; X_{ξψ(i)}; X_{ξφ(i−1)}; X_{ξψ(i−1)}; X_{ξψ(i)}]

shows that (ξ, ⟨x_{k}⟩, ⟨δ_{k}⟩) · (φ, ⟨v_{i}⟩, ⟨α_{i}⟩) ∼ (ξ, ⟨x_{k}⟩, ⟨δ_{k}⟩) · (ψ, ⟨w_{i}⟩, ⟨β_{i}⟩).

3.8. The Construction of ℙath_{∗}. Let 𝔸 be a double category. We construct a new double category ℙath_{∗} 𝔸 which has the same objects and vertical arrows as 𝔸. A horizontal arrow of ℙath_{∗} 𝔸 is a path of horizontal arrows of 𝔸. For n ⩾ 1, a cell with boundary

[figure: A_{0}; •; v_{0}; f_{1}; A_{1}; f_{2}; f_{n}; A_{n}; •; v_{n}; B_{0}; g_{1}; B_{1}; g_{2}; g_{m}; B_{m}]

is an equivalence class of fences (φ, ⟨v_{i}⟩, ⟨α_{i}⟩) where the equivalence relation is the ∼ of Proposition 3.7. Such an equivalence class will be denoted [φ, ⟨v_{i}⟩, ⟨α_{i}⟩] or [α_{n}, α_{n−1}, …, α_{1}]. (A more suggestive notation might be α_{n}⊗α_{n−1}⊗⋯⊗α_{1} or α_{n}⊗_{v_{n−1}} α_{n−1}⊗_{v_{n−2}} ⋯⊗_{v_{1}} α_{1}.) The number n is called the degree of the cell. The degree zero cells or scalars are cells of type 2,

[figure: A; ι_{A}^{−1}; A; 1_{A}; •; λ; A; •; B_{0}; B_{1}; B_{n}]

which we will denote simply by λ. They are in bijection with cells of degree 1 with vertical domain an identity, but it is important to distinguish between the two. The first notation does: it gives us [λ] as opposed to λ, even though the equivalence relation is trivial in degree 1. The ⊗ notation does not make the distinction and with this notation we will rely on alphabetical distinction, writing α, β as opposed to λ, μ etc. When confusion is possible, we will revert to the first notation.

We are now ready to define horizontal and vertical composition of cells. First the horizontal:

[β_{m}, …, β_{1}][α_{n}, …, α_{1}] = [β_{m}, …, β_{1}, α_{n}, …, α_{1}]
λ[α_{n}, …, α_{1}] = [λα_{n}, …, α_{1}]
[β_{m}, …, β_{1}]μ = [β_{m}, …, β_{1}μ]
λμ = λμ.

The vertical structure comes from that of ℙath 𝔸 in degree ⩾ 1.

[ψ, ⟨w_{j}⟩, ⟨β_{j}⟩][φ, ⟨v_{i}⟩, ⟨α_{i}⟩] = [ψφ, ⟨w_{φ(i)} · v_{i}⟩, ⟨β_{φ(i)}^{φ(i−1)} · α_{i}⟩]
λ · [α_{n}, …, α_{1}] = [λ · α_{n}, 1_{v} · α_{n−1}, …, 1_{v} · α_{1}]
[β_{m}, …, β_{1}] · μ = (β_{m} ⋯ β_{1}) · μ = β_{m}^{0} · μ
λ · μ = λ · μ.

Also, define Ξ_{∗}: 𝔸 → ℙath_{∗} 𝔸 to be the identity on objects and vertical arrows and inclusion as paths of length 1 on arrows, and ξ_{∗}(α) = [α] on cells.

3.9. Proposition.

1. ℙath_{∗} 𝔸 is a (strict) double category.

2. Ξ_{∗}: 𝔸 → ℙath_{∗} 𝔸 is an oplax morphism.

3. Ξ_{∗} is vertically full and faithful.

Proof.

1. That composition of horizontal or vertical arrows is associative and unitary is obvious.

There are eight instances of horizontal associativity for cells that must be checked but only one is not entirely obvious:

([β_{m}, …, β_{1}]λ)[α_{n}, …, α_{1}] = [β_{m}, …, β_{1}λ, α_{n}, …, α_{1}]
[β_{m}, …, β_{1}](λ[α_{n}, …, α_{1}]) = [β_{m}, …, β_{1}, λα_{n}, …, α_{1}]

which are equal as a consequence of the equivalence relation. The horizontal identity on v is given by the scalar 1_{v}. There are also eight instances of vertical associativity depending on the type of factors. All of these can be proved by fairly straightforward calculations. We do a representative example, the case of the multiplication of a type 1 cell with a scalar on each side. We have that λ · ([α_{n}, …, α_{1}] · μ) = λ · (α_{n}^{0} · μ) = λ · α_{n}^{0} · μ, whereas

(λ · [α_{n}, …, α_{1}]) · μ
= [λ · α_{n}, 1 · α_{n−1}, …, 1 · α_{1}] · μ
= ((λ · α_{n})(1 · α_{n−1}) ⋯ (1 · α_{1})) · μ

which is represented by

[figure: X; •; •; μ; A_{0}; f_{1}; •; α_{1}; A_{1}; f_{2}; •; α_{2}; A_{n−1}; •; α_{n}; f_{n}; A_{n}; •; B; •; 1; B; •; B; •; λ; B; •; C_{0}; C_{1}; C_{p} .]

By general associativity [DP1], this is the same as λ · α_{n}^{0} · μ.

The vertical identity on [figure: A_{0}; f_{1}; A_{1}; f_{2}; f_{n}; A_{n}] is [id_{f_{n}}, …, id_{f_{1}}] and the vertical identity on the empty path A is the scalar id_{1_{A}} = 1_{id_{A}}. The four cases to be checked to verify that these actually work are trivial. Finally, the middle four interchange law involves checking sixteen cases, which all work either for trivial reasons or because of the equivalence relation.

2. Ξ_{∗}: 𝔸 → ℙath_{∗} 𝔸 clearly preserves vertical composition of arrows and cells as well as vertical identities. The cells expressing oplaxity come from those for Ξ: 𝔸 → ℙath 𝔸, so they satisfy the required coherence conditions. Finally, the cell (ξ_{∗})_{A}: Ξ_{∗}(1_{A}) → 1_{Ξ_{∗}A} comparing units is

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

which has the scalar

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

as its inverse. Indeed, id_{1_{A}} · [id_{1_{A}}] = [id_{1_{A}} · id_{1_{A}}] = [id_{1_{A}}] which is the identity on 1_{A} in ℙath_{∗} 𝔸, and [id_{1_{A}}] · id_{1_{A}} = id_{1_{A}} · id_{1_{A}} = id_{1_{A}}.

3. Ξ_{∗} is the identity on vertical arrows and as the equivalence relation is trivial on cells of degree 1, there is a bijection between cells of the form

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

in ℙath_{∗} 𝔸 and similar ones in 𝔸.

We can now state the main result of this section:

3.10. Theorem. For any double category 𝔸, Ξ_{∗}: 𝔸 → ℙath_{∗} 𝔸 is the universal oplax normal morphism, i.e., for any (strict) double category 𝔹 composing with Ξ_{∗} induces an isomorphism of categories

Doub(ℙath_{∗}𝔸, 𝔹) ⟶^{≅} Doub_{OplN}(𝔸, 𝔹).

Proof. Given an oplax normal morphism F as in the diagram below, we wish to show that it extends uniquely to a double functor G

\xymatrix{𝔸 \ar[dr]_{F} \ar[r]^{Ξ_{∗}} & ℙath_{∗} 𝔸 \ar@{.>}[d]^{G} \\  & 𝔹 & .}

As Ξ_{∗} is the identity on objects and vertical arrows, G is uniquely determined on these, and as ℙath_{∗} 𝔸 is free on horizontal arrows G is also uniquely determined on these. Since F is oplax it extends uniquely to a double functor on ℙath 𝔸, so there is only one possible choice for G on cells of type 1. It is easily checked that G respects the instances of ∼ described in Proposition 3.4, so G is well-defined on equivalence classes. Finally, any cell of type 2 (scalar) λ can be written as [λ] · 1_{A} and G(1_{A}) has to be

[figure: F A; φ_{A}; F A; F 1_{A}; F A .]

This shows that there is a unique well-defined G extending F and we only need to show that it preserves horizontal and vertical composition. On cells of type 1 there is no problem as the compositions are already preserved at the ℙath 𝔸 stage.

To check the other cases we need explicit formulas for G[α_{n}, …, α_{1}] and G(λ). They are

G[α_{n}, …, α_{1}]
= [figure: F A_{0}; F f_{1}; •; F α_{1}; F A_{1}; F f_{2}; •; F α_{2}; ···; F f_{n}; F α_{n}; F A_{n}; •; F B_{φ(0)}; F (g_{φ(1)}^{φ(0)}); φ_{g_{φ(1)},··· ,g_{1}}; F B_{φ(1)}; F (g_{φ(2)}^{φ(1)}); ···; F B_{φ(n)}; F B_{0}; F B_{1}; F B_{φ(1)}; F B_{m}]

= (φ_{g_{m},··· ,g_{φ(n−1)+1}} · F α_{n})(φ_{g_{φ(n−1)}···g_{φ(n−2)+1}} · F α_{n−1}) ⋯ (φ_{g_{φ(1)}···g_{1}} · F α_{1}),

and

[figure: F A; φ_{A}; G(λ) =; F A; F 1_{A}; •; F (λ); F A; •; F B_{0}; F (g_{m}^{0}); φ_{gm,...,g_{1}}; F B_{m}; F B_{0}; F g_{1}; F B_{1}; F g_{2}; F g_{m}; F B_{m} .]

We need to check that

G(λ · [α_{n}, …, α_{1}]) = G(λ) · G([α_{n}, …, α_{1}]),  (7)
G([α_{n}, …, α_{1}] · λ) = G([α_{n}, …, α_{1}]) · G(λ),  (8)

and

G(λ · μ) = G(λ) · G(μ).  (9)

To prove (7), note that in order for λ to be composable with [α_{n}, …, α_{1}], the vertical codomains of all the α_{i} are identity arrows, so

G(λ · [α_{n}, …, α_{1}]) = G([λ · α_{n}, 1 · α_{n−1}, …, 1 · α_{1}])
= (φ_{g_{m},...,g_{1}} · F (λ · α_{n}))F α_{n−1} ⋯ F α_{1}
= (φ_{g_{m},...,g_{1}} · F (λ) · F (α_{n}))F (α_{n−1}) ⋯ F (α_{1})
= (φ_{g_{m},...,g_{1}} · F (λ)) · (F (α_{n})F (α_{n−1}) ⋯ F (α_{1}))
= G(λ) · G([α_{n}, …, α_{1}]).

To prove (8),

G([α_{n}, …, α_{1}] · λ)
= φ_{g_{m},...,g_{1}} · F (α_{n}^{0} · λ)
= φ_{g_{m},...,g_{1}} · F (α_{n}^{0}) · F (λ)
= ((φ_{g_{m},··· ,g_{φ(n−1)+1}} · F α_{n}) ⋯ (φ_{g_{φ(1)}···g_{1}} · F α_{1})) · (φ_{f_{n},··· ,f_{1}} · F (λ))
= G([α_{n}, …, α_{1}]) · G(λ).

Finally, (9) is straightforward, and left as an exercise for the reader.

This shows that composing with Ξ_{∗} is bijective on objects. To show that it is also bijective on morphisms, replace 𝔹 with 𝔹^{↓^{•}}, as defined in the next paragraph, and then invoke Proposition 3.11 below.

Let ↓^{}represent the double category with two objects and only one non-identity arrow, a vertical arrow. So for any double category 𝔻, there is a bijection between double functors ↓^{}→ 𝔻 and vertical arrows of 𝔻. Now Doub, being categories in Cat, is cartesian closed and we have the vertical arrow double category 𝔹^{↓^{•}} of 𝔹, for which double functors

𝔸 → 𝔹^{↓^{•}}

are in bijective correspondence with vertical transformations

\xymatrix{𝔸 \ar[r]|{⇓} \ar[r] & 𝔹} .

Explicitly, the objects of 𝔹^{↓^{•}} are vertical arrows of 𝔹, its horizontal arrows are cells

[figure: B_{0}; •; w; b_{0}; β; B′_{0}; •; w′; B_{1}; b_{1}; B′_{1}; ,]

its vertical arrows are commutative squares

\xymatrix{B_{0} \ar[d]|{•} \ar[r]|{•} & B_{2} \ar[d]|{•} \\ B_{1} \ar[r]|{•} & B_{3} & ,}

and its cells are commutative cubes

[figure: B_{0}; •; •; B′_{0}; •; •; B_{2}; •; B′_{2}; •; B_{1}; •; B′_{1}; •; B_{3}; B′_{3}; ,]

or in plane language,

[figure: B_{0}; •; w_{1}; β_{1}; B′_{0}; •; w′_{1}; B_{0}; •; w_{2}; β_{2}; B′_{0}; •; w′_{2}; B_{1}; •; _{\overline{w}_{1}}; _{\overline{β}_{1}}; B′_{1}; =; •; _{\overline{w}′1}; B_{2}; •; _{\overline{w}_{2}}; _{\overline{β}_{2}}; B′_{2}; •; _{\overline{w}′2}; B_{3}; B′_{3}; B_{3}; B′_{3}; .]

3.11. Proposition. There are double functors D_{0}, D_{1} : 𝔹^{↓^{•}} → 𝔹 and a vertical transformation \xymatrix{v: D_{0} \ar[r]|{•} & D_{1}} which establish a bijection between oplax morphisms 𝔸 → 𝔹^{↓^{•}} and pairs of oplax morphisms 𝔸 → 𝔹 with a vertical transformation between them. This bijection respects normality.

Proof. Straightforward calculation.

3.12. The Comonad ℙath_{∗}. The isomorphism of categories given in Theorem 3.10 shows that ℙath_{∗} is a left 2-adjoint to the inclusion Doub ↪ Doub_{OplN} so in fact ℙath_{∗} is a 2-comonad in Doub. The following proposition is obvious, but nevertheless illuminates the nature of oplax normal morphisms.

3.13. Proposition. Doub_{OplN} is the Kleisli 2-category for the comonad ℙath_{∗} on Doub.

We have the following analog of Theorem 1.21 for the normal case.

3.14. Theorem. The comonad ℙath_{∗} on Doub is oplax idempotent.

Proof. The proof is the same as that of Theorem 1.21 except for the addition of a few ∗s as subscripts.

In view of this theorem we should figure out what the 2-category of Eilenberg-Moore coalgebras is. These will be the oplax normal double categories, i.e., the natural objects on which oplax normal morphisms are defined. Because ℙath_{∗} is oplax idempotent, each double category will have at most one such structure, so being an Eilenberg-Moore coalgebra is again a property rather than extra structure: 𝔸 is a coalgebra if and only if Ξ_{∗}: 𝔸 → ℙath_{∗} 𝔸 has a left adjoint, which should probably be composition in some form. This description, although accurate, is somewhat misleading. The example of ℙath suggests identifying 𝔸 with an oplax double category of some sort, and this does indeed work.

The vertical dual of Definition 2.7 gives us the notion of an n-fold composite being strongly representable in an oplax double category. For n = 0 we talk about an identity being strongly representable.

3.15. Definition. Let 𝔸 be an oplax double category and A an object of 𝔸. The identity on A is strongly representable if there is an arrow 1_{A}: A → A and a cell

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

with the following universal property. For any cell

[figure: A_{0}; •; α; A_{1}; A_{n}; •; B_{0}; B_{1}; B_{m−1}; A; C_{1}; C_{p}]

there exists a unique cell \overline{α}, as indicated below, such that

[figure: A_{0}; •; \overline{α}; A_{1}; A_{n}; •; B_{0}; id; B_{1}; B_{m−1}; id; A; 1_{A}; ι_{A}; A; id; C_{1}; id; C_{p}; B_{0}; B_{1}; B_{m−1}; A; C_{1}; C_{p}]

is equal to α. We say that 𝔸 is oplax normal if all identities are strongly representable. A morphism of oplax normal double categories is a morphism of oplax double categories which preserves the universal cells

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

Actually, as with all definitions involving representability, the arrows of the form 1_{A} are only determined up to vertical isomorphism. If 𝔸 is oplax normal we pick a universal cell

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

for each object A in 𝔸. Then preservation of universal cells says that the unique cell \overline{F ι}_{A} such that

[figure: F A; F 1_{A}; _{\overline{F ι}_{A}}; F A; F A; F 1_{A}; F ι_{A}; F A; F A; 1_{F A}; ι_{F A}; F A; =; F A; F A]

is a vertical isomorphism. (This is analogous to the preservation of limits in ordinary category theory.)

Let OplaxN be the locally full and faithful sub-2-category of Oplax, determined by the oplax normal double categories and morphisms of such (with arbitrary vertical transformations as 2-cells).

Recall from Section 2.10 the construction 𝕆plax which takes a double category 𝔸 and considers it as an oplax double category with the same objects, vertical and horizontal arrows, with multicells

[figure: A; •; f; α; A′; •; B_{0}; g_{1}; B_{1}; g_{2}; g_{m}; B_{m}]

given by double cells

[figure: A; f; •; α; A′; •; B_{0}; g_{m}^{0}; B_{2}]

in 𝔸.

3.16. Proposition. Let 𝔸 and 𝔹 be double categories, then 𝕆plax 𝔸 and 𝕆plax 𝔹 are normal and a morphism of oplax normal double categories 𝕆plax 𝔸 → 𝕆plax 𝔹 is the same as a normal oplax morphism 𝔸 → 𝔹. In fact, 𝕆plax is a fully faithful and locally fully faithful 2-functor Doub_{OplN} → OplaxN.

We denote by 𝕆plax_{∗}: Doub → OplaxN the 2-functor 𝕆plax whose codomain has been restricted to OplaxN. We shall show that ℙath_{∗} gives a left 2-adjoint to this inclusion. That is, ℙath_{∗}𝔸 is the free double category generated by an oplax normal 𝔸. We first must extend ℙath_{∗} to OplaxN.

3.17. The Extension of ℙath_{∗}. The construction follows closely that of ℙath_{∗} for actual double categories. First we need some definitions. Let 𝔸 be an arbitrary oplax normal double category.

3.18. Definition. Given a path [figure: A_{0}; f_{1}; A_{1}; f_{2}; f_{n}; A_{n}] in 𝔸 and 0 ⩽ i ⩽ j ⩽

n, we let f_{j}^{i} denote the path [figure: A_{i}; f_{i+1}; A_{i+1}; f_{i+2}; f_{j}; A_{j}] (if i = j this is of course the empty path). We also extend this notation to cells: given a fence in ℙath 𝔸,

[figure: A_{0}; •; v_{0}; α_{1}; A_{1}; •; v_{1}; α_{n}; A_{n}; •; v_{n}; B_{0}; B_{1}; B_{m},]

α_{j}^{i} denotes the formal composite α_{j}α_{j−1} ⋯ α_{i+1}.

If 𝔸 is an actual double category, then the definitions of f_{j}^{i} and α_{j}^{i} are inconsistent in the sense that id_{f_{j}^{i}} is not the same thing as ⟨id_{f}⟩_{i}^{j}. However, there will be no confusion if we keep the distinction between 𝕆plax 𝔸 and 𝔸 clear.

The definition of ℙath_{∗} uses composition of general cells with scalars (cells whose vertical domain is an identity), both in the definition of the equivalence relation on fences and that of horizontal composition.

3.19. Definition. Consider cells

[figure: A; 1_{A}; •; λ; A; •; f; α; A′; •; μ; 1_{A′}; A′; •; X_{0}; x_{1}; X_{1}; x_{2}; x_{q}; B_{0}; g_{1}; B_{1}; g_{2}; g_{m}; B_{m}; y_{1}; Y_{1}; y_{2}; y_{p}; Y_{p}]

in 𝔸. The cells αλ and μα are defined to be the composites

[figure: A; f; _{\overline{id}_{f}}; A′; A; •; 1_{A}; λ; A; •; f; α; A′; •; X_{0}; X_{1}; B_{0}; B_{1}; B_{m}]

and

[figure: A; f; _{\overline{id}_{f}}; A′; A; f; α; •; A′; 1_{A′}; •; μ; A′; •; B_{0}; B_{1}; B_{m}; Y_{1}; Y_{p}]

respectively. (Note that the cells \overline{id}_{f} are different in these two composites, but this will cause no problem.)

These horizontal composites obey all the associativity and unitary laws that make sense. They are best understood in the following more general context which will be of use later. (Recall the definition of strong representability for composable paths of arrows from Definition 2.7.)

3.20. Proposition. Let \xymatrix{A \ar[r]^{f} & B \ar[r]^{g} & C \ar[r]^{h} & D} be arrows of 𝔸.

1. If gf is strongly representable, then h(gf) is strongly representable if and only if hgf is. Moreover, in this case there is a canonical isomorphism h(gf) ≅ hgf.

2. If 1_{A} is strongly representable, then so is f1_{A} and f1_{A} ≅ f.

3. If 1_{B} is strongly representable then so is 1_{B}f and 1_{B}f ≅ f.

Proof. Straightforward.

3.21. Corollary. If gf and hg are strongly representable, then h(gf) is strongly representable if and only if (hg)f is. Moreover, in this case we have h(gf) ≅ (hg)f.

Once the composite of certain horizontal arrows is strongly representable, the horizontal composite of cells with these as vertical domains is automatically defined and indeed satisfies all reasonable associativity and unitary properties.

3.22. Definition. Suppose gf is strongly representable and consider cells The horizontal composite βα is defined to be ⟨β, α⟩ · ι_{g,f}

[figure: A; •; α; f; B; •; β; g; C; •; X_{0}; X_{1}; X_{n}; X_{n+1}; X_{m}.]

[figure: A; ι_{g,f}; gf; C; A; •; α; f; B; •; β; g; C; •; X_{0}; X_{n}; X_{m}.]

3.23. Proposition. Let α, β, γ be cells with vertical domains f, g, h, respectively and assume that gf, hg, h(gf) and (hg)f are strongly representable. Then γ(βα) = (γβ)α (by which we mean that (γβ)α composed with the canonical isomorphism h(gf) ≅ (hg)f is γ(βα).)

Proof. This follows immediately from the definition of horizontal composition and the canonical isomorphism.

3.24. Corollary. Let α be an arbitrary cell and λ and μ scalars with the appropriate identities as vertical domains. Then:

1. The three possible meanings of μλ agree;

2. (μα)λ = μ(αλ);

3. (αμ)λ = α(μλ);

4. μ(λα) = (μλ)α.

Proof. The only thing to check is part 1. The other results follow from the previous proposition. The three meanings referred to are the following. The universal property of 1_{A} gives cells ρ and σ such that

[figure: A; ρ; 1_{A}; A; A; 1_{A}; σ; A; A; 1_{A}; ι_{A}; A; 1_{A}; _{id_{1_{A}}}; A; and; A; 1_{A}; A; _{id_{1_{A}}}; 1_{A}; ι_{A}; A; A; 1_{A}; A; A; 1_{A}; A]

are both equal to id_{1_{A}}, and representability of the composite gives

[figure: A; 1_{A}; ι_{1_{A},1_{A}}; A; A; 1_{A}; A; 1_{A}; A.]

So μλ could alternately be defined as ⟨μ, λ⟩ · ρ, ⟨μ, λ⟩ · σ or ⟨μ, λ⟩ · ι_{1_{A},1_{A}}. In fact, showing that 1_{A}1_{A} is representable requires us to construct ι_{1_{A},1_{A}} and depending on whether we invoke property 2 or 3 of Proposition 3.20, it is taken to be ⟨μ, λ⟩·ρ or ⟨μ, λ⟩·σ respectively. So we must show that these last two cells are the same and indeed they are. In fact, the composite

[figure: A; ρ; 1_{A}; A; A; 1_{A}; ι_{A}; A; 1_{A}; _{id_{1_{A}}}; A; A; 1_{A}; ι_{A}; A; A]

is equal, by associativity and the unit law, to

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

which is by the same token equal to

[figure: A; ρ; 1_{A}; A; A; 1_{A}; A; _{id_{1_{A}}}; 1_{A}; ι_{A}; A; A; 1_{A}; ι_{A}; A; A; .]

We can cancel ι off the bottom and thus see that ρ satisfies the same property as σ.

With these technicalities out of the way, we can now define the equivalence relation ∼ on the fences of the oplax normal double category 𝔸 as in Proposition 3.7 and note that it is still a congruence of double categories on ℙath 𝔸. The construction of ℙath_{∗}𝔸 is exactly the same as in Section 3.8 and it again forms a strict double category (Proposition 3.9). Ξ_{∗} is defined as before which is now understood as a morphism of oplax normal double categories

Ξ_{∗}: 𝔸 → 𝕆plax_{∗}ℙath_{∗}𝔸.

It is still vertically full and faithful in the obvious sense for oplax double categories. We now have the extension (to its natural domain) of Theorem 3.10.

3.25. Theorem. Let 𝔸 be an oplax normal double category. Then

Ξ_{∗}: 𝔸 → 𝕆plax_{∗}ℙath_{∗}𝔸

is the universal oplax normal morphism, i.e., for any strict double category 𝔹, composition with Ξ_{∗} induces an isomorphism of categories

\xymatrix{Doub(ℙath_{∗}𝔸, 𝔹) \ar[r]^{≅} & OplaxN(𝔸, 𝕆plax_{∗}𝔹).}

Proof. The proof of Theorem 3.10 was written in such a way as to go through, mutatis mutandis.

This theorem shows that ℙath_{∗} is a left 2-adjoint to the ‘inclusion’

𝕆plax_{∗}: Doub → OplaxN

and consequently extends in a unique way to a 2-functor. The 2-comonad ℙath_{∗} induced on Doub is of course the same ℙath_{∗} introduced at the beginning of Section 3.12.

3.26. Eilenberg-Moore Algebras for ℙath_{∗}. We are now in the position to describe the Eilenberg-Moore algebras for the comonad ℙath_{∗} on Doub.

3.27. Theorem. ℙath_{∗}: OplaxN → Doub is comonadic.

Proof. ℙath_{∗} has a right 2-adjoint 𝕆plax_{∗} and the induced comonad is what we simply called ℙath_{∗} in Section 3.8.

Let 𝔸 be a double category and F: 𝔸 → ℙath_{∗}𝔸 a coalgebra structure. The unit law

\xymatrix{𝔸 \ar[r]^{F} \ar[dr]_{1_{𝔸}} & ℙath_{∗}𝔸 \ar[d]^{E} \\  & 𝔸}

tells us that F is the identity on objects and vertical arrows and that it assigns to each horizontal arrow f a factorisation of it, f = f_{n}f_{n−1} ⋯ f_{1}. As in the case of ℙath (and Path) this makes the horizontal arrows of 𝔸 into a free category generated by the arrows of degree 1 (i.e., whose assigned factorisation has only one factor). F also assigns to each cell α a factorisation of it, α = α_{n} ⋯ α_{1}, although this time not a unique one, but in fact an equivalence class of factorisations. Also, the length of this factorisation is not uniquely determined, because it may contain scalars (i.e., cells whose vertical domain has degree 0). However, the equivalence relation is such that scalars can be absorbed into any adjacent nonscalar, so each equivalence class contains a representative factorisation containing no scalars, though not a canonical one (provided of course that the cell itself is not a pure scalar). Call a factorisation of α reduced if it is either scalar or contains no scalars. Then F provides a reduced factorisation α = α_{n} ⋯ α_{1} for each α and the length n is uniquely determined, namely the length of the factorisation of its vertical domain.

We construct an oplax normal double category 𝔸_{0} as follows. It is the suboplax double category of 𝕆plax_{∗}𝔸 with the same objects and vertical arrows and whose horizontal arrows and cells are those of degree ⩽ 1. It is clear that 𝔸_{0} is a suboplax double category, since the degree of the cells is the degree of the top cell. It is also clearly normal, since the degree of the canonical cell ι_{A} has degree 1 and the cells whose existence is required for the universal property of ι_{A} are the same as the test cells.

The inclusion 𝔸_{0} ⊆ 𝕆plax_{∗}𝔸 corresponds to a double functor ℙath_{∗}𝔸_{0} → 𝔸 which is nothing but horizontal composition of arrows and cells. We claim that it is an isomorphism of double categories. We have already argued that it is one-to-one and onto on objects and both kinds of arrows, and that it is onto on cells. Suppose that we have two reduced paths of cells ⟨α_{n}, …, α_{1}⟩ and ⟨β_{n}, …, β_{1}⟩ whose composites are equal in 𝔸, α_{n} ⋯ α_{1} = β_{n} ⋯ β_{1}. Then F (α_{n} ⋯ α_{1}) = F (α_{n}) ⋯ F (α_{1}) = [α_{n}, …, α_{1}] as F is a double functor and F (α_{i}) = [α_{i}]. Similarly, F (β_{n} ⋯ β_{1}) = [β_{n}, …, β_{1}], so [α_{n}, …, α_{1}] = [β_{n}, …, β_{1}] and we see that ℙath_{∗}𝔸_{0} → 𝔸 is one-to-one on cells. This shows that every coalgebra is of the form ℙath_{∗}𝔸_{0} for a unique oplax normal double category 𝔸_{0}.

If G: 𝔹 → ℙath_{∗}𝔹 is another coalgebra structure, a morphism of coalgebras is a double functor H such that

\xymatrix{𝔸 \ar[d]_{H} \ar[r]^{F} & ℙath_{∗}𝔸 \ar[d]^{ℙath_{∗}H} \\ 𝔹 \ar[r]_{G} & ℙath_{∗}𝔸}

commutes. As such it preserves the degree of horizontal arrows and cells so it restricts to a morphism of oplax double categories, H_{0} : 𝔸_{0} → 𝔹_{0}, which is normal as H preserves all identities.

Finally, vertical transformations between coalgebra homomorphisms

\xymatrix{H \ar[r]|{•} & K}

are exactly the same as vertical transformations

\xymatrix{H_{0} \ar[r]|{•} & K_{0}} .

This shows that the 2-category Doub_{ℙath_{∗}} of coalgebras on the comonad ℙath_{∗} is equivalent to the 2-category OplaxN, thus concluding the proof.

The preceding theorem shows that oplax normal double categories are the correct objects for studying oplax normal double functors. In the sequel to this paper [DPP4] we will introduce a more restricted class of oplax double categories, the paranormal ones and make an argument for their study.

Acknowledgements. We wish to thank the referee for a thorough and prompt review of this manuscript.

References

[Ba] M. Barr, Coalgebras in a category of algebras, in Category Theory, Homology and their applications, Springer LNM 86 (1969), pp. 1–12.

[Bé] J. Bénabou, Introduction to bicategories, in Reports of the Midwest Category Theory Seminar, Springer, LNM 47 (1967), pp. 1–77.

[Bu] A. Burroni, T -catégories, Cahiers Top. Geom. Diff., Vol. XII (1971), No. 3, pp. 215-321.

[CR] A. Carboni, R. Rosebrugh, Lax monads. Indexed monoidal monads. J. Pure Appl. Algebra 76 (1991), pp. 13–32.

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

[CKS1] J. R. B. Cockett, J. Koslowski, R. A. G. Seely, Introduction to linear bicategories, in The Lambek Festschrift: mathematical structures in computer science (Montreal, QC, 1997). Math. Structures Comput. Sci. 10 (2000), no. 2, pp. 165–203.

[CKS2] J. R. B. Cockett, J. Koslowski, R. A. G. Seely, Morphisms and modules for poly-bicategories. Theory Appl. Categ. 11 (2003), No. 2, pp. 15–74.

[DP1] R. J. M. Dawson, R. Paré, What is a free double category like? J. Pure Appl. Algebra 168 (2002), no. 1, pp. 19–34.

[DP2] R. J. M. Dawson, R. Paré, General associativity and general composition for double categories, Cahiers Topologie Géom. Différentielle Catég. 34 (1993), no. 1, pp. 57–79.

[DPP1] R. J. M. Dawson, R. Paré, D. A. Pronk, Adjoining adjoints, Adv. in Math. 178 (2003), pp. 99–140.

[DPP2] R. J. M. Dawson, R. Paré, D. A. Pronk, Undecidability of the free adjoint construction, Applied Categorical Structures 11 (2003), pp. 403–419.

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

[DPP4] R. J. M. Dawson, R. Paré, D. A. Pronk, More general spans, in preparation.

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

[G] M. Grandis, Lax 2-categories and directed homotopy, Cah. Topol. Geom. Diff. Categ., to appear.

[GP] M. Grandis, R. Paré, Limits in double categories, Cahiers Topologie Géom. Différentielle Catég., Vol. XL-3 (1999), pp. 162–220.

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

[H2] C. Hermida, From coherent structures to universal properties, J. Pure Appl. Algebra 165 (2001), pp. 7–61.

[H3] C. Hermida, A categorical outlook on relational modalities and simulations, preprint.

[HMP] C. Hermida, M. Makkai, J. Power, On weak higher dimensional categories I: Part 1, in: Category theory and its applications (Montreal, QC, 1997), J. Pure Appl. Algebra 154 (2000), pp. 221–246.

[KLSS] G. M. Kelly, A. Labella, V. Schmitt, R. Street, Categories enriched on two sides, J. Pure Appl. Algebra 168 (2002), no. 1, pp. 53–98.

[KL] G. M. Kelly, S. Lack, On property-like structures, Theory Appl. Categ. 3 (1997), pp. 213–250.

[K] A. Kock, Monads for which structures are adjoint to units, J. Pure Appl. Algebra 104 (1993), pp. 41–50.

[Kos] J. Koslowski, A monadic approach to polycategories, Theory Appl. Categ. 14 (2005), pp. 125–156.

[Lac] S. Lack, A convenient 2-category of bicategories, Presentation at CT2006, www.mathstat.dal.ca/∼selinger/ct2006/slides/CT06-Lack.pdf

[Lam] J. Lambek, Deductive systems and categories II: standard constructions and closed categories, in: Category Theory, Homology Theory and their Applications I, ed. P. Hilton, Springer LNM 86 (1969).

[L1] T. Leinster, fc-multicategories, E-print math.CT/9903004 (1999).

[L2] T. Leinster, Higher Operads, Higher Categories, London Mathematical Society Lecture Note Series 298, Cambridge University Press, 2003.

[L3] T. Leinster, Generalized enrichment of categories, J. Pure Appl. Algebra 168 (2002), pp. 391–406.

[M] F. Marmolejo, Monads whose structure forms a fully faithful adjoint string, Theory Appl. Categ. 3 (1997), pp. 22–44.

[W] R. J. Wood, private communication [Z] V. Zöberlein, Doktrinen auf 2-Kategorien, PhD-thesis, University of Düsseldorf,

1974.

Department of Mathematics and Computing Science, Saint Mary’s University, Halifax, NS B3H 3C3, Canada

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

Email: rdawson@cs.saintmarys.ca
      pare@mathstat.dal.ca
      pronk@mathstat.dal.ca

This article may be accessed via WWW at http://www.tac.mta.ca/tac/ or by anony-

mous ftp at ftp://ftp.tac.mta.ca/pub/tac/html/volumes/16/18/16-18.{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. The method of distribution of the journal is via the Internet tools WWW/ftp. The journal is archived electronically and in printed paper format.

Subscription information. Individual subscribers receive (by e-mail) abstracts of articles as they are published. Full text of published articles is available in .dvi, Postscript and PDF. Details will be e-mailed to new subscribers. 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 is the preferred flavour. TEX source of articles for publication should be submitted by e-mail directly to an appropriate Editor. They are listed below. Please obtain detailed information on submission format and style files from the journal’s WWW server at http://www.tac.mta.ca/tac/. You may also write to tac@mta.ca to receive details by e-mail.

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

TEXnical editor. Michael Barr, McGill University: mbarr@barrs.org

Transmitting editors.

Richard Blute, Université d’ Ottawa: rblute@mathstat.uottawa.ca Lawrence Breen, Université de Paris 13: breen@math.univ-paris13.fr Ronald Brown, University of North Wales: r.brown@bangor.ac.uk Aurelio Carboni, Università dell Insubria: aurelio.carboni@uninsubria.it Valeria de Paiva, Xerox Palo Alto Research Center: paiva@parc.xerox.com

Ezra Getzler, Northwestern University: getzler(at)math(dot)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 G. Max Kelly, University of Sydney: maxk@maths.usyd.edu.au Anders Kock, University of Aarhus: kock@imf.au.dk Stephen Lack, University of Western Sydney: s.lack@uws.edu.au F. William Lawvere, State University of New York at Buffalo: wlawvere@acsu.buffalo.edu 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 Brooke Shipley, University of Illinois at Chicago: bshipley@math.uic.edu James Stasheff, University of North Carolina: jds@math.unc.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