Theory and Applications of Categories, Vol. 28, No. 1, 2013, pp. 1–23.

THE MONOIDAL STRUCTURE OF STRICTIFICATION

NICK GURSKI

Abstract. We study the monoidal structure of the standard strictification functor st : Bicat → 2Cat. In doing so, we construct monoidal structures on the 2-category whose objects are bicategories and on the 2-category whose objects are 2-categories.

Introduction

The study of coherence in higher category theory is the study of the relationship between strict structures and their weak variants. A strict structure is one which imposes many axioms, while a weak structure is one in which axioms are replaced by coherent isomorphisms whenever possible. The classic example of a coherence theorem is Mac Lane’s result [17] that every monoidal category is equivalent to a strict monoidal category. Here, the notion of a strict monoidal category includes the requirement that (x ⊗ y) ⊗ z = x ⊗ (y ⊗ z), while for a general monoidal category we only insist on there being a natural isomorphism between these two composite tensors (satisfying certain other axioms). Thus Mac Lane’s theorem states that when considering monoidal structures, there is no essential difference between the strict sort and the more general sort having isomorphisms in place of the usual monoid axioms.

Moving more firmly into the realm of higher category theory, the coherence theorem for monoidal categories can be modified to become a coherence theorem for bicategories. This theorem (see [18]) states that every bicategory is biequivalent to a strict 2-category. Once again, this particular coherence theorem shows how every “weakly defined” structure of a particular sort is essentially the same as a “strictly defined” version of the same sort of structure. Additionally, these theorems can be extended to functors as well, proving that every weak functor between bicategories can be replaced, up to biequivalence, by a strict 2-functor between 2-categories.

In fact, this kind of pattern has been studied intensely by 2-category theorists. One begins with a 2-monad T on a 2-category K; this is the appropriate notion of a kind of algebraic structure (given by T) on objects of the 2-category K. Then there are different notions of algebra for T, using the 2-dimensional nature of K in different ways. Thus one can study lax T -algebras, pseudo-T -algebras, and strict T -algebras, as well as various kinds of algebra maps between them. Within this context, there are two kinds of coherence theorems. First, one might show that the inclusion of stricter algebras or maps into weaker ones has a left adjoint. Such a theorem shows that there is a classifier for weak maps, and can be interpreted as a kind of coherence theorem for morphisms. Second, one might show that the adjunction has a unit with components which are equivalences, giving a method for turning weak algebras into strict ones up to equivalence. This abstract setting captures the most important aspects of the example of monoidal categories. The reader interested in pursuing this further should read [1, 14].

Received by the editors 2012-10-12 and, in revised form, 2013-01-17.

Transmitted by Giuseppe Rosolini. Published on 2013-01-24.

2010 Mathematics Subject Classification: Primary 18D05, 18D10.

Key words and phrases: Gray tensor product, strictification.

\begin{matrix}c \\ ◯ \end{matrix} Nick Gurski, 2013. Permission to copy for private use granted.

Moving up to the study of various kinds of 3-categories, the situation becomes much more interesting. The coherence theorem for tricategories states that every tricategory is triequivalent to a Gray-category, but that there are tricategories which are not triequivalent to strict 3-categories. Strict 3-categories are exactly what the name implies, a fully strict version of a three-dimensional category with associativity and unit axioms imposed directly at each dimension. A tricategory is, in contrast, a fully weak version of a 3category, introduced first by Gordon, Power, and Street in [7] and then modified slightly by the author in [9]. A Gray-category is an intermediate notion, and is sometimes referred to as a semi-strict notion of 3-category because while it retains many of the axioms that hold in a 3-category it does have one notable exception: the interchange law for 2-cells only holds up to a coherence isomorphism, which then itself satisfies some axioms reminiscent of the braid relations. Gray-categories can be defined using enriched category theory through the introduction of the Gray tensor product, and it is the relationship between strictification of bicategories and the Gray tensor product that is the focus of this paper.

The particular interest in showing that strictification is monoidal arises from the proof of coherence for tricategories. One version of coherence for bicategories can be proved in a single step by constructing the Yoneda embedding B ↪ [B^{op}, Cat]. By general results, the target bicategory for this functor is actually a 2-category since Cat is a 2-category, so the Yoneda lemma for bicategories embeds a bicategory within a strict 2-category; taking the essential image shows that every bicategory is biequivalent to a strict 2-category. The same strategy will not work without modification in dimension three. Here, we would get a Yoneda embedding T ↪ [T^{op}, Bicat], but since Bicat is not very strict as a tricategory, the target of this embedding will also not be as strict as desired. Instead, one replaces a general tricategory T with what is called a cubical tricategory \overline{T}, and then it is possible to embed any cubical tricategory in a Gray-category. The original construction of this embedding in [7] uses the Gray-category of pre-representations, while the author’s proof in [9, 11] once again uses a Yoneda lemma for cubical tricategories.

For the purposes of this paper, the crucial step in this proof is the construction of a cubical tricategory \overline{T} which is triequivalent to the original tricategory T. Now a cubical tricategory is one in which the hom-bicategories are actually 2-categories, and in which the functors giving composition and units are cubical. In order to strictify the hombicategories, one applies the strictification functor st : Bicat → 2Cat. This strictification functor, constructed using the coherence theorems for bicategories and functors, has the property that it comes with a comparison map

stX × stY → st(X × Y).

The insight in [7] is that this comparison functor is cubical, and so the cubical tricategory \overline{T} can be constructed by applying st to the hom-bicategories of T and then using this comparison functor to define composition.

Studying the monoidal structure on this functor was the impetus for this paper. There are errors in both [7] and [9] claiming that the comparison functor given above equips the functor st with a lax monoidal structure. This is in fact false, as the maps above are not natural in the usual sense. They are natural up to an invertible icon, which is a kind of 2-cell that shows up in various constructions involving bicategories and 2-categories (see [15, 16]). Thus the goal of this paper is to construct relevant monoidal structures on the 2-categories of bicategories, functors, and icons on the one hand and 2-categories, 2-functors, and icons on the other hand such that strictification has a monoidal structure. This is achieved in Theorem 5.7.

One of the major goals of “low-dimensional” category theory is a good monoidal structure on the category of Gray-categories, as an example see [4] for an attempt to construct such a monoidal structure directly. The results in this paper suggest that an alternate approach to this problem consists of studying the monoidal structure on the strictification process for tricategories. This will necessarily have to take place in a higher dimensional context as strictification for tricategories will not be a monoidal functor between monoidal categories just as the functor st is not, but it will also likely not be a monoidal functor between monoidal tetracategories, once again just as st is monoidal on the level of 2-categories. The results in this paper suggest that one avenue of approach would be to start with the low-dimensional structures constructed in [6], and then to study the monoidal structure on the strictification T ↦ GrT of [9, 11].

