Enriched Categories for Parameterized Circuit Semantics

TL;DR

This work develops a categorical framework for parameterized circuit semantics using enrichment. It shows that if a category of interpretations $\mathcal{C}$ is enriched over a Cartesian monoidal category $\mathcal{V}$, then parameterized maps of the form $P \to \mathcal{C}^{\mathcal{V}}(X,Y)$ yield a well-defined category of parameterized morphisms, and that a $\mathcal{V}$-monoidal (resp. braided) structure on $\mathcal{C}^{\mathcal{V}}$ lifts to a symmetric (resp. braided) monoidal structure on the parameterized category $\mathbf{Param}(P, \mathcal{C})$. The construction includes a strict monoidal functor $\mathrm{ev}_{\theta}$ for each $\theta$ and a canonical embedding $j: \mathcal{C} \to \mathbf{Param}(P, \mathcal{C})$ that recovers parameter-free semantics as constant families. The framework is illustrated via a Top-enriched example $\mathcal{D}=\mathbf{Param}(\mathbb{R}^2, \mathbf{FVect})$ and is positioned to extend to classical circuit analysis and parameterized equivalence checking, with potential connections to abstract interpretation and logic-based parameterizations.

Abstract

It is well-known that combinatorial circuits are modeled mathematically by string diagrams in a monoidal category. Given a gate set $Σ$, the circuits over $Σ$ can be thought of as string diagrams in the free monoidal category generated by $Σ$. In this model, circuit semantics are then given by monoidal functors out of this free category. For quantum circuits, this functor is often valued in the category of unitary matrices. This model suffices for concrete quantum circuits, but fails to describe parameterized families of quantum circuits, such as those which arise in the analysis of ansatz circuits. Intuitively, this functor should be valued in parameterized families of unitary matices, though it is not immediately clear what this mean through a categorical lens. In this paper, we show that the parameterized semantics studied in prior work can be understood through enrichment and internal constructions. We determine sufficient conditions under which this construction yields a symmetric monoidal category, and suggest how these semantics could be extended to classical circuit analysis and parameterized equivalence checking.

Theorems & Definitions (6)

