Let $\Scal$ be a small category admitting binary products. We show that the whole theory of monoidal $\Scal$-fibered categories can be rephrased using the external tensor product everywhere in place of the usual internal tensor product. More precisely, we construct a canonical dictionary relating the classical structures and properties of the internal tensor product with analogous structures and properties of the external tensor product: this applies to associativity, commutativity and unit constraints, to projection formulae, as well as to monoidality of morphisms between monoidal $\Scal$-fibered categories.

§ INTRODUCTION

§.§ Motivation and goal of the paper

For every small category $\Scal$, the theory of $\Scal$-fibered categories can be merged with the theory of monoidal categories into a theory of monoidal $\Scal$-fibered categories. The basic definitions of this theory can be found, for example, in <cit.>. In a nutshell, giving a monoidal $\Scal$-fibered category amounts to giving an $\Scal$-fibered category $\Hbb$ equipped with a collection of tensor product functors

\begin{equation*}
- \otimes - = - \otimes_S -: \Hbb(S) \times \Hbb(S) \rightarrow \Hbb(S), \quad (A,B) \rightsquigarrow A \otimes B \qquad (S \in \Scal)
\end{equation*}

carrying an associativity constraint (and possibly also a commutativity constraint and a unit constraint) together with, for every morphism $f: T \rightarrow S$ in $\Scal$, a natural isomorphism of functors $\Hbb(S) \times \Hbb(S) \rightarrow \Hbb(T)$

\begin{equation}\label{m_f:intro-ch1}
m = m_f: f^* A \otimes f^* B \xrightarrow{\sim} f^*(A \otimes B)
\end{equation}

witnessing the monoidality of the inverse image functor $f^*: \Hbb(S) \rightarrow \Hbb(T)$. These structures are required to satisfy a certain list of compatibility conditions that we do not need to specify here.
If the base category $\Scal$ admits binary products, one can also define the external tensor product functors

\begin{equation*}
- \boxtimes - = - \boxtimes_{S_1,S_2} -: \Hbb(S_1) \times \Hbb(S_2) \rightarrow \Hbb(S_1 \times S_2), \quad (A_1,A_2) \mapsto A_1 \boxtimes A_2 \qquad (S_1, S_2 \in \Scal)
\end{equation*}

by the formula

\begin{equation}\label{formulae_int_to_ext}
A_1 \boxtimes A_2 := pr^{12*}_{1} A_1 \otimes pr^{12*}_{2} A_2,
\end{equation}

where $pr^{12}_{i}: S_1 \times S_2 \rightarrow S_i$, $i = 1,2$, denote the canonical projections. Informally, the usual tensor product - also called the internal tensor product - can be recovered from the external tensor product via the formula

\begin{equation}\label{formulae_ext_to_int}
A \otimes B = \Delta_S^*(A \boxtimes B),
\end{equation}

where $\Delta_S: S \hookrightarrow S \times S$ denotes the diagonal embedding.
However, strictly speaking, the two constructions in (<ref>) and (<ref>) are not mutually inverse. Moreover, it is a priori unclear whether the monoidality isomorphisms (<ref>) and the various additional constraints (together with their coherence and mutual compatibility conditions) can be expressed purely in terms of the external tensor product. A similar issue arises when studying monoidality of morphisms between $\Scal$-fibered categories equipped with monoidal structures. The main goal of this paper is to provide a precise answer to all these questions.

Our main motivation behind this work comes from the theory of perverse sheaves. To fix notation, let $k$ be a subfield of the complex numbers, and consider the category $\Var_k$ of (quasi-projective) algebraic $k$-varieties. To every $S \in \Var_k$ one can attach the algebraically constructible $\Q$-linear derived category $D^b_c(S,\Q)$, a tensor-triangulated category; as $S$ varies, these categories assemble into a monoidal triangulated $\Var_k$-fibered category. The theory of [6] yields a perverse $t$-structure on $D^b_c(S,\Q)$ whose heart is the $\Q$-linear category $\Perv(S)$ of perverse sheaves on $S$; as shown by Beilinson in [5], the triangulated category $D^b_c(S,\Q)$ can be canonically recovered as the bounded derived category $D^b(\Perv(S))$. In light of Beilinson's result, it is natural to wonder how much of the functoriality of the triangulated categories $D^b_c(S,\Q)$ can be reconstructed directly on the level of the abelian categories $\Perv(S)$. This question is intimately related to the emerging theory of perverse Nori motives introduced by F. Ivorra and S. Morel in [11]: more specifically, it is related to the functoriality of the bounded derived categories of perverse Nori motives, which should perfectly mimic the usual functoriality of perverse sheaves. In fact, we are ultimately interested in applying the general results of the present paper as a first reduction step towards the construction of a monoidal structure on perverse Nori motives, which we obtain in [15]. From this perspective, the main issue of working directly with the internal tensor product lies in its lack of $t$-exactness for the perverse $t$-structures: indeed, it is well-known that the internal tensor product

\begin{equation}\label{otimes:Dbc-intro}
- \otimes -: D^b(S,\Q) \times D^b(S,\Q) \rightarrow D^b(S,\Q)
\end{equation}

does not respect the perverse $t$-structure unless $\dim(S) = 0$. On the other hand, for every choice of $S_1, S_2 \in \Var_k$, the external tensor product

\begin{equation*}
- \boxtimes -: D^b(S_1,\Q) \times D^b(S_2,\Q) \rightarrow D^b(S_1 \times S_2,\Q)
\end{equation*}

restricts to a bi-exact functor

\begin{equation*}
- \boxtimes -: \Perv(S_1) \times \Perv(S_2) \rightarrow \Perv(S_1 \times S_2)
\end{equation*}

and, in fact, can be canonically recovered as the trivial bi-derived functor of the latter modulo Beilinson's equivalences (see <cit.>). For this reason, the external tensor product is a priori more adapted to a direct motivic lifting than the internal tensor product. It is worth remarking that the strategy of deducing the internal tensor product from the external one via formula (<ref>) has been already implemented in Saito's theory of mixed Hodge modules in [14], where, however, the formal details of the construction were not studied systematically. In the case of peverse Nori motives, the highly unexplicit nature of the categories involved forces us to be as formally precise as possible. For this reason, having a general explicit dictionary expressing the structure and properties of the internal tensor product as structure and properties of the external tensor product is highly desirable.

Of course, in view of the classical formula (<ref>), the lack of $t$-exactness of the internal tensor product depends on the lack of $t$-exactness of the inverse image functor $\Delta_S^*$. Hence, in order to fully recover the internal tensor product (<ref>) on the level of perverse sheaves, one still needs to understand whether the functor $\Delta_S^*$ can be conveniently expressed in terms of $t$-exact functors. This is indeed the case, as a consequence of the results collected in <cit.>; in fact this approach has been used successfully in the construction of motivic inverse image functors in <cit.>. However, we prefer to gloss over this technical point since it does not play any role in the present paper.

§.§ Main results

In order not to restrict the application range of our techniques unnecessarily, and also for sake of notational and conceptual clarity, we formulate our results in the general framework of fibered categories, thus avoiding any reference to perverse sheaves or to concrete geometric situations.

Given a small category $\Scal$ admitting binary products, we introduce the language of internal and external tensor structures on a given $\Scal$-fibered category $\Hbb$.
Our treatment of internal tensor structures is just a re-arrangement of the classical theory of monoidal $\Scal$-fibered categories: for example, we introduce associativity, commutativity, and unit constraints (as well as their compatibility conditions) as formalized in Mac Lane's classical paper [12], and we describe their compatibility with inverse image functors as done in Ayoub's work [2]. The only difference is that, in order to make the exposition as neat as possible, we prefer not to include an associativity constraint from the very beginning but rather treat it as a separate structure, exactly as one sometimes does with commutativity and unit constraints.
Our theory of external tensor structures should be new in the literature. The main notions that we introduce are nothing but the natural transliteration of the corresponding notions for internal tensor structures. This operation works nicely both for monoidality isomorphisms and for each of the three types of additional constraint (as well as for their compatibility conditions).

Motivated by the theory of perverse sheaves and by the abstract theory of six functor formalisms (as formalized in [2, 3], [7] or [9]), we also study projection formulae in our setting of tensor structures. Not surprisingly, it turns out that the usual formulation in terms of the internal tensor product admits a natural translation in terms of the external tensor product.
Again, the main difference with respect to the existing literature is that we treat the validity of projection formulae as a separate property rather than imposing it from the beginning.

Generally speaking, the main new ingredient in our presentation is the notion of equivalence between internal or external tensor structures: this allows us to make it precise in which sense the classical formulae (<ref>) and (<ref>) should be considered to be mutually inverse.
Our first main result can be stated as follows:

[<Ref>, <Ref>]
Fix an $\Scal$-fibered category $\Hbb$. Then there exist canonical mutually inverse bijections between equivalence classes of (unitary, symmetric, associative) internal and external tensor structures on $\Hbb$; moreover, these bijections respect the validity of projection formulae.

It is worth noting that all the equivalences between tensor structures involved in the proofs are explicit and canonical, so that the actual result is more precise than what asserted.

In the same spirit, given a morphism of $\Scal$-fibered categories $R: \Hbb_1 \rightarrow \Hbb_2$, we introduce the notion of internal and external tensor structures on $R$ (with respect to two given internal or external tensor structures on $\Hbb_1$ and $\Hbb_2$, respectively). In the internal setting, we recover the usual notion of monoidal morphism between monoidal $\Scal$-fibered categories; in the external setting, we consider its natural transliteration. We then study the compatibility of internal and external tensor structures on $R$ with given associativity, commutativity, or unit constraints on $\Hbb_1$ and $\Hbb_2$.
Our second main result can be stated as follows:

Fix a morphism of $\Scal$-fibered categories $R: \Hbb_1 \rightarrow \Hbb_2$. Then, under the bijective correspondence of the previous theorem, there exist canonical mutually inverse bijections between (unitary, symmetric, associative) internal and external tensor structures on $R$ with respect to two given (unitary, symmetric, associative) tensor structures on $\Hbb_1$ and $\Hbb_2$.

In order for this statement to even make sense, one needs to use the explicit equivalences witnessing the bijections between internal and external tensor structures on $\Hbb_1$ and on $\Hbb_2$ as mentioned above.

In conclusion, we construct a canonical dictionary between the languages of internal tensor structures and of external tensor structures.
Concretely, all the axioms introduced in the course of the paper ask for the commutativity of suitable natural diagrams; similarly, both the main results described above and all the intermediate results used to prove them amount to showing the commutativity of certain natural diagrams. Checking the commutativity of these diagrams directly is not hard and, in fact, does not require any new insight once the various claims are made explicit. The main issue is that one often has to decompose the diagrams under consideration into several pieces, and the resulting figures rarely fit into the space of one or two pages.
As a partial workaround, we have chosen to include a few auxiliary results (<Ref>, <Ref>, <Ref> and <Ref>) which allow us to cleverly simplify the diagrams in question; in this way, it also becomes easier to understand the roles that the various axioms play in each proof.
These auxiliary results have independent interest, since they show that internal and external tensor structures, both on fibered categories and on morphisms of such, are just suitable variations on the theme of fibered categories.
This observation is certainly not new: in fact, one could formalize the entire picture in a more systematic way following, for example, F. Hörmann's approach to six functor formalisms as developed in [10]. One might thus be tempted to rewrite the whole theory presented here in even more abstract terms; however, in view of our applications, it is preferable for us to have the explicit axioms written down instead of encoding everything into a more conceptual framework.

§.§ Structure of the paper

Throughout the paper, we work over a fixed small category $\Scal$. Essentially, all fibered categories involved are fibered over $\Scal$; the only exception is represented by certain auxiliary fibered categories which are not involved explicitly in the proofs of the main results.

In <Ref> we fix our general conventions and notation about fibered categories, including the notions of section, morphism, and image of a section under a morphism. We also prove a couple of useful auxiliary results (<Ref> and <Ref>) which are repeatedly used in the sequel in order to shorten certain constructions and simplify certain proofs.

Starting from <Ref>, we assume that the base category $\Scal$ admits binary products: this is only needed to define the external tensor product; it is irrelevant for our discussion whether $\Scal$ possesses or not a terminal object. In <Ref> we explain how to rephrase the structure of a monoidal $\Scal$-fibered category purely in terms of the external tensor product. In order to highlight the symmetry between the internal and external versions of the tensor product, it is useful to write down the corresponding axioms of the two versions of the theory in parallel. To this end, we introduce appropriate notions of internal tensor structure and of external tensor structure (<Ref>(1) and <Ref>(1), respectively) that only include the single tensor product functors and their monoidality isomorphisms: in particular, the structure that we consider in the internal setting is coarser that the commonly used notions of monoidal $\Scal$-fibered categories, since it does not include any notion of associativity, symmetry, or unit. We then explain how to transform internal tensor structures into external tensor structures (<Ref>) and conversely (<Ref>). Moreover, we  introduce natural notions of equivalence between internal or external tensor structures (<Ref>(2) and <Ref>(2), respectively) that allow us to make it precise in what sense the two formulae (<ref>) and (<ref>) can be promoted to mutually inverse constructions (<Ref>).

In <Ref>, <Ref> and <Ref> we consider associativity, commutativity, and unit constraints, respectively. Following the approach of <Ref>, we start by introducing the internal and external versions of the relevant constraint, and we refine the notions of equivalence of tensor structures accordingly; we then explain how to transform an internal constraint into an external one and conversely; lastly, we show that the canonical bijection between equivalence classes of internal and external tensor structures can be refined compatibly with the constraints under consideration.

In <Ref> we examine the mutual compatibility conditions between associativity, commutativity and unit constraints. Again, each of these condition can be formulated both in the internal and in the external setting, and the homologous conditions correspond to one another under the bijection between internal and external tensor structures. Once we have this last ingredient, we are able to deduce our first main result (<Ref>) in its full strength.

The short <Ref> is devoted to the study of projection formulae, which are an important property of most monoidal fibered categories of geometric nature. We show that the usual projection formulae in the language of internal tensor structures have a natural analogue in the language of external tensor structures in such a way that the bijection of <Ref> respects the validity of projection formulae (<Ref>).

In <Ref> we study monoidality of morphisms of $\Scal$-fibered categories. In the first part, we introduce the notion of internal tensor structure and of external tensor structure on a morphism between $\Scal$-fibered categories with respect to given internal or external tensor structures on the two single $\Scal$-fibered categories involved (<Ref> and <Ref>, respectively). Then, by analogy with the case of monoidal structures on single $\Scal$-fibered categories, we explain how to transform internal tensor structures on a morphism into external tensor structures on the same morphism (<Ref>) and conversely (<Ref>); this is done coherently with the translation procedure between internal and external tensor structures on the two $\Scal$-fibered categories involved. Finally, we prove that these two constructions are mutually inverse modulo equivalence of internal and external tensor structures on the two sides (<Ref>).
In the second part of <Ref> we refine such a bijection with respect to associativity, commutativity, and unit constraints: to this end, we consider the natural properties of associativity, symmetry and unitarity for tensor structures on morphisms, both in the internal and in the external setting. We show without difficulty that the correspondence between internal and external tensor structures is compatible with each of these properties. Once we have this last ingredient, we are able to deduce our second main result (<Ref>) in its full strength.

In the final <Ref>, motivated by our applications to perverse sheaves and perverse Nori motives, we specialize our discussion to the case of triangulated $\Scal$-fibered categories. We fully spell out the natural triangulated analogues of the various definitions and results obtained previously, but we omit all details of proof. The commutativity conventions that we have chosen here are coherent with the usual conventions for derived categories of abelian ($\Scal$-fibered) categories endowed with bi-exact tensor product functors.

§.§ Acknowledgments

The contents of this paper correspond to the first chapter of my Ph.D. thesis, written at the University of Freiburg under the supervision of Annette Huber-Klawitter. It is a pleasure to thank her for many useful discussions around the subject of this article, as well as for her constant support and encouragement. I would also like to thank Swann Tubach for some helpful notational comments on an earlier version of this work.

§ NOTATION AND CONVENTIONS

* Unless otherwise dictated, categories are assumed to be small with respect to some fixed universe.

* Let $\Scal$ be a small category.

* The notation $S \in \Scal$ means that $S$ is an object of $\Scal$.

* A composable tuple in $\Scal$ is a tuple of the form $\underline{g} = (g_1,\dots,g_r)$ where $g_1, \dots, g_r$ are morphisms in $\Scal$ such that the composition $g_r \circ \cdots \circ g_1$ makes sense in $\Scal$.

* We say that a sequence $\underline{g}^{(1)} = (g_1^{(1)}, \dots, g_{r_1}^{(1)}), \dots, \underline{g}^{(n)} = (g_1^{(n)}, \dots, g_{r_n}^{(n)})$ of composable tuples in $\Scal$ is composable if, for each $i = 1, \dots, n-1$, the composition $g_1^{(i+1)} \circ g_{r_i}^{(i)}$ makes sense in $\Scal$.

* Let $\Scal$ be a small category admitting binary products.

* Given two composable tuples in $\Scal$ with the same length

\begin{equation*}
\underline{g}^{(1)} = (g_1^{(1)}, \dots, g_r^{(1)}), \quad \underline{g}^{(2)} = (g_1^{(2)}, \dots, g_r^{(2)}),
\end{equation*}

we let $\underline{g}^{(1)} \times \underline{g}^{(2)}$ denote the composable tuple $(g_1^{(1)} \times g_1^{(2)}, \dots, g_r^{(1)} \times g_r^{(2)})$.

* For every object $S \in \Scal$ and every integer $n \geq 2$, we let

\begin{equation*}
\Delta_S^{(n)}: S \hookrightarrow S \times \dots \times S
\end{equation*}

denote the diagonal embedding of $S$ into the direct product of $n$ copies of $S$ in $\Scal$. In the special case where $n = 2$, we omit the superscript from the notation.

* Given a collection of objects $S_{i_1}, \dots, S_{i_n} \in \Scal$ indexed by natural numbers $i_1, \dots, i_n$, for every substring $j_1 \dots j_r$ of the string $i_1 \dots i_n$ we let

\begin{equation*}
pr^{i_1 \dots i_n}_{j_1 \dots j_r}: S_{i_1} \times \dots \times S_{i_n} \rightarrow S_{j_1} \times \dots \times S_{j_r}
\end{equation*}

denote the canonical projection.

* Given a collection of objects $S_{i_1}, \dots, S_{i_n} \in \Scal$ indexed by a set of natural numbers $I = \left\{i_1, \dots, i_n\right\}$, for every permutation $\sigma \in \textup{Sym}(I)$ we let

\begin{equation*}
\tau_{\sigma}: S_{i_1} \times \dots S_{i_n} \xrightarrow{\sim} S_{\sigma(i_1)} \times \dots \times S_{\sigma(i_n)}
\end{equation*}

denote the canonical permutation isomorphism. In the special case where $n = 2$ and $\sigma$ is the non-identity permutation, we omit the subscript from the notation.

* Given categories $\Ccal_1, \dots, \Ccal_n$, we let $\Ccal_1 \times \cdots \times \Ccal_n$ denote their direct product category.

§ RECOLLECTIONS ON FIBERED CATEGORIES

Throughout this paper, we fix a small category $\Scal$; starting from <Ref> we will need to assume binary products to exist in $\Scal$, but this is not necessary for the moment. All fibered categories mentioned in this paper are fibered over $\Scal$ unless stated otherwise.

The conventions on $2$-categories and $2$-functors that we follow are those adopted in <cit.> and in <cit.>: what we call a fibered category here is what in the original reference <cit.> is called a "catégorie clivée normalisée"; we consider $2$-categories in the strict sense but $2$-functors in the lax sense. See <cit.> for generalities on $2$-categories.

§.§ Fibered categories and sections

In the first part of this section, we quickly review $\Scal$-fibered categories. We define an $\Scal$-fibered category as a contravariant $2$-functor from $\Scal$ to the $2$-category of small categories. For simplicity, we assume every such $2$-functor to be strictly unital; in fact, this is not a severe requirement (see for example <cit.>). In detail:

An $\Scal$-fibered category $\Hbb$ is the datum of

* for every $S \in \Scal$, a category $\Hbb(S)$,

* for every morphism $f: T \rightarrow S$ in $\Scal$, a functor

\begin{equation*}
f^*: \Hbb(S) \rightarrow \Hbb(T),
\end{equation*}

called the inverse image functor along $f$,

* for every pair of composable morphisms $f: T \rightarrow S$ and $g: S \rightarrow V$ in $\Scal$, a natural isomorphism of functors $\Hbb(V) \rightarrow \Hbb(T)$