This paper will proceed as follows. The first section contains a review of the Gray tensor product of 2-categories, but omits most of the proofs. The interested reader should consult the original work of Gray [8], the monograph of Gordon, Power, Street [7], or the author’s forthcoming book [11]. The second section reviews some basic notions from the theory of monoidal bicategories, as well as giving some terminology for a stricter variant (strongly monoidal 2-categories) that will appear naturally. The third section begins with the definition of an icon, and then goes on to prove that icons appear naturally as the 2-cells in both a strongly monoidal 2-category of bicategories and a strongly monoidal 2-category of 2-categories. The fourth section studies the structure of strictification as a 2-functor, and the final section is devoted to providing this functor with a monoidal structure. This can be done in a straightforward, calculational fashion, but we have chosen to prove that strictification is a monoidal functor on the level of 2-categories using the theory of doctrinal adjunction [13].

The author would like to thank Steve Lack, John Power, and Ross Street for conversations and correspondence which have contributed to the research in this paper, as well as the referees for comments which have helped shape the final form of this paper.

1. The Gray tensor product

The Gray tensor product gives a monoidal structure on the category of 2-categories and 2functors which differs from the usual Cartesian structure. Here we give a quick overview of the generators-and-relations definition of the Gray tensor product of a pair of 2-categories, A ⊗ B; we do not give details, and refer the reader to [7, 8, 11] for more information.

1.1. Notation. We will denote horizontal composition of any kind in a 2-category by ∗ when such a symbol is necessary, and vertical composition of 2-cells by concatenation.

Let A, B be 2-categories. Then A ⊗ B is the 2-category with

• objects a ⊗ b where a ∈ A, b ∈ B;

• 1-cells generated by

\begin{matrix}f ⊗ 1 : a ⊗ b → a′ ⊗ b, & f : a → a′ in A, b ∈ B, \\ 1 ⊗ g : a ⊗ b → a ⊗ b′, & a ∈ A, g : b → b′ in B, \end{matrix}

subject to the relations

\begin{aligned}(f ⊗ 1) ∗ (f′ ⊗ 1) & = & (f ∗ f′) ⊗ 1, \\ (1 ⊗ g) ∗ (1 ⊗ g′) & = & 1 ⊗ (g ∗ g′), \end{aligned}

where the composite on the lefthand side is taken in A ⊗ B while the composite on the righthand side is in A or B, respectively;

• 2-cells generated by

α ⊗ 1 : f ⊗ 1 ⇒ f′ ⊗ 1,
1 ⊗ β : 1 ⊗ g ⇒ 1 ⊗ g′,
Σ_{f,g} : (f ⊗ 1) ∗ (1 ⊗ g) ⇒ (1 ⊗ g) ∗ (f ⊗ 1),

where α is a 2-cell in A and β is a 2-cell in B.

These 2-cells are subject to further relations. Some of these relations require that the function A → A ⊗ B sending δ to δ ⊗ b is a 2-functor for every b ∈ B, and analogously if the A-variable is fixed. There are also naturality axioms for the 2-cells Σ_{f,g}, together with some braid-like axioms governing composites of different Σ’s.

The Gray tensor product serves a variety of functions, one of those functions being to classify cubical functors as defined below.

1.2. Definition. A functor F : A_{1}×A_{2}×⋯ A_{n} → B is cubical if the following condition holds: if (f_{1}, f_{2}, …, f_{n}) ∗ (g_{1}, g_{2}, …, g_{n}) is a composable pair of morphisms in the 2-category A_{1} × A_{2} × ⋯ A_{n} such that for all i > j, either g_{i} or f_{j} is an identity map, then the comparison 2-cell

ϕ : F (f_{1}, f_{2}, …, f_{n}) ∗ F (g_{1}, g_{2}, …, g_{n}) ⇒ F ((f_{1}, f_{2}, …, f_{n}) ∗ (g_{1}, g_{2}, …, g_{n}))

is an identity.

1.3. Remark. This definition is equivalent to the condition that, for any 1 ≤ j ≤ n, the comparison 2-cell

(1, 1, …, 1, f_{j}, f_{j+1}, …, f_{n}) ∗ F (g_{1}, …, g_{j}, 1, …, 1) ⇒ F (g_{1}, …, g_{j−1}, f_{j}g_{j}, f_{j+1}, …, f_{n})

is the identity 2-cell.

1.4. Remark. 1. Every cubical functor strictly preserves identity 1-cells.

2. A cubical functor of one variable is necessarily a 2-functor.

The relationship between the Gray tensor product and cubical functors is described by the theorem below. Before stating it, we require a definition.

1.5. Definition. Let A_{1}, …, A_{n}, B be 2-categories. Then 2Cat_{c}(A_{1}, …, A_{n}; B) is the set of cubical functors A_{1} × ⋯ × A_{n} → B.

1.6. Theorem. Let A, B, and C be 2-categories. There is a cubical functor

c : A × B → A ⊗ B,

natural in A and B, such that composition with c induces an isomorphism

2Cat_{c}(A, B; C) ≅ 2Cat(A ⊗ B, C).

Proof (Sketch). The functor c is defined by sending (a, b) to a ⊗ b, (f, 1) to f ⊗ 1, (1, g) to 1 ⊗ g, and similarly for 2-cells. We force this functor to be cubical, and then it is easy to check the isomorphism in the theorem.

We will need the following lemma later.

1.7. Lemma. The universal cubical functor c : A × B → A ⊗ B is a bijective-on-objects biequivalence.

Proof (Sketch). First, the explicit construction of c makes it obvious that it is bijectiveon-objects. Since every strict functor is cubical, we use the universal property of c to produce a unique 2-functor π making the diagram below commute.

All that remains is to show that cπ is equivalent to 1_{A⊗B}, a calculation we leave for the reader.

[figure: A × B; A ⊗ B; c; A ⊗ B; A × B; π; A × B; A × B; 1]

6  NICK GURSKI

2. Monoidal bicategories

We begin by reminding the reader of the definitions of monoidal bicategory and monoidal functor, and then go on to state a stricter, Cat-enriched version of these definitions that will play a role later. Because the monoidal structures we will construct are actually monoidal category structures extended to take into account the 2-cells, these stricter kinds of monoidal bicategories will arise naturally. 2.1. Definition. A monoidal bicategory is a one-object tricategory in the fully algebraic sense of [9]. Thus a monoidal bicategory consists of

• a bicategory B;

• a functor ⊗ : B × B → B;

• a functor I : 1 → B;

• adjoint equivalence a, l, and r as in the definition of a tricategory; and

• invertible modifications π, μ, λ, and ρ as in the definition of a tricategory all subject to the tricategory axioms. 2.2. Definition. A monoidal functor between monoidal bicategories is a functor between the one-object tricategories. Such a monoidal functor consists of

• a functor of the underlying bicategories F : B_{1} → B_{2};

• adjoint equivalences χ and ι as in the definition of weak functor between tricategories; and

• invertible modifications ω, δ, and γ as in the definition of weak functor all subject to axioms which are identical to the tricategory functor axioms aside from source and target considerations. 2.3. Definition. A lax monoidal functor between monoidal bicategories consists of

• a functor of the underlying bicategories F : B_{1} → B_{2};

• transformations χ and ι as in the definition of weak functor between tricategories; and