• Definition 2.1: Kelly1982
• Definition 2.2: Kelly1982
• Definition 2.3: Kelly1982
• Example 2.4
• Definition 2.5: KongZheng2018
• Definition 2.6: [KongZheng2018] Let $\mathcal{V}$ be a smc with braiding $\sigma$. A commutative $\mathcal{V}$-functor is a $\mathcal{V}$-functor $F^{\mathcal{V}}: \mathcal{C}^{\mathcal{V}} \times \mathcal{D}^{\mathcal{V}} \to \mathcal{E}^{\mathcal{V}}$ such that the data $F^{\mathrm{rev}}_0: ( x, y ) \mapsto F^{\mathcal{V}}_0( y, x )$ and $F^{\mathrm{rev}} = F \circ \sigma$ defines a $\mathcal{V}$-functor $F^{\textrm{rev}}: \mathcal{D}^{\mathcal{V}} \times \mathcal{C}^{\mathcal{V}} \to \mathcal{E}^{\mathcal{V}}$. Let $\mathcal{V}$ be a smc and $( \mathcal{C}^{\mathcal{V}}, \otimes^{\mathcal{V}}, \mathbb{I}^{\mathcal{V}}, \alpha^{\mathcal{V}}, \lambda^{\mathcal{V}}, \rho^{\mathcal{V}} )$ be a monoidal $\mathcal{V}$-category such that $\otimes^{\mathcal{V}}$ commutative. A $\mathcal{V}$-braiding for $\mathcal{C}^{\mathcal{V}}$ is a $\mathcal{V}$-natural isomorphism $\beta^{\mathcal{V}}: \otimes^{\mathcal{V}} \to \otimes^{\mathrm{rev}}$ such that $( \mathcal{C}, \otimes, \mathbb{I}, \alpha, \lambda, \rho, \beta )$ is a braided monoidal category. Moreover, if $( \mathcal{C}, \otimes, \mathbb{I}, \alpha, \lambda, \rho, \beta )$ is symmetric monoidal then $( \mathcal{C}^{\mathcal{V}}, \otimes^{\mathcal{V}}, \mathbb{I}^{\mathcal{V}}, \alpha^{\mathcal{V}}, \lambda^{\mathcal{V}}, \rho^{\mathcal{V}}, \beta^{\mathcal{V}} )$ is a symmetric $\mathcal{V}$-monoidal category. Recall from \ref{['Ex:Enriched']} that FVect is a Top-enriched category. Moreover, FVect is Top-monoidal with respect to the Kronecker tensor product. This is because the tensor product of matrices can be written as a multivariate polynomial function in the components of the two matrices, and is therefore continuous. Since permutations are continuous, FVect is also braided monoidal. Fix a Cartesian category $( \mathcal{V}, \times, \mathbb{I}, \alpha, \rho, \lambda )$. If $\mathcal{C}^{\mathcal{V}}$ is a $\mathcal{V}$-category, then the morphisms in its underlying category can be seen as generalized elements in $\mathcal{V}$. Given some object $P \in \mathcal{V}_0$, one can then consider the generalized elements of $\mathcal{V}$ which factor through $P$, commonly known as the the $P$-shaped elements. In this section, $P$ will be thought of as the parameters used to construct parameterized families of morphisms in $\mathcal{C}^{\mathcal{V}}$. First, it will be shown that using the Cartesian structure on $\mathcal{V}$, these $P$-shaped elements can be assembled into a category $\textbf{Param}( P, \mathcal{C} )$ which generalizes the parameterized constructions in MillerBakewell2020JeandelPerdrix2018. Second, it will be shown that if $\mathcal{C}^{\mathcal{V}}$ is $\mathcal{V}$-monoidal, then $\textbf{Param}( P, \mathcal{C} )$ is monoidal. Third, it will be shown that if $\mathcal{C}^{\mathcal{V}}$ is braided (resp. symmetric), then so is $\textbf{Param}( P, \mathcal{C} )$. $g \star f$ $i_X$ $g \boxtimes f$ $a_A$ $\ell_X$ $r_X$ The categorical and monoidal structure on $\mathbf{Param}( P, \mathcal{C} )$, depicted as string diagrams. In these diagrams $X,Y,Z \in \textbf{Param}( P, \mathcal{C} )$ with $f: X \to Y$, $g: Y \to Z$, and $h: X' \to Y'$. We write $Q = X \otimes ( Y \otimes Z )$, $R = ( X \otimes Y) \otimes Z$, and $A = ( X, Y, Z )$. This section provides the data for $\textbf{Param}( P, \mathcal{C} )$ and proves that this data satisfies the conditions of a category. The objects in $\textbf{Param}( P, \mathcal{C} )$ are defined to be the objects in $\mathcal{C}$, since parameterized morphisms in $\textbf{Param}( P, \mathcal{C} )$ should have the same sources and targets as the morphisms in $\mathcal{C}$. The morphisms from $X$ to $Y$ are defined to be the $P$-shaped elements of $\mathcal{C}^{\mathcal{V}}( X, Y )$, that is, elements of $\mathcal{V}( P, \mathcal{C}^{\mathcal{V}}( X, Y ) )$. For each $X \in \mathcal{C}_0$, the unit $i_X$ for $X$ in $\textbf{Param}( P, \mathcal{C} )( X, X )$ is defined to be $1_X^{\mathcal{V}} \circ e_P$. Given $f \in \textbf{Param}( P, \mathcal{C} )( X, Y )$ and $g \in \textbf{Param}( P, \mathcal{C} )( Y, Z )$, the composite $g \star f$ is defined to be $M_\mathcal{C} \circ ( g \times f ) \circ \Delta_P$, which first copies the parameter to pass to both of the morphisms, and then composes the morphisms in $\mathcal{C}^{\mathcal{V}}$. Both $i_{(-)}$ and $( - ) \star ( - )$ are illustrated diagrammatically in \ref{['Fig:Param1']}. $\mathbf{Param}( P, \mathcal{C} )$ is a category for each $P \in \mathcal{V}_0$. Moreover, $\mathbf{Param}( \mathbb{I}, \mathcal{C} ) = \mathcal{C}$. Let $P \in \mathcal{V}_0$. First, it must be shown that $( \star )$ is associative. Let $X \xrightarrow{f} Y \xrightarrow{g} Z \xrightarrow{h} W$ in $\mathbf{Param}( P, \mathcal{C} )$. Then the following equation of diagrams hold. $h \star ( g \star f )$ = = = = $( h \star g ) \star f$ Since $f$, $g$, and $h$ were arbitrary, then $( \star )$ is associative. Next, it must be shown that $( \star )$ is unital. Let $f: X \to Y$ in $\mathbf{Param}( P, \mathcal{C} )$. Then the following equation of diagrams hold. $f \star i_x$ = = = = = $f$ It follows by a symmetric argument that $i_y \star f = f$. Since $f$ was arbitrary, then $( \star )$ is unital. Since $P$ was arbitrary, then $\mathbf{Param}( P, \mathcal{C} )$ is a category for each $P \in \mathcal{V}_0$. Next, let $\mathcal{D} = \textbf{Param}( \mathbb{I}, \mathcal{C} )$. Clearly, $\mathcal{D}_0 = \mathcal{C}_0$ and $\mathcal{D}( X, Y ) = \mathcal{C}( X, Y )$ for each $X, Y \in \mathcal{C}_0$. Since $e_{\mathbb{I}} = 1_{\mathbb{I}}$, then $i_X = 1_X^{\mathcal{V}}$. Since $\Delta_{\mathbb{I}} = \rho_{\mathbb{I}}$, then $g \star f = M_{\mathcal{C}} \circ ( g \times f ) \circ \Delta_{\mathbb{I}} = M_{\mathcal{C}} \circ ( g \times f ) \circ \rho_{\mathbb{I}}$ for each $X \xrightarrow{f} Y \xrightarrow{g} Z$ in $\mathcal{C}$. In conclusion $\mathcal{D} = \mathcal{C}$. When $\mathcal{V}( \mathbb{I}, P ) \ne \varnothing$, each morphism $\theta \in \mathcal{V}( \mathcal{I}, P )$ can be thought of as a generalized parameter. Then evaluating a parameterized morphism at $\theta$ is the same as composition with $\theta$. In prior work, evaluation of parameterized functions could be proven to distribute over function composition JeandelPerdrix2018MillerBakewell2020. That is to say, if $M$ and $N$ are parameterized families of matrices, and $\theta$ is a parameter for the matrices, then $(M \circ N)( \theta ) = (M(\theta)) (N(\theta))$. This equation suggests that evaluation should be functorial. For each $\theta \in \mathcal{V}( \mathcal{I}, P )$, define the data for a functor $\textsf{ev}_\theta: \mathbf{Param}( P, \mathcal{C} ) \to \mathcal{C}$ to be $( \textsf{ev}_\theta )_0: X \mapsto X$ and $( \textsf{ev}_\theta )_{X,Y}: f \mapsto f \circ \theta$. This is well-defined since $( \mathbf{Param}( P, \mathcal{C} ) )_0 = \mathcal{C}_0$ and $\mathcal{V}( \mathbb{I}, \mathcal{C}^{\mathcal{V}}( X, Y ) ) = \mathcal{C}( X, Y )$. An important fact about $\textsf{ev}_{\theta}$ is that cancels out composition with $e_P$. It follows from this fact that $\textsf{ev}_{\theta}$ preserves many categorical structures, such as identities. Let $\mathcal{V}$ be a Cartesian monoidal category with $P \in \mathcal{V}_0$ and $\mathcal{C}$ a $\mathcal{V}$-category. If $f \in \mathcal{C}( X, Y )$ and $\theta \in \mathcal{V}( \mathbb{I}, P )$, then $(\textsf{ev}_\theta)_{X,Y}( f \circ e_P ) = f$. Let $f \in \mathcal{C}( X, Y )$ and $\theta \in \mathcal{V}( \mathbb{I}, P )$. Then the following equation of diagrams holds. $(\textsf{ev}_\theta)_{X,Y}( f \circ e_P )$ = = = = $f$ Since $f$ and $\theta$ were arbitrary, then if $f \in \mathcal{C}( X, Y )$ and $\theta \in \mathcal{V}( \mathbb{I}, P )$. $\textsf{ev}_\theta: \mathbf{Param}( P, \mathcal{C} ) \to \mathcal{C}$ is a functor for each $\theta \in \mathcal{V}( \mathbb{I}, P )$. Fix some $\theta \in \mathcal{V}( \mathbb{I}, P )$. First, it must be show that $\textsf{ev}_\theta$ preserves morphism composition. Let $X \xrightarrow{f} Y \xrightarrow{g} Z$ in $\mathbf{Param}( P, \mathcal{C} )$. Then the following equation of diagrams hold. $( \textsf{ev}_\theta )_{X, Z}( g \star f )$ = = = $( ( \textsf{ev}_\theta )_{Y,Z}( g ) ) \circ ( ( \textsf{ev}_\theta )_{X,Y}( f ) )$ Since $f$ and $g$ were arbitrary, then $\textsf{ev}_\theta$ preserves morphism composition. Next, it must be shown that $\textsf{ev}_\theta$ preserves identities. Let $X \in \mathcal{C}_0$. Since $i_X = 1_X \circ e_P$, then $( \textsf{ev}_\theta )_{X, X}( i_X ) = 1_X$ by \ref{['Lem:InclEv']}. Since $X$ was arbitrary, then $\textsf{ev}_\theta$ preserves identities. Then $\textsf{ev}_\theta$ is a functor. Since $\theta$ was arbitrary, then $\textsf{ev}_\theta$ is a functor for each $\theta \in \mathcal{V}( \mathbb{I}, P )$. Recall from \ref{['Ex:EnirchedMon']} that FVect is Top-enriched. Since Top is Cartesian, then there exists a category $\textbf{D} = \textbf{Param}( \mathbb{R}^2, \textbf{FVect} )$. This category provides semantics for quantum circuits in two variables. For any continuous map $f: \mathbb{R}^2 \to \mathbb{R}$, the $X$-rotation $R_X( f( \theta ) ) = \cos( f( \theta ) ) I + i \sin( f( \theta ) ) X$ is a morphism in $\mathcal{D}( 2, 2 )$. Moreover, $R_X( \theta_1 ) \star R_X( 2\theta_2 ) = R_X( \theta_1 + 2\theta_2 )$, as expected. Moreover, each $\theta \in \textbf{Top}( \mathbb{I}, \mathbb{R}^2 )$ picks out a parameter $( \theta_1, \theta_2 )$. If $\theta$ picks out $( \pi / 2, 0 )$, then $\textsf{ev}_\theta( R_X( \theta_1 ) \star R_X( 2\theta_2 ) ) = iX$. In categories like Set and Top, objects can be thought of as sets and every non-empty set has generalized elements. However, there exists concrete Cartesian monoidal categories, such as meet semilattices which do not admit interesting generalized elements. Then in meet semilattices, it does not make sense to evaluate prameterized morphisms. However, the construction still makes sense and yields interesting results. For example, consider the $3$-element poset $X = \{ \bot, 1, \top \}$ with the self-evident order $\bot < 1 < \top$. This poset forms a meet semilattice with $\land: X \times X \to X$ defined as follows. \bot \land \bot= \bot\bot \land 1= \bot\bot \land \top= \bot1 \land \bot= \bot1 \land 1= 11 \land \top= 1\top \land \bot= \bot\top \land 1= 1\top \land \top= \top Then $( X, \le, \land )$ defines a Cartesian monoidal category $\mathcal{V}$ where $\land$ is the monoidal product and $\top$ is the monoidal unit. Every $\mathcal{V}$-enriched category corresponds to a (possibly infinite) directed graph whose edges are labeled by elements of $X$, with pairs of composable edges $f: X \to Y$ and $g: Y \to Z$ satisfying $g \land f \le ( g \circ f)$. Moreover, each vertex $X$ must have a self-loop $X \to X$ labeled by the element $T$. This is because $1_X \in \mathcal{V}( \top, \mathcal{C}^{\mathcal{V}}( X, X )$ implies $\top \le \mathcal{C}^{\mathcal{V}}( X, X )$. As a simple example, consider a category $\mathcal{C}^{\mathcal{V}}$ such that $\mathcal{C}^{\mathcal{V}}_0 = \{ A, B, C, D \}$ and the homsets are defined as follows. \mathcal{C}( A, A )= \top\mathcal{C}( A, B )= \top\mathcal{C}( A, C )= 1\mathcal{C}( A, D )= \top\mathcal{C}( B, A )= \bot\mathcal{C}( B, B )= \top\mathcal{C}( B, C )= \bot\mathcal{C}( B, D )= 1\mathcal{C}( C, A )= \bot\mathcal{C}( C, B )= \bot\mathcal{C}( C, C )= \top\mathcal{C}( C, D )= \top\mathcal{C}( D, A )= \bot\mathcal{C}( D, B )= \bot\mathcal{C}( D, C )= \bot\mathcal{C}( D, D )= \top The corresponding graph is illustrated below. Since $\mathcal{C}( X, Y ) = \mathcal{V}( \top, \mathcal{C}^{\mathcal{V}}( X, Y ) )$, then the underlying category $\mathcal{C}$ picks out the posetal category such that $X \rightarrow Y$ if and only if $\mathcal{C}( X, Y ) = \top$. The corresponding graph is illustrated below. From a logical perspective, $\mathcal{C}$ picks out the edges which as absolutely certain. Another reasonable construction is to first pick out a truth value $P \in X$, and then construct the posetal category containing the edges entailed by $P$. Since $( \textbf{Param}( P, \mathcal{C} ) )( X, Y ) = \mathcal{V}( P, \mathcal{C}( X, Y ) )$, then this is precisely the construction outlined in this section. For example, $\textbf{Param}( 1, \mathcal{C} )$ corresponds to the following graph. Moreover, $\textbf{Param}( \bot, \mathcal{C} )$ is the complete graph on $4$ vertices. Assume that $\mathcal{C}^{\mathcal{V}}$ admits a $\mathcal{V}$-monoidal structure $( \mathcal{C}^{\mathcal{V}}, \otimes^{\mathcal{V}}, \mathbb{J}^{\mathcal{V}}, \alpha^{\mathcal{V}}, \lambda^{\mathcal{V}}, \rho^{\mathcal{V}} )$. This section shows how $\mathcal{D} = \mathbf{Param}( P, \mathcal{C} )$ inherits the monoidal structure of $\mathcal{C}^{\mathcal{V}}$. The first step is to define a monoidal product $\boxtimes: \mathcal{D} \times \mathcal{D} \to \mathcal{D}$. As expected, $\boxtimes_0 = \otimes_0$. Then for each pair of functions $f: X \to Y$ and $g: X' \to Y'$ in $\mathcal{D}$, $f \boxtimes g$ is defined to be $\otimes^{\mathcal{V}}_{((X,X'),(Y,Y'))} \circ ( f \times g) \circ \Delta_P$, as illustrated in \ref{['Fig:Param1']}. $\boxtimes: \mathbf{Param}( P, \mathcal{C} ) \times \mathbf{Param}( P, \mathcal{C} ) \to \mathbf{Param}( P, \mathcal{C} )$ is a functor. The next step is to show that $\boxtimes$ is unital and associative. Since the objects of $\mathcal{D}$ share the same monoidal structure as $\mathcal{C}$, then the monoidal unit for $\boxtimes$ should be $\mathbb{J}$. It remains to define the natural transformations $a: ( - ) \boxtimes ( ( - ) \boxtimes ( - ) ) \Rightarrow ( ( - ) \boxtimes ( - ) ) \boxtimes ( - )$, $\ell: \mathbb{J} \boxtimes ( - ) \to ( - )$ and $r: ( - ) \boxtimes \mathbb{J} \to ( - )$. For each choice of $X, Y, Z \in \mathcal{C}_0$, define $a_{(X,Y,Z)}$ to be $\alpha^{\mathcal{V}}_{(X,Y,Z)} \circ e_P$. Analogously, for each $X \in \mathcal{C}$, define $\ell_X$ to be $\lambda^{\mathcal{V}}_X \circ e_P$ and $r_X$ to be $\rho^{\mathcal{V}}_X \circ e_P$. Of course, each component of $a$, $\ell$, and $r$ must be invertible, so that the transformations are isomorphisms. Thankfully, composition with $e_P$ always preserves inverses. Diagrammatic illustrations of $a$, $\ell$, and $r$ can be found in \ref{['Fig:Param1']}. If $X \xrightarrow{f} Y$ is invertible in $\mathcal{C}$, then $k = f \circ e_P$ is invertible in $\mathbf{Param}( P, \mathcal{C} )$. It suffices to show that $f^{-1} \circ e_P$ is the inverse to $k$. $( f^{-1} \circ e_p ) \star k$ = = = = = $i_X$ Then $f^{-1} \circ e_P$ is the left inverse to $k$ in $\textbf{Param}( P, \mathcal{C} )$. By a symmetric argument, $f^{-1} \circ e_P$ is also the right inverse to $k$ in $\textbf{Param}( P, \mathcal{C} )$. In conclusion, $k$ is invertible in $\textbf{Param}( P, \mathcal{C} )$. $a: ( - ) \boxtimes ( ( - ) \boxtimes ( - ) ) \Rightarrow ( ( - ) \boxtimes ( - ) ) \boxtimes ( - )$ is a natural isomorphism. $\ell: \mathbb{J} \boxtimes ( - ) \Rightarrow ( - )$ and $r: ( - ) \boxtimes \mathbb{J} \Rightarrow ( - )$ are natural isomorphisms. It remains to be shown that $a$, $\ell$, and $r$ satisfy the coherence conditions of a monoidal category. This is true, since $a$, $\ell$, and $r$ are defined to be the inclusions of $\alpha$, $\lambda$, and $\rho$ from $\mathcal{C}$ into $\textbf{Param}( P, \mathcal{C} )$. This inclusion is explored more in \ref{['Sect:Embed']}. For now, this property is used to show that $\textbf{Param}( P, \mathcal{C} )$ also inherits the coherence equations from $\mathcal{C}$. $( \mathbf{Param}( P, \mathcal{C} ), \boxtimes, a, \ell, r )$ is a monoidal category for each $P \in \mathcal{V}_0$. $\textsf{ev}_\theta: \mathbf{Param}( P, \mathcal{C} ) \to \mathcal{C}$ is a strict monoidal functor for each $\theta \in \mathcal{V}( \mathbb{I}, P )$. Let $\theta \in \mathcal{V}( \mathbb{I}, P )$. Clearly $\textsf{ev}_\theta$ preserves the monoidal unit, since $(\textsf{ev}_\theta)_0$ is the identity. Next, it must be shown that $\textsf{ev}_\theta$ preserves monoidal composition. Let $X \xrightarrow{f} Y$ and $X' \xrightarrow{g} Y'$ in $\textbf{Param}( P, \mathcal{C} )$. Then the follow equation of diagrams holds. $( \textsf{ev}_\theta )_{X \boxtimes X', Y \boxtimes Y'}( g \boxtimes f )$ = = = $( ( \textsf{ev}_\theta )_{X,Y}( g ) ) \otimes ( ( \textsf{ev}_\theta )_{X',Y'}( f ) )$ Since $f$ and $g$ were arbitrary, then $\textsf{ev}_\theta$ preserves monoidal composition. It remains to be shown that $\textsf{ev}_\theta$ preserves the structural natural transformations. Let $X, Y, Z \in \mathcal{C}_0$. Then it follows from \ref{['Lem:InclEv']} that $\textsf{ev}_\theta( a_{(X,Y,Z)} ) = \alpha_{(X,Y,Z)}$, $\textsf{ev}_\theta( \ell_X ) = \lambda_X$, and $\textsf{ev}_\theta( r_X ) = \rho_X$. Since $X$, $Y$, and $Z$ were arbitrary, then $\textsf{ev}_\theta$ preserves the structural natural transformations of $\mathcal{C}$. In conclusion, $\textsf{ev}_\theta$ is a strict monoidal functor. Recall the example of $\mathcal{D} = \textbf{Param}( \mathbb{R}^2, \textbf{FVect} )$ from \ref{['Ex:ParamElt']}. Since FVect is Top-monoidal with respect to the Kronecker tensor product $\otimes$, then $\mathcal{D}$ inherits this monoidal structure of $( \textbf{FVect}, \otimes, \mathbb{C}, \alpha, \lambda, \rho )$. For example, $R_X( \theta_1 ) \boxtimes R_X( 2 \theta_2 )$ is an element of $\mathcal{D}( 4, 4 )$. This operator corresponds to a $2$-qubit circuit, which rotates the first qubit by $\theta_1$ degrees, and the second qubit by $\theta_2$ degrees. If $\theta \in \textbf{Top}( \mathbb{I}, \mathbb{R}^2 )$ picks out $( \pi / 2, 0 )$, then $\textsf{ev}_\theta( R_X( \theta_1 ) \boxtimes R_X( 2 \theta_2 ) ) = iX \otimes I$. Assume that $( \mathcal{C}^{\mathcal{V}}, \otimes^{\mathcal{V}}, \mathbb{J}^{\mathcal{V}}, \alpha^{\mathcal{V}}, \lambda^{\mathcal{V}}, \rho^{\mathcal{V}} )$ admits a $\mathcal{V}$-braiding $\beta^{\mathcal{V}}$. This sections show how $\mathcal{D}$ inherits the monoidal structure of $\mathcal{C}^{\mathcal{V}}$. The first step is to define a natural isomorphism $b: ( - ) \boxtimes ( - ) \Rightarrow ( - ) \boxtimes ( - ) \circ c$ where $c$ is the symmetric braiding on Cat as a Cartesian category. As in the cases of $a$, $\ell$, and $r$, the solution is to simply define each $b_{(X,Y)}$ to be the inclusion $\beta_{(X,Y)}^{\mathcal{V}} \circ e_P$ of $\beta_{(X,Y)}^{\mathcal{V}}$ into $\mathcal{D}( X, Y )$. Unfortunately, the naturality of $\beta^{\mathcal{V}}$ does not immediately imply the naturality of $b$. This is because $b$ is natural with respect to $c$, whereas $\beta^{\mathcal{V}}$ is natural with respect to $\sigma$, the braiding on $\mathcal{V}$. Of course, $\beta$ is natural with respect to $c$, though this naturality only concerns the generalized elements of $\mathcal{C}$, rather than the $P$-shaped elements of $\mathcal{C}$. To handle $P$-shaped elements of $\mathcal{C}$, the naturality of $\beta$ must be combined with the naturality of $\sigma$, to introduce a $c$ term. To introduce a $\sigma$ term, it suffices to recall that $\Delta = \sigma \circ \Delta$. $b: ( - ) \boxtimes ( - ) \Rightarrow ( - ) \boxtimes ( - ) \circ c$ is a natural isomorphism. It remains to be shown that $b$ satisfies the coherence conditions for a monoidal braiding. However, this part of the proof is straight-forward, and follows from the same techniques used to prove the coherence of $a$, $\ell$, and $r$. That is, the coherence of $\beta$ yields several diagrammatic equations, which immediately imply the coherence for $b$, once all of the $a$, $b$, and $i$ terms have been expanded. This yields a braiding on $\textbf{Param}( P, \mathcal{C} )$, which is symmetric provided $\beta^{\mathcal{V}}$ is symmetric. $( \mathbf{Param}( P, \mathcal{C} ), \boxtimes, a, , r, b )$ is a braided monoidal category. Moreover, if $\beta$ is symmetric, then $b$ is also symmetric. $\textsf{ev}_\theta: \mathbf{Param}( P, \mathcal{C} ) \to \mathcal{C}$ is a strict braided monoidal functor for each $\theta \in \mathcal{V}( \mathbb{I}, P )$. Let $\theta \in \mathcal{V}( \mathbb{I}, P )$. By \ref{['Thm:ParamEv']} the functor $\textsf{ev}_\theta$ is strict monoidal and by \ref{['Thm:ParamBraid']} the monoidal category $\textbf{Param}( P, \mathcal{C} )$ admits a braiding $b$. Let $X, Y \in \mathcal{C}_0$. Since $b_{X,Y} = \beta_{X,Y} \circ e_P$, then $\textsf{ev}_\theta( b_{X,Y} ) = \beta_{X,Y}$ by \ref{['Lem:InclEv']}. Since $X$ and $Y$ were arbitrary, then $\textsf{ev}_\theta$ preserves the braiding on $\textbf{Param}( P, \mathcal{C} )$. Then $\textsf{ev}_\theta$ is a strict braided monoidal functor. Since $\theta$ was arbitrary, then $\textsf{ev}_\theta$ is a strict braided monoidal functor for each $\theta \in \mathcal{V}( \mathbb{I}, \mathcal{C} )$. Recall the example of $\mathcal{D} = \textbf{Param}( \mathbb{R}^2, \textbf{FVect} )$ from \ref{['Ex:ParamMon']}. Since FVect is braided Top-monoidal, then $\mathcal{D}$ also inherits a braiding from FVect. For example the braiding on $\mathbb{C} \oplus \mathbb{C}$ is $b_{(1,1)} = \beta_{(1,1)} \circ e_P$. Unpacking this definition in Top, $b_{(1,1)}: ( \theta_1, \theta_2 ) \mapsto 0110.$ This construction behaves as expected. For example, $b_{(1,1)}( \theta ) \star R_Z( \theta_1 ) \star b_{(1,1)}( \theta ) = 0110 \star e^{i\theta}00e^{-i\theta} \star 0110 = e^{-i\theta}00e^{i\theta} = R_Z( -\theta_1 ).$ Intuitively, $b_{(1,1)}$ is the inclusion of $\beta_{(1,1)}$ into $\mathcal{D}( 1, 1 )$. This is made precise in the next section. As in previous sections, let $\mathcal{V}$ be a smc and $\mathcal{C}$ be a $\mathcal{V}$-category. In previous work MillerBakewell2020JeandelPerdrix2018PehamBurgholzer2022XuLi2022, parameterized circuits are thought of as a generalization of parameter-free circuits. That is to say, every parameter-free circuit is trivially a parameterized circuit. Formally, if $C$ is a parameter-free circuit with semantic interpretation $[\![C]\!]$, then its parameterized interpretation should be a constant function valued at $[\![C]\!]$. Indeed, there exists an embedding $j$ of $\mathcal{C}$ into $\mathcal{D} = \textbf{Param}( P, \mathcal{C} )$ such that each $[\![C]\!]$ maps to a constant function $j( [\![C]\!] )$ which always evaluates to [ [C] ]. Stated categorically, this means that for each $\theta \in \mathcal{V}( \mathbb{I}, \mathcal{C} )$, the functor $\textsf{ev}_\theta$ is a retraction of $\mathcal{D}$ onto $\mathcal{C}$ in Cat. Moreover, the corresponding section $j: \mathcal{C} \to \mathcal{D}$ is the same for all choices of $\theta$. In this sense, $j$ is the inclusion of $\mathcal{C}$ into $\mathcal{D}$ such that each morphism in $\mathcal{C}$ maps to a constant function in $\mathcal{D}$. The functor $j: \mathcal{C} \to \textbf{Param}( P, \mathcal{C} )$ is defined such that $j_0: X \mapsto X$ and for each $f \in \mathcal{C}( X, Y )$, $j_{X,Y}( f ) = f \circ e_P$. $j: \mathcal{C} \to \textbf{Param}( P, \mathcal{C} )$ is functorial. If $\mathcal{C}^{\mathcal{V}}$ is $\mathcal{V}$-monoidal, then $j$ is strict monoidal. If $\mathcal{C}^{\mathcal{V}}$ is $\mathcal{V}$-braided, then $j$ is strict braided monoidal. If $\mathcal{V}( \mathbb{I}, P ) \ne \varnothing$, then $j$ is faithful. For each $\theta \in \mathcal{V}( \mathbb{I}, \mathcal{C} )$, $\textsf{ev}_\theta$ is a retraction with $\textsf{ev}_\theta \circ j = 1_{\mathcal{C}}$. Let $\theta \in \mathcal{V}( \mathbb{I}, \mathcal{C} )$. It must be shown that $F = \textsf{ev}_\theta \circ j$ is the identity functor on $\mathcal{C}$. Clearly, $F_0$ is the identity on objects, since $F_( X ) = (\textsf{ev}_\theta)_0( j_0( X ) ) = (\textsf{ev}_\theta)_0( X ) = X$ for each $X \in \mathcal{C}_0$. Next, let $f: X \to Y$ in $\mathcal{C}$. Since $j_{X,Y}( f ) = f \circ e_P$, then $F_{X,Y}( f ) = f$ by \ref{['Lem:InclEv']}. Since $f$ was arbitrary, then $F$ is also the identity on homsets. Then $\textsf{ev}_\theta \circ j = 1_{\mathcal{C}}$. Since $\theta$ was arbitrary, then for each $\theta \in \mathcal{V}( \mathbb{I}, \mathcal{C} )$, $\textsf{ev}_\theta$ is a retraction with $\textsf{ev}_\theta \circ j = 1_{\mathcal{C}}$. Recall the example of $\mathcal{D} = \textbf{Param}( \mathbb{R}^2, \textbf{FVect} )$ from \ref{['Ex:ParamMon']}. For each choice of $n$ and $m$ in $\mathbb{N}$, the morphism $b_{(n,m)}$ is the inclusion of the permutation matrix $\beta_{(n,m)}$ into $\mathcal{D}( n, m )$. That is, $b_{(n,m)} = j\left( \beta_{(n,m)} \right)$. Since $\mathcal{V}( \mathbb{I}, \mathbb{R}^2 )$ is non-empty, then $j$ is also faithful. Indeed, if $j( f ) = j( g )$, then $f = g$ because $( \textsf{ev}_\theta )_{X,Y}( j( f ) ) = ( \textsf{ev}_\theta )_{X,Y}( j( g ) )$ where $\theta = (0, 0)$. Since every retraction defines an idempotent, it is natural to ask how these idempotents act on $\textbf{Param}( P, \mathcal{C} )$. Pick $\theta \in \mathcal{V}( \mathbb{I}, P )$ and define $\textsf{const}_\theta = j \circ \textsf{ev}_\theta$. Then given any parameterized morphism $f: X \to Y$ in $\mathcal{D}$, the functor $(\textsf{const}_\theta)_{X,Y}( f )$ picks out the constant function in $\mathcal{D}( X, Y )$ that agrees with $f$ when evaluated at $\theta$. Formally, this means that $\textsf{ev}_\kappa( \textsf{const}_\theta( f ) ) = \textsf{ev}_\theta( f )$ for all $\kappa \in \mathcal{V}( \mathbb{I}, P )$. This is illustrated by the following equation of diagrams. $\textsf{ev}_\kappa( \textsf{const}_\theta( f ) )$ = = = = $\textsf{ev}_\theta( f )$ Recall the example of $\mathcal{D} = \textbf{Param}( \mathbb{R}^2, \textbf{FVect} )$ from \ref{['Ex:ParamMon']}. As before, let $\theta = ( \pi / 2, 0 )$. Since $\textsf{ev}_\theta( R_X( \theta_1 ) ) = iX$, then $\textsf{const}_\theta( R_X( \theta_1 ) ): ( \theta_1, \theta_2 ) \mapsto iX$. This paper introduced a notion of parameterized morphism through enrichment, which characterizes the semantics of parameterized quantum circuits, and also more abstract logical constructions. To the best of our knowledge, this is the first work to consider categorical semantics for parameterized circuits. There is ongoing work outlined in KoziellPipe2024 to model parameterized circuits though lenses, though this work has not been published yet. We propose several directions for future work. An important problem in parameterized circuit analysis is parameterized equivalence checking. Given two circuits $C_1$ and $C_2$ parameterized by $P$, this question asks if $[\![C_1]\!]( \theta ) = [\![C_2]\!]( \theta )$ for all $\theta \in P$. An obvious direction for future work is to reconstruct the problem of parameterized equivalence in this more general framework. It can then be asked which domain-specific equivalence checking techniques, such as the analytic methods of PehamBurgholzer2022 generalize to wider classes of parameterized semantics. It would also be interesting to rephrase standard techniques, such as reparameterization (see, e.g., WateringYeung2024), in this framework, to see if any new insights can be gained. As outlined in \ref{['Ex:Heyting']}, all Heyting semilattices are Cartesian categories. This means that any categories enriched over a Heyting semilattices can be parameterized by valuations in the underlying model intuitionistic logic. It would be interesting to expand \ref{['Ex:LatticeParam']} in this direction, and to explore applications to program analysis. In enriched category theory, there is a notion of basis change, which maps $\mathcal{U}$-enriched categories to $\mathcal{V}$-enriched categories via a functor from $\mathcal{U}$ to $\mathcal{V}$. In a similar fashion, computer scientists often employ a technique called abstract interpretation which maps complicated concrete domains to simpler abstract domains modeled by lattices CousotCousot1977. We conjecture that a carefully selected change of base could yield an abstract interpretation for parameterized circuits. @book{HeunenVicary2019, author={Chris Heunen and Jamie Vicary}, title={Categories for Quantum Theory: An Introduction}, publisher={Oxford University Press}, year={2019}, doi={10.1093/oso/9780198739623.001.0001} }@book{MacLane2010, author={Saunders Mac Lane}, title={Categories for the Working Mathematician}, publisher={Springer}, year={2010}, doi={10.1007/978-1-4757-4721-8} }@book{Kelly1982, author={Max Kelly}, title={Basic Concepts of Enriched Category Theory}, publisher={Springer}, year={1982}, doi={10.1112/blms/15.1.96} }@incollection{Selinger2010, author={Peter Selinger}, title={A survey of graphical languages for monoidal categories}, year={2010}, publisher={Springer}, booktitle={New Structures for Physics}, pages={289--355}, doi={10.1007/978-3-642-12821-9_4} }@misc{KoziellPipe2024, title={Hybrid quantum-classical machine learning with string diagrams}, author={Alexander Koziell-Pipe and Aleks Kissinger}, year={2024}, eprint={2407.03673}, archiveprefix={arXiv}, primaryclass={quant-ph} }@article{KongZheng2018, title={Drinfeld center of enriched monoidal categories}, volume={323}, doi={10.1016/j.aim.2017.10.038}, journal={Advances in Mathematics}, publisher={Elsevier BV}, author={Liang Kong and Hao Zheng}, year={2018}, pages={411–426} }@book{Vollmer1982, author={Heribert Vollmer}, title={Introduction to Circuit Complexity: A Uniform Approach}, publisher={Springer}, year={1982}, doi={10.1007/978-3-662-03927-4} }@article{BaezCoya2010, title={Props in network theory}, volume={33}, number={25}, journal={Theory and Applications of Categories}, author={John C. Baez and Brandon Coya and Franciscus Rebro}, year={2010}, pages={727--783} }@article{Lafont2003, title={Towards an algebraic theory of Boolean circuits}, journal={Journal of Pure and Applied Algebra}, volume={184}, number={2}, pages={257--310}, year={2003}, author={Yves Lafont} }@inproceedings{JeandelPerdrix2018, title={Diagrammatic reasoning beyond Clifford+T quantum mechanics}, doi={10.1145/3209108.3209139}, booktitle={Logic in Computer Science}, publisher={ACM}, author={Emmanuel Jeandel and Simon Perdrix and Renaud Vilmart}, year={2018}, pages={569--578} }@article{MillerBakewell2020, title={Finite verification of infinite families of diagram equations}, volume={318}, doi={10.4204/eptcs.318.3}, journal={EPTCS}, publisher={Open Publishing Association}, author={Hector Miller-Bakewell}, year={2020}, pages={27--52} }@article{HugginsPatil2019, title={Towards quantum machine learning with tensor networks}, volume={4}, doi={10.1088/2058-9565/aaea94}, number={2}, journal={Quantum Science and Technology}, publisher={IOP Publishing}, author={William Huggins and Piyush Patil and Bradley Mitchell and K. Birgitta Whaley and E. Miles Stoudenmire}, year={2019}, pages={024001} }@article{PehamBurgholzer2022, title={Equivalence Checking of Quantum Circuits With the ZX-Calculus}, volume={12}, doi={10.1109/jetcas.2022.3202204}, number={3}, journal={IEEE Journal on Emerging and Selected Topics in Circuits and Systems}, publisher={IEEE}, author={Tom Peham and Lukas Burgholzer and Robert Wille}, year={2022}, pages={662--675} }@book{Hammack2009, author={Richard Hammack}, title={Book of Proof}, publisher={Self-published}, url={https://richardhammack.github.io/BookOfProof/}, year={2009} }@book{Jech2003, author={Thomas Jech}, title={Set Theory}, publisher={Springer}, year={2003}, doi={10.1007/3-540-44761-X} }@article{Kelly1964, title={On MacLane's conditions for coherence of natural associativities, commutativities, etc.}, journal={Journal of Algebra}, volume={1}, number={4}, pages={397--402}, year={1964}, doi={10.1016/0021-8693(64)90018-3}, author={G. M Kelly} }@article{MacLane1963, title={Natural associativity and commutativity}, journal={Rice University Studies}, volume={49}, pages={28--46}, year={1963}, author={Saunders Mac Lane} }@inproceedings{XuLi2022, author={Mingkuan Xu and Zikun Li and Oded Padon and Sina Lin and Jessica Pointing and Auguste Hirth and Henry Ma and Jens Palsberg and Alex Aiken and Umut A. Acar and Zhihao Jia}, title={Quartz: superoptimization of quantum circuits}, year={2022}, publisher={ACM}, doi={10.1145/3519939.3523433}, booktitle={Programming Language Design and Implementation (PLDI)}, pages={625--640} }@book{HarrisWeste2010, author={David Harris and Neil Weste}, title={CMOS VLSI Design: A Circuits and Systems Perspective}, publisher={Pearson}, year={2010}, doi={10.5555/1841628} }@article{CrossJavadiAbhari2022, author={Andrew Cross and Ali Javadi-Abhari and Thomas Alexander and Niel De Beaudrap and Lev S. Bishop and Steven Heidel and Colm A. Ryan and Prasahnt Sivarajah and John Smolin and Jay M. Gambetta and Blake R. Johnson}, title={OpenQASM 3: A Broader and Deeper Assembly Language}, year={2022}, publisher={ACM}, volume={3}, number={3}, journal={ACM Trans. on Quantum Comp.}, articleno={12}, numpages={50} }@article{Hotz1965, author={Günter Hotz}, title={Eine Algebraisierung des Syntheseproblems von Schaltkreisen I}, year={1965}, publisher={Justus-Liebig Universität}, volume={1}, number={1}, journal={Elektronische Informationsverarbeitung und Kybernetik}, pages={185--205} }@article{Backens2021, title={There and back again: A circuit extraction tale}, volume={5}, doi={10.22331/q-2021-03-25-421}, journal={Quantum}, publisher={Verein zur Forderung des Open Access Publizierens in den Quantenwissenschaften}, author={Miriam Backens and Hector Miller-Bakewell and Giovanni de Felice and Leo Lobski and John van de Wetering}, year={2021}, pages={421} }@incollection{BluteScott2004, series={London Mathematical Society Lecture Note Series}, title={Category Theory for Linear Logicians}, booktitle={Linear Logic in Computer Science}, publisher={Cambridge University Press}, author={Richard Blute and Philip Scott}, editor={Thomas Ehrhard and Jean-Yves Girard and Paul Ruet and Philip Scott}, year={2004}, pages={3--64}, collection={London Mathematical Society Lecture Note Series} }@misc{WateringYeung2024, title={Optimal compilation of parametrised quantum circuits}, author={John van de Wetering and Richie Yeung and Tuomas Laakkonen and Aleks Kissinger}, year={2024}, eprint={2401.12877}, archiveprefix={arXiv}, primaryclass={quant-ph}, doi={10.48550/arXiv.2401.12877} }@inproceedings{CousotCousot1977, author={Patrick Cousot and Radhia Cousot}, title={Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints}, year={1977}, publisher={Association for Computing Machinery}, doi={10.1145/512950.512973}, booktitle={Principles of Programming Languages}, pages={238--252} }@article{JoyalStreet1991, title={The geometry of tensor calculus, I}, journal={Advances in Mathematics}, volume={88}, number={1}, pages={55--112}, year={1991}, doi={10.1016/0001-8708(91)90003-P}, author={André Joyal and Ross Street} } A reoccurring theme in mathematics is to study structure preserving transformations between categories of mathematical objects. For example, extension program semantics is the study of structure preserving transformations between a category of syntactic constructions, and some category of semantic interpretations. A defining characteristic of category theory is that homomorphisms are seen as the defining characteristic of a category, rather than their specific objects. Following this perspective, the key object of study in category theory is that of the functor, which describes homomorphisms between categories. A (locally small) category $\mathcal{C}$ consists of the following data. Objects. A collection $\mathcal{C}_0$.Morphisms. For each $X, Y \in \mathcal{C}_0$, a set $\mathcal{C}( X, Y )$ whose elements are denoted $X \xrightarrow{f} Y$.Identities. For each $X \in \mathcal{C}_0$, a morphism $1_X \in \mathcal{C}( X, X )$.Composition. For each $X, Y, Z \in \mathcal{C}_0$, a function $\circ: \mathcal{C}( Y, Z ) \times \mathcal{C}( X, Y ) \to \mathcal{C}( X, Z )$. This data satisfies the following conditions. Associativity. For each $X \xrightarrow{f} Y \xrightarrow{g} Z \xrightarrow{h} Z$, $h \circ ( g \circ f ) = ( h \circ g ) \circ f$.Unitality. For each $X \xrightarrow{f} Y$, $1_Y \circ f = f = f \circ 1_X$. Common categories include Set (sets and functions), FVect (finite-dimensional $\mathbb{C}$-vector spaces and linear transformations), Top (topological spaces and continuous functions), Cat (categories and functors) and Pos (posets and monotone maps). If $( P, \le )$ is a poset, then there exists a category $\mathcal{P}$ such that $\mathcal{P}_0 = P$ and there exists a unique arrow from $x \in P$ to $y \in P$ if and only if $x \le y$. A common trend in category theory is to define mathematical constructions by their data, and the equations it satisfies. Often, these equations can become tedious to write out. Instead, commuting diagrams are used to communicate the equations in a visual fashion. A diagram for a category $\mathcal{C}$ is a directed graph whose vertices are labeled by objects in $\mathcal{C}_0$, and whose edges are labeled by morphisms in $\mathcal{C}( X, Y )$ where $X$ is the label for the source of the edge and $Y$ is the label for the target of the edge. A diagram is said to commute if for each pair of paths with the same source and the same target, their labels compose to the same morphism (this is unambiguous by associativity). For example, $X \xrightarrow{f} Y$ and $Y \xrightarrow{f} X$ are inverses if the following diagram commutes. Equationally, this says that $h \circ f = 1_X$ and $f \circ h = 1_Y$. Note that when $h \circ f = 1_X$ we say that $f$ is a section and $h$ is a retraction. A functor $F: \mathcal{C} \to \mathcal{D}$ between categories is a choice of objects $F_0( X ) \in \mathcal{D}_0$ for each $X \in \mathcal{C}_0$, and an indexed family of functions $F_{X,Y}: \mathcal{C}( X, Y ) \to \mathcal{D}( F_0( X ), F_0( Y ) )$, satisfying the following conditions. Composition Preservation. For each $X \xrightarrow{f} Y \xrightarrow{g} Z$, $F_{X,Z}( g \circ f ) = F_{Y,Z}( g ) \circ F_{X,Y}( f )$.Identity Preservation. For each $X \in \mathcal{C}_0$, $F_{X,X}( 1_X ) = 1_{F_0(X)}$. If $F_{X,Y}$ is inject for each $X, Y \in \mathcal{C}$, then $F$ is faithful. A natural transformation $\eta: F \Rightarrow G$ between functors is an indexed family of morphisms $\eta_X: F_0( X ) \to G_0( X )$ such that the following diagram commutes. Every category $\mathcal{C}$ admits an identity functor $1_{\mathcal{C}}: \mathcal{C} \to \mathcal{C}$ which acts as the identity both on objects and on moprhisms. There exists a functor $\Delta: \textbf{Set} \to \textbf{Set}$ such that $\Delta_0( X ) = X \times X$ and $\Delta_{X,Y}( f ) = ( x \mapsto ( f(x), f(x) )$. This concept will be generalized in the next section. An important construction in the category of sets is the Cartesian product. In set theory, the Cartestian product is usually defined explicitly using set-builder notation, as in Jech2003Hammack2009. However, the Cartesian product is also characterized by its projection maps, together with a universal property. This characterization generalizes to other categories, as follows. A category $\mathcal{C}$ has (finite) products if for each pair of objects $X_1$ and $X_2$ in $\mathcal{C}$, there exists an object $X_1 \times X_2$ in $\mathcal{C}$ with morphisms $X_1 \times X_2 \xrightarrow{\pi_1} X_1$ and $X_1 \times X_2 \xrightarrow{\pi_2} X_2$ such that for each pair of morphisms $C \xrightarrow{f} X_1$ and $C \xrightarrow{g} X_2$ in $\mathcal{C}$, there exists a unique morphism $C \xrightarrow{h} X_1 \times X_2$ such that the following diagram commutes. The canonical example of a categorical product is the Cartesian product in Set. The categories Top and FVect also have finite products (the projections $\pi_1$ and $\pi_2$ are continuous). In Top this is given by the Cartesian product of topological spaces with the product topology. In FVect this is given by the direct product of vector spaces (the projections $\pi_1$ and $\pi_2$ are linear). In Pos this is given by the Cartesian product of the underlying set and order relation (the projections are trivially monotone). The product Cat also has finite products. This means that for each pair of categories $\mathcal{C}$ and $\mathcal{D}$ in Cat, there exists a product category $\mathcal{C} \times \mathcal{D}$. The objects in $( \mathcal{C} \times \mathcal{D} )_0$ are tuples of the form $( X, Y )$, where $X \in \mathcal{C}_0$ and $Y \in \mathcal{D}_0$. The morphisms in $\mathcal{C}( ( X, Y ), ( X', Y' ) )$ are the elements of $\mathcal{C}( X, Y ) \times \mathcal{D}( X', Y' )$. Composition of morphisms is defined component-wise. It follows that the identity morphism for $( X, Y )$ is $( 1_X, 1_Y )$. Moreover, there exists a functor $c_{\mathcal{C},\mathcal{D}}: \mathcal{C} \times \mathcal{D} \to \mathcal{D} \times \mathcal{C}$ such that $F_0( X, Y ) = ( Y, X )$ and $F_{X,Y}( f, g ) = ( g, f )$. A poset $( P, \le )$ has products if and only if it is a semilattice. That is, there exists a meet $\land: P \times P \to P$ and a top element $\top \in P$ such that: (1) $a \le \top$ for all $a \in P$; (2) if $c \le a$ and $c \le b$ then $c \le a \land b$; (3) $a \le b \land a$ and $b \le a \land b$ for all $a \in P$ and $b \in P$. Moreover, if there exists an implication $\implies: P \times P \to P$ such that $c \land c \le b$ if and only if $c \le (a \implies b)$, then the poset is a model of intuitionistic propositional logic (also called a Heyting semilattice). The categorical product describes a composition for objects in a category, which extends to all morphisms in the category. However, the categorical product comes with far more data, such as the projection maps $\pi_1$ and $\pi_2$. More generally, one can consider a monoid-like structure on the objects which extends to all morphisms in the category. This generalization can be motivated by many constructions in mathematics, such as the Kronecker tensor product of vector spaces, and the parallel composition of circuits. Both examples can be described as monoidal categories. A monoidal category $( \mathcal{C}, \otimes, \mathbb{I}, \alpha, \lambda, \rho )$ is a category $\mathcal{C}$ with the following data. Monoidal Product. A functor $\otimes: \mathcal{C} \times \mathcal{C} \to \mathcal{C}$.Monoidal Unit. An object $\mathbb{I} \in \mathcal{C}_0$.Associator. A natural isomorphism $\alpha: ( - ) \otimes ( ( - ) \otimes ( - ) ) \Rightarrow ( ( - ) \otimes ( - ) ) \otimes ( - )$.Unitors. Natural isomorphism $\lambda: \mathbb{I} \otimes ( - ) \Rightarrow ( - )$ and $\rho: ( - ) \otimes \mathbb{I} \Rightarrow ( - )$. This data is subject to the condition that the following diagrams commute for all $X, Y, Z, W \in \mathcal{C}_0$. A braiding on $( \mathcal{C}, \otimes, \mathbb{I}, \alpha, \lambda, \rho )$ is a natural isomorphism $\beta: ( - ) \otimes ( - ) \Rightarrow ( ( - ) \otimes ( - ) ) \circ c$ such that the following diagrams commute for all $X, Y, Z \in \mathcal{C}_0$ (where $c$ is the braiding on Cat). If $\beta_{(X,Y)}^{-1} = \beta_{(Y,X)}$ for all $X, Y \in \mathcal{C}_0$, then $( \mathcal{C}, \otimes, \mathbb{I}, \alpha, \lambda, \rho, \beta )$ is a symmetric monoidal category (smc). Every category with finite products and a terminal object (see \ref{['Def:Term']}) is a monoidal category. In this case, the monoidal product maps each object $( X, Y ) \to X \times Y$ and each morphism $( f, g )$ to $f \times g$. In general, defining a functor $F: \mathcal{C} \times \mathcal{C} \to \mathcal{C}$ is challenging. In suffices to check that: (1) $F$ is functorial in the first component, that is $F( -, 1_X )$ is a functor for each $X \in \mathcal{C}_0$; (2) $F$ is functorial in the second component; (3) $F$ satisfies the interchange condition, that is $F( i_{Y}, g ) \circ F( f, i_{X'}) = F( f, g ) = F( f, i_{Y'} ) \circ F( i_X, g )$ for all $f: X \to Y$ and $g: X' \to Y'$. For example, the Kronecker tensor product of vector spaces satisfies these properties. The category $\textbf{FVect}$ is monoidal with respect to the Kronecker tensor product and the monoidal unit $\mathbb{C}$. Let $\mathcal{M} = ( \mathcal{C}, \otimes, \mathbb{I}, \alpha, \lambda, \rho )$ and $\mathcal{N} = ( \mathcal{D}, \boxtimes, \mathbb{J}, a, \ell, r )$ be monoidal categories. A (strict) monoidal functor from $\mathcal{M}$ to $\mathcal{N}$ is a functor $F: \mathcal{C} \to \mathcal{D}$, satisfying the following conditions. Preserves Units. $\mathbb{J} = F( \mathbb{I} )$.Preserves Products. If $X \xrightarrow{f} Y$ and $X' \xrightarrow{g} Y'$, then $F( f \otimes g ) = F( f ) \boxtimes F( g )$.Preserves Structure. For each $X, Y, Z \in \mathcal{C}_0$, $F( \alpha_{(X,Y,Z)} ) = a_{(X,Y,Z)}$, $F( \lambda_X ) = \ell_X$, and $F( \rho_X ) = r_X$. Moreover, when $\mathcal{C}$ admits a braiding $\beta$ and $\mathcal{D}$ admits a braiding $b$, then $F$ is a (strict) braided monoidal functor when $F( \beta_{(X,Y)} ) = b_{(F(X), F(Y))}$ for each $X, Y \in \mathcal{C}_0$. The equations satisfied by the natural transformations in a monoidal category are referred to as coherence conditions. These ensure the uniqueness of structural morphisms composed from $\alpha$, $\lambda$, $\rho$, $\beta$, and the identities Kelly1964MacLane1963. More specifically, if there exists a structural morphism from an object $X$ to an object $Y$, then that morphism is unique. This coherence leads to a graphical language in two dimensions, such that the horizontal dimension corresponds to morphism composition, and the vertical dimension corresponds to monoidal composition (see Selinger2010). In these language, morphisms are depicted as circuits (called string diagrams), with wires corresponding to objects and morphisms corresponding to gates. The monoidal unit $\mathbb{I}$ is denoted by an invisible wire. Each string diagram corresponds to an equivalence class of equations up to a choice of associators and unitors. By labeling the boundaries of the string diagram (i.e., including the domains and codomains), all associators and unitors become fixed (up to coherence), and a unique morphism is selected (see JoyalStreet1991). These equivalence classes are preserved by appropriate isometries of the diagrams (see Selinger2010). In particular, monoidal isometries occur on the plane, braided monoidal isometries occur in three-dimensions (i.e., wires may pass over one-another), and symmetric monoidal isometries occur in four dimensions (i.e. wires may pass through one-another). The monoidal structure on Set defined by $\otimes = \times$ and $\mathbb{I} = \{ * \}$ has many nice properties. For example, each set $X$ has a unique function $X \to \mathbb{I}$ defined by $x \mapsto *$, and each function $\mathbb{I} \to X$ picks out a unique element in $X$. Moreover, for each object $X$, there exists a function $X \to X \times X$ defined by $a \mapsto ( a, a )$ which duplicates the elements in $X$. These observations lead to two equivalent generalizations of this monoidal structure on Set, referred to as Cartesian categories. Let $( \mathcal{C}, \otimes, \mathbb{I}, \alpha, \lambda, \rho )$ be a monoidal category. A generalized element of $X \in \mathcal{C}_0$ is a morphism $\mathbb{I} \to X$. A terminal object in $\mathcal{C}$ is an object $T \in \mathcal{C}_0$ such that for each $X \in \mathcal{C}_0$, there exists a unique morphism $X \xrightarrow{!} T$. A Cartesian category is a smc $( \mathcal{C}, \otimes, \mathbb{I}, \alpha, \lambda, \rho, \beta )$ such that $\otimes$ is the product functor for $\mathcal{C}$ and $\mathbb{I}$ is the terminal object for $\mathcal{C}$. A smc $( \mathcal{C}, \otimes, \mathbb{I}, \alpha, \lambda, \rho, \beta )$ has uniform copying if there exists a natural transformation $\Delta: ( - ) \Rightarrow ( - ) \otimes ( - )$ such that $\Delta_I = \rho_I$ and the following equations are satisfied for all $X, Y \in \mathcal{C}_0$. = = $= \Delta_{X \otimes Y}$ A smc $( \mathcal{C}, \otimes, \mathbb{I}, \alpha, \lambda, \rho, \beta )$ has uniform deleting if there exists a natural transformation $e: ( - ) \Rightarrow \mathbb{I}$ such that $e_\mathbb{I} = 1_\mathbb{I}$ and the following diagram commutes for all $X, Y \in \mathcal{C}_0$. Let $\mathcal{M} = ( \mathcal{C}, \otimes, \mathbb{I}, \alpha, \lambda, \rho, \beta )$ be a smc. Then $\mathcal{M}$ is a Cartesian category if and only if $\mathcal{M}$ has uniform copying and uniform deleting with the following equation satisfied for all $X \in \mathcal{C}_0$. = = It is important to note that the naturality of $\Delta$ states that $\Delta_Y \circ f = (f \otimes f) \circ \Delta_X$ for each $f \in \mathcal{C}( X, Y )$. Moreover, if $Y = \mathbb{I}$, then $e_{I \otimes I} = \lambda_I$ and consequently $\Delta_Y \circ f = f \otimes f$. It is in this sense that $\Delta$ captures the notion of uniform copying. When uniform deleting is combined with a terminal unit, then it is also possible to "delete" morphisms, since $e_Y \circ f = e_X$ and $e_\mathbb{I} = 1_{\mathbb{I}}$ by uniqueness. These observations are captured by the following graphical equations. = = = Let $( \mathcal{C}, \otimes^{\mathcal{V}}, \alpha^{\mathcal{V}}, \lambda^{\mathcal{V}}, \rho^{\mathcal{V}} )$ be a $\mathcal{V}$-monoidal category. First, let $X, Y, Z, X', Y', Z' \in \mathcal{C}^{\mathcal{V}}_0$. Then the following equation captures composition preservation for $\otimes^{\mathcal{V}}$. = Next, let $X, Y \in \mathcal{C}^{\mathcal{V}}_0$. Then the following equation captures identity preservation for $\otimes^{\mathcal{V}}$. = Next, let $X, Y, Z, X', Y', Z' \in \mathcal{C}^{\mathcal{C}}_0$. Write $A = ( X, Y, Z )$ and $B = ( X', Y', Z' )$. Then the following equation captures the naturality of $\alpha^{\mathcal{V}}$. = Next, let $X, Y \in \mathcal{C}^{\mathcal{V}}_0$. Then the following equation capture the naturality of $\lambda^{\mathcal{V}}$ and $\rho^{\mathcal{V}}$. = = Next, let $X, Y, Z, W \in \mathcal{C}^{\mathcal{V}}_0$. Write $A = ( Y, Z, W )$, $B = ( X, Y \otimes Z, W )$, $C = ( X, Y ,Z )$, $D = ( X, Y, Z \otimes W )$, $E = ( X \otimes Y, Z, W )$, $S = X \otimes ( Y \otimes ( Z \otimes W ) )$, and $T = ( ( X \otimes Y ) \otimes Z ) \otimes W$. Then the following equation captures the coherence condition for the associator. = Finally, let $X, Y \in \mathcal{C}^{\mathcal{V}}_0$. Write $A = ( X, \mathbb{I}, Y )$. Then the following equation captures the coherence condition for the unitors. = Of course, $\alpha$, $\lambda$, and $\rho$ are not simply natural transformations, but rather natural isomorphisms. This means that each component of $\alpha$, $\lambda$, and $\rho$ each has an inverse morphism. These inverses behave the same as any $\mathcal{V}$-enriched inverse morphism. Let $( \mathcal{C}, \otimes^{\mathcal{V}}, \alpha^{\mathcal{V}}, \lambda^{\mathcal{V}}, \rho^{\mathcal{V}}, \beta^{\mathcal{V}} )$ be a braided $\mathcal{V}$-monoidal category. First, let $X, Y, Z, X', Y', Z' \in \mathcal{C}_0^{\mathcal{V}}$. Then the following equation captures composition preservation for $\otimes^{\textrm{rev}}$. = Next, let $X, Y \in \mathcal{C}_0^{\mathcal{V}}$. Then the following equation captures identity preservation for $\otimes^{\textrm{rev}}$. = Next, let $X, Y \in \mathcal{C}_0^{\mathcal{V}}$. Then the following equation captures the naturality of $\beta^{\mathcal{V}}$ where $A = ( X, Y )$ and $B = ( X', Y' )$. = Next, let $X, Y, Z \in \mathcal{C}_0$. Write $A = ( X, Z )$, $B = ( X, Z, Y )$, $C = ( Y, Z )$, $D = ( Z, X, Y )$, $E = ( X \otimes Y, Z )$, and $S = ( X, Y, Z )$. Then the following equation captures the first coherence condition for $b$. = Finally, let $X, Y, Z \in \mathcal{C}_0$. Write $A = ( X, Z )$, $B = ( Y, X, Z )$, $C = ( X, Y )$, $D = ( Y, Z, X )$, $E = ( X, Y \otimes Z )$, $S = ( X, Y, Z )$, and $\tau = \alpha^{-1}$. Then the following equation captures the second coherence condition for $b$. = As with $\alpha$, $\lambda$, and $\rho$, $\beta$ is also a natural isomorphism. This means that for each component of $\beta$, there exists an inverse $\mathcal{V}$-morphism with its corresponding diagrams. First, it must be shown that $\boxtimes$ is functorial in the second component. Let $X \in \mathcal{C}_0$. Then for each morphism $f: Y \to Z$, the expression $i_X \boxtimes f$ simplifies as follows. $i_X \boxtimes f = \quad\;\;\; \quad\;\;\; = \quad\;\;\; \quad\;\;\; = \quad\;\;\; $ To show composition preservation, let $X \xrightarrow{f} Y \xrightarrow{g} Z$. The following equation of diagrams holds. = = = Then $( i_X \boxtimes g ) \star ( i_X \boxtimes f ) = i_X \boxtimes( g \star f )$. Since $f$ and $g$ were arbitrary, then $i_X \boxtimes ( - )$ preserves composition. To show identity preservation, let $Y \in \mathcal{C}_0$. Then the following equation of diagrams holds. $i_X \boxtimes i_Y$ = = = = $i_{X \boxtimes Y}$ Since $Y$ was arbitrary, then $i_X \boxtimes ( - )$ preserves identities. Then $i_X \boxtimes ( - )$ is a functor. Since $X$ was arbitrary, then $\boxtimes$ is functorial in the second component. It follows by a symmetric argument that $\boxtimes$ is functorial in the first component. Finally, it must be shown that $\boxtimes$ satisfies the interchange condition. Let $f: X \to Y$ and $g: X' \to Y'$ in $\textbf{Param}( P, \mathcal{C} )$. Starting from $( i_{Y} \boxtimes g ) \star ( f \boxtimes i_{X'} )$, the composition in $\mathcal{C}^{\mathcal{V}}$ is pulled into $\otimes^{\mathcal{V}}$ and then simplified. = = Next, the two components of $\otimes$ are simplified to obtain $f \boxtimes g$. = = = Then $( i_{Y} \boxtimes g ) \star ( f \boxtimes 1_{X'} ) = f \boxtimes g$. To obtain the second half of the interchange condition, identities are reintroduced on the opposite side of each component in $\otimes^{\mathcal{V}}$. = = Finally, $\otimes^{\mathcal{V}}$ can be distributed over the multiplication in $\mathcal{C}^{\mathcal{V}}$ to obtain $( f \boxtimes i_{Y'} ) \star ( i_{X} \boxtimes g )$. = = Since $f$ and $g$ were arbitrary, then $\boxtimes$ satisfies the interchange condition. In conclusion, $\boxtimes$ is a functor. Let $X \xrightarrow{f} X'$, $Y \xrightarrow{g} Y'$, and $Z \xrightarrow{h} Z'$ in $\textbf{Param}( P, \mathcal{C} )$. Write $A = (X', Y', Z' )$ and $B =( X, Y, Z )$. Starting from $a_{A} \star ( f \boxtimes ( g \boxtimes h) )$, the term $a_A$ is expanded and simplified. = = Next, the associativity of $\otimes^{\mathcal{V}}$ is invoked via the naturality of $\alpha^{\mathcal{V}}$. = = Finally, the $e_P$ term is reintroduced to recover $a_B$ on the right-hand side of the composite. = = Then $a_{A} \star ( f \boxtimes ( g \boxtimes h) ) = ( ( f \boxtimes g ) \boxtimes h ) \star a_{B}$. Since $f$, $g$ and $h$ were arbitrary, then $a$ is natural. It remains to be shown that $a$ is a natural isomorphism. Let $X, Y, Z \in \mathcal{C}_0$. Since $a_{(X,Y,Z)} = \alpha_{(X,Y,Z)} \circ e_P$ with $\alpha_{(X,Y,Z)}$ invertible, then $a_{(X,Y,Z)}$ is invertible by \ref{['Lem:IncInv']}. Since $X$, $Y$, and $Z$ were arbitrary, then $a$ is a natural isomorphism. Let $f \in \textbf{Param}( P, \mathcal{C} )$. Starting from $\ell_Y \star ( i_{\mathbb{J}} \boxtimes f )$ and equation \ref{['Eq:1VarBox']}, the expression simplifies as follows. = = Then by the naturality of $\lambda$, the monoidal product in the equation is eliminated as follows. = = = Then $\ell_Y \star ( i_{\mathbb{J}} \boxtimes f ) = f \star \ell_{X}$. Since $f$was arbitrary, then $\ell$ is natural. It remains to be shown that $\ell$ is a natural isomorphism. Let $X \in \mathcal{C}_0$. Since $\ell_X = \lambda_X \circ e_P$ with $\lambda_X$ invertible, then $\ell_X$ is invertible by \ref{['Lem:IncInv']}. Since $X$ was arbitrary, then $a$ is a natural isomorphism. Then proof that $r$ is also a natural isomorphism is symmetric. By \ref{['Lem:BoxFunc']}, the data of $\boxtimes: \textbf{Param}( P, \mathcal{C} ) \times \textbf{Param}( P, \mathcal{C} ) \to \textbf{Param}( P, \mathcal{C} )$ defines a functor. Then by \ref{['Lem:BoxAssoc']} and \ref{['Lem:BoxUnitors']}, the bifunctor admits an associator $a$, a unit $\textbf{I}$, a left unitor $\ell$, and a right unitor $r$. It remains to be shown that $a$, $\ell$, and $r$ obey the coherence conditions of a monoidal category. First, the coherence for the associator is established. Let $X, Y, Z, W \in \mathcal{C}_0^{\mathcal{V}}$. Write $A = ( Y, Z, W )$, $B = ( X, Y \boxtimes Z, W)$, $C = ( X, Y, Z )$, $D = ( X, Y, Z \boxtimes W )$, $E = ( X \boxtimes Y, Z, W )$, $S = X \boxtimes ( Y \boxtimes ( Z \boxtimes W ) )$, and $T = ( ( X \boxtimes Z ) \boxtimes Z ) \boxtimes W$. Starting from $( a_A \star i_W ) \star ( a_B \star ( i_X \boxtimes a_C ) )$ and equation \ref{['Eq:1VarBox']}, the expression simplifies as follows. = $=\;\cdots\;=$ The top half of the diagram is then rewritten using the associator coherence from $\mathcal{C}^{\mathcal{V}}$. = = = = Then $( a_A \star i_W ) \star ( a_B \star ( i_X \boxtimes a_C ) ) = a_D \star a_E$. Since $A$, $B$, $C$, $D$, and $E$ were arbitrary, then coherence for the associator is established. It remains to establish coherence for the unitor. Let $X, Y \in \mathcal{C}_0^{\mathcal{V}}$. Write $A = ( X, \mathbb{J}, Y )$, $S = X \boxtimes ( \mathbb{J} \boxtimes Y )$, and $T = X \boxtimes Y$. Starting from $( r_X \boxtimes i_{\mathbb{J}} ) \star \alpha_A$ and equation \ref{['Eq:1VarBox']}, the expression simplifies as follows. = = = = = Then $( r_X \boxtimes i_{\mathbb{J}} ) \star \alpha_A = i_{\mathbb{J}} \boxtimes \lambda_Y$. Since $X$ and $Y$ were arbitrary, then then coherence for the unitor is established. Since $a$, $\ell$, and $r$ satisfy the coherence conditions for a monoidal category, then $\boxtimes$, $\mathbb{J}$, $a$, $\ell$, and $r$ define a monoidal structure for $\textbf{Param}( P, \mathcal{C} )$ . Let $f: X \to Y$ and $g: X' \to Y'$ in $\textbf{Param}( P, \mathcal{C} )$. Write $A = ( X, Y )$ and $B = ( X', Y' )$ Starting from $( g \boxtimes f ) \star B_A$, the expression simplifies as follows. = = Next, the naturality of $\beta$ is combined with the co-commutativity of $\Delta$ to transform the term $( - \boxtimes - )$ into the term $( - \boxtimes - ) \circ c$. = = = Finally, the $b$-term is reintroduced to obtain $b_B \star ( g \boxtimes f )$. = = Since $f$ and $g$ were arbitrary, then $b$ is natural. Next, let $X, Y \in \mathcal{C}_0$. Since $b_{(X,Y)} = \beta_{(X,Y)} \circ e_P$ with $beta_{(X,Y)}$ invertible, then $\ell_X$ is invertible by \ref{['Lem:IncInv']}. Since $X$ and $Y$ were arbitrary, then $b$ is a natural isomorphism. By \ref{['Thm:ParamMon']}, the data $( \textbf{Param}( P, \mathcal{C} ), \boxtimes, \mathbb{J}, a, \ell, r )$ defines a monoidal category. By \ref{['Lem:BoxSym']}, the data $b: ( - ) \boxtimes ( - ) \Rightarrow ( - ) \boxtimes ( - ) \circ c$ defines a natural isomorphism, where $c$ is the braiding for Cat as a Cartesian monoidal category. Then it suffices to show that $b$ satisfies the coherence conditions of a braided monoidal category. Let $X, Y, Z \in \mathcal{C}_0$. Write $A = ( X, Z )$, $B = ( X, Z, Y )$, $C = ( Y, Z )$, $D = ( Z, X, Y )$, $E = ( X \boxtimes Y, Z )$, $P = ( X, Y, Z )$, $S = X \boxtimes ( Y \boxtimes Z )$, and $T = ( Z \boxtimes X ) \boxtimes Y$. Starting from the expression $( b_A \star i_Y ) \star ( a_B \star ( i_X \boxtimes b_C ) )$ and equation \ref{['Eq:1VarBox']}, the terms simplify as follows. = $=\;\cdots\;=$ The top half of the diagram is then rewritten using the first braiding coherence from $\mathcal{C}^{\mathcal{V}}$ to obtain the expression $\alpha_D \star ( \beta_E \star \alpha_P )$. = = $=\;\cdots\;=$ Then $( b_A \star i_Y ) \star ( a_B \star ( i_X \boxtimes b_C ) ) = \alpha_D \star ( \beta_E \star \alpha_P )$. Since $X$, $Y$, and $Z$ were arbitrary, then $b$ satisfies the first coherence condition of a braided monoidal category. The proof that $b$ satisfies the second coherence condition follows in a similar fashion. In conclusion, $( \textbf{Param}( P, \mathcal{C} ), \boxtimes, \mathbb{J}, a, \ell, r, b )$ is a braided monoidal category. First, it will be shown that $j$ is a functor. Let $X \xrightarrow{f} Y \xrightarrow{g} Z$ in $\mathcal{C}$. Then the following equation of diagrams hold. $j( g \circ f )$ = = = $j( g ) \star j( f )$ Since $f$ and $g$ were arbitrary, then $j$ preserves composition. Next, let $X \in \mathcal{C}$. It follows by definition that $j( 1_X ) = j( 1_X^{\mathcal{V}} ) = 1_X^{\mathcal{V}} \circ e_P = i_X$. Since $X$ was arbitrary, then $j$ preserves identities. Then $j$ is a functor. Next, assume that $\mathcal{C}^{\mathcal{V}}$ admits $\mathcal{V}$-monoidal structure $( \mathcal{C}^{\mathcal{V}}, \otimes^{\mathcal{V}}, \mathbb{J}^{\mathcal{V}}, \alpha^{\mathcal{V}}, \lambda^{\mathcal{V}}, \rho^{\mathcal{V}} )$. It will be shown in this case that $j$ is a strict monoidal functor. Clearly $j$ preserves the monoidal unit, since $j_0$ is the identity. To show that $j$ preserves monoidal products, let $f: X \to Y$ and $g: X' \to Y'$ in $\mathcal{C}$. Then the following equation of diagrams hold. $j( g \otimes f )$ = = = $j( g ) \boxtimes j( f )$ Since $f$ and $g$ were arbitrary, then $j$ preserves monoidal products. Next, let $X, Y, Z \in \mathcal{C}_0$. It follows by definition that $j( \alpha_{(X,Y,Z)} ) = a_{(X,Y,Z)}$, $j( \lambda_X ) = \ell_X$, and $j( \rho_X ) = r_X$. Since $X$, $Y$, and $Z$ were arbitrary, then $j$ preserves the structural natural transformations of $\otimes$. Then $j$ is a strict monoidal functor. Next, assume that $( \mathcal{C}^{\mathcal{V}}, \otimes^{\mathcal{V}}, \mathbb{J}^{\mathcal{V}}, \alpha^{\mathcal{V}}, \lambda^{\mathcal{V}}, \rho^{\mathcal{V}} )$ admits a $\mathcal{V}$-braiding $\beta^{\mathcal{V}}$. Let $X, Y \in \mathcal{C}_0$. Then $j( \beta_{(X,Y)} ) = b_{(X,Y)}$ by definition. Since $X$ and $Y$ were arbitrary, then $j$ preserves the braiding. Therefore, $j$ is a strict braided monoidal functor. Finally, assume that $\mathcal{V}( \mathbb{I}, P ) \ne \varnothing$. Then there exists a $\theta \in \mathcal{V}( \mathbb{I}, P )$. Let $X, Y \in \mathcal{C}_0$. Let $f, g: X \to Y$. Assume that $j( f ) = j( g )$. Then $\textsf{ev}_\theta( j( f ) ) = \textsf{ev}_\theta( j( g ) )$. Moreover, $\textsf{ev}_\theta( j( f ) ) = f$ and $\textsf{ev}_\theta( j( g ) ) =g$ by \ref{['Lem:InclEv']}. Then $f = g$. Since $f$ and $g$ were arbitrary, then $j_{X,Y}$ is injective. Since $X$ and $Y$ were arbitrary, then $j$ is faithful.