Goto Chapter: Top 1 2 3 4 5 6 7 8 9 10 11 12 13 Ind

### 7 Tensor Product and Internal Hom

#### 7.1 Monoidal Categories

A $$6$$-tuple $$( \mathbf{C}, \otimes, 1, \alpha, \lambda, \rho )$$ consisting of

• a category $$\mathbf{C}$$,

• a functor $$\otimes: \mathbf{C} \times \mathbf{C} \rightarrow \mathbf{C}$$,

• an object $$1 \in \mathbf{C}$$,

• a natural isomorphism $$\alpha_{a,b,c}: a \otimes (b \otimes c) \cong (a \otimes b) \otimes c$$,

• a natural isomorphism $$\lambda_{a}: 1 \otimes a \cong a$$,

• a natural isomorphism $$\rho_{a}: a \otimes 1 \cong a$$,

is called a monoidal category, if

• for all objects $$a,b,c,d$$, the pentagon identity holds: $$(\alpha_{a,b,c} \otimes \mathrm{id}_d) \circ \alpha_{a,b \otimes c, d} \circ ( \mathrm{id}_a \otimes \alpha_{b,c,d} ) = \alpha_{a \otimes b, c, d} \circ \alpha_{a,b,c \otimes d}$$,

• for all objects $$a,c$$, the triangle identity holds: $$( \rho_a \otimes \mathrm{id}_c ) \circ \alpha_{a,1,c} = \mathrm{id}_a \otimes \lambda_c$$.

The corresponding GAP property is given by IsMonoidalCategory.

##### 7.1-1 TensorProductOnObjects
 ‣ TensorProductOnObjects( a, b ) ( operation )

Returns: an object

The arguments are two objects $$a, b$$. The output is the tensor product $$a \otimes b$$.

 ‣ AddTensorProductOnObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation TensorProductOnObjects. $$F: (a,b) \mapsto a \otimes b$$.