• invertible modifications ω, δ, and γ as in the definition of weak functor all subject to axioms which are identical to the tricategory functor axioms aside from source and target considerations.

2.4. Remark. Note that the difference in the two definitions above lies with χ, ι. In a monoidal functor, these are required to be part of adjoint equivalences χ ⊣_{eq} χ^{▪}, ι ⊣_{eq} ι^{▪}, while in a lax monoidal functor they are not. In particular, this implies that, for a lax monoidal functor, the components on objects

\begin{aligned}χ : & F x ⊗_{2} F y & → & F (x ⊗_{1} y), \\ ι : & I_{F x} & → & F I_{x} \end{aligned}

are not necessarily equivalences in B_{2}. The lax monoidal functors we use here are the same as the lax homomorphisms of [6].

2.5. Remark. For completeness, we should also define symmetric monoidal bicategories and the appropriate notion of monoidal functor between those, as the main theorem of this paper will be that a certain functor is a symmetric monoidal one. We omit these details and definitions here, as it is actually the monoidal aspects of this functor that are of primary interest, not the relationship with the symmetry. For readers interested in precise definitions, we refer to [5, 10, 19].

2.6. Definition. A strongly monoidal 2-category consists of

• a 2-category A,

• a 2-functor m : A × A → A,

• an object I of A,

• a 2-natural isomorphism μ,

[figure: A × A × A; A × A; m×1; A × A; A; m; A × A × A; A × A; 1×m; A × A; A; m; ⇓ μ]

• 2-natural isomorphisms λ, ρ,

such that the usual monoidal category axioms hold.

2.7. Remark. This definition is merely the Cat-enriched version of the definition of a monoidal category.

[figure: A × ∗; A × A; 1×I; A × A; A; m; A × ∗; A; ≅; ⇓ λ; ∗ × A; A × A; I×1; A × A; A; m; ∗ × A; A; ≅; ⇓ ρ]

2.8. Proposition. Every strongly monoidal 2-category has an underlying monoidal bicategory.

Proof. The underlying bicategory, tensor product, and unit are all the same as those in the strongly monoidal 2-category. The associativity adjoint equivalence is given by μ and μ^{−1} with unit and counit both being the identity; the analogous statements hold for the left and right unit adjoint equivalences. The remaining data (π, μ, λ, ρ in the notation of monoidal bicategories, not to be confused with the data above) can all be taken to be identities as they correspond to axioms or consequences of the axioms for strongly monoidal 2-categories.

2.9. Definition. Let A be a 2-category.

1. A product a × b of objects a, b ∈ A is an object a × b ∈ A together with 2-natural

isomorphisms

A(x, a × b) ≅ A(x, a) × A(x, b)

for all objects x ∈ A.

2. A terminal object of A is an object ∗ ∈ A together with 2-natural isomorphisms

A(x, ∗) ≅ 1

for all objects x ∈ A, where 1 denotes a terminal category.

2.10. Proposition. Let A be a 2-category with all binary products and a terminal object. Then a choice of product for every pair of objects and a choice of terminal object equip A with the structure of a strongly monoidal 2-category.

Proof. The proof here is identical to the proof that categories with chosen binary products and a chosen terminal object are monoidal.

2.11. Definition. A Cat-lax monoidal functor F : A_{1} → A_{2} between strongly monoidal 2-categories is a 2-functor F equipped with

• 1-cells

χ_{x,y} : F x ⊗_{2} F y → F (x ⊗_{1} y)

in A_{2} for every pair of objects x, y in A_{1}, which are 2-natural in x, y; and

• a 1-cell

ι : I_{2} → F I_{1}

in A_{2} where I_{j} denotes the unit object in A_{j}.

These are required to satisfy the usual axioms for a lax monoidal functor between monoidal categories.

2.12. Definition. A Cat-oplax monoidal functor F : A → B between strongly monoidal 2-categories is a 2-functor F equipped with

• 1-cells

χ_{x,y} : F (x ⊗_{1} y) → F x ⊗_{2} F y

in A_{2} for every pair of objects x, y in A_{1}, which are 2-natural in x, y; and

• a 1-cell

ι : F I_{1} → I_{2}

in A_{2} where I_{j} denotes the unit object in A_{j}.

These are required to satisfy the usual axioms for an oplax monoidal functor between monoidal categories.

2.13. Remark. Once again, these are merely the Cat-enriched versions of the definitions of lax monoidal functor and oplax monoidal functor. In particular, we can consider the free monoidal V-category 2-monad on the 2-category of V-categories, V-functors, and V-natural transformations for suitably nice V. When V = Cat, the algebras for this 2-monad are the strongly monoidal 2-categories, and the (op)lax algebra morphisms are the Cat-(op)lax monoidal functors. This observation will be useful when applying the theory of doctrinal adjunction.

2.14. Proposition. Let F : A_{1} → A_{2} be a Cat-lax monoidal functor between strongly monoidal 2-categories. Then F can be equipped with the structure of a lax monoidal functor between the underlying monoidal bicategories. Furthermore, if the components

\begin{aligned}χ_{x,y} : & F x ⊗_{2} F y & → & F (x ⊗_{1} y) \\ ι : & I_{2} & → & F I_{1} \end{aligned}

are all internal equivalences in A_{2}, then this lax monoidal functor is a monoidal functor.

Proof. The underlying monoidal functor between monoidal bicategories is just F, and the transformations χ, ι are those given in the Cat-lax structure. As in the proof of Proposition 2.8, the top-dimensional data (in the notation of monoidal functors between monoidal bicategories, ω, δ, γ) can all be taken to be identities. Since the only difference between a lax monoidal functor (in the sense used here) and a monoidal functor is the structure of χ, ι, the final claim follows from the observation that a pseudonatural transformation is part of an adjoint equivalence if and only if all the components are equivalences.

We give two results here related to the process of turning an Cat-oplax monoidal functor into a monoidal functor between monoidal bicategories. The first is related to doctrinal adjunction [13], and while we do not use the result directly, we will need the formula given in the proof below. The second will be used in the proof of the main result, Theorem 5.7.

2.15. Lemma. Let (A_{1}, ⊗_{1}), (A_{2}, ⊗_{2}) be strongly monoidal 2-categories, and let F ⊣ U be a 2-adjunction between them with F : A_{1} → A_{2}. Assume that the components of the unit and counit for this adjunction are all internal equivalences, and that U has been given a Cat-lax monoidal structure. Then if the components

φ_{xy} : Ux ⊗_{1} Uy → U(x ⊗_{2} y)

are all internal equivalences, so are the components

ψ_{xy} : F (x ⊗_{1} y) → F x ⊗_{2} F y

for the corresponding Cat-oplax monoidal structure for F. If the 1-cell

φ : I_{2} → UI_{1}

for the monoidal structure on U is an internal equivalence in A_{2}, then so is the 1-cell

ψ : F I_{2} → I_{1}

for the oplax structure on F.

Proof. The component ψ_{xy} : F (x ⊗_{1} y) → F x ⊗_{2} F y is given by the composite below:

F (x ⊗_{1} y) ⟶^{F (η⊗_{1}η)} F (UF x ⊗_{1} UF y) ⟶^{F φ_{F x,F y}} F U(F x ⊗_{2} F y) ⟶^{ε} F x ⊗_{2} F y.

If η is an equivalence, then so is η ⊗_{1} η. Since any 2-functor sends equivalences to equivalences, we get that each of the three 1-cells above is an equivalence, so their composite is as well. The proof for the unit is similar.

2.16. Lemma. Let (A_{1}, ⊗_{1}), (A_{2}, ⊗_{2}) be strongly monoidal 2-categories, and let F : A_{1} → A_{2} be an Cat-oplax monoidal functor between them. If the components

\begin{matrix}φ : F I_{1} → I_{2}, \\ φ_{xy} : F (x ⊗_{1} y) → F x ⊗_{2} F y \end{matrix}

are all internal equivalences in A_{2}, then their pseudo-inverses φ_{0}^{▪}, φ_{xy}^{▪} are part of the structure of a monoidal functor F : A_{1} → A_{2} on the underlying monoidal bicategories.

Proof. Equip the pseudo-inverse pairs (φ_{0}, φ_{0}^{▪}) and (φ_{xy}, φ_{xy}^{▪}) with the structure of adjoint equivalences φ ⊣_{eq} φ^{▪}. Using this structure, the 2-naturality of the φ_{xy} gives the φ_{xy}^{▪} the structure of a pseudonatural transformation ⊗_{2} ∘ (F × F) ⇒ F ∘ ⊗_{1}. The invertible 2-cells ω, δ, γ for the monoidal functor F are then the mates of the identity 2-cells for the three Cat-oplax monoidal functor axioms. We leave it to the reader to verify that the monoidal functor axioms are then a consequence of the triangle identities.

3. Icons

While for many purposes the default notion of 2-cell between functors of bicategories is that of pseudonatural transformation (or some variant), there is another equally natural notion of 2-cell called an icon. Icons are essentially the many-object version of monoidal transformations, and thus appear when studying degeneracy and monoidal structures for higher categories (see [2, 3]). Icons also appear naturally when viewing bicategories as the algebras for a 2-monad [15, 16]. Here the underlying 2-category is that of categoryenriched graphs, and the algebra 2-cells that the relevant 2-monad produces are precisely icons. This section will give a brief review of the basic definitions required, and then use icons as the 2-cells in the construction of two strongly monoidal 2-categories.

3.1. Definition. Let F, G : B → C be lax functors between bicategories with constraints φ_{0}, φ_{2} for F, and ψ_{0}, ψ_{2} for G. Assume that F and G agree on objects. An icon α : F ⇒ G consists of natural transformations

α_{ab} : F_{ab} ⇒ G_{ab} : B(a, b) → C(F a, F b)

(note here that we require F a = Ga, F b = Gb so that the functors F_{ab}, G_{ab} have a common target) such that the following diagrams commute. (Note that we suppress the 0-cell source and target subscripts for the transformations α_{ab} and instead only list the 1-cell for which a given 2-cell is the component.)

[figure: I_{F a}; F I_{a}; φ_{0}; F I_{a}; GI_{a}; α_{I}; I_{F a}; GI_{a}; ψ_{0}; F f ∗ F g; F (f ∗ g); φ_{2}; F (f ∗ g); G(f ∗ g); α_{f∗g}; F f ∗ F g; Gf ∗ Gg; α_{f} ∗α_{g}; Gf ∗ Gg; G(f ∗ g); ψ_{2}]

3.2. Definition. The 2-category Icon is defined to have objects bicategories, 1-cells functors, and 2-cells icons between them.

3.3. Remark. Note that this 2-category was called Hom in [16]. To actually prove these cells, with their obvious composition laws, give a 2-category is a relatively basic calculation that we leave to the reader.

The following lemma is an immediate consequence of the fact that the universal cubical functor c : A × B → A ⊗ B is a bijective-on-objects biequivalence, i.e., an internal equivalence in Icon.

3.4. Lemma. Let A, B, C be 2-categories, and let F, G : A × B → C be a pair of cubical functors that agree on objects. Then icons α : F ⇒ G are in natural bijection with icons α̃ : F̃ ⇒ G̃ between the 2-functors induced by the universal property.

We now have the following easy corollary of Proposition 2.10.

3.5. Corollary. The 2-category Icon of bicategories, functors, and icons can be given the structure of a strongly monoidal 2-category under products.

Proof. The usual product of bicategories and terminal bicategory are products and terminal in the sense of Definition 2.9.

3.6. Definition. The 2-category Gray_{icon} is defined to be the locally full sub-2-category of Icon consisting of 2-categories, 2-functors, and icons.

3.7. Proposition. The Gray tensor product equips Gray_{icon} with the structure of a strongly monoidal 2-category.

Proof. The multiplication in Gray_{icon} is to be the Gray tensor product, so we must equip it with the structure of a 2-functor

⊗ : Gray_{icon} × Gray_{icon} → Gray_{icon}.

It is clear that ⊗(A, B) = A ⊗ B and that ⊗(F, G) = F ⊗ G, but we must define it on icons as well. Let α : F ⇒ F′, β : G ⇒ G′ be icons. Then (F ⊗ G)(a, b) = (F a, Gb) = (F′a, G′b) = (F′ ⊗ G′)(a, b) so F ⊗ G and F′ ⊗ G′ agree on objects, hence we may define an icon between them. Since the 1-cells of A ⊗ B are generated by 1-cells of the form f ⊗1, 1⊗g, we will give the components of the icon α ⊗β at these 1-cells and then extend over composition. These components are defined as

\begin{aligned}(α ⊗ β)_{f⊗1} & = & α_{f} ⊗ 1 : F f ⊗ 1_{Gb} ⇒ F′f ⊗ 1_{Gb}, \\ (α ⊗ β)_{1⊗g} & = & 1 ⊗ β_{g} : 1_{F a} ⊗ Gg ⇒ 1_{F a} ⊗ G′g. \end{aligned}

In the case that we consider the 1-cell 1_{a} ⊗ 1_{b}, both of these definitions agree to give that

(α ⊗ β)_{1⊗1} = 1_{F a} ⊗ 1_{Gb} = 1_{(F a,Gb)}

by the icon axioms since F, G are both 2-functors; this also verifies the icon unit axiom for α ⊗ β. To extend this over composition, we must check that it respects the two relations on 1-cells in A ⊗ B:

\begin{aligned}(f ⊗ 1) ∗ (f′ ⊗ 1) & = & (f ∗ f′) ⊗ 1, \\ (1 ⊗ g) ∗ (1 ⊗ g′) & = & 1 ⊗ (g ∗ g′). \end{aligned}

This is easy to compute using the icon axioms, the axioms for the Gray tensor product, and the fact that F, G are strict 2-functors, as shown below for the first relation.