\begin{equation}\label{conn_fg}
\conn = \conn_{f,g}: (gf)^* A \xrightarrow{\sim} f^* g^* A
\end{equation}

called the connection isomorphism at $(f,g)$

such that the following conditions are satisfied:

($\Scal$-fib-0) For every $S \in \Scal$, we have $\id_S^* = \id_{\Hbb(S)}$.

($\Scal$-fib-1) For every triple of composable morphisms $f: T \rightarrow S$, $g: S \rightarrow V$ and $h: V \rightarrow W$ in $\Scal$, the diagram of functors $\Hbb(W) \rightarrow \Hbb(T)$

\begin{equation}\label{dia_conn}
\begin{tikzcd}
(hgf)^* A \arrow{rr}{\conn_{f,hg}} \arrow{d}{\conn_{gf,h}} && f^* (hg)^* \arrow{d}{\conn_{g,h}} A \\
(gf)^* h^* A \arrow{rr}{\conn_{f,g}} && f^* g^* h^* A
\end{tikzcd}
\end{equation}

is commutative.

Given a composable tuple $\underline{g} = (g_1,\dots,g_r)$ in $\Scal$, we let $\underline{g}^*$ denote the composite of inverse image functors $g_1^* \circ \cdots \circ g_r^*$ in any $\Scal$-fibered category.
In order to avoid possible confusion, we agree that giving an empty composable tuple $\underline{g}$ just means giving an object $S \in \Scal$; in this case, we set $\underline{g}^* := \id_S^* = \id_{\Hbb(S)}$.

The following result explains the full meaning of axiom ($\Scal$-fib-1); it will serve as a model for similar results obtained in <Ref> and <Ref>.

Let $\Hbb$ be a $\Scal$-fibered category, and fix a morphism $f: T \rightarrow S$ in $\Scal$. For every composable tuple in $\Scal$

\begin{equation*}
\underline{g} = (g_1,\dots,g_r)
\end{equation*}

satisfying $g_r \circ \cdots \circ g_1 = f$, consider the functor $F_{\underline{g}}: \Hbb(S) \rightarrow \Hbb(T)$ defined by the formula

\begin{equation*}
F_{\underline{g}}(A) := \underline{g}^* A.
\end{equation*}

Then, given any two tuples $\underline{g}^{(1)}$, $\underline{g}^{(2)}$ as above, all natural isomorphisms of functors $\Hbb(S) \rightarrow \Hbb(T)$

\begin{equation*}
F_{\underline{g}^{(1)}}(A) \xrightarrow{\sim} F_{\underline{g}^{(2)}}(A)
\end{equation*}

obtained by composing connection isomorphisms (and inverses thereof) coincide.

It suffices to show that, for every tuple $\underline{g}$ as in the statement, every natural isomorphism of functors $\Hbb(S) \rightarrow \Hbb(T)$

\begin{equation*}
\phi: F_{\underline{g}}(A) \xrightarrow{\sim} f^* A
\end{equation*}

obtained by composing connection isomorphisms (and inverses thereof) coincides with the composite of inverse connection isomorphisms

\begin{equation*}
\alpha_{\underline{g}}: F_{\underline{g}}(A) := g_1^* \cdots g_r^* A \xleftarrow{\conn} (g_2 g_1)^* \cdots g_r^* \xleftarrow{\conn} \dots \xleftarrow{\conn} (g_r \dots g_1)^* A = f^* A.
\end{equation*}

To see this, write $\phi$ explicitly as

\begin{equation*}
\phi: F_{\underline{g}^{(0)}} \xrightarrow{\phi_1} F_{\underline{g}^{(1)}} \xrightarrow{\phi_2} \dots \xrightarrow{\phi_N} F_{\underline{g}^{(N)}}
\end{equation*}

where we set $\underline{g}^{(0)} := \underline{g}$, $\underline{g}^{(N)} := (f)$, and each factor $\phi_i$ is either a direct or an inverse connection isomorphism; note that, by construction, the number of inverse minus the number of direct connection isomorphisms among the $\phi_i$'s equals $r-1$. We prove our claim by analyzing the following cases separately:

* Suppose that all factors $\phi_i$ are inverse connection isomorphisms. Then, by repeated applications of axiom ($\Scal$-fib-1), the claim follows by induction on $N = r-1$.

* Suppose that there exists an index $n$ with $0 < n < N$ such that $\phi_i$ is a direct connection isomorphism for $1 \leq i \leq n$ and an inverse connection isomorphism for $n + 1 \leq i \leq N$. Then we can consider the factorization

\begin{equation*}
\phi: F_{\underline{g}^{(0)}} \xrightarrow{\psi_1} F_{\underline{g}^{(n)}} \xrightarrow{\psi_2} F_{\underline{g}^{(N)}}
\end{equation*}

where $\psi_1 := \phi_n \circ \dots \circ \phi_1$ and $\psi_2 := \phi_N \circ \dots \circ \phi_{n+1}$. By the previous case, we know that every natural isomorphism

\begin{equation*}
F_{\underline{g}^{(n)}}(A) \xrightarrow{\sim} F_{\underline{g}^{(N)}}(A) := f^* A
\end{equation*}

obtained as the composite of inverse connection isomorphisms coincides with $\alpha_{\underline{g}^{(n)}}$. In particular, we have

\begin{equation*}
\psi_2 = \alpha_{\underline{g}^{(n)}} = \alpha_{\underline{g}^{(0)}} \circ \psi_1^{-1}.
\end{equation*}

The claim follows from this, since we have the equality

\begin{equation*}
\phi = \psi_2 \circ \psi_1 = \alpha_{\underline{g}^{(n)}} \circ \psi_1 = \alpha_{\underline{g}^{(0)}}.
\end{equation*}

* Suppose only that at least one of the factors $\phi_i$ is a direct connection isomorphism. We want to transform this factorization into one of the form considered in the previous case. To this end it suffices to show that, given two consecutive factors $\phi_i$ and $\phi_{i+1}$ with $\phi_i$ inverse and $\phi_{i+1}$ direct, it is possible to write the composite $\phi_{i+1} \circ \phi_i$ in the form $\phi'_{i+1} \circ \phi'_i$ with $\phi'_i$ direct and $\phi'_{i+i}$ inverse. We prove this by distinguishing the following cases:

* If $\phi_i$ and $\phi_{i+1}$ are mutually inverse, they can be just cancelled out.

* If $\phi_i$ and $\phi_{i+1}$ are not mutually inverse and the sets of morphisms where they act are disjoint from one another, then the corresponding natural transformations can be interchanged.

* If $\phi_i$ and $\phi_{i+1}$ are not mutually inverse and the sets of morphisms where they act are not disjoint, then they fit into the bottom-right corner of a square of type (<ref>). By axiom ($\Scal$-fib-1) we can replace them with the edges in the top-left corner of the same square.

Therefore the claim follows from the previous case.

This concludes the proof.

Let us briefly review sections of $\Scal$-fibered categories: this notion will play a role in the discussion about unit constraints in <Ref> and in the final part of <Ref>.

Let $\Hbb$ be an $\Scal$-fibered category.

* A section $A$ of $\Hbb$ over $\Scal$ is the datum of

* for every $S \in \Scal$, an object $A_S \in \Hbb(S)$,

* for every morphism $f: T \rightarrow S$ in $\Scal$, an isomorphism in $\Hbb(T)$

\begin{equation*}
A^* = A_f^*: f^* A_S \xrightarrow{\sim} A_T
\end{equation*}

satisfying the following condition:

($\Scal$-sect) For every pair of composable morphisms $f: T \rightarrow S$, $g: S \rightarrow V$ in $\Scal$, the diagram in $\Hbb(T)$

\begin{equation*}
\begin{tikzcd}
f^* g^* A_V \arrow{r}{A_g^*} \arrow{d}{\conn_{f,g}} & f^* A_S \arrow{d}{A_f^*} \\
(gf)^* A_V \arrow{r}{A_{gf}^*} & A_T \\
\end{tikzcd}
\end{equation*}

is commutative.

* Let $A$ and $B$ be two sections of $\Hbb$. A morphism of sections $w: A \rightarrow B$ is the datum of

* for every $S \in \Scal$, a morphism

\begin{equation*}
w_S: A_S \rightarrow B_S
\end{equation*}

satisfying the following condition:

(mor-$\Scal$-sect) For every morphism $f: T \rightarrow S$ in $\Scal$, the diagram in $\Hbb(T)$

\begin{equation*}
\begin{tikzcd}
f^* A_S \arrow{r}{w_S} \arrow{d}{A^*_f} & f^* B_S \arrow{d}{B^*_f} \\
A_T \arrow{r}{w_T} & B_T
\end{tikzcd}
\end{equation*}

is commutative.

There are natural notions of identity and of composition for morphisms between sections of a same $\Scal$-fibered categories $\Hbb$. Of course, a morphism of sections $w: A \rightarrow B$ is invertible with respect to this composition if and only if each morphism $w_S: A_S \rightarrow B_S$ is an isomorphism in $\Hbb(S)$ for every $S \in \Scal$: this yields the notion of isomorphism of sections.

§.§ Morphisms of fibered categories

In the second part of this section, we quickly review morphisms of $\Scal$-fibered categories. Let $\Hbb_1$ and $\Hbb_2$ be two $\Scal$-fibered categories as in <Ref>; for every pair of composable pair $(f,g)$ in $\Scal$, we write the connection isomorphism at $(f,g)$ for $\Hbb_1$ and $\Hbb_2$ as $\conn_{f,g}^{(1)}$ and $\conn_{f,g}^{(2)}$, respectively.

* A morphism of $\Scal$-fibered categories $R: \Hbb_1 \rightarrow \Hbb_2$ is the datum of

* for every $S \in \Scal$, a functor

\begin{equation*}
R_S: \Hbb_1(S) \rightarrow \Hbb_2(S),
\end{equation*}

* for every morphism $f: T \rightarrow S$ in $\Scal$, a natural isomorphism of functors $\Hbb_1(S) \rightarrow \Hbb_2(T)$

\begin{equation*}
\theta = \theta_f: f^* R_S(A) \xrightarrow{\sim} R_T (f^* A),
\end{equation*}

called the $R$-transition isomorphism along $f$

such that the following condition is satisfied:

(mor-$\Scal$-fib) For every pair of composable morphisms $f: T \rightarrow S$ and $g: S \rightarrow V$ in $\Scal$, the diagram of functors $\Hbb_1(V) \rightarrow \Hbb_2(T)$

\begin{equation*}
\begin{tikzcd}
(gf)^* R_V(A) \arrow{rr}{\theta_{gf}} \arrow{d}{\conn^{(2)}_{f,g}} && R_T ((gf)^* A) \arrow{d}{\conn^{(1)}_{f,g}} \\
f^* g^* R_V(A) \arrow{r}{\theta_g} & f^* R_S (g^* A) \arrow{r}{\theta_f} & R_T (f^* g^* A)
\end{tikzcd}
\end{equation*}

is commutative.

* If  we are already given a family of functors $\Rcal := \left\{R_S: \Hbb_1(S) \rightarrow \Hbb_2(S) \right\}_{S \in \Scal}$, we say that a collection of natural isomorphisms $\theta = \left\{\theta_f: f^* \circ R_S \xrightarrow{\sim} R_T \circ f^* \right\}_{f: T \rightarrow S}$ satisfying condition (mor-$\Scal$-fib) defines an $\Scal$-structure on the family $\Rcal$.

Fix $S \in \Scal$. In view of axiom ($\Scal$-fib-0) from <Ref>, condition (mor-$\Scal$-fib) in the case where $f = g = \id_S$ means that the natural isomorphism of functors $\Hbb_1(S) \rightarrow \Hbb_2(S)$

\begin{equation*}
\theta_{\id_S}: R_S(A) \xrightarrow{\sim} R_S(A)
\end{equation*}

is idempotent. Hence it must be the identity.

The full meaning of axiom (mor-$\Scal$-fib) is explained by the following result, which is the generalization of <Ref> to morphisms of $\Scal$-fibered categories:

Let $R: \Hbb_1 \rightarrow \Hbb_2$ be a morphism of $\Scal$-fibered categories, and fix a morphism $f: T \rightarrow S$ in $\Scal$. For every composable pair of composable tuples in $\Scal$

\begin{equation*}
\underline{g} = (g_1, \dots, g_r), \quad \underline{h} = (h_1, \dots, h_s)
\end{equation*}

satisfying $h_s \circ \cdots \circ h_1 \circ g_r \circ \cdots \circ g_1 = f$, consider the functor $\Hbb_1(S) \rightarrow \Hbb_2(T)$