##### 7.1-3 TensorProductOnMorphisms
 ‣ TensorProductOnMorphisms( alpha, beta ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(a \otimes b, a' \otimes b')$$

The arguments are two morphisms $$\alpha: a \rightarrow a', \beta: b \rightarrow b'$$. The output is the tensor product $$\alpha \otimes \beta$$.

##### 7.1-4 TensorProductOnMorphismsWithGivenTensorProducts
 ‣ TensorProductOnMorphismsWithGivenTensorProducts( s, alpha, beta, r ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(a \otimes b, a' \otimes b')$$

The arguments are an object $$s = a \otimes b$$, two morphisms $$\alpha: a \rightarrow a', \beta: b \rightarrow b'$$, and an object $$r = a' \otimes b'$$. The output is the tensor product $$\alpha \otimes \beta$$.

 ‣ AddTensorProductOnMorphismsWithGivenTensorProducts( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation TensorProductOnMorphismsWithGivenTensorProducts. $$F: ( a \otimes b, \alpha: a \rightarrow a', \beta: b \rightarrow b', a' \otimes b' ) \mapsto \alpha \otimes \beta$$.

##### 7.1-6 AssociatorRightToLeft
 ‣ AssociatorRightToLeft( a, b, c ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( a \otimes (b \otimes c), (a \otimes b) \otimes c )$$.

The arguments are three objects $$a,b,c$$. The output is the associator $$\alpha_{a,(b,c)}: a \otimes (b \otimes c) \rightarrow (a \otimes b) \otimes c$$.

##### 7.1-7 AssociatorRightToLeftWithGivenTensorProducts
 ‣ AssociatorRightToLeftWithGivenTensorProducts( s, a, b, c, r ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( a \otimes (b \otimes c), (a \otimes b) \otimes c )$$.

The arguments are an object $$s = a \otimes (b \otimes c)$$, three objects $$a,b,c$$, and an object $$r = (a \otimes b) \otimes c$$. The output is the associator $$\alpha_{a,(b,c)}: a \otimes (b \otimes c) \rightarrow (a \otimes b) \otimes c$$.

 ‣ AddAssociatorRightToLeftWithGivenTensorProducts( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation AssociatorRightToLeftWithGivenTensorProducts. $$F: ( a \otimes (b \otimes c), a, b, c, (a \otimes b) \otimes c ) \mapsto \alpha_{a,(b,c)}$$.

##### 7.1-9 AssociatorLeftToRight
 ‣ AssociatorLeftToRight( a, b, c ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( (a \otimes b) \otimes c \rightarrow a \otimes (b \otimes c) )$$.

The arguments are three objects $$a,b,c$$. The output is the associator $$\alpha_{(a,b),c}: (a \otimes b) \otimes c \rightarrow a \otimes (b \otimes c)$$.

##### 7.1-10 AssociatorLeftToRightWithGivenTensorProducts
 ‣ AssociatorLeftToRightWithGivenTensorProducts( s, a, b, c, r ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( (a \otimes b) \otimes c \rightarrow a \otimes (b \otimes c) )$$.

The arguments are an object $$s = (a \otimes b) \otimes c$$, three objects $$a,b,c$$, and an object $$r = a \otimes (b \otimes c)$$. The output is the associator $$\alpha_{(a,b),c}: (a \otimes b) \otimes c \rightarrow a \otimes (b \otimes c)$$.

 ‣ AddAssociatorLeftToRightWithGivenTensorProducts( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation AssociatorLeftToRightWithGivenTensorProducts. $$F: (( a \otimes b ) \otimes c, a, b, c, a \otimes (b \otimes c )) \mapsto \alpha_{(a,b),c}$$.

##### 7.1-12 TensorUnit
 ‣ TensorUnit( C ) ( attribute )

Returns: an object

The argument is a category $$\mathbf{C}$$. The output is the tensor unit $$1$$ of $$\mathbf{C}$$.

 ‣ AddTensorUnit( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation TensorUnit. $$F: ( ) \mapsto 1$$.

##### 7.1-14 LeftUnitor
 ‣ LeftUnitor( a ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}(1 \otimes a, a )$$

The argument is an object $$a$$. The output is the left unitor $$\lambda_a: 1 \otimes a \rightarrow a$$.

##### 7.1-15 LeftUnitorWithGivenTensorProduct
 ‣ LeftUnitorWithGivenTensorProduct( a, s ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(1 \otimes a, a )$$

The arguments are an object $$a$$ and an object $$s = 1 \otimes a$$. The output is the left unitor $$\lambda_a: 1 \otimes a \rightarrow a$$.

 ‣ AddLeftUnitorWithGivenTensorProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation LeftUnitorWithGivenTensorProduct. $$F: (a, 1 \otimes a) \mapsto \lambda_a$$.

##### 7.1-17 LeftUnitorInverse
 ‣ LeftUnitorInverse( a ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}(a, 1 \otimes a)$$

The argument is an object $$a$$. The output is the inverse of the left unitor $$\lambda_a^{-1}: a \rightarrow 1 \otimes a$$.

##### 7.1-18 LeftUnitorInverseWithGivenTensorProduct
 ‣ LeftUnitorInverseWithGivenTensorProduct( a, r ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(a, 1 \otimes a)$$

The argument is an object $$a$$ and an object $$r = 1 \otimes a$$. The output is the inverse of the left unitor $$\lambda_a^{-1}: a \rightarrow 1 \otimes a$$.

 ‣ AddLeftUnitorInverseWithGivenTensorProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation LeftUnitorInverseWithGivenTensorProduct. $$F: (a, 1 \otimes a) \mapsto \lambda_a^{-1}$$.

##### 7.1-20 RightUnitor
 ‣ RightUnitor( a ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}(a \otimes 1, a )$$

The argument is an object $$a$$. The output is the right unitor $$\rho_a: a \otimes 1 \rightarrow a$$.

##### 7.1-21 RightUnitorWithGivenTensorProduct
 ‣ RightUnitorWithGivenTensorProduct( a, s ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(a \otimes 1, a )$$

The arguments are an object $$a$$ and an object $$s = a \otimes 1$$. The output is the right unitor $$\rho_a: a \otimes 1 \rightarrow a$$.

 ‣ AddRightUnitorWithGivenTensorProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation RightUnitorWithGivenTensorProduct. $$F: (a, a \otimes 1) \mapsto \rho_a$$.

##### 7.1-23 RightUnitorInverse
 ‣ RightUnitorInverse( a ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}( a, a \otimes 1 )$$

The argument is an object $$a$$. The output is the inverse of the right unitor $$\rho_a^{-1}: a \rightarrow a \otimes 1$$.

##### 7.1-24 RightUnitorInverseWithGivenTensorProduct
 ‣ RightUnitorInverseWithGivenTensorProduct( a, r ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( a, a \otimes 1 )$$

The arguments are an object $$a$$ and an object $$r = a \otimes 1$$. The output is the inverse of the right unitor $$\rho_a^{-1}: a \rightarrow a \otimes 1$$.

 ‣ AddRightUnitorInverseWithGivenTensorProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation RightUnitorInverseWithGivenTensorProduct. $$F: (a, a \otimes 1) \mapsto \rho_a^{-1}$$.

##### 7.1-26 LeftDistributivityExpanding
 ‣ LeftDistributivityExpanding( a, L ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( a \otimes (b_1 \oplus \dots \oplus b_n), (a \otimes b_1) \oplus \dots \oplus (a \otimes b_n) )$$

The arguments are an object $$a$$ and a list of objects $$L = (b_1, \dots, b_n)$$. The output is the left distributivity morphism $$a \otimes (b_1 \oplus \dots \oplus b_n) \rightarrow (a \otimes b_1) \oplus \dots \oplus (a \otimes b_n)$$.

##### 7.1-27 LeftDistributivityExpandingWithGivenObjects
 ‣ LeftDistributivityExpandingWithGivenObjects( s, a, L, r ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( s, r )$$

The arguments are an object $$s = a \otimes (b_1 \oplus \dots \oplus b_n)$$, an object $$a$$, a list of objects $$L = (b_1, \dots, b_n)$$, and an object $$r = (a \otimes b_1) \oplus \dots \oplus (a \otimes b_n)$$. The output is the left distributivity morphism $$s \rightarrow r$$.

 ‣ AddLeftDistributivityExpandingWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation LeftDistributivityExpandingWithGivenObjects. $$F: (a \otimes (b_1 \oplus \dots \oplus b_n), a, L, (a \otimes b_1) \oplus \dots \oplus (a \otimes b_n)) \mapsto \mathrm{LeftDistributivityExpandingWithGivenObjects}(a,L)$$.

##### 7.1-29 LeftDistributivityFactoring
 ‣ LeftDistributivityFactoring( a, L ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( (a \otimes b_1) \oplus \dots \oplus (a \otimes b_n), a \otimes (b_1 \oplus \dots \oplus b_n) )$$

The arguments are an object $$a$$ and a list of objects $$L = (b_1, \dots, b_n)$$. The output is the left distributivity morphism $$(a \otimes b_1) \oplus \dots \oplus (a \otimes b_n) \rightarrow a \otimes (b_1 \oplus \dots \oplus b_n)$$.

##### 7.1-30 LeftDistributivityFactoringWithGivenObjects
 ‣ LeftDistributivityFactoringWithGivenObjects( s, a, L, r ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( s, r )$$

The arguments are an object $$s = (a \otimes b_1) \oplus \dots \oplus (a \otimes b_n)$$, an object $$a$$, a list of objects $$L = (b_1, \dots, b_n)$$, and an object $$r = a \otimes (b_1 \oplus \dots \oplus b_n)$$. The output is the left distributivity morphism $$s \rightarrow r$$.

 ‣ AddLeftDistributivityFactoringWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation LeftDistributivityFactoringWithGivenObjects. $$F: ((a \otimes b_1) \oplus \dots \oplus (a \otimes b_n), a, L, a \otimes (b_1 \oplus \dots \oplus b_n)) \mapsto \mathrm{LeftDistributivityFactoringWithGivenObjects}(a,L)$$.

##### 7.1-32 RightDistributivityExpanding
 ‣ RightDistributivityExpanding( L, a ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( (b_1 \oplus \dots \oplus b_n) \otimes a, (b_1 \otimes a) \oplus \dots \oplus (b_n \otimes a) )$$

The arguments are a list of objects $$L = (b_1, \dots, b_n)$$ and an object $$a$$. The output is the right distributivity morphism $$(b_1 \oplus \dots \oplus b_n) \otimes a \rightarrow (b_1 \otimes a) \oplus \dots \oplus (b_n \otimes a)$$.

##### 7.1-33 RightDistributivityExpandingWithGivenObjects
 ‣ RightDistributivityExpandingWithGivenObjects( s, L, a, r ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( s, r )$$

The arguments are an object $$s = (b_1 \oplus \dots \oplus b_n) \otimes a$$, a list of objects $$L = (b_1, \dots, b_n)$$, an object $$a$$, and an object $$r = (b_1 \otimes a) \oplus \dots \oplus (b_n \otimes a)$$. The output is the right distributivity morphism $$s \rightarrow r$$.

 ‣ AddRightDistributivityExpandingWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation RightDistributivityExpandingWithGivenObjects. $$F: ((b_1 \oplus \dots \oplus b_n) \otimes a, L, a, (b_1 \otimes a) \oplus \dots \oplus (b_n \otimes a)) \mapsto \mathrm{RightDistributivityExpandingWithGivenObjects}(L,a)$$.

##### 7.1-35 RightDistributivityFactoring
 ‣ RightDistributivityFactoring( L, a ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( (b_1 \otimes a) \oplus \dots \oplus (b_n \otimes a), (b_1 \oplus \dots \oplus b_n) \otimes a)$$

The arguments are a list of objects $$L = (b_1, \dots, b_n)$$ and an object $$a$$. The output is the right distributivity morphism $$(b_1 \otimes a) \oplus \dots \oplus (b_n \otimes a) \rightarrow (b_1 \oplus \dots \oplus b_n) \otimes a$$.

##### 7.1-36 RightDistributivityFactoringWithGivenObjects
 ‣ RightDistributivityFactoringWithGivenObjects( s, L, a, r ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( s, r )$$

The arguments are an object $$s = (b_1 \otimes a) \oplus \dots \oplus (b_n \otimes a)$$, a list of objects $$L = (b_1, \dots, b_n)$$, an object $$a$$, and an object $$r = (b_1 \oplus \dots \oplus b_n) \otimes a$$. The output is the right distributivity morphism $$s \rightarrow r$$.

 ‣ AddRightDistributivityFactoringWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation RightDistributivityFactoringWithGivenObjects. $$F: ((b_1 \otimes a) \oplus \dots \oplus (b_n \otimes a), L, a, (b_1 \oplus \dots \oplus b_n) \otimes a) \mapsto \mathrm{RightDistributivityFactoringWithGivenObjects}(L,a)$$.

#### 7.2 Braided Monoidal Categories

A monoidal category $$\mathbf{C}$$ equipped with a natural isomorphism $$B_{a,b}: a \otimes b \cong b \otimes a$$ is called a braided monoidal category if

• $$\lambda_a \circ B_{a,1} = \rho_a$$,

• $$(B_{c,a} \otimes \mathrm{id}_b) \circ \alpha_{c,a,b} \circ B_{a \otimes b,c} = \alpha_{a,c,b} \circ ( \mathrm{id}_a \otimes B_{b,c}) \circ \alpha^{-1}_{a,b,c}$$,

• $$( \mathrm{id}_b \otimes B_{c,a} ) \circ \alpha^{-1}_{b,c,a} \circ B_{a,b \otimes c} = \alpha^{-1}_{b,a,c} \circ (B_{a,b} \otimes \mathrm{id}_c) \circ \alpha_{a,b,c}$$.

The corresponding GAP property is given by IsBraidedMonoidalCategory.

##### 7.2-1 Braiding
 ‣ Braiding( a, b ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( a \otimes b, b \otimes a )$$.

The arguments are two objects $$a,b$$. The output is the braiding $$B_{a,b}: a \otimes b \rightarrow b \otimes a$$.

##### 7.2-2 BraidingWithGivenTensorProducts
 ‣ BraidingWithGivenTensorProducts( s, a, b, r ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( a \otimes b, b \otimes a )$$.

The arguments are an object $$s = a \otimes b$$, two objects $$a,b$$, and an object $$r = b \otimes a$$. The output is the braiding $$B_{a,b}: a \otimes b \rightarrow b \otimes a$$.

 ‣ AddBraidingWithGivenTensorProducts( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation BraidingWithGivenTensorProducts. $$F: (a \otimes b, a, b, b \otimes a) \rightarrow B_{a,b}$$.

##### 7.2-4 BraidingInverse
 ‣ BraidingInverse( a, b ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( b \otimes a, a \otimes b )$$.

The arguments are two objects $$a,b$$. The output is the inverse of the braiding $$B_{a,b}^{-1}: b \otimes a \rightarrow a \otimes b$$.

##### 7.2-5 BraidingInverseWithGivenTensorProducts
 ‣ BraidingInverseWithGivenTensorProducts( s, a, b, r ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( b \otimes a, a \otimes b )$$.

The arguments are an object $$s = b \otimes a$$, two objects $$a,b$$, and an object $$r = a \otimes b$$. The output is the braiding $$B_{a,b}^{-1}: b \otimes a \rightarrow a \otimes b$$.

 ‣ AddBraidingInverseWithGivenTensorProducts( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation BraidingInverseWithGivenTensorProducts. $$F: (b \otimes a, a, b, a \otimes b) \rightarrow B_{a,b}^{-1}$$.

#### 7.3 Symmetric Monoidal Categories

A braided monoidal category $$\mathbf{C}$$ is called symmetric monoidal category if $$B_{a,b}^{-1} = B_{b,a}$$. The corresponding GAP property is given by IsSymmetricMonoidalCategory.

#### 7.4 Symmetric Closed Monoidal Categories

A symmetric monoidal category $$\mathbf{C}$$ which has for each functor $$- \otimes b: \mathbf{C} \rightarrow \mathbf{C}$$ a right adjoint (denoted by $$\mathrm{\underline{Hom}}(b,-)$$) is called a symmetric closed monoidal category. The corresponding GAP property is given by IsSymmetricClosedMonoidalCategory.

##### 7.4-1 InternalHomOnObjects
 ‣ InternalHomOnObjects( a, b ) ( operation )

Returns: an object

The arguments are two objects $$a,b$$. The output is the internal hom object $$\mathrm{\underline{Hom}}(a,b)$$.

 ‣ AddInternalHomOnObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation InternalHomOnObjects. $$F: (a,b) \mapsto \mathrm{\underline{Hom}}(a,b)$$.

##### 7.4-3 InternalHomOnMorphisms
 ‣ InternalHomOnMorphisms( alpha, beta ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{\underline{Hom}}(a',b), \mathrm{\underline{Hom}}(a,b') )$$

The arguments are two morphisms $$\alpha: a \rightarrow a', \beta: b \rightarrow b'$$. The output is the internal hom morphism $$\mathrm{\underline{Hom}}(\alpha,\beta): \mathrm{\underline{Hom}}(a',b) \rightarrow \mathrm{\underline{Hom}}(a,b')$$.

##### 7.4-4 InternalHomOnMorphismsWithGivenInternalHoms
 ‣ InternalHomOnMorphismsWithGivenInternalHoms( s, alpha, beta, r ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{\underline{Hom}}(a',b), \mathrm{\underline{Hom}}(a,b') )$$

The arguments are an object $$s = \mathrm{\underline{Hom}}(a',b)$$, two morphisms $$\alpha: a \rightarrow a', \beta: b \rightarrow b'$$, and an object $$r = \mathrm{\underline{Hom}}(a,b')$$. The output is the internal hom morphism $$\mathrm{\underline{Hom}}(\alpha,\beta): \mathrm{\underline{Hom}}(a',b) \rightarrow \mathrm{\underline{Hom}}(a,b')$$.

 ‣ AddInternalHomOnMorphismsWithGivenInternalHoms( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation InternalHomOnMorphismsWithGivenInternalHoms. $$F: (\mathrm{\underline{Hom}}(a',b), \alpha: a \rightarrow a', \beta: b \rightarrow b', \mathrm{\underline{Hom}}(a,b') ) \mapsto \mathrm{\underline{Hom}}(\alpha,\beta)$$.

##### 7.4-6 EvaluationMorphism
 ‣ EvaluationMorphism( a, b ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{\underline{Hom}}(a,b) \otimes a, b )$$.

The arguments are two objects $$a, b$$. The output is the evaluation morphism $$\mathrm{ev}_{a,b}: \mathrm{\underline{Hom}}(a,b) \otimes a \rightarrow b$$, i.e., the counit of the tensor hom adjunction.

##### 7.4-7 EvaluationMorphismWithGivenSource
 ‣ EvaluationMorphismWithGivenSource( a, b, s ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{\underline{Hom}}(a,b) \otimes a, b )$$.

The arguments are two objects $$a,b$$ and an object $$s = \mathrm{\underline{Hom}}(a,b) \otimes a$$. The output is the evaluation morphism $$\mathrm{ev}_{a,b}: \mathrm{\underline{Hom}}(a,b) \otimes a \rightarrow b$$, i.e., the counit of the tensor hom adjunction.

 ‣ AddEvaluationMorphismWithGivenSource( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation EvaluationMorphismWithGivenSource. $$F: (a, b, \mathrm{\underline{Hom}}(a,b) \otimes a) \mapsto \mathrm{ev}_{a,b}$$.

##### 7.4-9 CoevaluationMorphism
 ‣ CoevaluationMorphism( a, b ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( a, \mathrm{\underline{Hom}}(b, a \otimes b) )$$.

The arguments are two objects $$a,b$$. The output is the coevaluation morphism $$\mathrm{coev}_{a,b}: a \rightarrow \mathrm{\underline{Hom}(b, a \otimes b)}$$, i.e., the unit of the tensor hom adjunction.

##### 7.4-10 CoevaluationMorphismWithGivenRange
 ‣ CoevaluationMorphismWithGivenRange( a, b, r ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( a, \mathrm{\underline{Hom}}(b, a \otimes b) )$$.

The arguments are two objects $$a,b$$ and an object $$r = \mathrm{\underline{Hom}(b, a \otimes b)}$$. The output is the coevaluation morphism $$\mathrm{coev}_{a,b}: a \rightarrow \mathrm{\underline{Hom}(b, a \otimes b)}$$, i.e., the unit of the tensor hom adjunction.

 ‣ AddCoevaluationMorphismWithGivenRange( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation CoevaluationMorphismWithGivenRange. $$F: (a, b, \mathrm{\underline{Hom}}(b, a \otimes b)) \mapsto \mathrm{coev}_{a,b}$$.

 ‣ TensorProductToInternalHomAdjunctionMap( a, b, f ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( a, \mathrm{\underline{Hom}}(b,c) )$$.

The arguments are objects $$a,b$$ and a morphism $$f: a \otimes b \rightarrow c$$. The output is a morphism $$g: a \rightarrow \mathrm{\underline{Hom}}(b,c)$$ corresponding to $$f$$ under the tensor hom adjunction.

 ‣ AddTensorProductToInternalHomAdjunctionMap( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation TensorProductToInternalHomAdjunctionMap. $$F: (a, b, f: a \otimes b \rightarrow c) \mapsto ( g: a \rightarrow \mathrm{\underline{Hom}}(b,c) )$$.

 ‣ InternalHomToTensorProductAdjunctionMap( b, c, g ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(a \otimes b, c)$$.

The arguments are objects $$b,c$$ and a morphism $$g: a \rightarrow \mathrm{\underline{Hom}}(b,c)$$. The output is a morphism $$f: a \otimes b \rightarrow c$$ corresponding to $$g$$ under the tensor hom adjunction.

 ‣ AddInternalHomToTensorProductAdjunctionMap( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation InternalHomToTensorProductAdjunctionMap. $$F: (b, c, g: a \rightarrow \mathrm{\underline{Hom}}(b,c)) \mapsto ( g: a \otimes b \rightarrow c )$$.

##### 7.4-16 MonoidalPreComposeMorphism
 ‣ MonoidalPreComposeMorphism( a, b, c ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{\underline{Hom}}(a,b) \otimes \mathrm{\underline{Hom}}(b,c), \mathrm{\underline{Hom}}(a,c) )$$.

The arguments are three objects $$a,b,c$$. The output is the precomposition morphism $$\mathrm{MonoidalPreComposeMorphismWithGivenObjects}_{a,b,c}: \mathrm{\underline{Hom}}(a,b) \otimes \mathrm{\underline{Hom}}(b,c) \rightarrow \mathrm{\underline{Hom}}(a,c)$$.

##### 7.4-17 MonoidalPreComposeMorphismWithGivenObjects
 ‣ MonoidalPreComposeMorphismWithGivenObjects( s, a, b, c, r ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{\underline{Hom}}(a,b) \otimes \mathrm{\underline{Hom}}(b,c), \mathrm{\underline{Hom}}(a,c) )$$.

The arguments are an object $$s = \mathrm{\underline{Hom}}(a,b) \otimes \mathrm{\underline{Hom}}(b,c)$$, three objects $$a,b,c$$, and an object $$r = \mathrm{\underline{Hom}}(a,c)$$. The output is the precomposition morphism $$\mathrm{MonoidalPreComposeMorphismWithGivenObjects}_{a,b,c}: \mathrm{\underline{Hom}}(a,b) \otimes \mathrm{\underline{Hom}}(b,c) \rightarrow \mathrm{\underline{Hom}}(a,c)$$.

 ‣ AddMonoidalPreComposeMorphismWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation MonoidalPreComposeMorphismWithGivenObjects. $$F: (\mathrm{\underline{Hom}}(a,b) \otimes \mathrm{\underline{Hom}}(b,c),a,b,c,\mathrm{\underline{Hom}}(a,c)) \mapsto \mathrm{MonoidalPreComposeMorphismWithGivenObjects}_{a,b,c}$$.

##### 7.4-19 MonoidalPostComposeMorphism
 ‣ MonoidalPostComposeMorphism( a, b, c ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{\underline{Hom}}(b,c) \otimes \mathrm{\underline{Hom}}(a,b), \mathrm{\underline{Hom}}(a,c) )$$.

The arguments are three objects $$a,b,c$$. The output is the postcomposition morphism $$\mathrm{MonoidalPostComposeMorphismWithGivenObjects}_{a,b,c}: \mathrm{\underline{Hom}}(b,c) \otimes \mathrm{\underline{Hom}}(a,b) \rightarrow \mathrm{\underline{Hom}}(a,c)$$.

##### 7.4-20 MonoidalPostComposeMorphismWithGivenObjects
 ‣ MonoidalPostComposeMorphismWithGivenObjects( s, a, b, c, r ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{\underline{Hom}}(b,c) \otimes \mathrm{\underline{Hom}}(a,b), \mathrm{\underline{Hom}}(a,c) )$$.

The arguments are an object $$s = \mathrm{\underline{Hom}}(b,c) \otimes \mathrm{\underline{Hom}}(a,b)$$, three objects $$a,b,c$$, and an object $$r = \mathrm{\underline{Hom}}(a,c)$$. The output is the postcomposition morphism $$\mathrm{MonoidalPostComposeMorphismWithGivenObjects}_{a,b,c}: \mathrm{\underline{Hom}}(b,c) \otimes \mathrm{\underline{Hom}}(a,b) \rightarrow \mathrm{\underline{Hom}}(a,c)$$.

 ‣ AddMonoidalPostComposeMorphismWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation MonoidalPostComposeMorphismWithGivenObjects. $$F: (\mathrm{\underline{Hom}}(b,c) \otimes \mathrm{\underline{Hom}}(a,b),a,b,c,\mathrm{\underline{Hom}}(a,c)) \mapsto \mathrm{MonoidalPostComposeMorphismWithGivenObjects}_{a,b,c}$$.

##### 7.4-22 DualOnObjects
 ‣ DualOnObjects( a ) ( attribute )

Returns: an object

The argument is an object $$a$$. The output is its dual object $$a^{\vee}$$.

 ‣ AddDualOnObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation DualOnObjects. $$F: a \mapsto a^{\vee}$$.

##### 7.4-24 DualOnMorphisms
 ‣ DualOnMorphisms( alpha ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}( b^{\vee}, a^{\vee} )$$.

The argument is a morphism $$\alpha: a \rightarrow b$$. The output is its dual morphism $$\alpha^{\vee}: b^{\vee} \rightarrow a^{\vee}$$.

##### 7.4-25 DualOnMorphismsWithGivenDuals
 ‣ DualOnMorphismsWithGivenDuals( s, alpha, r ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( b^{\vee}, a^{\vee} )$$.

The argument is an object $$s = b^{\vee}$$, a morphism $$\alpha: a \rightarrow b$$, and an object $$r = a^{\vee}$$. The output is the dual morphism $$\alpha^{\vee}: b^{\vee} \rightarrow a^{\vee}$$.

 ‣ AddDualOnMorphismsWithGivenDuals( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation DualOnMorphismsWithGivenDuals. $$F: (b^{\vee},\alpha,a^{\vee}) \mapsto \alpha^{\vee}$$.

##### 7.4-27 EvaluationForDual
 ‣ EvaluationForDual( a ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}( a^{\vee} \otimes a, 1 )$$.

The argument is an object $$a$$. The output is the evaluation morphism $$\mathrm{ev}_{a}: a^{\vee} \otimes a \rightarrow 1$$.

##### 7.4-28 EvaluationForDualWithGivenTensorProduct
 ‣ EvaluationForDualWithGivenTensorProduct( s, a, r ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( a^{\vee} \otimes a, 1 )$$.

The arguments are an object $$s = a^{\vee} \otimes a$$, an object $$a$$, and an object $$r = 1$$. The output is the evaluation morphism $$\mathrm{ev}_{a}: a^{\vee} \otimes a \rightarrow 1$$.

 ‣ AddEvaluationForDualWithGivenTensorProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation EvaluationForDualWithGivenTensorProduct. $$F: (a^{\vee} \otimes a, a, 1) \mapsto \mathrm{ev}_{a}$$.

##### 7.4-30 CoevaluationForDual
 ‣ CoevaluationForDual( a ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}(1,a \otimes a^{\vee})$$.

The argument is an object $$a$$. The output is the coevaluation morphism $$\mathrm{coev}_{a}:1 \rightarrow a \otimes a^{\vee}$$.

##### 7.4-31 CoevaluationForDualWithGivenTensorProduct
 ‣ CoevaluationForDualWithGivenTensorProduct( s, a, r ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(1,a \otimes a^{\vee})$$.

The arguments are an object $$s = 1$$, an object $$a$$, and an object $$r = a \otimes a^{\vee}$$. The output is the coevaluation morphism $$\mathrm{coev}_{a}:1 \rightarrow a \otimes a^{\vee}$$.

 ‣ AddCoevaluationForDualWithGivenTensorProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation CoevaluationForDualWithGivenTensorProduct. $$F: (1, a, a \otimes a^{\vee}) \mapsto \mathrm{coev}_{a}$$.

##### 7.4-33 MorphismToBidual
 ‣ MorphismToBidual( a ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}(a, (a^{\vee})^{\vee})$$.

The argument is an object $$a$$. The output is the morphism to the bidual $$a \rightarrow (a^{\vee})^{\vee}$$.

##### 7.4-34 MorphismToBidualWithGivenBidual
 ‣ MorphismToBidualWithGivenBidual( a, r ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(a, (a^{\vee})^{\vee})$$.

The arguments are an object $$a$$, and an object $$r = (a^{\vee})^{\vee}$$. The output is the morphism to the bidual $$a \rightarrow (a^{\vee})^{\vee}$$.

 ‣ AddMorphismToBidualWithGivenBidual( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation MorphismToBidualWithGivenBidual. $$F: (a, (a^{\vee})^{\vee}) \mapsto (a \rightarrow (a^{\vee})^{\vee})$$.

##### 7.4-36 TensorProductInternalHomCompatibilityMorphism
 ‣ TensorProductInternalHomCompatibilityMorphism( a, a', b, b' ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b'), \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b'))$$.

The arguments are four objects $$a, a', b, b'$$. The output is the natural morphism $$\mathrm{TensorProductInternalHomCompatibilityMorphismWithGivenObjects}_{a,a',b,b'}: \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b') \rightarrow \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b')$$.

##### 7.4-37 TensorProductInternalHomCompatibilityMorphismWithGivenObjects
 ‣ TensorProductInternalHomCompatibilityMorphismWithGivenObjects( a, a', b, b', L ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b'), \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b'))$$.

The arguments are four objects $$a, a', b, b'$$, and a list $$L = [ \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b'), \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b') ]$$. The output is the natural morphism $$\mathrm{TensorProductInternalHomCompatibilityMorphismWithGivenObjects}_{a,a',b,b'}: \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b') \rightarrow \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b')$$.

 ‣ AddTensorProductInternalHomCompatibilityMorphismWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation TensorProductInternalHomCompatibilityMorphismWithGivenObjects. $$F: ( a,a',b,b', [ \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b'), \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b') ]) \mapsto \mathrm{TensorProductInternalHomCompatibilityMorphismWithGivenObjects}_{a,a',b,b'}$$.

##### 7.4-39 TensorProductDualityCompatibilityMorphism
 ‣ TensorProductDualityCompatibilityMorphism( a, b ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( a^{\vee} \otimes b^{\vee}, (a \otimes b)^{\vee} )$$.

The arguments are two objects $$a,b$$. The output is the natural morphism $$\mathrm{TensorProductDualityCompatibilityMorphismWithGivenObjects}: a^{\vee} \otimes b^{\vee} \rightarrow (a \otimes b)^{\vee}$$.

##### 7.4-40 TensorProductDualityCompatibilityMorphismWithGivenObjects
 ‣ TensorProductDualityCompatibilityMorphismWithGivenObjects( s, a, b, r ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( a^{\vee} \otimes b^{\vee}, (a \otimes b)^{\vee} )$$.

The arguments are an object $$s = a^{\vee} \otimes b^{\vee}$$, two objects $$a,b$$, and an object $$r = (a \otimes b)^{\vee}$$. The output is the natural morphism $$\mathrm{TensorProductDualityCompatibilityMorphismWithGivenObjects}_{a,b}: a^{\vee} \otimes b^{\vee} \rightarrow (a \otimes b)^{\vee}$$.

 ‣ AddTensorProductDualityCompatibilityMorphismWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation TensorProductDualityCompatibilityMorphismWithGivenObjects. $$F: ( a^{\vee} \otimes b^{\vee}, a, b, (a \otimes b)^{\vee} ) \mapsto \mathrm{TensorProductDualityCompatibilityMorphismWithGivenObjects}_{a,b}$$.

##### 7.4-42 MorphismFromTensorProductToInternalHom
 ‣ MorphismFromTensorProductToInternalHom( a, b ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( a^{\vee} \otimes b, \mathrm{\underline{Hom}}(a,b) )$$.

The arguments are two objects $$a,b$$. The output is the natural morphism $$\mathrm{MorphismFromTensorProductToInternalHomWithGivenObjects}_{a,b}: a^{\vee} \otimes b \rightarrow \mathrm{\underline{Hom}}(a,b)$$.

##### 7.4-43 MorphismFromTensorProductToInternalHomWithGivenObjects
 ‣ MorphismFromTensorProductToInternalHomWithGivenObjects( s, a, b, r ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( a^{\vee} \otimes b, \mathrm{\underline{Hom}}(a,b) )$$.

The arguments are an object $$s = a^{\vee} \otimes b$$, two objects $$a,b$$, and an object $$r = \mathrm{\underline{Hom}}(a,b)$$. The output is the natural morphism $$\mathrm{MorphismFromTensorProductToInternalHomWithGivenObjects}_{a,b}: a^{\vee} \otimes b \rightarrow \mathrm{\underline{Hom}}(a,b)$$.

 ‣ AddMorphismFromTensorProductToInternalHomWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation MorphismFromTensorProductToInternalHomWithGivenObjects. $$F: ( a^{\vee} \otimes b, a, b, \mathrm{\underline{Hom}}(a,b) ) \mapsto \mathrm{MorphismFromTensorProductToInternalHomWithGivenObjects}_{a,b}$$.

##### 7.4-45 IsomorphismFromTensorProductToInternalHom
 ‣ IsomorphismFromTensorProductToInternalHom( a, b ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( a^{\vee} \otimes b, \mathrm{\underline{Hom}}(a,b) )$$.

The arguments are two objects $$a,b$$. The output is the natural morphism $$\mathrm{IsomorphismFromTensorProductToInternalHom}_{a,b}: a^{\vee} \otimes b \rightarrow \mathrm{\underline{Hom}}(a,b)$$.

 ‣ AddIsomorphismFromTensorProductToInternalHom( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation IsomorphismFromTensorProductToInternalHom. $$F: ( a, b ) \mapsto \mathrm{IsomorphismFromTensorProductToInternalHom}_{a,b}$$.

##### 7.4-47 MorphismFromInternalHomToTensorProduct
 ‣ MorphismFromInternalHomToTensorProduct( a, b ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{\underline{Hom}}(a,b), a^{\vee} \otimes b )$$.

The arguments are two objects $$a,b$$. The output is the inverse of $$\mathrm{MorphismFromTensorProductToInternalHomWithGivenObjects}$$, namely $$\mathrm{MorphismFromInternalHomToTensorProductWithGivenObjects}_{a,b}: \mathrm{\underline{Hom}}(a,b) \rightarrow a^{\vee} \otimes b$$.

##### 7.4-48 MorphismFromInternalHomToTensorProductWithGivenObjects
 ‣ MorphismFromInternalHomToTensorProductWithGivenObjects( s, a, b, r ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{\underline{Hom}}(a,b), a^{\vee} \otimes b )$$.

The arguments are an object $$s = \mathrm{\underline{Hom}}(a,b)$$, two objects $$a,b$$, and an object $$r = a^{\vee} \otimes b$$. The output is the inverse of $$\mathrm{MorphismFromTensorProductToInternalHomWithGivenObjects}$$, namely $$\mathrm{MorphismFromInternalHomToTensorProductWithGivenObjects}_{a,b}: \mathrm{\underline{Hom}}(a,b) \rightarrow a^{\vee} \otimes b$$.

 ‣ AddMorphismFromInternalHomToTensorProductWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation MorphismFromInternalHomToTensorProductWithGivenObjects. $$F: ( \mathrm{\underline{Hom}}(a,b),a,b,a^{\vee} \otimes b ) \mapsto \mathrm{MorphismFromInternalHomToTensorProductWithGivenObjects}_{a,b}$$.

##### 7.4-50 IsomorphismFromInternalHomToTensorProduct
 ‣ IsomorphismFromInternalHomToTensorProduct( a, b ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{\underline{Hom}}(a,b), a^{\vee} \otimes b )$$.

The arguments are two objects $$a,b$$. The output is the inverse of $$\mathrm{IsomorphismFromTensorProductToInternalHom}$$, namely $$\mathrm{IsomorphismFromInternalHomToTensorProduct}_{a,b}: \mathrm{\underline{Hom}}(a,b) \rightarrow a^{\vee} \otimes b$$.

 ‣ AddIsomorphismFromInternalHomToTensorProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation IsomorphismFromInternalHomToTensorProduct. $$F: ( a,b ) \mapsto \mathrm{IsomorphismFromInternalHomToTensorProduct}_{a,b}$$.

##### 7.4-52 TraceMap
 ‣ TraceMap( alpha ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}(1,1)$$.

The argument is a morphism $$\alpha$$. The output is the trace morphism $$\mathrm{trace}_{\alpha}: 1 \rightarrow 1$$.

 ‣ AddTraceMap( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation TraceMap. $$F: \alpha \mapsto \mathrm{trace}_{\alpha}$$

##### 7.4-54 RankMorphism
 ‣ RankMorphism( a ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}(1,1)$$.

The argument is an object $$a$$. The output is the rank morphism $$\mathrm{rank}_a: 1 \rightarrow 1$$.

 ‣ AddRankMorphism( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation RankMorphism. $$F: a \mapsto \mathrm{rank}_{a}$$

##### 7.4-56 IsomorphismFromDualToInternalHom
 ‣ IsomorphismFromDualToInternalHom( a ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}(a^{\vee}, \mathrm{\underline{Hom}}(a,1))$$.

The argument is an object $$a$$. The output is the isomorphism $$\mathrm{IsomorphismFromDualToInternalHom}_{a}: a^{\vee} \rightarrow \mathrm{\underline{Hom}}(a,1)$$.

 ‣ AddIsomorphismFromDualToInternalHom( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation IsomorphismFromDualToInternalHom. $$F: a \mapsto \mathrm{IsomorphismFromDualToInternalHom}_{a}$$

##### 7.4-58 IsomorphismFromInternalHomToDual
 ‣ IsomorphismFromInternalHomToDual( a ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}(\mathrm{\underline{Hom}}(a,1), a^{\vee})$$.

The argument is an object $$a$$. The output is the isomorphism $$\mathrm{IsomorphismFromInternalHomToDual}_{a}: \mathrm{\underline{Hom}}(a,1) \rightarrow a^{\vee}$$.

 ‣ AddIsomorphismFromInternalHomToDual( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation IsomorphismFromInternalHomToDual. $$F: a \mapsto \mathrm{IsomorphismFromInternalHomToDual}_{a}$$

##### 7.4-60 UniversalPropertyOfDual
 ‣ UniversalPropertyOfDual( t, a, alpha ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(t, a^{\vee})$$.

The arguments are two objects $$t,a$$, and a morphism $$\alpha: t \otimes a \rightarrow 1$$. The output is the morphism $$t \rightarrow a^{\vee}$$ given by the universal property of $$a^{\vee}$$.

 ‣ AddUniversalPropertyOfDual( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation UniversalPropertyOfDual. $$F: ( t,a,\alpha: t \otimes a \rightarrow 1 ) \mapsto ( t \rightarrow a^{\vee} )$$.

##### 7.4-62 LambdaIntroduction
 ‣ LambdaIntroduction( alpha ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}( 1, \mathrm{\underline{Hom}}(a,b) )$$.

The argument is a morphism $$\alpha: a \rightarrow b$$. The output is the corresponding morphism $$1 \rightarrow \mathrm{\underline{Hom}}(a,b)$$ under the tensor hom adjunction.

 ‣ AddLambdaIntroduction( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation LambdaIntroduction. $$F: ( \alpha: a \rightarrow b ) \mapsto ( 1 \rightarrow \mathrm{\underline{Hom}}(a,b) )$$.

##### 7.4-64 LambdaElimination
 ‣ LambdaElimination( a, b, alpha ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(a,b)$$.

The arguments are two objects $$a,b$$, and a morphism $$\alpha: 1 \rightarrow \mathrm{\underline{Hom}}(a,b)$$. The output is a morphism $$a \rightarrow b$$ corresponding to $$\alpha$$ under the tensor hom adjunction.

 ‣ AddLambdaElimination( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation LambdaElimination. $$F: ( a,b,\alpha: 1 \rightarrow \mathrm{\underline{Hom}}(a,b) ) \mapsto ( a \rightarrow b )$$.

##### 7.4-66 IsomorphismFromObjectToInternalHom
 ‣ IsomorphismFromObjectToInternalHom( a ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}(a, \mathrm{\underline{Hom}}(1,a))$$.

The argument is an object $$a$$. The output is the natural isomorphism $$a \rightarrow \mathrm{\underline{Hom}}(1,a)$$.

##### 7.4-67 IsomorphismFromObjectToInternalHomWithGivenInternalHom
 ‣ IsomorphismFromObjectToInternalHomWithGivenInternalHom( a, r ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(a, \mathrm{\underline{Hom}}(1,a))$$.

The argument is an object $$a$$, and an object $$r = \mathrm{\underline{Hom}}(1,a)$$. The output is the natural isomorphism $$a \rightarrow \mathrm{\underline{Hom}}(1,a)$$.

 ‣ AddIsomorphismFromObjectToInternalHomWithGivenInternalHom( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation IsomorphismFromObjectToInternalHomWithGivenInternalHom. $$F: ( a, \mathrm{\underline{Hom}}(1,a) ) \mapsto ( a \rightarrow \mathrm{\underline{Hom}}(1,a) )$$.

##### 7.4-69 IsomorphismFromInternalHomToObject
 ‣ IsomorphismFromInternalHomToObject( a ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}(\mathrm{\underline{Hom}}(1,a),a)$$.

The argument is an object $$a$$. The output is the natural isomorphism $$\mathrm{\underline{Hom}}(1,a) \rightarrow a$$.

##### 7.4-70 IsomorphismFromInternalHomToObjectWithGivenInternalHom
 ‣ IsomorphismFromInternalHomToObjectWithGivenInternalHom( a, s ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(\mathrm{\underline{Hom}}(1,a),a)$$.

The argument is an object $$a$$, and an object $$s = \mathrm{\underline{Hom}}(1,a)$$. The output is the natural isomorphism $$\mathrm{\underline{Hom}}(1,a) \rightarrow a$$.

 ‣ AddIsomorphismFromInternalHomToObjectWithGivenInternalHom( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation IsomorphismFromInternalHomToObjectWithGivenInternalHom. $$F: ( a, \mathrm{\underline{Hom}}(1,a) ) \mapsto ( \mathrm{\underline{Hom}}(1,a) \rightarrow a )$$.

#### 7.5 Rigid Symmetric Closed Monoidal Categories

A symmetric closed monoidal category $$\mathbf{C}$$ satisfying

• the natural morphism $$\mathrm{\underline{Hom}}(a_1,b_1) \otimes \mathrm{\underline{Hom}}(a_2,b_2) \rightarrow \mathrm{\underline{Hom}}(a_1 \otimes a_2,b_1 \otimes b_2)$$ is an isomorphism,

• the natural morphism $$a \rightarrow \mathrm{\underline{Hom}}(\mathrm{\underline{Hom}}(a, 1), 1)$$ is an isomorphism

is called a rigid symmetric closed monoidal category.

##### 7.5-1 TensorProductInternalHomCompatibilityMorphismInverse
 ‣ TensorProductInternalHomCompatibilityMorphismInverse( a, a', b, b' ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b'), \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b'))$$.

The arguments are four objects $$a, a', b, b'$$. The output is the natural morphism $$\mathrm{TensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects}_{a,a',b,b'}: \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b') \rightarrow \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b')$$.

##### 7.5-2 TensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects
 ‣ TensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects( a, a', b, b', L ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b'), \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b'))$$.

The arguments are four objects $$a, a', b, b'$$, and a list $$L = [ \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b'), \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b') ]$$. The output is the natural morphism $$\mathrm{TensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects}_{a,a',b,b'}: \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b') \rightarrow \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b')$$.

 ‣ AddTensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation TensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects. $$F: ( a,a',b,b', [ \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b'), \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b') ]) \mapsto \mathrm{TensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects}_{a,a',b,b'}$$.

##### 7.5-4 MorphismFromBidual
 ‣ MorphismFromBidual( a ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}((a^{\vee})^{\vee},a)$$.

The argument is an object $$a$$. The output is the inverse of the morphism to the bidual $$(a^{\vee})^{\vee} \rightarrow a$$.

##### 7.5-5 MorphismFromBidualWithGivenBidual
 ‣ MorphismFromBidualWithGivenBidual( a, s ) ( operation )

Returns: a morphism in $$\mathrm{Hom}((a^{\vee})^{\vee},a)$$.

The argument is an object $$a$$, and an object $$s = (a^{\vee})^{\vee}$$. The output is the inverse of the morphism to the bidual $$(a^{\vee})^{\vee} \rightarrow a$$.

 ‣ AddMorphismFromBidualWithGivenBidual( C, F ) ( operation )
The arguments are a category $$C$$ and a function $$F$$. This operations adds the given function $$F$$ to the category for the basic operation MorphismFromBidualWithGivenBidual. $$F: (a, (a^{\vee})^{\vee}) \mapsto ((a^{\vee})^{\vee} \rightarrow a)$$.