(α ⊗ β)_{f⊗1} ∗ (α ⊗ β)_{f′⊗1} = (α_{f} ⊗ 1) ∗ (α_{f′} ⊗ 1)
= (α_{f} ∗ α_{f′}) ⊗ 1
= α_{f∗f′} ⊗ 1
= (α ⊗ β)_{(f∗f′)⊗1}

Thus we can define the icon α ⊗ β as above on generating 1-cells, and extend it to an icon by setting (α ⊗ β)_{f∗g} = (α ⊗ β)_{f} ∗ (α ⊗ β)_{g} for composite 1-cells. This completes the definition of the functor ⊗ on cells.

Next we must show that ⊗ is a 2-functor. Now (F ⊗G)∗(F′ ⊗G′) = (F ∗F′)⊗(G∗G′) and 1_{A} ⊗ 1_{B} = 1_{A⊗B}, so ⊗ strictly preserves composition and units at the level of 1-cells. The equality

(α_{f} ⊗ 1) ∗ (α′_{f} ⊗ 1) = (α_{f} ∗ α′_{f}) ⊗ 1

also shows that (α ⊗ β) ∗ (α′ ⊗ β′) and (α ∗ α′) ⊗ (β ∗ β′) have the same component at f ⊗ 1; a similar calculation shows that these icons also have the same component at 1 ⊗ g. Since they have the same component for every generating 1-cell, this shows that

(α ⊗ β) ∗ (α′ ⊗ β′) = (α ∗ α′) ⊗ (β ∗ β′).

It is immediately clear that the Gray tensor product of two identity icons is the identity, proving that ⊗ is a 2-functor.

Finally, we must show that the associativity and unit isomorphisms are 2-natural. Since the category of 2-categories and 2-functors is a monoidal category under the Gray tensor product, we know that these constraints satisfy naturality for 1-cells; we must therefore check the 2-dimensional aspect. Thus given icons

α : F ⇒ F′ : A → A′,
β : G ⇒ G′ : B → B′,
γ : H ⇒ H′ : C → C′,

we must check that

a_{A′,B′,C′} ∗ ((α ⊗ β) ⊗ γ) = (α ⊗ (β ⊗ γ)) ∗ a_{A,B,C}

as icons. Therefore we must check that they have the same components on 1-cells, which by the icon axioms reduces to checking that they have the same components on generating 1-cells. For a generating 1-cell of the form (f ⊗ 1) ⊗ 1, the component of (α ⊗ β) ⊗ γ is (α_{f} ⊗1)⊗1. Horizontal composition with the 2-functor a_{A′,B′,C′} then gives the component

a_{A′,B′,C′}((α_{f} ⊗ 1) ⊗ 1) = α_{f} ⊗ (1 ⊗ 1).

On the other hand, the component of (α ⊗ (β ⊗ γ)) ∗ a_{A,B,C} at (f ⊗ 1) ⊗ 1 is just the

component of (α ⊗ (β ⊗ γ)) at

a_{A,B,C}((f ⊗ 1) ⊗ 1) = f ⊗ (1 ⊗ 1),

and these are clearly equal. Analogous computation for the two other kinds of generating 1-cells then show that the associator is 2-natural. The unit isomorphisms can be shown to be 2-natural in a similar fashion.

3.8. Remark. It is relatively simple to extend the strongly monoidal structures in Corollary 3.5 and Proposition 3.7 to symmetric ones by noting that the symmetry isomorphisms are 2-natural. Thus we get a Cat-enriched symmetric structure, which can then be viewed as a (special kind of) symmetric monoidal structure on the underlying bicategories.

4. Strictification

This section will review the construction of the strictification functor st : Bicat → 2Cat. Doing so produces the functor between categories, but that will not suffice for our purposes later. Thus we will also extend st to a 2-functor st : Icon → Gray_{icon}, and in fact show that this functor is left adjoint to the inclusion 2-functor i : Gray_{icon} → Icon. In order to construct the unit and counit for this adjunction, we will use the explicit construction of biequivalences e : stB → B, f : B → stB for any bicategory B. The main technical tool in this section is the coherence theorem for bicategories, and we refer the reader to [12, 18] for a review.

It should be noted that the main result of this section, Theorem 4.1, is not quite a consequence of the general theory of 2-monads as developed in [1, 14]. The general theory gives at least two ways to show that the inclusion Gray_{icon} ↪ Icon has a left 2-adjoint. One method shows that each of the two inclusions in the composite

Gray_{icon} ↪ Icon_{s} ↪ Icon

has a left 2-adjoint, the first because it is of the form f :^{∗}: S-Alg_{s} → T -Alg_{s} for a map of 2-monads f : T → S and the second because it is of the form T -Alg_{s} → T -Alg. The other method to abstractly produce a left 2-adjoint uses that Icon is nearly the 2-category of pseudo-algebras for the 2-monad S whose strict algebras are 2-categories. Unfortunately, neither of these methods immediately shows that the left adjoint is the familiar strictification functor st. Furthermore, the explicit form of the unit and counit of this adjunction will be useful later, so we verify this adjunction using elementary means.

Let B be a bicategory. We will begin by constructing a 2-category stB, and then show that it is biequivalent to the original bicategory B. In order to define the 2-cells of stB, it will be necessary to define the action of the functor e : stB → B on the 0- and 1-cells. Now for the definition. The 2-category stB will have the same objects as B. A 1-cell from a to b will be a string of composable 1-cells of B starting at a and ending at b. There is unique empty or length 0 string ∅_{a} from a to a for each object, and this will serve as the identity 1-cell.

Now we will define the function on underlying 0- and 1-cells of e. On 0-cells, e is the identity function. On 1-cells, we define

e(f_{n}f_{n−1}f_{1}) = (⋯ (f_{n} ∗ f_{n−1}) ∗ f_{n−2}) ⋯ ∗ f_{2}) ∗ f_{1};

for the empty string ∅ : a → a, we set e(∅) = I_{a}. The set of 2-cells between the strings f_{n}f_{n−1} ⋯ f_{1} and g_{m}g_{m−1} ⋯ g_{1} is defined to be the set of 2-cells between e(f_{n}f_{n−1} ⋯ f_{1}) and e(g_{m}g_{m−1} ⋯ g_{1}) in B. It is now obvious how e acts on 2-cells.

We will now give stB the structure of a 2-category. Composition of 1-cells is given by concatenation of strings, with the empty string as the identity. It is immediate that this is strictly associative and unital. Vertical composition of 2-cells is as in B, and this is strictly associative and unital since vertical composition of 2-cells in a bicategory is always strict in this way.

For horizontal composition of 2-cells, note that coherence for bicategories implies that there is a unique coherence isomorphism

e(f_{n} ⋯ f_{1}) ∗ e(g_{m} ⋯ g_{1}) ≅ e(f_{n} ⋯ f_{1}g_{m} ⋯ g_{1}).

Thus we can now define the horizontal composition α ∗ β in stB as the composite

e(f_{n} ⋯ f_{1}g_{m} ⋯ g_{1}) ≅ e(f_{n} ⋯ f_{1})e(g_{m} ⋯ g_{1})
⟶^{α∗β} e(f′_{n} ⋯ f′_{1})e(g′_{m} ⋯ g′_{1})
≅ e(f′_{n} ⋯ f′_{1}g′_{m} ⋯ g′_{1})