\begin{equation*}
F^R_{(\underline{g}, \underline{h})}(A) := \underline{g}^* R_{T'}(\underline{h}^* A)
\end{equation*}

where $T'$ denotes the domain of $h_1$. Then, given any two pairs of tuples $(\underline{g}^{(1)}, \underline{h}^{(1)})$ and $(\underline{g}^{(2)}, \underline{h}^{(2)})$ as above, all natural isomorphisms of functors $\Hbb_1(S) \rightarrow \Hbb_2(T)$

\begin{equation*}
F^R_{(\underline{g}^{(1)}, \underline{h}^{(1)})}(A) \xrightarrow{\sim} F^R_{(\underline{g}^{(2)}, \underline{h}^{(2)})}(A)
\end{equation*}

obtained by composing connection isomorphisms and $R$-transition isomorphisms (and inverses thereof) coincide.

It would be possible to prove this result via a detailed case-by-case analysis as done for <Ref>; however, the mixture of connection isomorphisms and $R$-transition isomorphisms would force us to consider more cases and introduce more reduction steps in the argument. We prefer to introduce an auxiliary construction which will reduce us directly to the situation of <Ref>, thereby avoiding all additional difficulties. To this end, we need to introduce some more notation:

* We let $\Ical$ be the category with two objects, denoted $1$ and $2$, and exactly one non-identity arrow $r: 2 \rightarrow 1$.

* Given a small category $\Scal$, we consider the product category $\Scal \times \Ical$. We write an object $\Ssf \in \Scal \times \Ical$ as a pair $(S;i)$ with $S \in \Scal$ and $i \in \left\{1,2\right\}$. For every $S \in \Scal$, we let $r_S$ denote the morphism $(\id_S,r): (S;2) \rightarrow (S;1)$.
Note that there exists a natural partition of morphisms in $\Scal \times \Ical$ into the following three families, each of which is parameterized by the family of all morphisms $f: T \rightarrow S$ in $\Scal$:

* morphisms of the form $(f;1): (T;1) \rightarrow (S;1)$;

* morphisms of the form $(f;2): (T;2) \rightarrow (S;2)$;

* morphisms of the form $r_S \circ (f;2): (T;2) \rightarrow (S;1)$.

We will always use this presentation for morphisms in $\Scal \times \Ical$.

Let $R: \Hbb_1 \rightarrow \Hbb_2$ be a morphism of $\Scal$-fibered categories. Then, following <Ref>, we can define an $(\Scal \times \Ical)$-fibered category $\Hbb_1 \coprod_R \Hbb_2$ out of it, as follows:

* For every $(S;i) \in \Scal \times \Ical$, we set $(\Hbb_1 \coprod_R \Hbb_2)(S;i) := \Hbb_i(S)$.

* Given a morphism $\phi$ in $\Scal\times \Ical$, we define the functor $\phi^*$ according to the type of $\phi$:

* if $\phi = (f;1): (T;1) \rightarrow (S;1)$, we set $\phi^* A := f^* A$;

* if $\phi = (f;2): (T;2) \rightarrow (S;2)$, we set $\phi^* B := f^* B$;

* if $\phi = r_S \circ (f;2)$, we set $\phi^* A := f^* R_S(A)$.

* Given two composable morphisms $\phi$ and $\psi$ in $\Scal \times \Ical$, we define the connection isomorphism $\conn_{\phi,\psi}$ according to the type of $\phi$ and $\psi$:

(i) if $\phi = (f;1)$ and $\psi = (g;1)$, we set

\begin{equation*}
\conn_{\phi,\psi}(A): (gf)^* A \xrightarrow{\conn_{f,g}^{(1)}} f^* g^* A;
\end{equation*}

(ii) if $\phi = (f;2)$ and $\psi = (g;2)$, we set

\begin{equation*}
\conn_{\phi,\psi}(B) : (gf)^* B \xrightarrow{\conn_{f,g}^{(2)}} f^* g^* B;
\end{equation*}

(iii) if $\phi = (f;2)$ and $\psi = r_V \circ (g;2)$, we set

\begin{equation*}
\conn_{\phi,\psi}(A): (gf)^* R_V(A)  \xrightarrow{\conn_{f,g}^{(2)}} f^* g^* R_V(A);
\end{equation*}

(iv) if $\phi = r_S \circ (f;2)$ and $\psi = (g;1)$, we set

\begin{equation*}
\conn_{\phi,\psi}: (gf)^* R_S(A) \xrightarrow{\conn_{f,g}^{(2)}} f^* g^* R_V(A) \xrightarrow{\theta_g} f^* R_S(g^* A).
\end{equation*}

Let us check that this really defines an $(\Scal \times \Ical)$-fibered category.
It is clear that condition (($\Scal \times \Ical$)-fib-0) is satisfied. We need to check that condition (($\Scal \times \Ical$)-fib-1) holds as well: given three composable morphisms $\phi, \psi, \xi$ in $\Scal \times \Ical$, we have to show that the diagram

\begin{equation*}
\begin{tikzcd}
(\xi \psi \phi)^* A \arrow{rr}{\conn_{\phi,\xi \psi}} \arrow{d}{\conn_{\phi,\xi \psi}} && \phi^* (\xi \psi)^* A \arrow{d}{\conn_{\psi,\xi}} \\
(\psi \phi)^* \xi^* A \arrow{rr}{\conn_{\phi,\psi}} && \phi^* \psi^* \xi^* A
\end{tikzcd}
\end{equation*}

is commutative. We have the following possibilities, parametrized by triples of composable morphisms $f: T \rightarrow S$, $g: S \rightarrow V$ and $h: V \rightarrow W$ in $\Scal$:

* If $\phi = (f;1)$, $\psi = (g;1)$ and $\xi = (h;1)$, we obtain the diagram

\begin{equation*}
\begin{tikzcd}[font=\small]
(hgf)^* A \arrow{rr}{\conn_{f,hg}^{(1)}} \arrow{d}{\conn_{gf,h}^{(1)}} && f^* (hg)^* A \arrow{d}{\conn_{g,h}^{(1)}} \\
(gf)^* h^* A \arrow{rr}{\conn_{f,g}^{(1)}} && f^* g^* h^* A
\end{tikzcd}
\end{equation*}

which is commutative by axiom ($\Scal$-fib-1).

* If $\phi = (f;2)$, $\psi = (g;2)$ and $\xi = (h;2)$, we obtain the diagram

\begin{equation*}
\begin{tikzcd}[font=\small]
(hgf)^* B \arrow{rr}{\conn_{f,hg}^{(2)}} \arrow{d}{\conn_{gf,h}^{(2)}} && f^* (hg)^* B \arrow{d}{\conn_{g,h}^{(2)}} \\
(gf)^* h^* B \arrow{rr}{\conn_{f,g}^{(2)}} && f^* g^* h^* B
\end{tikzcd}
\end{equation*}

which is commutative by axiom ($\Scal$-fib-1).

* If $\phi = (f;2)$, $\phi = (g;2)$ and $\xi = r_W \circ (h;2)$, we obtain the diagram

\begin{equation*}
\begin{tikzcd}[font=\small]
(hgf)^* R_W(A) \arrow{rr}{\conn_{f,hg}^{(2)}} \arrow{d}{\conn_{gf,h}^{(2)}} && f^* (hg)^* R_W(A) \arrow{d}{\conn_{g,h}^{(2)}} \\
(gf)^* h^* R_W(A) \arrow{rr}{\conn_{f,g}^{(2)}} && f^* g^* h^* R_W(A)
\end{tikzcd}
\end{equation*}

which is again commutative by axiom ($\Scal$-fib-1).

* If $\phi = (f;2)$, $\psi = r_V \circ (g;2)$ and $\xi = (h;1)$, we obtain the outer part of the diagram

\begin{equation*}
\begin{tikzcd}[font=\small]
(hgf)^* R_W(A) \arrow{rr}{\conn_{f,hg}^{(2)}} \arrow{d}{\conn_{gf,h}^{(2)}} && f^* (hg)^* R_W(A) \arrow{d}{\conn_{g,h}^{(2)}} \\
(gf)^* h^* R_W(A) \arrow{rr}{\conn_{f,g}^{(2)}} \arrow{d}{\theta_h} && f^* g^* h^* R_W(A) \arrow{d}{\theta_h} \\
(gf)^* R_V(h^* A) \arrow{rr}{\conn_{f,g}^{(2)}} && f^* g^* R_V(h^* A)
\end{tikzcd}
\end{equation*}

where the upper square is commutative by axiom ($\Scal$-fib-1) and the lower square is commutative by naturality.

* Finally, if $\phi = r_S \circ (f;2)$, $\psi = (g;1)$ and $\xi = (h;1)$, we obtain the outer part of the diagram

\begin{equation*}
\begin{tikzcd}[font=\small]
(hgf)^* R_W(A) \arrow{rr}{\conn_{f,hg}^{(2)}} \arrow{d}{\conn_{gf,h}^{(2)}} && f^* (hg)^* R_W(A) \arrow{r}{\theta_{hg}} \arrow{d}{\conn_{g,h}^{(2)}} & f^* R_S((hg)^* A) \arrow{dd}{\conn_{g,h}^{(1)}} \\
(gf)^* h^* R_W(A) \arrow{rr}{\conn_{f,g}^{(2)}} \arrow{d}{\theta_h} && f^* g^* h^* R_W(A) \arrow{d}{\theta_h} \\
(gf)^* R_V(h^* A) \arrow{rr}{\conn_{f,g}^{(2)}} && f^* g^* R_V(h^* A) \arrow{r}{\theta_g} & f^* R_S(g^* h^* A)
\end{tikzcd}
\end{equation*}

where the upper-left piece is commutative by axiom ($\Scal$-fib-1), the lower-left piece is commutative by naturality, and the right-most piece is commutative by axiom (mor-$\Scal$-fib).

In fact, the argument shows that giving a morphism of $\Scal$-fibered categories $R: \Hbb_1 \rightarrow \Hbb_2$ is the same as giving an $(\Scal \times \Ical)$-fibered category $\Hbb$ satisfying $\Hbb|_{(\Scal;i)} = \Hbb_i$ for $i = 1,2$ and $r_S^* = R_S$ for all $S \in \Scal$.

As a consequence of <Ref>, this is a particular case of <Ref> over the base category $\Scal \times \Ical$.

We conclude this preliminary discussion by reviewing the notion of image of a section along a morphism of $\Scal$-fibered categories.

Let $R: \Hbb_1 \rightarrow \Hbb_2$ be a morphism of $\Scal$-fibered categories, and let $A$ be a section of $\Hbb_1$ over $\Scal$.
We define the image of $A$ under $R$ to be the section $R(A)$ of $\Hbb_2$ over $\Scal$ defined as follows:

* for every $S \in \Scal$, the object $R(A)_S \in \Hbb_2(S)$ is just $R_S(A_S)$;

* for every morphism $f: T \rightarrow S$ in $\Scal$, the isomorphism in $\Hbb_2(T)$

\begin{equation*}
R(A)_f^*: f^* R(A)_S \xrightarrow{\sim} R(A)_T
\end{equation*}

is the composite

\begin{equation*}
f^* R_S(A_S) \xrightarrow{\theta_f} R_T(f^* A_S) \xrightarrow{\sim} R_T(A_T).
\end{equation*}

Let us check that this definition indeed satisfies condition ($\Scal$-sect): given two composable morphisms $f: T \rightarrow S$ and $g: S \rightarrow V$ in $\Scal$, we have to show that the diagram in $\Hbb_2(T)$

\begin{equation*}
\begin{tikzcd}
(gf)^* R(A)_V \arrow{rr}{R(A)_{gf}^*} \arrow{d}{\conn_{f,g}^{(2)}} && R(A)_T \arrow{d}{\conn_{f,g}^{(2)}} \\
f^* g^* R(A)_V \arrow{r}{R(A)_g^*} & f^* R(A)_S \arrow{r}{R(A)_f^*} & R(A)_T
\end{tikzcd}
\end{equation*}

is commutative. Expanding the definitions, we obtain the outer part of the diagram

\begin{equation*}
\begin{tikzcd}[font=\small]
(gf)^* R_V(A_V) \arrow{rr}{\theta_{gf}} \arrow{dd}{\conn_{f,g}^{(2)}} && R_T((gf)^* A_V) \arrow{r}{A_{gf}^*} \arrow{d}{\conn_{f,g}^{(1)}} & R_T(A_T) \\
&& R_T(f^* g^* A_V) \arrow{dr}{A_g^*} \\
f^* g^* R_V(A_V) \arrow{r}{\theta_g} & f^* R_S(g^* A_V) \arrow{r}{A_g^*} \arrow{ur}{\theta_f} & f^* R_S(A_S) \arrow{r}{\theta_f} & R_T(f^* A_S) \arrow{uu}{A_f^*}
\end{tikzcd}
\end{equation*}

where the lower central piece is commutative by naturality, the left-most piece is commutative by axiom (mor-$\Scal$-fib), and the right-most piece is commutative by axiom ($\Scal$-sect). This proves the claim.

§ INTERNAL AND EXTERNAL TENSOR STRUCTURES

From now henceforth, we assume that the small category $\Scal$ admits binary products; in most concrete applications $\Scal$ also happens to possess a terminal object, but this is not necessary for our constructions.

From now until the end of <Ref> we also fix an $\Scal$-fibered category $\Hbb$.
In the present section, we start our investigations about monoidal $\Scal$-fibered categories by introducing the notions of internal and external tensor structure on $\Hbb$ together with the corresponding notions of equivalence.

From now on, we simplify the notation by systematically adopting the following conventions:

* We write all connection isomorphisms of $\Scal$-fibered categories as equalities (this is legitimate in view of <Ref>).

* We write all transition isomorphisms $\theta_f$ associated to a morphism of $\Scal$-fibered categories simply as $\theta$.
More generally, when a structure on $\Scal$-fibered category is defined by a family of natural isomorphisms parameterized by objects or morphisms of $\Scal$, we often indicate all members of this family by the same symbol, without mentioning the specific parameter involved. In particular, this will be applied to all the notation concerning tensor structures.

§.§ Tensor structures and their equivalences

To begin with, we introduce internal and external tensor structures and equivalences thereof. In order to keep the exposition as neat as possible, it is convenient to start from the coarsest possible kind of structure including only monoidality isomorphisms: in particular, we do not include associativity constraints in the picture from the beginning but rather regard them as one possible additional structure (on the same level as commutativity and unit constraints) and treat them separately in <Ref>.

* An internal tensor structure $(\otimes,m)$ on $\Hbb$ is the datum of

* for every $S \in \Scal$, a functor

\begin{equation*}
-\otimes- = -\otimes_S-: \Hbb(S) \times \Hbb(S) \rightarrow \Hbb(S),
\end{equation*}

called the internal tensor product functor over $S$,

* for every morphism $f: T \rightarrow S$ in $\Scal$, a natural isomorphism of functors $\Hbb(S) \times \Hbb(S) \rightarrow \Hbb(T)$

\begin{equation*}
m = m_f: f^* A \otimes f^* B \xrightarrow{\sim} f^*(A \otimes B),
\end{equation*}

called the internal monoidality isomorphism along $f$

satisfying the following condition:

mITS($m$ITS) For every pair of composable morphisms $f: T \rightarrow S$ and $g: S \rightarrow V$ in $\Scal$, the diagram of functors $\Hbb(V) \times \Hbb(V) \rightarrow \Hbb(T)$

\begin{equation*}
\begin{tikzcd}
(gf)^* A \otimes (gf)^* B \arrow{rr}{m} \arrow[equal]{d} && (gf)^*(A \otimes B)  \arrow[equal]{d} \\
f^* g^* A \otimes f^* g^* B \arrow{r}{m} & f^* (g^* A \otimes g^* B) \arrow{r}{m} & f^* g^* (A \otimes B)
\end{tikzcd}
\end{equation*}

is commutative.

* Let $(\otimes,m)$ and $(\otimes',m')$ be two internal tensor structures on $\Hbb$. An equivalence of internal tensor structures $e: (\otimes,m) \xrightarrow{\sim} (\otimes',m')$ is the datum of

* for every $S \in \Scal$, a natural isomorphism of functors $\Hbb(S) \times \Hbb(S) \rightarrow \Hbb(S)$

\begin{equation*}
e = e_S: A \otimes B \xrightarrow{\sim} A \otimes' B
\end{equation*}

satisfying the following condition:

(eq-ITS) For every morphism $f: T \rightarrow S$ in $\Scal$, the diagram of functors $\Hbb(S) \times \Hbb(S) \rightarrow \Hbb(T)$

\begin{equation*}
\begin{tikzcd}
f^* A \otimes f^* B \arrow{r}{m} \arrow{d}{e} & f^* (A \otimes B)  \arrow{d}{e} \\
f^* A \otimes' f^* B \arrow{r}{m'} & f^* (A \otimes' B)
\end{tikzcd}
\end{equation*}

is commutative.

Fix $S \in \Scal$. In view of axiom ($\Scal$-fib-0) of <Ref>, condition ($m$ITS) in the case where $f = g = \id_S$  means that the natural isomorphism of functors $\Hbb(S) \times \Hbb(S) \rightarrow \Hbb(S)$

\begin{equation*}
m_{\id_S}: A \otimes B \xrightarrow{\sim} A \otimes B
\end{equation*}

is idempotent. Hence it must be the identity.

The following result clarifies the meaning of axiom ($m$ITS): it guarantees that, between any two given iterations of tensor product functors and inverse image functors, it is possible to construct at most one natural isomorphism by combining connection isomorphisms and internal monoidality isomorphisms in any possible order. As the reader might expect, this is just another variant of <Ref>.

Let $(\otimes,m)$ be an internal tensor structure on $\Hbb$, and let $f: T \rightarrow S$ be a morphism in $\Scal$. For every composable pair of composable tuples in $\Scal$

\begin{equation*}
\underline{g} = (g_1, \dots, g_r), \quad \underline{h} = (h_1, \dots, h_s)
\end{equation*}

satisfying $h_s \circ \dots \circ h_1 \circ g_r \circ \dots \circ g_1 = f$, consider the functor $\Hbb(S) \times \Hbb(S) \rightarrow \Hbb(T)$

\begin{equation*}
F^{\otimes}_{(\underline{g}, \underline{h})}(A,B) := \underline{g}^* (\underline{h}^* A \otimes \underline{h}^* B).
\end{equation*}

Then, given any two pairs of tuples $(\underline{g}^{(1)},\underline{h}^{(1)})$ and $(\underline{g}^{(2)},\underline{h}^{(2)})$ as above, all possible isomorphisms of functors $\Hbb(S) \times \Hbb(S) \rightarrow \Hbb(T)$

\begin{equation*}
F^{\otimes}_{(\underline{g}^{(1)}, \underline{h}^{(1)})}(A,B) \xrightarrow{\sim} F^{\otimes}_{(\underline{g}^{(2)}, \underline{h}^{(2)})}(A,B)
\end{equation*}

obtained by composing connection isomorphisms and internal monoidality isomorphisms (and inverses thereof) coincide.

It would be possible to prove this result directly; however, the argument would be quite cumbersome due to the mixture of connection isomorphisms and internal monoidality isomorphisms. We prefer to reduce ourselves directly to the setting of usual fibered categories considered in <Ref> via the following auxiliary construction:

Let $(\otimes,m)$ be an internal tensor structure on $\Hbb$. Then, following <Ref>, we can construct a $(\Scal \times \Ical)$-fibered category $\Hbb^{\otimes}$ out of it, as follows:

* For every $S \in \Scal$ we set $\Hbb^{\otimes}(S;1) := \Hbb(S)$ and $\Hbb^{\otimes}(S;2) := \Hbb(S) \times \Hbb(S)$.

* Given a morphism $\phi$ in $\Scal \times \Ical$, we define the functor $\phi^*$ according to the type of $\phi$:

* if $\phi = (f;1): (T;1) \rightarrow (S;1)$, we set $\phi^* A := f^* A$;

* if $\phi = (f;2): (T;2) \rightarrow (S;2)$, we set $\phi^*(A,B) := (f^* A,f^* B)$;

* if $\phi = r_S \circ (f;2)$, we set $\phi^*(A,B) := f^* (A \otimes B)$.

* Give two composable morphisms $\phi$ and $\psi$ in $\Scal \times \Ical$, we define the connection isomorphism $\conn_{\phi,\psi}$ according to the type of $\phi$ and $\psi$:

(i) if $\phi = (f;1)$ and $\psi = (g;1)$, we set

\begin{equation*}
\conn_{\phi,\psi}(A): (gf)^* A \xrightarrow{\conn_{f,g}} f^* g^* A;
\end{equation*}

(ii) if $\phi = (f;2)$ and $\psi = (g;2)$, we set

\begin{equation*}
\conn_{\phi,\psi}(A,B): ((gf)^* A, (gf)^* B) \xrightarrow{(\conn_{f,g}, \conn_{f,g})} (f^* g^* A, f^* g^* B);
\end{equation*}

(iii) if $\phi = (f;2)$ and $\psi = r_V \circ (g;2)$, we set

\begin{equation*}
\conn_{\phi,\psi}(A,B): (gf)^*(A \otimes B) \xrightarrow{\conn_{f,g}} f^* g^* (A \otimes B);
\end{equation*}

(iv) if $\phi = r_S \circ (f;2)$ and $\psi = (g;1)$, we set

\begin{equation*}
\conn_{\phi,\psi}(A,B): (gf)^*(A \otimes B) \xrightarrow{\conn_{f,g}} f^* g^* (A \otimes B) \xleftarrow{m_g} f^*(g^* A \otimes g^* B).
\end{equation*}

Let us check that this construction indeed defines a $(\Scal \times \Ical)$-fibered category. The validity of condition (($\Scal \times \Ical$)-fib-0) follows trivially from axiom ($\Scal$-fib-0). Let us check that condition (($\Scal \times \Ical$)-fib-1) holds as well: given three composable morphisms $\phi,\psi,\xi$ in $\Scal \times \Ical$, we have to show that the diagram

\begin{equation*}
\begin{tikzcd}
(\xi \psi \phi)^* A \arrow{rr}{\conn_{\phi,\xi \psi}} \arrow{d}{\conn_{\psi \phi,\xi}} && \phi^* (\xi \psi)^* A \arrow{d}{\conn_{\psi,\xi}} \\
(\psi \phi)^* \xi^* A \arrow{rr}{\conn_{\phi,\psi}} && \phi^* \psi^* \xi^* A
\end{tikzcd}
\end{equation*}

is commutative. We have the following possibilities, parametrized by triples of composable morphisms $f: T \rightarrow S$, $g: S \rightarrow V$ and $h: V \rightarrow W$ in $\Scal$:

* If $\phi = (f;1)$, $\psi = (g;1)$ and $\xi = (h;1)$, we obtain the diagram

\begin{equation*}
\begin{tikzcd}[font=\small]
(hgf)^* A \arrow[equal]{rr} \arrow[equal]{d} && f^* (hg)^* A \arrow[equal]{d} \\
(gf)^* h^* A \arrow[equal]{rr} && f^* g^* h^* A
\end{tikzcd}
\end{equation*}

which is commutative by axiom ($\Scal$-fib-1).

* If $\phi = (f;2)$, $\psi = (g;2)$ and $\xi = (h;2)$, we obtain the diagram

\begin{equation*}
\begin{tikzcd}[font=\small]
((hgf)^* A, (hgf)^* B) \arrow[equal]{rr} \arrow[equal]{d} && (f^* (hg)^* A, f^* (hg)^* B) \arrow[equal]{d} \\
((gf)^* h^* A, (gf)^* h^* B) \arrow[equal]{rr} && (f^* g^* h^* A, f^* g^* h^* B)
\end{tikzcd}
\end{equation*}

which is commutative by axiom ($\Scal$-fib-1).

* If $\phi = (f;2)$, $\phi = (g;2)$ and $\xi = r_W \circ (h;2)$, we obtain the diagram

\begin{equation*}
\begin{tikzcd}[font=\small]
(hgf)^* (A \otimes B) \arrow[equal]{rr} \arrow[equal]{d} && f^* (hg)^* (A \otimes B) \arrow[equal]{d} \\
(gf)^* h^* (A \otimes B) \arrow[equal]{rr} && f^* g^* h^* (A \otimes B)
\end{tikzcd}
\end{equation*}

which is again commutative by axiom ($\Scal$-fib-1).

* If $\phi = (f;2)$, $\psi = r_V \circ (g;2)$ and $\xi = (h;1)$, we obtain (the outer rectangle of) the diagram

\begin{equation*}
\begin{tikzcd}[font=\small]
(hgf)^* (A \otimes B) \arrow[equal]{rr} \arrow[equal]{d} && f^* (hg)^* (A \otimes B) \arrow[equal]{d} \\
(gf)^* h^* (A \otimes B) \arrow[equal]{rr} && f^* g^* h^* (A \otimes B) \\
(gf)^* (h^* A \otimes h^* B) \arrow[equal]{rr} \arrow{u}{m} && f^* g^* (h^* A \otimes h^* B) \arrow{u}{m}
\end{tikzcd}
\end{equation*}

where the upper square is commutative by axiom ($\Scal$-fib-1) and the lower square is commutative by naturality.

* If $\phi = r_S \circ (f;2)$, $\psi = (g;1)$ and $\xi = (h;1)$, we obtain (the outer rectangle of) the diagram

\begin{equation*}
\begin{tikzcd}[font=\small]
(hgf)^* (A \otimes B) \arrow[equal]{rr} \arrow[equal]{d} && f^* (hg)^* (A \otimes B)  \arrow[equal]{d} & f^* ((hg)^* A \otimes (hg)^* B) \arrow[equal]{dd} \arrow{l}{m} \\
(gf)^* h^* (A \otimes B) \arrow[equal]{rr}  && f^* g^* h^* (A \otimes B)  \\
(gf)^* (h^* A \otimes h^* B) \arrow[equal]{rr} \arrow{u}{m} && f^* g^* (h^* A \otimes h^* B) \arrow{u}{m} & f^* (g^* h^* A \otimes g^* h^* B) \arrow{l}{m}
\end{tikzcd}
\end{equation*}

where the upper-left piece is commutative by axiom ($\Scal$-fib-1), the lower-left piece is commutative by naturality, and the right-most piece is commutative by axiom ($m$ITS).

As a consequence of <Ref>, this is just a particular case of <Ref>.

In a similar way, we now introduce external tensor structures and equivalences thereof.

* An external tensor structure $(\boxtimes,m)$ on $\Hbb$ is the datum of

* for every $S_1, S_2 \in \Scal$, a functor

\begin{equation*}
-\boxtimes- = - \boxtimes_{S_1,S_2} -: \Hbb(S_1) \times \Hbb(S_2) \rightarrow \Hbb(S_1 \times S_2),
\end{equation*}

called the external tensor product functor over $(S_1,S_2)$,

* for every choice of morphisms $f_i: T_i \rightarrow S_i$ in $\Scal$, $i = 1,2$, a natural isomorphism of functors $\Hbb(S_1) \times \Hbb(S_2) \rightarrow \Hbb(T_1 \times T_2)$

\begin{equation*}
m = m_{f_1,f_2}: f_1^* A_1 \boxtimes f_2^* A_2 \xrightarrow{\sim} (f_1 \times f_2)^*(A_1 \boxtimes A_2),
\end{equation*}

called the external monoidality isomorphism along $(f_1,f_2)$

satisfying the following condition:

($m$ETS) For every choice of composable morphisms $f_i: T_i \rightarrow S_i$, $g_i: S_i \rightarrow V_i$, $i = 1,2$, the diagram of functors $\Hbb(V_1) \times \Hbb(V_2) \rightarrow \Hbb(T_1 \times T_2)$

\begin{equation*}
\begin{tikzcd}[font=\small]
(g_1 f_1)^* A_1 \boxtimes (g_2 f_2)^* A_2  \arrow{rr}{m} \arrow[equal]{d} && (g_1 f_1 \times g_2 f_2)^* (A_1 \boxtimes A_2)  \arrow[equal]{d} \\
f_1^* g_1^* A_1 \boxtimes f_2^* g_2^* A_2  \arrow{r}{m} & (f_1 \times f_2)^* (g_1^* A_1 \boxtimes g_2^* A_2) \arrow{r}{m} & (f_1 \times f_2)^* (g_1 \times g_2)^* (A_1 \boxtimes A_2)
\end{tikzcd}
\end{equation*}

is commutative.

* Let $(\boxtimes',m')$ and $(\boxtimes,m)$ be two external tensor structures on $\Hbb$. An equivalence of external tensor structures $e: (\boxtimes',m') \xrightarrow{\sim} (\boxtimes,m)$ is the datum of

* for every $S_1, S_2 \in \Scal$, a natural isomorphism of functors $\Hbb(S_1) \times \Hbb(S_2) \rightarrow \Hbb(S_1 \times S_2)$

\begin{equation*}
e = e_{S_1,S_2}: A_1 \boxtimes' A_2 \xrightarrow{\sim} A_1 \boxtimes A_2
\end{equation*}

satisfying the following condition:

(eq-ETS) For every pair of morphisms $f_i: T_i \rightarrow S_i$ in $\Scal$, the diagram of functors $\Hbb(S_1) \times \Hbb(S_2) \rightarrow \Hbb(T_1 \times T_2)$

\begin{equation*}
\begin{tikzcd}
f_1^* A_1 \boxtimes' f_2^* A_2 \arrow{rr}{m'} \arrow{d}{e} && (f_1 \times f_2)^*(A_1 \boxtimes' A_2)  \arrow{d}{e} \\
f_1^* A_1 \boxtimes f_2^* A_2 \arrow{rr}{m} && (f_1 \times f_2)^*(A_1 \boxtimes A_2)
\end{tikzcd}
\end{equation*}

is commutative.

For $i = 1,2$ fix $S_i \in \Scal$. In view of axiom ($\Scal$-fib-0) of <Ref>, condition ($m$ETS) in the case where $f_i = g_i = \id_{S_i}$ means that the natural isomorphism of functors $\Hbb(S_1) \times \Hbb(S_2) \rightarrow \Hbb(S_1 \times S_2)$

\begin{equation*}
m_{\id_{S_1},\id_{S_2}}: A_1 \boxtimes A_2 \xrightarrow{\sim} A_1 \boxtimes A_2
\end{equation*}

is idempotent. Hence it must be the identity.

As we now explain, the result of <Ref> has an analogue in the setting of external tensor structures, which clarifies the meaning of axiom ($m$ETS): between any two given iterations of external tensor product functors and inverse image functors (respecting the single factors), it is possible to construct at most one natural isomorphism by combining connection isomorphisms and external monoidality isomorphisms in any possible order.

Let $(\boxtimes,m)$ be an external tensor structure on $\Hbb$ and, for $i = 1,2$, let $f_i: T_i \rightarrow S_i$ be a morphism in $\Scal$. For every choice of two composable pairs of composable tuples in $\Scal$

\begin{equation*}
\underline{g}_i = (g_{i,1}, \dots, g_{i,r}), \quad \underline{h}_i = (h_{i,1}, \dots, h_{i,s}) \qquad (i = 1,2)
\end{equation*}

satisfying $h_{i,s} \circ \dots \circ h_{i,1} \circ g_{i,r} \circ \dots \circ g_{i,1} = f_i$, consider the functor $\Hbb(S_1) \times \Hbb(S_2) \rightarrow \Hbb(T_1 \times T_2)$

\begin{equation*}
F^{\boxtimes}_{(\underline{g}_1, \underline{h}_1), (\underline{g}_2, \underline{h}_2)}(A_1,A_2) := (\underline{g}_1 \times \underline{g}_2)^* (\underline{h}_1^* A_1 \boxtimes \underline{h}_2^* A_2).
\end{equation*}

Then, given, for $i = 1,2$, any two pairs of tuples $(\underline{g}_i^{(1)},\underline{h}_i^{(1)})$ and $(\underline{g}_i^{(2)},\underline{h}_i^{(2)})$ as above, all isomorphisms of functors $\Hbb(S_1) \times \Hbb(S_2) \rightarrow \Hbb(T_1 \times T_2)$

\begin{equation*}
F^{\boxtimes}_{(\underline{g}_1^{(1)}, \underline{h}_1^{(1)}), (\underline{g}_2^{(1)}, \underline{h}_2^{(1)})} \xrightarrow{\sim} F^{\boxtimes}_{(\underline{g}_1^{(2)}, \underline{h}_1^{(2)}), (\underline{g}_2^{(2)}, \underline{h}_2^{(2)})}
\end{equation*}

obtained by composing connection isomorphisms and external monoidality isomorphisms (and inverses thereof) coincide.

As in the case of internal tensor structures, we can reduce the proof of this result to the setting of usual fibered categories considered in <Ref> via an auxiliary construction:

Let $(\boxtimes,m)$ be an internal tensor structure on $\Hbb$. Then, following <Ref>, we can construct an $(\Scal^2 \times \Ical)$-fibered category $\Hbb^{\boxtimes}$ out of it, as follows:

* For every $S_1,S_2 \in \Scal$ we set $\Hbb^{\boxtimes}(S_1,S_2;1) := \Hbb(S_1) \times \Hbb(S_2)$ and $\Hbb^{\boxtimes}(S_1,S_2;2) := \Hbb(S_1 \times S_2)$.

* Given a morphism $\phi$ in $\Scal^2 \times \Ical$, we define the functor $\phi^*$ according to the type of $\phi$:

* if $\phi = (f_1,f_2;1): (T_1,T_2;1) \rightarrow (S_1,S_2;1)$, we set $\phi^*(A_1,A_2) := (f_1^* A_1, f_2^* A_2)$;

* if $\phi = (f,2): (T_1,T_2;2) \rightarrow (S_1,S_2;2)$, we set $\phi^* A := (f_1 \times f_2)^* A$;

* if $\phi = r_{S_1,S_2} \circ (f_1,f_2;2)$, we set $\phi^*(A_1,A_2) := (f_1 \times f_2)^* (A_1 \boxtimes A_2)$.

* Given two composable morphisms $\phi$ and $\psi$ in $\Scal^2 \times \Ical$, we define the connection isomorphism $\conn_{\phi,\psi}$ according to the type of $\phi$ and $\psi$:

(i) if $\phi = (f_1,f_2;1)$ and $\psi = (g_1,g_2;1)$, we set

\begin{equation*}
\conn_{\phi,\psi}(A_1,A_2): ((g_1 f_1)^* A_1, (g_2 f_2)^* A_2) \xrightarrow{(\conn_{f_1,g_1}, \conn_{f_2,g_2})} (f_1^* g_1^* A_1, f_2^* g_2^* A_2);
\end{equation*}

(ii) if $\phi = (f_1,f_2;2)$ and $\psi = (g_1,g_2;2)$, we set

\begin{equation*}
\conn_{\phi,\psi}(A): (g_1 f_1 \times g_2 f_2)^* A \xrightarrow{\conn_{f_1 \times f_2,g_1 \times g_2}} (f_1 \times f_2)^* (g_1 \times g_2)^* A;
\end{equation*}

(iii) if $\phi = (f,2)$ and $\psi = r_V \circ (g,2)$, we set

\begin{equation*}
\conn_{\phi,\psi}(A_1,A_2): (g_1 f_1 \times g_2 f_2)^*(A_1 \boxtimes A_2) \xrightarrow{\conn_{f_1 \times f_2,g_1 \times g_2}} (f_1 \times f_2)^* (g_1 \times g_2)^* (A_1 \boxtimes A_2);
\end{equation*}

(iv) if $\phi = r_S \circ (f,2)$ and $\psi = (g,1)$, we set

\begin{equation*}
\begin{tikzcd}
\conn_{\phi,\psi}(A_1,A_2): & (g_1 f_1 \times g_2 f_2)^*(A_1 \boxtimes A_2) \arrow{d}{\conn_{f_1 \times f_2,g_1 \times g_2}} \\
& (f_1 \times f_2)^* (g_1 \times g_2)^* (A_1 \boxtimes A_2) & \arrow{l}{m_{g_1,g_2}} (f_1 \times f_2)^*(g_1^* A_1 \boxtimes g_2^* A_2).
\end{tikzcd}
\end{equation*}

Arguing in the same way as in <Ref>, one can check that this construction indeed defines a $(\Scal^2 \times \Ical)$-fibered category; we omit the details.

As a consequence of <Ref>, this is just a particular case of <Ref>.

§.§ Correspondence between internal and external tensor structures

We now move towards the main goal of the present section: we want to prove that, modulo equivalence, giving an internal tensor structure on $\Hbb$ is the same as giving an external tensor structure on it.

The following result shows how to extend the classical formula (<ref>) to a construction from internal to external tensor structures:

Let $(\otimes,m)$ be an internal tensor structure on $\Hbb$. Then, assigning

* to every $S_1, S_2 \in \Scal$, the functor

\begin{equation*}
-\boxtimes- = -\boxtimes_{S_1,S_2}-: \Hbb(S_1) \times \Hbb(S_2) \rightarrow \Hbb(S_1 \times S_2)
\end{equation*}

defined by the formula

\begin{equation*}
A_1 \boxtimes A_1 := pr^{12*}_1 A_1 \otimes pr^{12*}_2 A_2,
\end{equation*}

* to every choice of morphisms $f_i: T_i \rightarrow S_i$ in $\Scal$, $i = 1,2$, the natural isomorphism of functors $\Hbb(S_1) \times \Hbb(S_2) \rightarrow \Hbb(T_1 \times T_2)$

\begin{equation*}
m^e = m^e_{f_1,f_2}: f_1^* A_1 \boxtimes f_2^* A_2 \xrightarrow{\sim} (f_1 \times f_2)^*(A_1 \boxtimes A_2)
\end{equation*}

defined as the composite

\begin{equation*}
\begin{tikzcd}[font=\small]
f_1^* A_1 \boxtimes f_2^* A_2 \arrow[equal]{d} && (f_1 \times f_2)^* (A_1 \boxtimes A_2) \arrow[equal]{d} \\
pr^{12,*}_1 f_1^* A_1 \otimes pr^{12,*}_2 f_2^* A_2 \arrow[equal]{r} & (f_1 \times f_2)^* pr^{12,*}_1 A_1 \otimes (f_1 \times f_2)^* pr^{12,*}_2 A_2  \arrow{r}{m} & (f_1 \times f_2)^* (pr^{12,*}_1 A_1 \otimes pr^{12,*}_2 A_2)
\end{tikzcd}
\end{equation*}

defines an external tensor structure $(\boxtimes,m^e)$ on $\Hbb$.

Let us check that this definition satisfies condition ($m$ETS): given, for $i = 1,2$, two composable morphisms $f_i: T_i \rightarrow S_i$ and $g_i: S_i \rightarrow V_i$ in $\Scal$, we have to show that the diagram of functors $\Hbb(V_1) \times \Hbb(V_2) \rightarrow \Hbb(T_1 \times T_2)$

\begin{equation*}
\begin{tikzcd}
(g_1 f_1)^* A_1 \boxtimes (g_2 f_2)^* A_2 \arrow{rr}{m^e} \arrow[equal]{d} && (g_1 f_1 \times g_2 f_2)^* (A_1 \boxtimes A_2)   \arrow[equal]{d} \\
f_1^* g_1^* A_1 \boxtimes f_1^* g_1^* A_2 \arrow{r}{m^e} & (f_1 \times f_2)^* (g_1^* A_1 \boxtimes g_2^* A_2) \arrow{r}{m^e} & (f_1 \times f_2)^* (g_1 \times g_2)^* (A_1 \boxtimes A_2)
\end{tikzcd}
\end{equation*}

is commutative. Unwinding the definitions in terms of the internal tensor product, we obtain the more explicit diagram

\begin{equation*}
\begin{tikzcd}[font=\small]
(g_{12} f_{12})^* pr^{12,*}_{1} A_1 \otimes (g_{12} f_{12})^* pr^{12,*}_{2} A_2 \arrow{r}{m} \arrow[equal]{d} & (g_1 f_1 \times g_2 f_2)^* (pr^{12,*}_{1} A_1 \otimes pr^{12,*}_{2} A_2) \arrow[equal]{d} \\
pr^{12,*}_{1} (g_1 f_1)^* A_1 \otimes pr^{12,*}_{2} (g_2 f_2)^* A_2 \arrow[equal]{u} \arrow[equal]{d} & f_{12}^* g_{12}^* (pr^{12,*}_{1} A_1 \otimes pr^{12,*}_{2} A_2) \\
pr^{12,*}_{1} f_1^* g_1^* A_1 \otimes pr^{12,*}_{2} f_2^* g_2^* A_2 \arrow[equal]{d} & f_{12}^*(g_{12}^* pr^{12,*}_{1} A_1 \otimes g_{12}^* pr^{12,*}_{2} A_2) \arrow{u}{m} \\
f_{12}^* pr^{12,*}_{1} g_1^* A_1 \otimes f_{12}^* pr^{12,*}_{2} g_2^* A_2 \arrow{r}{m} & f_{12}^* (pr^{12,*}_{1} g_1^* A_1 \otimes pr^{12,*}_{2} g_2^* A_2) \arrow[equal]{u}
\end{tikzcd}
\end{equation*}

that we decompose as

\begin{equation*}
\begin{tikzcd}[font=\small]
\bullet \arrow{rr}{m} \arrow[equal]{d} && \bullet \arrow[equal]{d} \\
\bullet \arrow[equal]{u} \arrow[equal]{d} && \bullet \\
\bullet \arrow[equal]{d} & f_{12}^* g_{12}^* pr^{12*}_{1} A_1 \otimes f_{12}^* g_{12}^* pr^{12*}_{2} A_2 \arrow[equal]{uul} \arrow[equal]{dl} \arrow{r}{m} & \bullet \arrow{u}{m} \\
\bullet \arrow{rr}{m} && \bullet \arrow[equal]{u}
\end{tikzcd}
\end{equation*}

Here, the left-most piece is commutative by <Ref>, the upper-right piece is commutative by axiom ($m$ITS), and the lower-right piece is commutative by naturality. This concludes the proof.

Conversely, the following result shows how to turn the classical formula (<ref>) into a construction from external to internal tensor structures:

Let $(\boxtimes,m)$ be an external tensor structure on $\Hbb$. Then, assigning

* to every $S \in \Scal$, the functor

\begin{equation*}
-\otimes- = -\otimes_S-: \Hbb(S) \times \Hbb(S) \rightarrow \Hbb(S)
\end{equation*}

defined by the formula

\begin{equation*}
A \otimes B := \Delta_S^*(A \boxtimes B),
\end{equation*}

* to every morphism $f: T \rightarrow S$ in $\Scal$, the natural isomorphism of functors $\Hbb(S) \times \Hbb(S) \rightarrow \Hbb(T)$

\begin{equation*}
m^i = m^i_f: f^* A \otimes f^* B \xrightarrow{\sim} f^*(A \otimes B)
\end{equation*}

defined as the composite

\begin{equation*}
\begin{tikzcd}[font=\small]
f^*A \otimes f^*B \arrow[equal]{d} && f^*(A \otimes B)   \arrow[equal]{d} \\
\Delta_T^*(f^*A \boxtimes f^*B) \arrow{r}{m} & \Delta_T^*(f \times f)^*(A \boxtimes B) \arrow[equal]{r} & f^* \Delta_S^*(A \boxtimes B)
\end{tikzcd}
\end{equation*}

defines an internal tensor structure $(\otimes,m^i)$ on $\Hbb$.

Let us check that this definition satisfies condition ($m$ITS): given two composable morphisms $f: T \rightarrow S$ and $g: S \rightarrow V$, we have to show that the diagram of functors $\Hbb(V) \times \Hbb(V) \rightarrow \Hbb(T)$

\begin{equation*}
\begin{tikzcd}
(gf)^* A \otimes (gf)^* B  \arrow{rr}{m^i} \arrow[equal]{d} && (gf)^*(A \otimes B) \arrow[equal]{d} \\
f^* g^* A \otimes f^* g^* B \arrow{r}{m^i} & f^* (g^* A \otimes g^* B) \arrow{r}{m^i} & f^* g^* (A \otimes B)
\end{tikzcd}
\end{equation*}

is commutative. Unwinding the definitions in terms of the external tensor product, we obtain the more explicit diagram

\begin{equation*}
\begin{tikzcd}[font=\small]
\Delta_T^*((gf)^* A \otimes (gf)^* B) \arrow{r}{m} \arrow[equal]{d} & \Delta_T^*(gf \times gf)^*(A \boxtimes B) \arrow[equal]{r} & (gf)^* \Delta_V^*(A \boxtimes B) \arrow[equal]{d} \\
\Delta_T^*(f^* g^* A \boxtimes f^* g^* B) \arrow{d}{m} && f^* g^* \Delta_V^*(A \boxtimes B) \arrow[equal]{d} \\
\Delta_T^*(f \times f)^*(g^* A \boxtimes g^* B)	\arrow[equal]{r} & f^* \Delta_S^*(g^* A \boxtimes g^* B) \arrow{r}{m} & f^* \Delta_S^* (g \times g)^*(A \boxtimes B)
\end{tikzcd}
\end{equation*}

that we decompose as

\begin{equation*}
\begin{tikzcd}[font=\small]
\bullet \arrow{r}{m} \arrow[equal]{d} & \bullet \arrow[equal]{r} & \bullet \arrow[equal]{d} \\
\bullet \arrow{d}{m} & \Delta_T^*(f \times f)^*(g \times g)^*(A \boxtimes B) \arrow[equal]{u} \arrow[equal]{dr} & \bullet \arrow[equal]{d} \\
\bullet	\arrow[equal]{r} \arrow{ur}{m} & \bullet \arrow{r}{m} & \bullet
\end{tikzcd}
\end{equation*}

Here, the upper-left piece is commutative by axiom ($m$ETS), the upper-right pice is commutative by <Ref>, and the lower piece is commutative by naturality. This concludes the proof.

We can finally prove the main result of this section, asserting that the two constructions just described are canonically mutually inverse modulo equivalence:

The constructions of <Ref> and <Ref> canonically define mutually inverse bijections between equivalence classes of internal and external tensor structures on $\Hbb$.

Start from an internal tensor structure $(\otimes,m)$ on $\Hbb$, and let $(\otimes',m')$ denote the internal tensor structure obtained from it by applying first <Ref> and then <Ref>: concretely, for every $S \in \Scal$, it is defined by the formula

\begin{equation*}
A \otimes' B := \Delta_S^*(pr^{12,*}_1 A \otimes pr^{12,*}_2 B).
\end{equation*}

We want to construct a canonical equivalence $e: (\otimes,m) \xrightarrow{\sim} (\otimes',m')$.
To this end, for every $S \in \Scal$ we define an isomorphism of functors $\Hbb(S) \times \Hbb(S) \rightarrow \Hbb(S)$

\begin{equation*}
e = e_S: A \otimes B \xrightarrow{\sim} A \otimes' B
\end{equation*}

by taking the composite

\begin{equation*}
A \otimes B = \Delta_S^* pr^{12,*}_1 A \otimes \Delta_S^* pr^{12,*}_2 B \xrightarrow{m} \Delta_S^* (pr^{12,*}_1 A \otimes pr^{12,*}_2 B) =: A \otimes' B.
\end{equation*}

We claim that, as $S$ varies in $\Scal$, these isomorphisms satisfy condition (eq-ITS): given a morphism $f: T \rightarrow S$ in $\Scal$, we have to check that the diagram of functors $\Hbb(S) \times \Hbb(S) \rightarrow \Hbb(T)$

\begin{equation*}
\begin{tikzcd}
f^* A \otimes f^* B \arrow{r}{m} \arrow{d}{e} & f^* (A \otimes B)  \arrow{d}{e} \\
f^* A \otimes' f^* B \arrow{r}{m'} & f^* (A \otimes' B)
\end{tikzcd}
\end{equation*}

is commutative. Unwinding the definitions, we obtain the more explicit diagram

\begin{equation*}
\begin{tikzcd}[font=\small]
& \Delta_T^* pr^{12,*}_1 f^* A \otimes \Delta_T^* pr^{12,*}_2 f^* B \arrow{r}{m} & \Delta_T^* (pr^{12,*}_1 f^* A \otimes pr^{12,*}_2 f^* B) \arrow[equal]{d} \\
f^* A \otimes f^* B \arrow[equal]{ur} \arrow{dd}{m} && \Delta_T^* ((f \times f)^* pr^{12,*}_1 A \otimes (f \times f)^* pr^{12,*}_2 B) \arrow{d}{m} \\
&& \Delta_T^* (f \times f)^* (pr^{12,*}_1 A \otimes pr^{12,*}_2 B) \arrow[equal]{d} \\
f^* (A \otimes B) \arrow[equal]{r} & f^*(\Delta_S^* pr^{12,*}_1 A \otimes \Delta_S^* pr^{12,*}_2 B) \arrow{r}{m} & f^* (\Delta_S^* (pr^{12,*}_1 A \otimes pr^{12,*}_2 B))
\end{tikzcd}
\end{equation*}

that we decompose as

\begin{equation*}
\begin{tikzcd}[font=\small]
& \bullet \arrow{r}{m} \arrow[equal]{d} & \bullet \arrow[equal]{d} \\
\bullet \arrow[equal]{ur} \arrow{dd}{m} \arrow[equal]{dr} & \Delta_T^* (f \times f)^* pr^{12,*}_1 A \otimes \Delta_T^* (f \times f)^* pr^{12,*}_2 B \arrow{r}{m} \arrow[equal]{d} & \bullet \arrow{d}{m} \\
& f^* \Delta_S^* pr^{12,*}_1 A \otimes f^* \Delta_S^* pr^{12,*}_2 B \arrow{d}{m} & \bullet \arrow[equal]{d} \\
\bullet \arrow[equal]{r} & \bullet \arrow{r}{m} & \bullet
\end{tikzcd}
\end{equation*}

Here, the upper-left piece is commutative by <Ref>, the lower-left and upper-right pieces are commutative by naturality, and the lower-right piece is commutative by <Ref>. This proves the claim.

Conversely, start from an external tensor structure $(\boxtimes,m)$ on $\Hbb$, and let $(\boxtimes',m')$ denote the external tensor structure obtained from it by applying first <Ref> and then <Ref>: concretely, for every $S_1,S_2 \in \Scal$, it is defined by the formula

\begin{equation*}
A_1 \boxtimes' A_2 := \Delta_{S_1 \times S_2}^*(pr_1^* A_1 \boxtimes pr_2^* A_2).
\end{equation*}

We want to construct a canonical equivalence $e: (\boxtimes',m') \xrightarrow{\sim} (\boxtimes,m)$.
To this end, for every $S_1, S_2 \in \Scal$ we define an isomorphism of functors $\Hbb(S_1) \times \Hbb(S_2) \rightarrow \Hbb(S_1 \times S_2)$

\begin{equation*}
e = e_{S_1,S_2}: A_1 \boxtimes' A_2 \xrightarrow{\sim} A_1 \boxtimes A_2
\end{equation*}

by taking the composite

\begin{equation*}
A_1 \boxtimes' A_2 := \Delta_{S_1 \times S_2}^* (pr^{12,*}_1 A_1 \boxtimes pr^{12,*}_2 A_2) \xrightarrow{m} \Delta_{S_1 \times S_2}^* (pr^{12}_1 \times pr^{12}_2)^* (A_1 \boxtimes A_2) = A_1 \boxtimes A_2.
\end{equation*}

We claim that, as $S_1,S_2$ vary in $\Scal$, these isomorphisms satisfy condition (eq-ETS): given two morphisms $f_i: T_i \rightarrow S_i$ in $\Scal$, $i = 1,2$, we have to show that the diagram of functors $\Hbb(S_1) \times \Hbb(S_2) \rightarrow \Hbb(T_1 \times T_2)$

\begin{equation*}
\begin{tikzcd}
f_1^* A_1 \boxtimes' f_2^* A_2 \arrow{r}{m'} \arrow{d}{e} & (f_1 \times f_2)^* (A_1 \boxtimes' A_2)  \arrow{d}{e} \\
f_1^* A_1 \boxtimes f_2^* A_2 \arrow{r}{m} & (f_1 \times f_2)^* (A_1 \boxtimes A_2)
\end{tikzcd}
\end{equation*}

is commutative. Unwinding the definitions, we obtain the outer part of the diagram

\begin{equation*}
\begin{tikzcd}[font=\tiny]
\Delta_{T_1 \times T_2}^* (pr^{12,*}_1 f_1^* A_1 \boxtimes pr^{12}_2 f_2^* A_2) \arrow{r}{m} \arrow[equal]{d} & \Delta_{T_1 \times T_2}^* (pr^{12}_1 \times pr^{12}_2)^* (f_1^* A_1 \boxtimes f_2^* A_2) \arrow[equal]{r} & f_1^* A_1 \boxtimes f_2^* A_2 \arrow{dd}{m} \\
\Delta_{T_1 \times T_2}^* (f_{12}^* pr^{12,*}_1 A_1 \boxtimes f_{12}^* pr^{12,*}_2 A_2) \arrow{d}{m} \\
\Delta_{T_1 \times T_2}^* (f_{12} \times f_{12})^* (pr^{12,*}_1 A_1 \boxtimes pr^{12,*}_2 A_2) \arrow[equal]{d} && (f_1 \times f_2)^* (A_1 \boxtimes A_2)\\
f_{12}^* \Delta_{S_1 \times S_2}^* (pr^{12,*}_1 A_1 \boxtimes pr^{12,*}_2 A_2) \arrow{r}{m} & f_{12}^* \Delta_{S_1 \times S_2}^* (pr^{12}_1 \times pr^{12}_2)^* (A_1 \boxtimes A_2) \arrow[equal]{ur}
\end{tikzcd}
\end{equation*}

that we decompose as

\begin{equation*}
\begin{tikzcd}[font=\small]
\bullet \arrow{r}{m} \arrow[equal]{d} & \bullet \arrow[equal]{r} \arrow{d}{m} & \bullet \arrow{dd}{m} \\
\bullet \arrow{d}{m} & \Delta_{T_1 \times T_2}^* (pr^{12}_1 \times pr^{12}_2)^* f_{12}^* (A_1 \boxtimes A_2) \arrow[equal]{dr} \arrow[equal]{d} \\
\bullet \arrow{r}{m} \arrow[equal]{d} & \Delta_{T_1 \times T_2}^* ((f_1 \times f_2) \times (f_1 \times f_2))^* (pr^{12}_1 \times pr^{12}_2)^* (A_1 \boxtimes A_2) \arrow[equal]{d} & \bullet \\
\bullet \arrow{r}{m} & \bullet \arrow[equal]{ur}
\end{tikzcd}
\end{equation*}

Here, the upper-left piece is commutative by <Ref>, the lower-left and upper-right pieces are commutative by naturality, and the lower-left piece is commutative by <Ref>. This proves the claim.

The constructions described in the second part of this section will serve as a model for all the main constructions of this paper. In the course of the next three sections we study associativity, commutativity, and unit constraints in the setting of internal and external tensor structures. In each case, we follow the same route as above, namely: firstly, we introduce the relevant constraint both in the internal and in the external setting, and we refine the corresponding notion of equivalence accordingly; secondly, we explain how to turn an internal constraint into an external one and conversely along the constructions of <Ref> and <Ref>; thirdly, we refine the bijection of <Ref> taking the relevant constraint into account. We do not discuss how to extend the results of <Ref> and <Ref> so as to include the additional constraints, since we do not need such an extension for our applications; however, we often make use of these two auxiliary results in order to simplify our computations.

§ ASSOCIATIVITY CONSTRAINTS

The goal of this section is to introduce associativity constraint in the setting of internal and of external tensor structures and to compare them.

The notion of associativity constraint for single monoidal categories comes from <cit.>; in the case of fibered categories, one needs to require inverse image functors to respect associativity constraints as in <cit.>. The latter definition can be formulated in our language of internal tensor structures as follows:

Let $(\otimes,m)$ be an internal tensor structure on $\Hbb$.

* An internal associativity constraint $a$ on $(\otimes,m)$ is the datum of

* for every $S \in \Scal$, a natural isomorphism between functors $\Hbb(S) \times \Hbb(S) \times \Hbb(S) \rightarrow \Hbb(S)$

\begin{equation*}
a = a_S: (A \otimes B) \otimes C \xrightarrow{\sim} A \otimes (B \otimes C)
\end{equation*}

satisfying the following conditions:

($a$ITS-1) For every $S \in \Scal$, the diagram of functors $\Hbb(S) \times \Hbb(S) \times \Hbb(S) \times \Hbb(S) \rightarrow \Hbb(S)$

\begin{equation*}
\begin{tikzcd}
((A \otimes B) \otimes C) \otimes D \arrow{d}{a} \arrow{rr}{a} && (A \otimes B) \otimes (C \otimes D) \arrow{d}{a} \\
(A \otimes (B \otimes C)) \otimes D \arrow{r}{a} & A \otimes ((B \otimes C) \otimes D) \arrow{r}{a} & A \otimes (B \otimes (C \otimes D))
\end{tikzcd}
\end{equation*}

is commutative.

($a$ITS-2) For every morphism $f: T \rightarrow S$ in $\Scal$, the diagram of functors $\Hbb(S) \times \Hbb(S) \times \Hbb(S) \rightarrow \Hbb(T)$

\begin{equation*}
\begin{tikzcd}
(f^*A \otimes f^*B) \otimes f^*C \arrow{r}{m} \arrow{d}{a} & f^*(A \otimes B) \otimes f^*C \arrow{r}{m} & f^*((A \otimes B) \otimes C) \arrow{d}{a} \\
f^*A \otimes (f^*B \otimes f^*C) \arrow{r}{m} & f^*A \otimes f^*(B \otimes C) \arrow{r}{m} & f^*(A \otimes (B \otimes C))
\end{tikzcd}
\end{equation*}

is commutative.

We say that $(\otimes,m;a)$ is an associative internal tensor structure on $\Hbb$.

* Let $(\otimes,m;a)$ and $(\otimes',m';a')$ be two associative internal tensor structures on $\Hbb$. An equivalence of associative internal tensor structures $e: (\otimes,m;a) \xrightarrow{\sim} (\otimes',m;a')$ is an equivalence of internal tensor structures $e: (\otimes,m) \xrightarrow{\sim} (\otimes',m')$ satisfying the following additional condition:

(eq-$a$ITS) For every $S \in \Scal$, the diagram of functors $\Hbb(S) \times \Hbb(S) \times \Hbb(S) \rightarrow \Hbb(S)$

\begin{equation*}
\begin{tikzcd}
(A \otimes B) \otimes C \arrow{r}{e} \arrow{d}{a} & (A \otimes' B) \otimes C \arrow{r}{e} & (A \otimes' B) \otimes' C \arrow{d}{a'} \\
A \otimes (B \otimes C) \arrow{r}{e} & A \otimes (B \otimes' C) \arrow{r}{e} & A \otimes' (B \otimes' C)
\end{tikzcd}
\end{equation*}

is commutative.

In order to get a similar notion in the setting of external tensor structures, we just need to transliterate the previous conditions in the obvious way, as follows:

Let $(\boxtimes,m)$ be an external tensor structure on $\Hbb$.

* An external associativity constraint $a$ on $(\boxtimes,m)$ is the datum of

* for every $S_1, S_2, S_3 \in \Scal$, a natural isomorphism between functors $\Hbb(S_1) \times \Hbb(S_2) \times \Hbb(S_3) \rightarrow \Hbb(S_1 \times S_2 \times S_3)$

\begin{equation*}
a = a_{S_1,S_2,S_3}: (A_1 \boxtimes A_2) \boxtimes A_3 \xrightarrow{\sim} A_1 \boxtimes (A_2 \boxtimes A_3)
\end{equation*}

satisfying the following conditions:

($a$ETS-1) For every $S_1, S_2, S_3, S_4 \in \Scal$, the diagram of functors $\Hbb(S_1) \times \Hbb(S_2) \times \Hbb(S_3) \times \Hbb(S_4) \rightarrow \Hbb(S_1 \times S_2 \times S_3 \times S_4)$

\begin{equation*}
\begin{tikzcd}
((A_1 \boxtimes A_2) \boxtimes A_3) \boxtimes A_4 \arrow{d}{a} \arrow{rr}{a} && (A_1 \boxtimes A_2) \boxtimes (A_3 \boxtimes A_4) \arrow{d}{a} \\
(A_1 \boxtimes (A_2 \boxtimes A_3)) \boxtimes A_4 \arrow{r}{a} & A_1 \boxtimes ((A_2 \boxtimes A_3) \boxtimes A_4) \arrow{r}{a} & A_1 \boxtimes (A_2 \boxtimes (A_3 \boxtimes A_4))
\end{tikzcd}
\end{equation*}

is commutative.

($a$ETS-2) For every three morphisms $f_i: T_i \rightarrow S_i$ in $\Scal$, $i = 1,2,3$, the diagram of functors $\Hbb(S_1) \times \Hbb(S_2) \times \Hbb(S_3) \rightarrow \Hbb(T_1 \times T_2 \times T_3)$

\begin{equation*}
\begin{tikzcd}
(f_1^* A_1 \boxtimes f_2^* A_2) \boxtimes f_3^* A_3 \arrow{r}{m} \arrow{d}{a} & (f_1 \times f_2)^* (A_1 \boxtimes A_2) \boxtimes f_3^* A_3 \arrow{r}{m} & (f_1 \times f_2 \times f_3)^* ((A_1 \boxtimes A_2) \boxtimes A_3) \arrow{d}{a} \\
f_1^* A_1 \boxtimes (f_2^* A_2 \boxtimes f_3^* A_3) \arrow{r}{m} & f_1^* A_1 \boxtimes (f_2 \times f_3)^* (A_2 \boxtimes A_3) \arrow{r}{m} & (f_1 \times f_2 \times f_3)^* (A_1 \boxtimes (A_2 \boxtimes A_3))
\end{tikzcd}
\end{equation*}

is commutative.

We say that $(\boxtimes,m;a)$ is an associative external tensor structure on $\Hbb$.

* Let $(\boxtimes',m';a')$ and $(\boxtimes,m;a)$ be two associative external tensor structures on $\Hbb$. An equivalence of associative external tensor structures $e: (\boxtimes',m';a') \xrightarrow{\sim} (\boxtimes,m;a)$ is an equivalence of external tensor structures $e: (\boxtimes',m') \xrightarrow{\sim} (\boxtimes,m)$ satisfying the following additional condition:

(eq-$a$ETS) For every $S_1, S_2, S_3 \in \Scal$, the diagram of functors $\Hbb(S_1) \times \Hbb(S_2) \times \Hbb(S_3) \rightarrow \Hbb(S_1 \times S_2 \times S_3)$

\begin{equation*}
\begin{tikzcd}
(A_1 \boxtimes' A_2) \boxtimes' A_3 \arrow{r}{e} \arrow{d}{a'} & (A_1 \boxtimes A_2) \boxtimes' A_3 \arrow{r}{e} & (A_1 \boxtimes A_2) \boxtimes A_3 \arrow{d}{a} \\
A_1 \boxtimes' (A_2 \boxtimes' A_3) \arrow{r}{e} & A_1 \boxtimes' (A_2 \boxtimes A_3) \arrow{r}{e} & A_1 \boxtimes (A_2 \boxtimes A_3)
\end{tikzcd}
\end{equation*}

is commutative.

As promised, we now describe how associativity constraints can be translated between the internal and the external setting along the constructions of <Ref> and <Ref>. This is the content of the following two results:

Let $(\otimes,m)$ be an internal tensor structure on $\Hbb$, and let $(\boxtimes,m^e)$ denote the external tensor structure defined from it via <Ref>. Suppose that we are given an internal associativity constraint $a$ on $(\otimes,m)$. Then, associating

* to every $S_1, S_2, S_3 \in \Scal$, the natural isomorphism of functors $\Hbb(S_1) \times \Hbb(S_2) \times \Hbb(S_3) \rightarrow \Hbb(S_1 \times S_2 \times S_3)$

\begin{equation*}
a^e = a^e_{S_1,S_2,S_3}: (A_1 \boxtimes A_2) \boxtimes A_3 \xrightarrow{\sim} A_1 \boxtimes (A_2 \boxtimes A_3)
\end{equation*}

defined by taking the composite

\begin{equation*}
\begin{tikzcd}[font=\small]
(A_1 \boxtimes A_2) \boxtimes A_3 \arrow[equal]{d} && A_1 \boxtimes (A_2 \boxtimes A_3) \arrow[equal]{d} \\
pr^{123,*}_{12} (pr^{12,*}_{1} A_1 \otimes pr^{12,*}_{2} A_2) \otimes pr^{123,*}_{3} A_3 && pr^{123,*}_{1} A_1 \otimes pr^{123,*}_{23} (pr^{23,*}_{2} A_2 \otimes pr^{23,*}_{3} A_3) \\
(pr^{123,*}_{12} pr^{12,*}_{1} A_1 \otimes pr^{123,*}_{12} pr^{12,*}_{2} A_2) \otimes pr^{123,*}_{3} A_3 \arrow{u}{m} \arrow[equal]{d} && pr^{123,*}_{1} A_1 \otimes (pr^{123,*}_{23} pr^{23,*}_{2} A_2 \otimes pr^{123,*}_{23} pr^{23,*}_{3} A_3) \arrow{u}{m} \arrow[equal]{d} \\
(pr^{123,*}_{1} A_1 \otimes pr^{123,*}_{2} A_2) \otimes pr^{123,*}_{3} A_3 \arrow{rr}{a} && pr^{123,*}_{1} A_1 \otimes (pr^{123,*}_{2} A_2 \otimes pr^{123,*}_{3} A_3)
\end{tikzcd}
\end{equation*}

defines an external associativity constraint $a^e$ on $(\boxtimes,m^e)$.

We have to check that the definition satisfies conditions ($a$ETS-1) and ($a$ETS-2).

We start from condition ($a$ETS-1): given $S_1, S_2, S_3, S_4 \in \Scal$, we have to show that the diagram of functors $\Hbb(S_1) \times \Hbb(S_2) \times \Hbb(S_3) \times \Hbb(S_4) \rightarrow \Hbb(S_1 \times S_2 \times S_3 \times S_4)$

\begin{equation*}
\begin{tikzcd}
((A_1 \boxtimes A_2) \boxtimes A_3) \boxtimes A_4 \arrow{d}{a^e} \arrow{rr}{a^e} && (A_1 \boxtimes A_2) \boxtimes (A_3 \boxtimes A_4) \arrow{d}{a^e} \\
(A_1 \boxtimes (A_2 \boxtimes A_3)) \boxtimes A_4 \arrow{r}{a^e} & A_1 \boxtimes ((A_2 \boxtimes A_3) \boxtimes A_4) \arrow{r}{a^e} & A_1 \boxtimes (A_2 \boxtimes (A_3 \boxtimes A_4))
\end{tikzcd}
\end{equation*}

is commutative. To this end, we decompose the diagram as

\begin{equation*}
\begin{tikzcd}[font=\small]
\bullet \arrow{ddd}{a^e} \arrow{rrrr}{a^e} \arrow{dr}{\sim} &&&& \bullet \arrow{ddd}{a^e} \arrow{dl}{\sim} \\
& ((B_1 \otimes B_2) \otimes B_3) \otimes B_4 \arrow{rr}{a} \arrow{d}{a} && (B_1 \otimes B_2) \otimes (B_3 \otimes B_4) \arrow{d}{a} \\
& (B_1 \otimes (B_1 \otimes B_3)) \otimes B_4 \arrow{r}{a} & B_1 \otimes ((B_2 \otimes B_3) \otimes B_4) \arrow{r}{a} & B_1 \otimes (B_2 \otimes (B_3 \otimes B_4)) \\
\bullet \arrow{rr}{a^e} \arrow{ur}{\sim} && \bullet \arrow{rr}{a^e} \isoarrow{u} && \bullet \arrow{ul}{\sim}
\end{tikzcd}
\end{equation*}

where, for notational convenience, we have set $B_i := pr^{1234,*}_i A_i$, $i = 1,2,3,4$. The five unnamed natural isomorphisms are obtained by combining connection isomorphisms and internal monoidality isomorphisms along suitable paths; by <Ref>, we know that the definitions do not depend on the chosen paths. Since the cental rectangle in the latter diagram is commutative by axiom ($a$ITS-1), it now suffices to show that the five lateral pieces are commutative as well. For each of them, it suffices to expand the definition of the two auxiliary isomorphisms involved in the most convenient way, using again the independence result of <Ref>; we omit the details.

We now treat condition ($a$ETS-2): given three morphisms $f_i: T_i \rightarrow S_i$ in $\Scal$, $i = 1,2,3$, we have to show that the diagram of functors $\Hbb(S_1) \times \Hbb(S_2) \times \Hbb(S_3) \rightarrow \Hbb(T_1 \times T_2 \times T_3)$

\begin{equation*}
\begin{tikzcd}
(f_1^* A_1 \boxtimes f_2^* A_2) \boxtimes f_3^* A_3 \arrow{r}{m^e} \arrow{d}{a^e} & f_{12}^* (A_1 \boxtimes A_2) \boxtimes f_3^* A_3 \arrow{r}{m^e} & f_{123}^* ((A_1 \boxtimes A_2) \boxtimes A_3) \arrow{d}{a^e} \\
f_1^* A_1 \boxtimes (f_2^* A_2 \boxtimes f_3^* A_3) \arrow{r}{m^e} & f_1^* A_1 \boxtimes f_{23}^* (A_2 \boxtimes A_3) \arrow{r}{m^e} & f_{123}^* (A_1 \boxtimes (A_2 \boxtimes A_3))
\end{tikzcd}
\end{equation*}

is commutative. To this end, we decompose the diagram as

\begin{equation*}
\begin{tikzcd}[font=\small]
\bullet \arrow{rr}{m^e} \arrow{ddd}{a^e} \arrow{dr}{\sim} && \bullet \arrow{rr}{m^e} \isoarrow{d} && \bullet \arrow{ddd}{a^e} \arrow{dl}{\sim} \\
& (f_{123}^* B_1 \otimes f_{123}^* B_2) \otimes f_{123}^* B_3 \arrow{r}{m} \arrow{d}{a} & f_{123}^*(B_1 \otimes B_2) \otimes f_{123}^* B_3 \arrow{r}{m} & f_{123}^*((B_1 \otimes B_2) \otimes B_3) \arrow{d}{a} \\
& f_{123}^* B_1 \otimes (f_{123}^* B_2 \otimes f_{123}^* B_3) \arrow{r}{m} & f_{123}^* B_1 \otimes f_{123}^*(B_2 \otimes B_3) \arrow{r}{m} & f_{123}^*(B_1 \otimes (B_2 \otimes B_3)) \\
\bullet \arrow{rr}{m^e} \arrow{ur}{\sim} && \bullet \arrow{rr}{m^e} \isoarrow{u} && \bullet \arrow{ul}{\sim}
\end{tikzcd}
\end{equation*}

where, for notational convenience, we have set $B_i := pr^{123,*}_i A_i$, $i = 1,2,3$. The six unnamed natural isomorphisms are obtained by combining connection isomorphisms and internal monoidality isomorphisms along suitable paths; by <Ref>, we know that the definitions do not depend on the chosen paths. Since the central rectangle is the latter diagram is commutative by axiom ($a$ITS-2), it now suffices to show that the six lateral pieces are commutative as well. This can be achieved using the same trick as for the first part of the proof; we omit the details.

Let $(\boxtimes,m)$ be an external tensor structure on $\Hbb$, and let $(\otimes,m^i)$ denote the internal tensor structure defined from it via <Ref>. Suppose that we are given an external associativity constraint $a$ on $(\boxtimes,m)$. Then, associating

* to every $S \in \Scal$, the natural isomorphism of functors $\Hbb(S) \times \Hbb(S) \times \Hbb(S) \rightarrow \Hbb(S)$

\begin{equation*}
a^i = a^i_S: (A \otimes B) \otimes C \xrightarrow{\sim} A \otimes (B \otimes C)
\end{equation*}

defined by taking the composite

\begin{equation*}
\begin{tikzcd}[font=\small]
(A \otimes B) \otimes C \arrow[equal]{d} && A \otimes (B \otimes C) \arrow[equal]{d} \\
\Delta_S^*(\Delta_S^*(A \boxtimes B) \boxtimes C) \arrow{d}{m} && \Delta_S^*(A \boxtimes \Delta_S^*(B \boxtimes C)) \arrow{d}{m} \\
\Delta_S^*(\Delta_S \times \id_S)^*((A \boxtimes B) \boxtimes C) \arrow[equal]{d} && \Delta_S^*(\id_S \times \Delta_S)^*(A \boxtimes (B \boxtimes C)) \arrow[equal]{d} \\
\Delta_S^{(3),*}((A \boxtimes B) \boxtimes C) \arrow{rr}{a} && \Delta_S^{(3),*}(A \boxtimes (B \boxtimes C))
\end{tikzcd}
\end{equation*}

defines an internal associativity constraint $a^i$ on $(\otimes,m^i)$.

We have to check that the definition satisfies conditions ($a$ITS-1) and ($a$ITS-2).

We start from condition ($a$ITS-1): given $S \in \Scal$, we have to show that the diagram of functors $\Hbb(S) \times \Hbb(S) \times \Hbb(S) \times \Hbb(S) \rightarrow \Hbb(S)$

\begin{equation*}
\begin{tikzcd}
((A \otimes B) \otimes C) \otimes D \arrow{d}{a^i} \arrow{rr}{a^i} && (A \otimes B) \otimes (C \otimes D) \arrow{d}{a^i} \\
(A \otimes (B \otimes C)) \otimes D \arrow{r}{a^i} & A \otimes ((B \otimes C) \otimes D) \arrow{r}{a^i} & A \otimes (B \otimes (C \otimes D))
\end{tikzcd}
\end{equation*}

is commutative. To this ends, we decompose it as

\begin{equation*}
\begin{tikzcd}[font=\small]
\bullet \arrow{ddd}{a^i} \arrow{rrrr}{a^i} \arrow{dr}{\sim} &&&& \bullet \arrow{ddd}{a^i} \arrow{dl}{\sim} \\
& \Delta_S^{(4)*} (((A \boxtimes B) \boxtimes C) \boxtimes D) \arrow{rr}{a} \arrow{d}{a} && \Delta_S^{(4)*} ((A \boxtimes B) \boxtimes (C \boxtimes D)) \arrow{d}{a} \\
& \Delta_S^{(4)*} ((A \boxtimes (B \boxtimes C)) \boxtimes D) \arrow{r}{a} & \Delta_S^{(4)*} (A \boxtimes ((B \boxtimes C) \boxtimes D)) \arrow{r}{a} & \Delta_S^{(4)*} (A \boxtimes (B \boxtimes (C \boxtimes D))) \\
\bullet \arrow{rr}{a^i} \arrow{ur}{\sim} && \bullet \arrow{rr}{a^i} \isoarrow{u} && \bullet \arrow{ul}{\sim}
\end{tikzcd}
\end{equation*}

Here, the five unnamed natural isomorphisms are obtained by combining connection isomorphisms and external monoidality isomorphisms along suitable paths; by <Ref>, we know that the definitions do not depend on the chosen paths. Since the central rectangle is commutative by axiom ($a$ETS-1), it suffices to show that the five lateral pieces are commutative as well. This can be achieved by the same trick mentioned in the proof of <Ref>; we omit the details.

We now treat condition ($a$ITS-2): given a morphism $f: T \rightarrow S$ in $\Scal$, we have to show that the diagram of functors $\Hbb(S) \times \Hbb(S) \times \Hbb(S) \rightarrow \Hbb(T)$

\begin{equation*}
\begin{tikzcd}
(f^*A \otimes f^*B) \otimes f^*C \arrow{r}{m^i} \arrow{d}{a^i} & f^*(A \otimes B) \otimes f^*C \arrow{r}{m^i} & f^*((A \otimes B) \otimes C) \arrow{d}{a^i} \\
f^*A \otimes (f^*B \otimes f^*C) \arrow{r}{m^i} & f^*A \otimes f^*(B \otimes C) \arrow{r}{m^i} & f^*(A \otimes (B \otimes C))
\end{tikzcd}
\end{equation*}

is commutative. To this end, we decompose it as

\begin{equation*}
\begin{tikzcd}[font=\small]
\bullet \arrow{rr}{m^i} \arrow{ddd}{a^i} \arrow{dr}{\sim} && \bullet \arrow{rr}{m^i} \isoarrow{d} && \bullet \arrow{ddd}{a^i} \arrow{dl}{\sim} \\
& (f^* A \boxtimes f^* B) \boxtimes f^* C \arrow{r}{m} \arrow{d}{a} & (f \times f)^*(A \boxtimes B) \boxtimes f^*C \arrow{r}{m} & (f \times f \times f)^* ((A \boxtimes B) \boxtimes C) \arrow{d}{a} \\
& f^* A \boxtimes (f^* B \boxtimes f^* C) \arrow{r}{m} & f^* A \boxtimes (f \times f)^*(B \boxtimes C) \arrow{r}{m} & (f \times f \times f)^*(A \boxtimes (B \boxtimes C)) \\
\bullet \arrow{rr}{m^i} \arrow{ur}{\sim} && \bullet \arrow{rr}{m^i} \isoarrow{u} && \bullet \arrow{ul}{\sim}
\end{tikzcd}
\end{equation*}

Again, the six unnamed natural isomorphisms are obtained by combining connection isomorphisms and external monoidality isomorphisms along suitable paths, the resulting definitions being independent of the chosen paths by <Ref>. Since the central rectangle is commutative by axiom ($a$ETS-2), it suffices to show that the five lateral pieces are commutative as well. Again, this can be achieved by the same trick mentioned in the proof of <Ref>; we omit the details.

Finally, we prove that the correspondence of <Ref> respects internal and external associativity constraints in a precise way:

The constructions of <Ref> and <Ref> refine the canonical bijection of <Ref> to a bijection between equivalence classes of associative internal and external tensor structures on $\Hbb$.

We keep the same notation adopted in the proof of <Ref>.

Start from an associative internal tensor structure $(\otimes,m;a)$ on $\Hbb$, and let $a'$ denote the internal associativity constraint on $(\otimes',m')$ obtained from $a$ by applying first <Ref> and then <Ref>. We claim that the equivalence of internal tensor structures $e: (\otimes,m) \xrightarrow{\sim} (\otimes',m')$ constructed in the first part of the proof of <Ref> satisfies condition (eq-$a$ITS): given $S \in \Scal$, we have to show that the diagram of functors $\Hbb(S) \times \Hbb(S) \times \Hbb(S) \rightarrow \Hbb(S)$

\begin{equation*}
\begin{tikzcd}
(A \otimes B) \otimes C \arrow{r}{e} \arrow{d}{a} & (A \otimes' B) \otimes C \arrow{r}{e} & (A \otimes' B) \otimes' C \arrow{d}{a'} \\
A \otimes (B \otimes C) \arrow{r}{e} & A \otimes (B \otimes' C) \arrow{r}{e} & A \otimes' (B \otimes' C)
\end{tikzcd}
\end{equation*}

is commutative. Expanding the definitions, we find that the internal associativity isomorphism $a'$ is given by the composite

\begin{equation*}
\begin{tikzcd}[font=\tiny]
(A \otimes' B) \otimes' C \arrow[equal]{d} & A \otimes' (B \otimes' C). \arrow[equal]{d} \\
\Delta_S^* (pr^{12,*}_1 \Delta_S^* (pr^{12,*}_1 A \otimes pr^{12,*}_2 B) \otimes pr^{12,*}_2 C) \arrow[equal]{d} & \Delta_S^* (pr^{12,*}_1 A \otimes pr^{12,*}_2 \Delta_S^* (pr^{12,*}_1 B \otimes pr^{12,*}_2 C)) \arrow[equal]{d} \\
\Delta_S^* ((\Delta_S \times \id_S)^* pr^{123,*}_{12} (pr^{12,*}_1 A \otimes pr^{12,*}_2 B) \otimes (\Delta_S \times \id_S)^* pr^{123,*}_3 C) \arrow{d}{m} & \Delta_S^* ((\Delta_S \times \id_S)^* pr^{123,*}_1 A \otimes (\Delta_S \times \id_S)^* pr^{123,*}_{23} (pr^{23,*}_2 B \otimes pr^{23,*}_3 C)) \arrow{d}{m} \\
\Delta_S^* (\Delta_S \times \id_S)^* (pr^{123,*}_{12}(pr^{12,*}_1 A \otimes pr^{12,*}_2 B) \otimes pr^{123,*}_3 C) \arrow[equal]{d} & \Delta_S^* (\id_S \times \Delta_S)^* (pr^{123,*}_1 A \otimes pr^{123,*}_{23}(pr^{23,*}_2 B \otimes pr^{23,*}_3 C)) \arrow[equal]{d} \\
\Delta_S^{(3),*} (pr^{123,*}_{12}(pr^{12,*}_1 A \otimes pr^{12,*}_2 B) \otimes pr^{123,*}_3 C) &  \Delta_S^{(3),*} (pr^{123,*}_1 A \otimes pr^{123,*}_{23}(pr^{23,*}_2 B \otimes pr^{23,*}_3 C)) \\
\Delta_S^{(3),*} ((pr^{123,*}_{12} pr^{12,*}_1 A \otimes pr^{123,*}_{12} pr^{12,*}_2 B) \otimes pr^{123,*}_3 C) \arrow{u}{m} \arrow[equal]{d} & \Delta_S^{(3),*} (pr^{123,*}_1 A \otimes (pr^{123,*}_{23} pr^{23,*}_2 B \otimes pr^{123,*}_{23} pr^{23,*}_3 C)) \arrow{u}{m} \arrow[equal]{d} \\
\Delta_S^{(3),*} ((pr^{123,*}_1 A \otimes pr^{123,*}_2 B) \otimes pr^{123,*}_3 C) \arrow{r}{a} & \Delta_S^{(3),*} (pr^{123,*}_1 A \otimes (pr^{123,*}_2 B \otimes pr^{123,*}_3 C))
\end{tikzcd}
\end{equation*}

Substituting this composite in the above diagram, we obtain a diagram of the form

\begin{equation*}
\begin{tikzcd}[font=\small]
(A \otimes B) \otimes C \arrow{r}{\sim} \arrow{d}{a} & \Delta_S^{(3),*} ((pr^{123,*}_1 A \otimes pr^{123,*}_2 B) \otimes pr^{123,*}_3 C) \arrow{d}{a} \\
A \otimes (B \otimes C) \arrow{r}{\sim} & \Delta_S^{(3),*} (pr^{123,*}_1 A \otimes (pr^{123,*}_2 B \otimes pr^{123,*}_3 C))
\end{tikzcd}
\end{equation*}

where the two horizontal arrows are composites of connection isomorphisms and internal monoidality isomorphisms along suitable paths. Since, by <Ref>, we know that the resulting isomorphisms are independent of the chosen paths, we deduce that the latter diagram coincides, for example, with the outer part of the diagram

\begin{equation*}
\begin{tikzcd}[font=\tiny]
(A \otimes B) \otimes C \arrow[equal]{r} \arrow{ddd}{a} & (\Delta_S^{(3),*} pr^{123,*}_1 A \otimes \Delta_S^{(3),*} pr^{123,*}_2 B) \otimes \Delta_S^{(3),*} pr^{123,*}_3 C \arrow{r}{m} \arrow{ddd}{a} & \Delta_S^{(3),*}(pr^{123,*}_1 A \otimes pr^{123,*}_2 B) \otimes \Delta_S^{(3),*} pr^{123,*}_3 C \arrow{d}{m} \\
&& \Delta_S^{(3),*} ((pr^{123,*}_1 A \otimes pr^{123,*}_2 B) \otimes pr^{123,*}_3 C) \arrow{d}{a} \\
&& \Delta_S^{(3),*} (pr^{123,*}_1 A \otimes (pr^{123,*}_2 B \otimes pr^{123,*}_3 C)) \\
A \otimes (B \otimes C) \arrow[equal]{r}& \Delta_S^{(3),*} pr^{123,*}_1 A \otimes (\Delta_S^{(3),*} pr^{123,*}_2 B \otimes \Delta_S^{(3),*} pr^{123,*}_3 C) \arrow{r}{m} & \Delta_S^{(3),*} pr^{123,*}_1 A \otimes \Delta_S^{(3),*} (pr^{123,*}_2 B \otimes pr^{123,*}_3 C) \arrow{u}{m}
\end{tikzcd}
\end{equation*}

where the left-most piece is commutative by naturality while the right-most piece is commutative by axiom ($a$ITS-2). This proves the claim.

Conversely, start from an associative external tensor structure $(\boxtimes,m;a)$ on $\Hbb$, and let $a'$ denote the external associativity constraint on $(\boxtimes',m')$ obtained from $a$ by applying first <Ref> and then <Ref>. We claim that the equivalence of external tensor structures $e: (\boxtimes',m') \xrightarrow{\sim} (\boxtimes,m)$ constructed in the second part of the proof of <Ref> satisfies condition (eq-$a$ETS): given $S_1, S_2, S_3 \in \Scal$, we have to show that the diagram of functors $\Hbb(S_1) \times \Hbb(S_2) \times \Hbb(S_3) \rightarrow \Hbb(S_1 \times S_2 \times S_3)$

\begin{equation*}
\begin{tikzcd}
(A_1 \boxtimes' A_2) \boxtimes' A_3 \arrow{r}{e} \arrow{d}{a'} & (A_1 \boxtimes A_2) \boxtimes' A_3 \arrow{r}{e} & (A_1 \boxtimes A_2) \boxtimes A_3 \arrow{d}{a} \\
A_1 \boxtimes' (A_2 \boxtimes' A_3) \arrow{r}{e} & A_1 \boxtimes' (A_2 \boxtimes A_3) \arrow{r}{e} & A_1 \boxtimes (A_2 \boxtimes A_3)
\end{tikzcd}
\end{equation*}

is commutative. Expanding the definitions, we find that the external associativity isomorphism $a'$ is given by the composite

\begin{equation*}
\begin{tikzcd}[font=\tiny]
(A_1 \boxtimes' A_2) \boxtimes' A_3 \arrow[equal]{d} & A_1 \boxtimes' (A_2 \boxtimes' A_3) \arrow[equal]{d} \\
\Delta_{S_{123}}^* (pr^{123,*}_{12} \Delta_{S_{12}}^* (pr^{12,*}_1 A_1 \boxtimes pr^{12,*}_2 A_2) \boxtimes pr^{123,*}_3 A_3) \arrow[equal]{d} & \Delta_{S_{123}}^*(pr^{123,*}_1 A_1 \boxtimes pr^{123,*}_{23} \Delta_{S_{23}}^*(pr^{23,*}_2 A_2 \boxtimes pr^{23,*}_3 A_3)) \arrow[equal]{d} \\
\Delta_{S_{123}}^* (\Delta_{S_{123}}^* (pr^{123,*}_{12} \times pr^{123,*}_{12})(pr^{12,*}_1 A_1 \boxtimes pr^{12,*}_2 A_2) \boxtimes pr^{123,*}_3 A_3) & \Delta_{S_{123}}^* (pr^{123,*}_1 A_1 \boxtimes \Delta_{S_{123}}^* (pr^{123,*}_{23} \times pr^{123,*}_{23}) (pr^{23,*}_2 A_2 \boxtimes pr^{23,*}_3 A_3)) \\
\Delta_{S_{123}}^* (\Delta_{S_{123}}^* (pr^{123,*}_{12} pr^{12,*}_1 A_1 \boxtimes pr^{123,*}_{12} pr^{12,*}_2 A_2) \boxtimes pr^{123,*}_3 A_3) \arrow{u}{m} \arrow[equal]{d} & \Delta_{S_{123}}^* (pr^{123,*}_1 A_1 \boxtimes \Delta_{S_{123}}^* (pr^{123,*}_{23} pr^{23,*}_2 A_2 \boxtimes pr^{123,*}_{23} pr^{23,*}_3 A_3)) \arrow{u}{m} \arrow[equal]{d} \\
\Delta_{S_{123}}^* (\Delta_{S_{123}}^* (pr^{123,*}_1 A_1 \boxtimes pr^{123,*}_2 A_2) \boxtimes pr^{123,*}_3 A_3) \arrow{d}{m} & \Delta_{S_{123}}^* (pr^{123,*}_1 A_1 \boxtimes \Delta_{S_{123}}^* (pr^{123,*}_2 A_2 \boxtimes pr^{123,*}_3 A_3)) \arrow{d}{m} \\
\Delta_{S_{123}}^* (\Delta_{S_{123}} \times \id_{S_{123}})^* ((pr^{123,*}_1 A_1 \boxtimes pr^{123,*}_2 A_2) \boxtimes pr^{123,*}_3 A_3) \arrow[equal]{d} & \Delta_{S_{123}}^* (\id_{S_{123}} \times \Delta_{S_{123}})^* (pr^{123,*}_1 A_1 \boxtimes (pr^{123,*}_2 A_2 \boxtimes pr^{123,*}_3 A_3)) \arrow[equal]{d} \\
\Delta_{S_{123}}^{(3),*} ((pr^{123,*}_1 A_1 \boxtimes pr^{123,*}_2 A_2) \boxtimes pr^{123,*}_3 A_3) \arrow{r}{a} & \Delta_{S_{123}}^{(3),*} (pr^{123,*}_1 A_1 \boxtimes (pr^{123,*}_2 A_2 \boxtimes pr^{123,*}_3 A_3))
\end{tikzcd}
\end{equation*}

Substituting this composite in the above diagram, we obtain a diagram of the form

\begin{equation*}
\begin{tikzcd}[font=\small]
\Delta_{S_{123}}^{(3),*} ((pr^{123,*}_1 A_1 \boxtimes pr^{123,*}_2 A_2) \boxtimes pr^{123,*}_3 A_3) \arrow{r}{\sim} \arrow{d}{a} & (A_1 \boxtimes A_2) \boxtimes A_3 \arrow{d}{a} \\
\Delta_{S_{123}}^{(3),*} (pr^{123,*}_1 A_1 \boxtimes (pr^{123,*}_2 A_2 \boxtimes pr^{123,*}_3 A_3)) \arrow{r}{\sim} & A_1 \boxtimes (A_2 \boxtimes A_3)
\end{tikzcd}
\end{equation*}

where the two horizontal arrows are composites of connection isomorphisms and internal monoidality isomorphisms along suitable paths. Since, by <Ref>, we know that the resulting isomorphisms are independent of the chosen paths, we deduce that the latter diagram coincides, for example, with the outer part of the diagram

\begin{equation*}
\begin{tikzcd}[font=\tiny]
\Delta_{S_{123}}^{(3),*} ((pr^{123}_1 \times pr^{123}_2)^* (A_1 \boxtimes A_2) \boxtimes pr^{123,*}_3 A_3) \arrow{r}{m} & \Delta_{S_{123}}^{(3),*} (pr^{123}_1 \times pr^{123}_2 \times pr^{123}_3)^*((A_1 \boxtimes A_2) \boxtimes A_3) \arrow[equal]{r} \arrow{ddd}{a} & (A_1 \boxtimes A_2) \boxtimes A_3 \arrow{ddd}{a} \\
\Delta_{S_{123}}^{(3),*} ((pr^{123,*}_1 A_1 \boxtimes pr^{123,*}_2 A_2) \boxtimes pr^{123,*}_3 A_3) \arrow{u}{m} \arrow{d}{a} \\
\Delta_{S_{123}}^{(3),*} (pr^{123,*}_1 A_1 \boxtimes (pr^{123,*}_2 A_2 \boxtimes pr^{123,*}_3 A_3)) \arrow{d}{m} \\
\Delta_{S_{123}}^{(3),*} (pr^{123,*}_1 A_1 \boxtimes (pr^{123}_2 \times pr^{123}_3)^* (A_2 \boxtimes A_3)) \arrow{r}{m} & \Delta_{S_{123}}^{(3),*} (pr^{123}_1 \times pr^{123}_2 \times pr^{123}_3)^*(A_1 \boxtimes (A_2 \boxtimes A_3)) \arrow[equal]{r} & A_1 \boxtimes (A_2 \boxtimes A_3)
\end{tikzcd}
\end{equation*}

where the left-most piece is commutative by axiom ($a$ETS-2) while the right-most piece is commutative by naturality. This proves the claim and concludes the proof.

§ COMMUTATIVITY CONSTRAINTS

The goal of this section is to introduce commutativity constraints in the setting of internal and external tensor structures and to compare them.

The notion of commutativity constraint for single monoidal categories comes from <cit.>; in the case of fibered categories, one needs to require inverse image functors to respect commutativity constraints as in <cit.>. The latter definition can be formulated in the language of internal tensor structures as follows:

Let $(\otimes,m)$ be an internal tensor structure on $\Hbb$.

* An internal commutativity constraint $c$ on $(\otimes,m)$ is the datum of

* for every $S \in \Scal$, a natural isomorphism between functors $\Hbb(S) \times \Hbb(S) \rightarrow \Hbb(S)$

\begin{equation*}
c = c_S: A \otimes B \xrightarrow{\sim} B \otimes A
\end{equation*}

satisfying the following condition

($c$ITS-1) For every $S \in \Scal$, the diagram of functors $\Hbb(S) \times \Hbb(S) \rightarrow \Hbb(S)$

\begin{equation*}
\begin{tikzcd}
A \otimes B \arrow{r}{c} \arrow{dr}{\id} & B \otimes A \arrow{d}{c} \\
& A \otimes B
\end{tikzcd}
\end{equation*}

is commutative.

($c$ITS-2) For every morphism $f: T \rightarrow S$ in $\Scal$, the diagram of functors $\Hbb(S) \times \Hbb(S) \rightarrow \Hbb(T)$

\begin{equation*}
\begin{tikzcd}
f^* A \otimes f^* B \arrow{r}{c} \arrow{d}{m} & f^* B \otimes f^* A \arrow{d}{m} \\
f^* (A \otimes B)  \arrow{r}{c} & f^* (B \otimes A)
\end{tikzcd}
\end{equation*}

is commutative.

We say that $(\otimes,m;c)$ is a symmetric internal tensor structure on $\Hbb$.

* Let $(\otimes,m;c)$ and $(\otimes',m';c')$ be two symmetric internal tensor structures on $\Hbb$. An equivalence of symmetric internal tensor structures $e: (\otimes,m;c) \xrightarrow{\sim} (\otimes',m';c')$ is an equivalence of internal tensor structures $e: (\otimes,m) \xrightarrow{\sim} (\otimes',m')$ satisfying the following additional condition:

(eq-$c$ITS) For every $S \in \Scal$, the diagram of functors $\Hbb(S) \times \Hbb(S) \rightarrow \Hbb(S)$

\begin{equation*}
\begin{tikzcd}
A \otimes B \arrow{r}{e} \arrow{d}{c} & A \otimes' B \arrow{d}{c} \\
B \otimes A \arrow{r}{e} & B \otimes' A
\end{tikzcd}
\end{equation*}

is commutative.

In order to get a similar notion in the setting of external tensor structures, we need to reformulate the operation of switching factors with the help of suitable permutation isomorphisms, as follows:

Let $(\boxtimes,m)$ be an external tensor structure on $\Hbb$.

* An external commutativity constraint $c$ on $(\boxtimes,m)$ is the datum of

* for every $S_1, S_2 \in \Scal$, a natural isomorphism between functors $\Hbb(S_1) \times \Hbb(S_2) \rightarrow \Hbb(S_1 \times S_2)$

\begin{equation*}
c = c_{S_1,S_2}: A_1 \boxtimes A_2 \xrightarrow{\sim} \tau^*(A_2 \boxtimes A_1),
\end{equation*}

where $\tau = \tau_{(12)}: S_1 \times S_2 \rightarrow S_2 \times S_1$ denotes the permutation isomorphism

satisfying the following conditions:

($c$ETS-1)  For every $S_1, S_2 \in \Scal$, the diagram of functors $\Hbb(S_1) \times \Hbb(S_2) \rightarrow \Hbb(S_1 \times S_2)$

\begin{equation*}
\begin{tikzcd}
A_1 \boxtimes A_2 \arrow{r}{c} \arrow[equal]{dr} & \tau^*(A_2 \boxtimes A_1) \arrow{d}{c} \\
& \tau^* \tau^*(A_1 \boxtimes A_2)
\end{tikzcd}
\end{equation*}

is commutative.

($c$ETS-2) For every choice of of morphisms $f_i: T_i \rightarrow S_i$ in $\Scal$, $i = 1,2$, the diagram of functors $\Hbb(S_1) \times \Hbb(S_2) \rightarrow \Hbb(T_2 \times T_1)$

\begin{equation*}
\begin{tikzcd}
f_1^* A_1 \boxtimes f_2^* A_2 \arrow{rr}{c} \arrow{d}{m} && \tau^* (f_2^* A_2 \boxtimes f_1^* A_1) \arrow{d}{m} \\
(f_1 \times f_2)^* (A_1 \boxtimes A_2)\arrow{r}{c} & (f_1 \times f_2)^* \tau^* (A_2 \boxtimes A_1) \arrow[equal]{r} & \tau^* (f_2 \times f_1)^* (A_2 \boxtimes A_1)
\end{tikzcd}
\end{equation*}

is commutative.

We say that $(\boxtimes,m;c)$ is a symmetric external tensor structure on $\Hbb$.

* Let $(\boxtimes',m';c')$ and $(\boxtimes,m;c)$ be two symmetric external tensor structures on $\Hbb$. An equivalence of symmetric external tensor structures $e: (\boxtimes',m';c') \xrightarrow{\sim} (\boxtimes,m;c)$ is an equivalence of external tensor structures $e: (\boxtimes',m') \xrightarrow{\sim} (\boxtimes,m)$ satisfying the following additional condition:

(eq-$c$ETS) For every $S_1,S_2 \in \Scal$, the diagram of functors $\Hbb(S_1) \times \Hbb(S_2) \rightarrow \Hbb(S_1 \times S_2)$

\begin{equation*}
\begin{tikzcd}
A_1 \boxtimes' A_2 \arrow{r}{e} \arrow{d}{c'} & A_1 \boxtimes A_2 \arrow{d}{c} \\
\tau^*(A_2 \boxtimes' A_1) \arrow{r}{e}  & \tau^*(A_2 \boxtimes A_1)
\end{tikzcd}
\end{equation*}

is commutative.

In the same spirit as for the previous section, we now describe how commutativity constraints can be translated between the internal and the external setting along the constructions of <Ref> and <Ref>. This is the content of the following two results:

Let $(\otimes,m)$ be an internal tensor structure on $\Hbb$, and let $(\boxtimes,m^e)$ denote the external tensor structure defined from it via <Ref>. Suppose that we are given an internal commutativity constraint $c$ on $(\otimes,m)$. Then, associating

* to every choice of $S_1, S_2 \in \Scal$, the natural isomorphism of functors $\Hbb(S_1) \times \Hbb(S_2) \rightarrow \Hbb(S_1 \times S_2)$

\begin{equation}\label{symm_int_to_ext}
c^e = c^e_{S_1,S_2}: A_1 \boxtimes A_2 \xrightarrow{\sim} \tau^*(A_2 \boxtimes A_1)
\end{equation}

defined by taking the composite

\begin{equation*}
\begin{tikzcd}[font=\small]
A_1 \boxtimes A_2 \arrow[equal]{d} & \tau^* (A_2 \boxtimes A_1)  \\
pr^{12,*}_{1} A_1 \otimes pr^{12,*}_{2} A_2 \arrow[equal]{d} & \tau^*(pr^{21,*}_{2} A_2 \otimes pr^{21,*}_{1} A_1) \arrow[equal]{u}  \\
\tau^* pr^{21,*}_{1} A_1 \otimes \tau^* pr^{21,*}_{2} A_2 \arrow{r}{c} & \tau^* pr^{21,*}_{2} A_2 \otimes \tau^* pr^{21,*}_{1} A_1 \arrow{u}{m}
\end{tikzcd}
\end{equation*}

defines an external commutativity constraint $c^e$ on $(\boxtimes,m^e)$.

We have to show that the definition satisfies conditions ($c$ETS-1) and ($c$ETS-2).

We start from condition ($c$ETS-1): given $S_1, S_2 \in \Scal$, we have to show that the diagram of functors $\Hbb(S_1) \times \Hbb(S_2) \rightarrow \Hbb(S_1 \times S_2)$

\begin{equation*}
\begin{tikzcd}
A_1 \boxtimes A_2 \arrow{r}{c^e} \arrow[equal]{dr} & \tau^*(A_2 \boxtimes A_1) \arrow{d}{c^e} \\
& \tau^* \tau^*(A_1 \boxtimes A_2)
\end{tikzcd}
\end{equation*}

is commutative. Expanding the definitions, we obtain the outer part of the diagram

\begin{equation*}
\begin{tikzcd}[font=\tiny]
pr^{12,*}_{1} A_1 \otimes pr^{12,*}_{2} A_2 \arrow[equal]{r} \arrow[equal]{dddrrr} & \tau^* pr^{21,*}_{1} A_1 \otimes \tau^* pr^{21,*}_{2} A_2 \arrow{r}{c} & \tau^* pr^{21,*}_{2} A_2 \otimes \tau^* pr^{21,*}_{1} A_1 \arrow{r}{m} & \tau^*(pr^{21,*}_{2} A_2 \otimes pr^{21,*}_{1} A_1) \arrow[equal]{d} \\
&&& \tau^* (\tau^* pr^{12,*}_2 A_2 \otimes \tau^* pr^{12,*}_1 A_1) \arrow{d}{c} \\
&&& \tau^* (\tau^* pr^{12,*}_1 A_1 \otimes \tau^* pr^{12,*}_2 A_2) \arrow{d}{m} \\
&&& \tau^* \tau^* (pr^{12,*}_{1} A_1 \otimes pr^{12,*}_{2} A_2)
\end{tikzcd}
\end{equation*}

that we decompose as

\begin{equation*}
\begin{tikzcd}[font=\small]
\bullet \arrow[equal]{r} \arrow[dddrrr, bend right=50, equal] & \bullet \arrow{r}{c} \arrow{dr}{\id} & \bullet \arrow{r}{m} \arrow{d}{c} & \bullet \arrow[equal]{d} \arrow[bend left]{ddl}{c} \\
&& \tau^* pr^{21,*}_{1} A_1 \otimes \tau^* pr^{21,*}_{2} A_2 \arrow{d}{m} & \bullet \arrow{d}{c} \\
&& \tau^*(pr^{21,*}_{1} A_1 \otimes pr^{21,*}_{2} A_2) \arrow[equal]{r} & \bullet \arrow{d}{m} \\
&&& \bullet
\end{tikzcd}
\end{equation*}

Here, the upper central triangle is commutative by axiom ($c$ITS-1) while the remaining pieces are commutative by naturality, by axiom ($c$ITS-2) and by <Ref>. Hence the outer part of the diagram is commutative as well.

We now treat condition ($c$ETS-2): given two morphisms $f_i: T_i \rightarrow S_i$ in $\Scal$, $i = 1,2$, we have to show that the diagram

\begin{equation*}
\begin{tikzcd}
f_1^* A_1 \boxtimes f_2^* A_2 \arrow{rr}{c^e} \arrow{d}{m^e} && \tau^*(f_2^* A_2 \boxtimes f_1^* A_1) \arrow{d}{m^e} \\
(f_1 \times f_2)^*(A_1 \boxtimes A_2)\arrow{r}{c^e} & (f_1 \times f_2)^* \tau^* (A_2 \boxtimes A_1) \arrow[equal]{r} & \tau^* (f_2 \times f_1)^*(A_2 \boxtimes A_1)
\end{tikzcd}
\end{equation*}

is commutative. Expanding the definitions, we obtain the diagram

\begin{equation*}
\begin{tikzcd}[font=\tiny]
\tau^* pr^{21,*}_{1} f_1^* A_1 \otimes \tau^* pr^{21,*}_{2} f_2^* A_2 \arrow{r}{c} \arrow[equal]{d} & \tau^* pr^{21,*}_{2} f_2^* A_2 \otimes \tau^* pr^{21,*}_{1} f_1^* A_1 \arrow{r}{m} & \tau^* (pr^{21,*}_{2} f_2^* A_2 \otimes pr^{21,*}_{1} f_1^* A_1) \arrow[equal]{d} \\
pr^{12,*}_{1} f_1^* A_1 \otimes pr^{12,*}_{2} f_2^* A_2 \arrow[equal]{d} && \tau^* ((f_2 \times f_1)^* pr^{21,*}_{2} A_2 \otimes (f_2 \times f_1)^* pr^{21,*}_{1} A_1) \arrow{d}{m} \\
(f_1 \times f_2)^* pr^{12,*}_1 A_1 \otimes (f_1 \times f_2)^* pr^{12,*}_2 A_2 \arrow{d}{m} && \tau^* (f_2 \times f_1)^* (pr^{21,*}_{2} A_2 \otimes pr^{21,*}_{1} A_1) \\
(f_1 \times f_2)^* (pr^{12,*}_1 A_1 \otimes pr^{12,*}_2 A_2) \arrow[equal]{d} \\
(f_1 \times f_2)^* (\tau^* pr^{21,*}_{1} A_1 \otimes \tau^* pr^{21,*}_{2} A_2) \arrow{r}{c} & (f_1 \times f_2)^* (\tau^* pr^{21,*}_{2} A_2 \otimes \tau^* pr^{21,*}_{1} A_1) \arrow{r}{m} & (f_1 \times f_2)^* \tau^* (pr^{21,*}_{2} A_2 \otimes pr^{21,*}_{1} A_1) \arrow[equal]{uu}
\end{tikzcd}
\end{equation*}

that we decompose as

\begin{equation*}
\begin{tikzcd}[font=\tiny]
\bullet \arrow{rr}{c} \arrow[equal]{d} \arrow[equal]{dr} && \bullet \arrow{rr}{m} \arrow[equal]{dr} && \bullet \arrow[equal]{d} \\
\bullet \arrow[equal]{d} & \tau^* (f_1 \times f_2)^* pr^{21,*}_{1} A_1 \otimes \tau^* (f_1 \times f_2)^* pr^{21,*}_{2} A_2 \arrow[equal]{d} \arrow{rr}{c} && \tau^* (f_2 \times f_1)^* pr^{21,*}_{2} A_2 \otimes \tau^* (f_2 \times f_1)^* pr^{21,*}_{1} A_1 \arrow{r}{m} \arrow[equal]{d} & \bullet \arrow{d}{m} \\
\bullet \arrow{d}{m} \arrow[equal]{r} & (f_1 \times f_2)^* \tau^* pr^{21,*}_1 A_1 \otimes (f_1 \times f_2)^* \tau^* pr^{21,*}_2 A_2 \arrow{ddl}{m} \arrow{rr}{c} && (f_1 \times f_2)^* \tau^* pr^{21,*}_{2} A_2 \otimes (f_1 \times f_2)^* \tau^* pr^{21,*}_{1} A_1 \arrow{ddl}{m} & \bullet \\
\bullet \arrow[equal]{d} \\
\bullet \arrow{rr}{c} && \bullet \arrow{rr}{m} && \bullet \arrow[equal]{uu}
\end{tikzcd}
\end{equation*}

Here, the lower-left piece is commutative by axiom ($c$ITS-2) while the other pieces are commutative by naturality, by axiom ($m$ITS) and by <Ref>. Hence the outer part of the diagram is commutative as well.

Let $(\boxtimes,m)$ be an external tensor structure on $\Hbb$, and let $(\otimes,m^i)$ denote the external tensor structure defined from it via <Ref>. Suppose that we are given an internal commutativity constraint $c$ on $(\boxtimes,m)$. Then, associating

* to every $S \in \Scal$, the natural isomorphism of functors $\Hbb(S) \times \Hbb(S) \rightarrow \Hbb(S)$

\begin{equation*}
c^i = c^i_S: A \otimes B \xrightarrow{\sim} B \otimes A
\end{equation*}

defined by taking the composite

\begin{equation*}
\begin{tikzcd}[font=\small]
A \otimes B \arrow[equal]{d} && B \otimes A \arrow[equal]{d} \\
\Delta_S^*(A \boxtimes B) \arrow{r}{c} & \Delta_S^* \tau^*(B \boxtimes A) \arrow[equal]{r} & \Delta_S^*(B \boxtimes A)
\end{tikzcd}
\end{equation*}

defines an internal commutativity constraint $c^i$ on $(\otimes,m^i)$.

We have to show that the definition satisfies conditions ($c$ITS-1) and ($c$ITS-2).

We start from condition ($c$ITS-1): given $S \in \Scal$, we have to show that the diagram of functors $\Hbb(S) \times \Hbb(S) \rightarrow \Hbb(S)$

\begin{equation*}
\begin{tikzcd}
A \otimes B \arrow{r}{c^i} \arrow{dr}{\id} & B \otimes A \arrow{d}{c^i} \\
& A \otimes B
\end{tikzcd}
\end{equation*}

is commutative. Expanding the definitions, we obtain the outer part of the diagram

\begin{equation*}
\begin{tikzcd}[font=\small]
\Delta_S^*(A \boxtimes B) \arrow{r}{c} \arrow{ddrr}{\id} & \Delta_S^* \tau^*(B \boxtimes A) \arrow[equal]{r} & \Delta_S^*(B \boxtimes A) \arrow{d}{c} \\
&& \Delta_S^* \tau^*(A \boxtimes B) \arrow[equal]{d} \\
&& \Delta_S^*(A \boxtimes B)
\end{tikzcd}
\end{equation*}

that we decompose as

\begin{equation*}
\begin{tikzcd}[font=\small]
\bullet \arrow{r}{c} \arrow[bend right]{ddrr}{\id} \arrow[equal]{dr} & \bullet \arrow[equal]{r} \arrow{d}{c} & \bullet \arrow{d}{c} \\
& \Delta_S^* \tau^* \tau^*(A \boxtimes B) \arrow[equal]{r} & \bullet \arrow[equal]{d} \\
&& \bullet
\end{tikzcd}
\end{equation*}

Here, the upper-right triangle is commutative by axiom ($c$ETS-1) while the remaining pieces are commutative by naturality and by <Ref>.

We now treat condition ($c$ETS-2): given a morphism $f: T \rightarrow S$ in $\Scal$, we have to show that the diagram of functors $\Hbb(S) \times \Hbb(S) \rightarrow \Hbb(T)$

\begin{equation*}
\begin{tikzcd}
f^* A \otimes f^* B \arrow{r}{c^i} \arrow{d}{m^i} & f^* B \otimes f^* A \arrow{d}{m^i} \\
f^*(A \otimes B)  \arrow{r}{c^i} & f^*(B \otimes A)
\end{tikzcd}
\end{equation*}

is commutative. Expanding the definitions, we obtain the diagram

\begin{equation*}
\begin{tikzcd}[font=\small]
\Delta_T^* (f^* A \boxtimes f^* B) \arrow{r}{c} \arrow{d}{m} & \Delta_T^* \tau^* (f^* B \boxtimes f^* A) \arrow[equal]{r} & \Delta_T^* (f^* B \boxtimes f^* A) \arrow{d}{m} \\
\Delta_T^* (f \times f)^* (A \boxtimes B) \arrow[equal]{d} && \Delta_T^* (f \times f)^* (B \boxtimes A) \arrow[equal]{d} \\
f^* \Delta_S^* (A \boxtimes B) \arrow{r}{c} & f^* \Delta_S^* \tau^* (B \boxtimes A) \arrow[equal]{r} & f^* \Delta_S^* (B \boxtimes A)
\end{tikzcd}
\end{equation*}

that we decompose as

\begin{equation*}
\begin{tikzcd}[font=\small]
\bullet \arrow{r}{c} \arrow{dd}{m} & \bullet \arrow[equal]{r} \arrow{d}{m} & \bullet \arrow{d}{m} \\
& \Delta_T^* \tau^* (f \times f)^* (B \boxtimes A) \arrow[equal]{r} \arrow[equal]{d} & \bullet \arrow[equal]{dd} \\
\bullet \arrow{r}{c} \arrow[equal]{d} & \Delta_T^* (f \times f)^* \tau^* (B \boxtimes A) \arrow[equal]{d} \\
\bullet \arrow{r}{c} & \bullet \arrow[equal]{r} & \bullet
\end{tikzcd}
\end{equation*}

Here, upper-left piece is commutative by axiom ($c$ETS-2) while the other pieces are commutative by naturality and by <Ref>. This proves the claim.

The constructions of <Ref> and <Ref> canonically define mutually inverse bijections between equivalence classes of symmetric internal and external tensor structures on $\Hbb$.

We keep the same notation adopted in the proof of <Ref>.

Start from a symmetric internal tensor structure $(\otimes,m;c)$ on $\Hbb$, and let $c'$ denote the internal commutativity constraint on $(\otimes',m)$ obtained from $c$ by applying first <Ref> and then <Ref>. We claim that the equivalence of internal tensor structures $e: (\otimes,m) \xrightarrow{\sim} (\otimes',m')$ constructed in <Ref> satisfies condition (eq-$c$ITS): given $S \in \Scal$, we have to show that the diagram of functors $\Hbb(S) \times \Hbb(S) \rightarrow \Hbb(S)$

\begin{equation*}
\begin{tikzcd}
A \otimes B \arrow{r}{e} \arrow{d}{c} & A \otimes' B \arrow{d}{c'} \\
B \otimes A \arrow{r}{e} & B \otimes' A
\end{tikzcd}
\end{equation*}

is commutative. Unwinding the definitions, we obtain the more explicit diagram

\begin{equation*}
\begin{tikzcd}[font=\small]
A \otimes B \arrow{rr}{c} \arrow[equal]{d} && B \otimes A \arrow[equal]{d} \\
\Delta_S^* pr^{12,*}_1 A \otimes \Delta_S^* pr^{12,*}_2 B \arrow{d}{m} && \Delta_S^* pr^{21,*}_2 B \otimes \Delta_S^* pr^{21,*}_1 A \arrow{d}{m} \\
\Delta_S^*(pr^{12,*}_1 A \otimes pr^{12,*}_2 B) \arrow[equal]{d} && \Delta_S^*(pr^{21,*}_2 B \otimes pr^{21,*}_1 A) \arrow[equal]{d} \\
\Delta_S^*(\tau^* pr^{21,*}_1 A \otimes \tau^* pr^{21,*}_2 B) \arrow{r}{c} & \Delta_S^*(\tau^* pr^{21,*}_2 B \otimes \tau^* pr^{21,*}_1 A) \arrow{r}{m} & \Delta_S^* \tau^* (pr^{21,*}_2 B \otimes pr^{21,*}_1 A)
\end{tikzcd}
\end{equation*}

that we decompose as

\begin{equation*}
\begin{tikzcd}[font=\small]
\bullet \arrow{rrr}{c} \arrow[equal]{d} &&& \bullet \arrow[equal]{d} \\
\bullet \arrow{d}{m} \arrow{rr}{c} && \Delta_S^* pr^{12,*}_2 B \otimes \Delta_S^* pr^{12,*}_1 A \arrow{dl}{m} \arrow[equal]{ur} & \bullet \arrow{d}{m}  \\
\bullet \arrow[equal]{d} \arrow{r}{c} & \Delta_S^*(pr^{12*}_2 B \otimes pr^{12,*}_1 A) \arrow[equal]{dr} & \Delta_S^* \tau^* pr^{21,*}_2 B \otimes \Delta_S^* \tau^* pr^{21,*}_1 A \arrow[equal]{ur} \arrow[equal]{u} \arrow{d}{m}  & \bullet \arrow[equal]{d} \\
\bullet \arrow{rr}{c} && \bullet \arrow{r}{m} & \bullet
\end{tikzcd}
\end{equation*}

Here, the left central piece is commutative by axiom ($c$ITS-2) while the other pieces are commutative by axiom ($m$ITS) and by naturality. This proves the claim.

Conversely, start from a symmetric external tensor structure $(\boxtimes,m;c)$ on $\Hbb$, and let $c'$ denote the commutativity constraint on $(\boxtimes',m')$ obtained from $c$ by applying first <Ref>  and then <Ref>. We claim that the equivalence of external tensor structures $e: (\boxtimes',m') \xrightarrow{\sim} (\boxtimes,m)$ constructed in the proof of <Ref> satisfies condition (eq-$c$ETS): given $S_1, S_2 \in \Scal$, we have to show that the diagram of functors $\Hbb(S_1) \times \Hbb(S_2) \rightarrow \Hbb(S_1 \times S_2)$

\begin{equation*}
\begin{tikzcd}
A_1 \boxtimes' A_2 \arrow{r}{e} \arrow{d}{c'} & A_1 \boxtimes A_2 \arrow{d}{c} \\
\tau^* (A_2 \boxtimes' A_1) \arrow{r}{e} & \tau^* (A_2 \boxtimes A_1)
\end{tikzcd}
\end{equation*}

is commutative. Unwinding the definitions, we obtain the more explicit diagram

\begin{equation*}
\begin{tikzcd}[font=\tiny]
A_1 \boxtimes A_2 \arrow[equal]{d} \arrow{r}{c} & \tau^* (A_2 \boxtimes A_1) \arrow[equal]{dr} \\
\Delta_{S_1 \times S_2}^*(pr^{12}_1 \times pr^{12}_2)^* (A_1 \boxtimes A_2)  && \tau^* \Delta_{S_2 \times S_1}^* (pr^{21}_2 \times pr^{21}_1)^* (A_2 \boxtimes A_1)  \\
&& \tau^* \Delta_{S_2 \times S_1}^* (pr^{21,*}_2 A_2 \boxtimes pr^{21,*}_1 A_1) \arrow[equal]{d} \arrow{u}{m} \\
\Delta_{S_1 \times S_2}^* (pr^{12,*}_1 A_1 \boxtimes pr^{12,*}_2 A_2) \arrow[equal]{d} \arrow{uu}{m} && \Delta_{S_1 \times S_2}^* (\tau \times \tau)^* (pr^{21,*}_2 A_2 \boxtimes pr^{21,*}_1 A_1) \\
\Delta_{S_1 \times S_2}^* (\tau^* pr^{21,*}_1 A_1 \boxtimes \tau^* pr^{21,*}_2 A_2) \arrow{r}{c} & \Delta_{S_1 \times S_2}^* \hat{\tau}^*(\tau^* pr^{21,*}_2 A_2 \boxtimes \tau^* pr^{21,*}_1 A_1) \arrow[equal]{r} & \Delta_{S_1 \times S_2}^* (\tau^* pr^{21,*}_2 A_2 \boxtimes \tau^* pr^{21,*}_1 A_1) \arrow{u}{m}
\end{tikzcd}
\end{equation*}

that we decompose as

\begin{equation*}
\begin{tikzcd}[font=\tiny]
\bullet \arrow[equal]{d} \arrow{rr}{c} && \bullet \arrow[equal]{dr} \arrow[equal]{dl} \\
\bullet \arrow{r}{c} & \Delta_{S_1 \times S_2}^* (pr^{12}_1 \times pr^{12}_2)^* \hat{\tau}^* (A_2 \boxtimes A_1) \arrow[equal]{r} & \Delta_{S_1 \times S_2}^* (\tau \times \tau)^* (pr^{21}_2 \times pr^{21}_1)^* (A_2 \boxtimes A_1) \arrow[equal]{r} & \bullet \\
& \Delta_{S_1 \times S_2}^* \hat{\tau}^* (pr^{12}_2 \times pr^{12}_1)^* (A_2 \boxtimes A_1) \arrow[equal]{u} \arrow[equal]{r} & \Delta_{S_1 \times S_2}^* \hat{\tau}^* (\tau \times \tau)^* (pr^{21}_2 \times pr^{21}_1)^* (A_2 \boxtimes A_1) \arrow[equal]{u} & \bullet \arrow[equal]{d} \arrow{u}{m} \\
\bullet \arrow[equal]{d} \arrow{uu}{m} \arrow{r}{c} & \Delta_{S_1 \times S_2}^* \hat{\tau}^* (pr^{12,*}_2 A_2 \boxtimes pr^{12,*}_1 A_1) \arrow{u}{m} & \Delta_{S_1 \times S_2}^* \hat{\tau}^* (\tau \times \tau)^* (pr^{21,*}_2 A_2 \boxtimes pr^{21,*}_1 A_1) \arrow{u}{m} & \bullet \arrow[equal]{l} \arrow[bend right]{uul}{m} \\
\bullet \arrow{r}{c} & \bullet \arrow[equal]{rr} \arrow[equal]{u} \arrow{ur}{m} && \bullet \arrow{u}{m}
\end{tikzcd}
\end{equation*}

Here, the central-left piece is commutative by axiom ($c$ETS-2) while the other pieces are commutative by axiom ($m$ETS) and by naturality. This proves the claim and concludes the proof.

§ UNIT CONSTRAINTS

The goal of this section is to introduce unit constraints in the setting of internal and external tensor structures and to compare them; in particular, we introduce unit sections following the general notions fixed in <Ref>.

The notion of unit constraint for a single monoidal category comes from <cit.>; in the case of fibered categories, one needs to require inverse image functors to respect unit constraints as in <cit.>. The latter definition can be formulated in the language of internal tensor structures as follows:

Let $(\otimes,m)$ be an internal tensor structure on $\Hbb$.

* An internal unit constraint $u$ on $(\otimes,m)$ is the datum of

* a section $\unit$ of the $\Scal$-fibered category $\Hbb$, called the unit section,

* for every $S \in \Scal$, two natural isomorphisms of functors $\Hbb(S) \rightarrow \Hbb(S)$

\begin{equation*}
u_r = u_{r,S}: A \otimes \unit_S \xrightarrow{\sim} A, \qquad \qquad u_l = u_{l,S}: \unit_S \otimes B \xrightarrow{\sim} B
\end{equation*}

satisfying the following conditions:

($u$ITS-0) For every $S \in \Scal$, the diagram in $\Hbb(S)$

\begin{equation*}
\begin{tikzcd}
\unit_S \otimes \unit_S \arrow[bend left=50]{d}{u_l} \arrow[bend right=50]{d}{u_r} \\
\unit_S
\end{tikzcd}
\end{equation*}

is commutative.

($u$ITS-1) For every morphism $f: T \rightarrow S$ in $\Scal$, the two diagrams of functors $\Hbb(S) \rightarrow \Hbb(T)$

\begin{equation*}
\begin{tikzcd}
f^* A \otimes f^* \unit_S \arrow{r}{\unit^*} \arrow{d}{m} & f^* A \otimes \unit_T \arrow{d}{u_r} \\
f^*(A \otimes \unit_S) \arrow{r}{u_r}  & f^* A
\end{tikzcd}
\qquad
\begin{tikzcd}
f^* \unit_S \otimes f^* B  \arrow{d}{m} \arrow{r}{\unit^*} & \unit_T \otimes f^* B \arrow{d}{u_l} \\
f^*(\unit_S \otimes B)  \arrow{r}{u_l} & f^* B
\end{tikzcd}
\end{equation*}

are commutative.

We say that $(\otimes,m;u)$ is a unitary internal tensor structure on $\Hbb$.

* Let $(\otimes,m;u)$ and $(\otimes',m';u')$ be unitary internal tensor structures on $\Hbb$. An equivalence of unitary internal tensor structures $e: (\otimes,m;u) \xrightarrow{\sim} (\otimes',m';u')$ is the datum of

* an equivalence of internal tensor structures $e: (\otimes,m) \xrightarrow{\sim} (\otimes',m')$,

* an isomorphism of unit sections $w: \unit \xrightarrow{\sim} \unit'$

satisfying the following additional condition:

(eq-$u$ITS) For every $S \in \Scal$, the two diagrams of functors $\Hbb(S) \rightarrow \Hbb(S)$

\begin{equation*}
\begin{tikzcd}
A \otimes \unit_S \arrow{r}{u_r} \arrow{d}{w} & A \\
A \otimes \unit'_S \arrow{r}{e} & A \otimes' \unit'_S \arrow{u}{u'_r}
\end{tikzcd}
\qquad
\begin{tikzcd}
\unit_S \otimes B \arrow{r}{u_l} \arrow{d}{w} & B \\
\unit'_S \otimes B \arrow{r}{e} & \unit'_S \otimes' B \arrow{u}{u'_l}
\end{tikzcd}
\end{equation*}

are commutative.

In order to obtain a similar notion of the setting of external tensor structures, we need to reformulate the action of unit objects with the help of suitable projection morphisms, as follows:

Let $(\boxtimes,m)$ be an external tensor structure on $\Hbb$.

* An external unit constraint $u$ on $(\boxtimes,m)$ is the datum of

* a section $\unit$ of the $\Scal$-fibered category $\Hbb$, called the unit section,

* for every $S_1, S_2 \in \Scal$, a natural isomorphism of functors $\Hbb(S_1) \rightarrow \Hbb(S_1 \times S_2)$

\begin{equation*}
u_r = u_{r,S_1,S_2}: A_1 \boxtimes \unit_{S_2} \xrightarrow{\sim} pr^{12,*}_1 A_1
\end{equation*}

as well as a natural isomorphism of functors $\Hbb(S_2) \rightarrow \Hbb(S_1 \times S_2)$

\begin{equation*}
u_l = u_{l,S_1,S_2}: \unit_{S_1} \boxtimes A_2 \xrightarrow{\sim} pr^{12,*}_2 A_2
\end{equation*}

satisfying the following conditions:

($u$ETS-0) For every $S \in \Scal$, the diagram in $\Hbb(S)$

\begin{equation*}
\begin{tikzcd}
pr^{12,*}_1 \unit_{S_1} \arrow{dr}{\unit^*} & \unit_{S_1} \boxtimes \unit_{S_2} \arrow{l}{u_l} \arrow{r}{u_r} & pr^{12,*}_2 \unit_{S_2} \arrow{dl}{\unit^*} \\
& \unit_{S_1 \times S_2}
\end{tikzcd}
\end{equation*}

is commutative.

($u$ETS-1) For every choice of morphisms $f_i: T_i \rightarrow S_i$ in $\Scal$, $i = 1,2$, the diagram of functors $\Hbb(S_1) \rightarrow \Hbb(T_1 \times T_2)$

\begin{equation*}
\begin{tikzcd}
f_1^* A_1 \boxtimes f_2^* \unit_{S_2} \arrow{r}{\unit^*} \arrow{d}{m} & f_1^* A_1 \boxtimes \unit_{T_2} \arrow{r}{u_r} & pr^{12,*}_1 f_1^* A_1 \arrow[equal]{d} \\
(f_1 \times f_2)^*(A_1 \boxtimes \unit_{S_2}) \arrow{rr}{u_r} && (f_1 \times f_2)^* pr^{12,*}_1 A_1
\end{tikzcd}
\end{equation*}

and the diagram of functors $\Hbb(S_2) \times \Hbb(T_1 \times T_2)$

\begin{equation*}
\begin{tikzcd}
f_1^* \unit_{S_1} \boxtimes f_2^* A_2 \arrow{r}{\unit^*} \arrow{d}{m} & \unit_{T_1} \boxtimes f_2^* A_2 \arrow{r}{u_r} & pr^{12,*}_2 f_2^* A_2 \arrow[equal]{d} \\
(f_1 \times f_2)^*(\unit_{T_1} \boxtimes A_2) \arrow{rr}{u_r} && (f_1 \times f_2)^* pr^{12,*}_2 A_2
\end{tikzcd}
\end{equation*}

are commutative.

We say that $(\boxtimes,m;u)$ is a unitary external tensor structure on $\Hbb$.

* Let $(\boxtimes,m;u)$ and $(\boxtimes',m';u')$ be unitary external tensor structures on $\Hbb$. An equivalence of unitary external tensor structures $e: (\boxtimes,m;u) \xrightarrow{\sim} (\boxtimes',m';u')$ is the datum of

* an equivalence of internal tensor structures $e: (\otimes,m) \xrightarrow{\sim} (\otimes',m')$,

* an isomorphism of unit sections $w: \unit \xrightarrow{\sim} \unit'$

satisfying the following additional condition:

(eq-$u$ETS) For every $S_1, S_2 \in \Scal$, the diagram of functors $\Hbb(S_1) \rightarrow \Hbb(S_1 \times S_2)$

\begin{equation*}
\begin{tikzcd}
A_1 \boxtimes' \unit'_{S_2} \arrow{r}{u'_r} \arrow{d}{w} & pr^{12,*}_1 A_1 \\
A_1 \boxtimes \unit_{S_2} \arrow{r}{e} & A_1 \boxtimes \unit_{S_2} \arrow{u}{u'_r}
\end{tikzcd}
\end{equation*}

and the diagram of functors $\Hbb(S_2) \rightarrow \Hbb(S_1 \times S_2)$

\begin{equation*}
\begin{tikzcd}
\unit_{S_1} \boxtimes' A_2 \arrow{r}{u'_l} \arrow{d}{w} & pr^{12,*}_2 A_2 \\
\unit_{S_1} \boxtimes A_2 \arrow{r}{e} & \unit_{S_2} \boxtimes A_2 \arrow{u}{u_l}
\end{tikzcd}
\end{equation*}

are commutative.

In the same spirit as for the previous two sections, we now describe how unit constraints can be translated between the internal and the external setting along the constructions of <Ref> and <Ref>. This is the content of the following two results:

Let $(\otimes,m)$ be an internal tensor structure on $\Hbb$, and let $(\boxtimes,m^e)$ denote the external tensor structure defined from it as in <Ref>. Suppose that we are given an internal unit constraint $u$ (with unit section $\unit$) on $(\otimes,m)$. Then, associating

* to every $S_1, S_2 \in \Scal$, the natural isomorphism of functors $\Hbb(S_1) \rightarrow \Hbb(S_1 \times S_2)$

\begin{equation*}
u_r^e: A_1 \boxtimes \unit_{S_2} := pr^{12,*}_1 A_1 \otimes pr^{12,*}_2 \unit_{S_2} \xrightarrow{\unit^*} pr^{12,*}_1 A_1 \otimes \unit_{S_1 \times S_2} \xrightarrow{u_r} pr^{12,*}_1 A_1
\end{equation*}

and the natural isomorphism of functors $\Hbb(S_2) \rightarrow \Hbb(S_1 \times S_2)$

\begin{equation*}
u_l^e: \unit_{S_2} \boxtimes A_2 := pr^{12,*}_1 \unit_{S_1} \otimes pr^{12,*}_2 A_2 \xrightarrow{\unit^*} \unit_{S_1 \times S_2} \otimes pr^{12,*}_2 A_2 \xrightarrow{u_l} pr^{12,*}_2 A_2
\end{equation*}

defines an external unit constraint $u^e$ with unit section $\unit$ on $(\boxtimes,m^e)$.

We have to show that the definition satisfies conditions ($u$ETS-0) and ($u$ETS-1).

We start from condition ($u$ETS-0): given $S_1, S_2 \in \Scal$, we have to show that the diagram in $\Hbb(S)$