in B, where the unlabeled isomorphisms are the unique coherence isomorphisms mentioned above. The uniqueness of these isomorphisms ensures that this definition satisfies the middle-four interchange laws as well as being strictly associative and unital. This completes the proof that stB is a 2-category.

Now we will finish proving that e : stB → B is a functor, and in particular a bijectiveon-objects biequivalence. By construction, e is functorial on vertical composition of 2-cells. The unit isomorphism is an invertible 2-cell I_{a} ⇒ e(∅_{a}), so we define it to be the identity. The constraint cell for composition is an isomorphism

e(f_{n} ⋯ f_{1}) ∗ e(g_{m} ⋯ g_{1}) ≅ e(f_{n} ⋯ f_{1}g_{m} ⋯ g_{1})

which once again is the unique such isomorphism given by coherence for bicategories. Coherence also implies that the functor axioms hold. To show that e is a bijective-on-objects biequivalence, we only have to show that it is locally an equivalence of categories. But by definition, it is locally full and faithful since B and stB have the same 2-cells. This functor is also locally essentially surjective, as every 1-cell in B is the image under e of a length 1 string.

We will also need the biequivalence f : B → stB in order to construct the 2-adjunction between Icon and Gray_{icon}. The functor f is defined to be the identity on objects, to include every 1-cell as a string of length one, and to be the identity function on 2-cells. It is then simple to show that f is a bijective-on-objects biequivalence. It should be noted that ef = 1_{B}, and fe is biequivalent to 1_{stB} in Bicat(stB, stB) by a transformation whose components on objects can all be taken to be identities and whose components on 1-cells all come from coherence; this in fact shows that fe is isomorphic to 1_{stB} in Icon, proving that every bicategory is equivalent to a 2-category in Icon. This result was first noted by Lack and Paoli in [16].

We will now use the coherence theorem for functors to construct a 2-functor stF : stB → stB′ given a functor F : B → B′ between bicategories. We define stF : stB → stB′ as follows. On 0-cells, stF agrees with F. On 1-cells, we define

stF (f_{n} ⋯ f_{1}) = F f_{n} ⋯ F f_{1},

and stF (∅_{a}) = ∅_{F a}. Now let α : e(f_{n} ⋯ f_{1}) ⇒ e(g_{m} ⋯ g_{1}) be a 2-cell in stB. Then we define stF (α) to be the 2-cell

e(F f_{n} ⋯ F f_{1}) ≅ F (e(f_{n} ⋯ f_{1})) ⟶^{F α} F (e(g_{m} ⋯ g_{1})) ≅ e(F g_{m} ⋯ F g_{1}),

where the unlabeled isomorphisms are the unique isomorphism 2-cells provided by coherence for functors.

One then uses coherence for functors to show that this is a strict functor, and that st(F ∘ G) = stF ∘ stG. The commutativity of the square

[figure: X; Y; F; X; stX; f; Y; stY; f; stX; stY; stF]

is immediate from the definitions. It is not the case that F ∘ e = e ∘ stF, but there is an invertible icon ω between these with each component given by the unique coherence 2-cell; in particular, this equation does hold when X, Y are 2-categories and F is a 2-functor, as the unique coherence 2-cell is necessarily an identity.

4.1. Theorem. The assignment B ↦ stB can be extended to a 2-functor

st : Icon → Gray_{icon}.

This 2-functor is the left 2-adjoint to the inclusion Gray_{icon} ↪ Icon.

Proof. To give B ↦ stB the structure of a 2-functor, we must define it on higher cells. We have given the construction of stF above, so let α : F → G be an icon between functors. Since stF (b) = F (b), we have that stF and stG agree on objects, so we can define icons between them. Let f_{1} ⋯ f_{n} be a 1-cell in stB from a to b. Then

stF (f_{1} ⋯ f_{n}) = F f_{1}F f_{2} ⋯ F f_{n}

by definition, so we define stα_{f_{1}···f_{n}} to be the 2-cell represented by α_{f_{1}} ∗ ⋯ ∗ α_{f_{n}}. For the empty string from a to a, define stα_{∅} = 1_{I_{F a}}. It is immediate that this is an icon stα : stF ⇒ stG.

We have already noted that st(F G) = stF stG, and it is clear that st(1_{B}) = 1_{stB}. We only must check that st preserves horizontal composition of icons, or that

stα ∗ stβ = st(α ∗ β).

Writing this down in terms of components, it becomes clear that this follows immediately from the definitions and interchange. Thus st : Icon → Gray_{icon} is a 2-functor.

To prove that st is the left 2-adjoint to the inclusion Gray_{icon} ↪ Icon, we must give a unit and counit for the adjunction. Denoting the inclusion by i, the counit would be a 2-natural transformation with components st i(A) → A for a 2-category A and the unit would be a 2-natural transformation with components B → i st(B) for a bicategory B. The counit is defined to be e : stA → A, which is a 2-functor when A is a 2-category, and the unit is defined to be f : B → stB. The 1-dimensional aspect of naturality for these components is contained in the remarks above, so we only need to check the 2-dimensional aspect. For f, the component of stα ∗ f at a 1-cell r : x → y is the 2-cell {F r} ⇒ {Gr} represented by α_{r}, and it is trivial to show that the same 2-cell is the component of f ∗ α; the calculation for e is analogous, confirming 2-naturality.

Finally, we must check the triangle identities. One reduces to showing that

A ⟶^{f} stA ⟶^{e} A

is the identity for any 2-category A, which we have already noted holds. The other involves showing that

stB ⟶^{stf} ststB ⟶^{e_{stB}} stB

is the identity for any bicategory B. This is simple to check on cells, so it only remains to show that the constraint isomorphisms are identities, but this is straightforward to check from the definition.

5. Monoidal structure

In this final section, we will prove that the strictification functor st : Icon → Gray_{icon} is monoidal at the level of bicategories. It is for the proof of the monoidal structure that we require the use of icons, as indicated by Proposition 5.2 below. We begin by first showing that the functor st is not monoidal in the 1-dimensional sense. The following proposition originally appeared in [7], although its statement there did not use the language of icons. As a proof can be found in any of [7, 9, 11], we omit it here.

5.1. Proposition. Let X, Y be bicategories. Then there exists a cubical functor ŝt : stX × stY → st(X × Y) such that

1. ŝt is the identity on objects and

2. there is an invertible icon ζ as pictured below.

[figure: stX × stY; st(X × Y); ŝt; stX × stY; X × Y; e_{X}×e_{Y}; st(X × Y); X × Y; e_{X×Y}; ζ]

For the next proposition, we will need to know explicitly what ŝt does to 1-cells. If we let {f_{n}, …, f_{1}} be a 1-cell in stX and let {g_{m}, …, g_{1}} be a 1-cell in stY, then the required formula is

ŝt ({f_{n}, …, f_{1}}, {g_{m}, …, g_{1}}) = (1, g_{m})(1, g_{m−1}) ⋯ (1, g_{1})(f_{n}, 1) ⋯ (f_{1}, 1).

5.2. Proposition. The cubical functor ŝt is natural in both variables, up to an invertible icon.

Proof. Let F : X → X′, G : Y → Y′ be functors between bicategories. To prove the naturality of ŝt, we must construct an invertible icon in the square below.

[figure: stX × stY; st(X × Y); ŝt; st(X × Y); st(X′ × Y′); st(F ×G); stX × stY; stX′ × stY′; stF ×stG; stX′ × stY′; st(X′ × Y′); ŝt; ≅]

First, it is clear that these agree on objects since both functors ŝt are the identity on objects and stF agrees with F on objects, so it is possible to define an icon between them.

By definition, ŝt(f, g) = ŝt(∅, g) ∗ ŝt(f, ∅) for a 1-cell (f, g) in stX × stY. Thus the top composite cubical functor gives

(F 1, Gg_{m})(F 1, Gg_{m−1}) ⋯ (F 1, Gg_{1})(F f_{n}, G1) ⋯ (F f_{1}, G1)

while the composite along the left and bottom is

(1, Gg_{m})(1, Gg_{m−1}) ⋯ (1, Gg_{1})(F f_{n}, 1) ⋯ (F f_{1}, 1).

We thus define the desired invertible icon as a horizontal composite of unit constraints for F and G. Naturality follows from the naturality of the associators in the bicategories X′, Y′ together with the interchange law. We leave the icon axioms to the reader, as they are entirely straightforward.

5.3. Remark. The proof of the previous proposition shows that ŝt is not natural in the sense of giving a natural transformation in the standard, 1-categorical sense, but only up to an icon. In particular, this shows that st is not a lax monoidal functor between monoidal categories.

In order to avoid complicated computations, we will employ the theory of doctrinal adjunction as in [13]. We begin by recalling the basic result. Let K be a 2-category, and T a 2-monad on K. Assume we have T -algebras x, y, and assume we have an adjunction f ⊣ u in K with f : x → y, u : y → x. Then there is a bijection, given by taking mates, between data making u into a lax T -algebra morphism and data making f into a oplax T -algebra morphism. In our case, the relevant 2-category is 2CAT, the 2-category of (potentially large) 2-categories, 2-functors, and 2-natural transformations, and the 2monad T is the free strongly monoidal 2-category 2-monad. We have algebras Icon and Gray_{icon}, and a 2-adjunction between them. We begin employing the theory of doctrinal adjunction by giving a lax structure on i in the following proposition.

5.4. Proposition. The 2-functor i : Gray_{icon} ↪ Icon is Cat-lax monoidal.

Proof. Since i sends the unit object in Gray_{icon} to the unit object in Icon, we must give a 2-natural transformation with components iA × iB → i(A ⊗ B) and then check the lax functor axioms. Now A, B are 2-categories, but the components above are in Icon, hence are pseudofunctors; thus we define these to be the universal cubical functors c : A × B → A ⊗ B. The proof that these components give a 2-natural transformation is a consequence of Lemma 3.4. There are now two unit axioms and one associativity axiom to check.

The left unit axiom is the commutativity of the diagram below, which is trivial to check.

[figure: 1 × A; 1 ⊗ A; c; 1 ⊗ A; A; ≅; 1 × A; A; ≅]

The right unit axiom is analogous. The associativity axiom is the commutativity of the following diagram.

[figure: (A × B) × C; (A ⊗ B) × C; c×1; (A ⊗ B) × C; (A ⊗ B) ⊗ C; c; (A ⊗ B) ⊗ C; A ⊗ (B ⊗ C); ≅; (A × B) × C; A × (B × C); ≅; A × (B × C); A × (B ⊗ C); 1×c; A × (B ⊗ C); A ⊗ (B ⊗ C); c]

This diagram clearly commutes on objects, and it is easy to check that it commutes on 1and 2-cells which have only a single non-identity component. Since both composites are cubical, this implies that they agree on all 1- and 2-cells. The constraints for both are given as composites of the canonical isomorphisms

(f ⊗ 1) ∘ (1 ⊗ g) ≅ (1 ⊗ g) ∘ (f ⊗ 1)

or as identities, and once again it is straightforward to verify that the Gray tensor product axioms force these to be equal.

Thus we have the following immediate consequence.

5.5. Corollary. The 2-functor st : Icon → Gray_{icon} is Cat-oplax monoidal.

We need one final preliminary result before proving the main theorem.

5.6. Proposition. The strict 2-functor χ_{XY} : stX ⊗ stY → st(X × Y) induced by ŝt is an internal equivalence in Gray_{icon}.

Proof. We must produce a 2-functor \overline{χ} : st(X×Y) → stX⊗stY and invertible icons \overline{χ}χ ≅ 1, χ\overline{χ} ≅ 1. Now by Proposition 5.1, we get that ŝt is a bijective-on-objects biequivalence because both e_{X×Y} and e_{X} × e_{Y} are, and bijective-on-objects biequivalence satisfy the 2-out-of-3 property in the following sense: if fg ≅ h in Icon, then all three functors are bijective-on-objects biequivalences if two of them are. This shows, by Lemma 3.4, that χ is also a bijective-on-objects biequivalence.

To construct the 2-functor \overline{χ}, we will use Theorem 4.1. The 2-functor

\overline{χ} : st(X × Y) → stX ⊗ stY

determines, and is determined by, a functor j : X ×Y → stX ⊗stY such that \overline{χ}f_{X×Y} = j. Define the functor j to be the composite below.

X × Y ⟶^{f_{X}×f_{Y}} stX × stY ⟶^{c} stX ⊗ stY

By Lemma 1.7, c is a bijective-on-objects biequivalence, and f_{X} × f_{Y} is as well. Once again by the 2-out-of-3 property, \overline{χ} is then a bijective-on-objects biequivalence.

Now bijective-on-objects biequivalences are the internal equivalences in Icon, and a 2-functor in Gray_{icon} is an internal equivalence if and only if it is an internal equivalence in Icon and there is a pseudoinverse which is a 2-functor. This implies that both χ and \overline{χ} are internal equivalences in Icon. If we show that \overline{χ}χ ≅ 1, then by the uniqueness (up to isomorphism) of pseudoinverses we will get that χ\overline{χ} ≅ 1 as well. Once again by Lemma 3.4, to show that \overline{χ}χ ≅ 1, we will prove that \overline{χ}χc ≅ c. By the definition of \overline{χ}, we have \overline{χ}f_{X×Y} = c(f_{X} × f_{Y}), so

\overline{χ} ≅ \overline{χ}f_{X×Y} e_{X×Y} = c(f_{X} × f_{Y})e_{X×Y} .

Thus we have the following calculation which finishes the proof.

\overline{χ}χc ≅ c(f_{X} × f_{Y})e_{X×Y} χc
= c(f_{X} × f_{Y})e_{X×Y} ŝt
≅^{11ζ} c(f_{X} × f_{Y})(e_{X} × e_{Y})
≅ c

5.7. Theorem. The 2-functor st : Icon → Gray_{icon} can be given the structure of a symmetric monoidal functor between the underlying monoidal bicategories.

Proof. By Corollary 5.5, we already know that the functor st : Icon → Gray_{icon} is Cat-oplax monoidal. The structure maps for the Cat-lax monoidal structure on i are the universal cubical functors c_{AB}, and we know these are internal equivalences in Icon by Lemma 1.7. Unfortunately, the unit and counit for the adjunction st ⊣ i are not both internal equivalences: the counit is the 2-functor e : st iA → A which is not an internal equivalence in Gray_{icon} since it has no pseudo-inverse which is also a 2-functor. But the formula given in Lemma 2.15 for the oplax structure constraints is easily checked to be the 2-functor \overline{χ} in the proof of Proposition 5.6. That theorem shows that the 2-functor st satisfies the hypotheses of Lemma 2.16, and moreover that we can take the structure map stA ⊗ stB → st(A × B) to be the 2-functor χ.

To give this monoidal functor the structure of a braided monoidal functor, we must provide an invertible modification U. By the isomorphism in Lemma 3.4, such an invertible modification will correspond to one with components as below.

[figure: stX × stY; stY × stX; ≅; stY × stX; st(Y × X); ŝt; stX × stY; st(X × Y); ŝt; st(X × Y); st(Y × X); st(≅); ⇓]

Let (f, g) be a 1-cell in stX × stY. Then the image of this 1-cell using the top and right functors is the composite string (1, f)(g, 1), while the image using the left and bottom functors is the composite string (g, 1)(1, f). To give an invertible 2-cell between these, we must give an invertible 2-cell between their images under e. Examining e((1, f)(g, 1)) and e((g, 1)(1, f)), we see that there is a unique coherence isomorphism (arising from the bicategory X × Y) between them, so we define that to be the component of U at (f, g).

There are now two axioms to check for the braided monoidal structure of this functor (see [10] for the axioms in the fully weak case). In both cases, the same argument shows that the axiom holds. First, all of the 2-cells in each pasting are the identity, except for (possibly) the naturality isomorphisms for χ and the components of U. For the naturality isomorphisms for χ, the 1-cells involved all have identity unit constraints, hence by the definition these naturality isomorphisms are also the identity. Now the components of U are not identities, but they all evaluate to unique coherence isomorphisms under e_{X×Y} : st(X × Y) → X × Y. We know that e is a biequivalence, and in particular a pair of 2-cells in stX are equal if and only if they are parallel and have the same image under e_{X}. Thus by the above, we see that applying e to the pastings of the braided monoidal functor axioms will produce a pair of parallel 2-cells which are both composites of coherence isomorphisms and therefore equal by the coherence theorem for bicategories. Thus the pastings in question will be equal after applying e, hence equal beforehand as well. This shows that st is a braided monoidal functor.

Finally, we complete the proof that st is symmetric monoidal. This involves checking a single axiom (see [5] or [19]), showing that st preserves the symmetry. As with the braiding, it is easy to check that all of the cells involved in the pasting are identities or are represented by unique coherence cells. Thus coherence for bicategories ensure that this axiom holds, and so st is symmetric monoidal.

5.8. Remark. At this point, one could go on to show that st : Bicat → Gray is a symmetric monoidal functor between symmetric monoidal tricategories. The underlying functor of tricategories is discussed in [9, 11], and we have established the symmetric monoidal structure above. All that remains is to interpret the above proof in the context of monoidal tricategories, and then to insert coherence cells to take care of the proliferation of units that would occur when changing the invertible icons used here to pseudonatural transformations with identity components.

References

[1] R. Blackwell, G. M. Kelly, and A. J. Power, Two-dimensional monad theory, J. Pure Appl. Algebra 59 (1989), 1–41.

[2] E. Cheng and N. Gurski, The periodic table of n-categories for low-dimensions I: degenerate categories and degenerate bicategories, in “Categories in Algebra, Geometry and Mathematical Physics”, 143–164, Contemp. Math., 431, Amer. Math. Soc., Providence, RI, 2007.

[3] E. Cheng and N. Gurski, The periodic table of n-categories for low-dimensions II: degenerate tricategories, Cahiers Topologie Géom. Différentielle Catég. 52 (2011), no 2., 82–125.

[4] S. Crans, A tensor product for Gray-categories, Theory Appl. Categ. 5 (1999), 12–69.

[5] Brian Day and Ross Street, Monoidal bicategories and Hopf algebroids, Adv. Math. 129 (1997), 99–157.

[6] R. Garner and N. Gurski, The low-dimensional structures formed by tricategories, Math. Proc. Cam. Phil. Soc. 146 (2009), no. 3, 551–589.

[7] R. Gordon, A. J. Power, and Ross Street, Coherence for tricategories, Mem. Amer. Math. Soc. 117 (1995), no. 558.

[8] J. W. Gray, “Formal Category Theory: Adjointness for 2-Categories”, Lecture Notes in Math. 391, Springer-Verlag, Berlin-New York, 1974.

[9] N. Gurski, An algebraic theory of tricategories, Ph. D. thesis, University of Chicago, 2006.

[10] N. Gurski, Loop spaces, and coherence for monoidal and braided monoidal bicategories, Adv. Math. 226 (2011), no. 5, 4225-4265.

[11] N. Gurski, Coherence in Three-Dimensional Category Theory, to appear in the Cambridge University Press Tracts in Mathematics series.

[12] A. Joyal and R. Street, Braided tensor categories, Adv. Math. 102 (1993), 20–78.

[13] G. M. Kelly, Doctrinal adjunction, Category Seminar (Proc. Sem., Sydney, 1972/1973), pp. 257280. Lecture Notes in Math., Vol. 420, Springer, Berlin, 1974.

[14] S. Lack, Codescent objects and coherence, Special volume celebrating the 70th birthday of Professor Max Kelly. J. Pure Appl. Algebra 175 (2002), no. 1-3, 223-241.

[15] S. Lack, Icons, Appl. Cat. Str. 18 (2010), no. 3, 289–307.

[16] S. Lack and S. Paoli, 2-nerves for bicategories, K-Theory 38 (2008), no. 2, 153– 175.

[17] S. Mac Lane, Natural associativity and commutativity, Rice University Studies 49 (1963), 28–46.

[18] S. Mac Lane and R. Paré, Coherence for bicategories and indexed categories, J. Pure Appl. Algebra 37 (1985), 59–80.

[19] C. Schommer-Pries, The Classification of Two-Dimensional Extended Topological Field Theories, Ph. D. thesis, U. C. Berkeley, 2009. Available at arXiv:1112.1000.

School of Mathematics and Statistics, University of Sheffield, Sheffield, UK, S3 7RH

Email: nick.gurski@sheffield.ac.uk

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

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/28/1/28-01.{dvi,ps,pdf}

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

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

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

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

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

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

gavin seal@fastmail.fm

Transmitting editors.

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

Valeria de Paiva: valeria.depaiva@gmail.com

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