Goto Chapter: Top 1 2 3 4 5 6 Ind

### 1 Monoidal Categories

#### 1.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}$$ compatible with the congruence of morphisms,

• 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} ) \sim \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} \sim \mathrm{id}_a \otimes \lambda_c$$.

The corresponding GAP property is given by IsMonoidalCategory.

##### 1.1-1 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$$.

##### 1.1-2 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$$.

##### 1.1-3 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$$.

##### 1.1-4 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$$.

##### 1.1-5 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)$$.

##### 1.1-6 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)$$.

##### 1.1-7 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$$.

##### 1.1-8 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$$.

##### 1.1-9 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$$.

##### 1.1-10 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$$.

##### 1.1-11 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$$.

##### 1.1-12 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$$.

##### 1.1-13 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$$.

##### 1.1-14 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$$.

##### 1.1-15 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 operation adds the given function $$F$$ to the category for the basic operation TensorProductOnObjects. $$F: (a,b) \mapsto a \otimes b$$.

##### 1.1-17 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 operation adds the given function $$F$$ to the category for the basic operation TensorUnit. $$F: ( ) \mapsto 1$$.

##### 1.2-1 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)$$.

##### 1.2-2 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$$.

##### 1.2-3 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)$$.

##### 1.2-4 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$$.

##### 1.2-5 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)$$.

##### 1.2-6 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$$.

##### 1.2-7 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$$.

##### 1.2-8 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$$.

#### 1.3 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} \sim \rho_a$$,

• $$(B_{c,a} \otimes \mathrm{id}_b) \circ \alpha_{c,a,b} \circ B_{a \otimes b,c} \sim \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} \sim \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.

##### 1.3-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$$.

##### 1.3-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$$.

##### 1.3-3 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 braiding $$B_{a,b}^{-1}: b \otimes a \rightarrow a \otimes b$$.

##### 1.3-4 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 inverse braiding $$B_{a,b}^{-1}: b \otimes a \rightarrow a \otimes b$$.

#### 1.4 Symmetric Monoidal Categories

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

#### 1.5 Left Closed Monoidal Categories

A monoidal category $$\mathbf{C}$$ which has for each functor $$- \otimes b: \mathbf{C} \rightarrow \mathbf{C}$$ a right adjoint (denoted by $$\mathrm{\underline{Hom}_\ell}(b,-)$$) is called a left closed monoidal category.

If no operations involving left duals are installed manually, the left dual objects will be derived as $$a^\vee \coloneqq \mathrm{\underline{Hom}_\ell}(a,1)$$.

The corresponding GAP property is called IsLeftClosedMonoidalCategory.

##### 1.5-1 LeftInternalHomOnObjects
 ‣ LeftInternalHomOnObjects( a, b ) ( operation )

Returns: an object

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

##### 1.5-2 LeftInternalHomOnMorphisms
 ‣ LeftInternalHomOnMorphisms( alpha, beta ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{\underline{Hom}_\ell}(a',b), \mathrm{\underline{Hom}_\ell}(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}_\ell}(\alpha,\beta): \mathrm{\underline{Hom}_\ell}(a',b) \rightarrow \mathrm{\underline{Hom}_\ell}(a,b')$$.

##### 1.5-3 LeftInternalHomOnMorphismsWithGivenLeftInternalHoms
 ‣ LeftInternalHomOnMorphismsWithGivenLeftInternalHoms( s, alpha, beta, r ) ( operation )

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

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

##### 1.5-4 LeftClosedMonoidalEvaluationMorphism
 ‣ LeftClosedMonoidalEvaluationMorphism( a, b ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{\underline{Hom}_\ell}(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}_\ell}(a,b) \otimes a \rightarrow b$$, i.e., the counit of the tensor hom adjunction.

##### 1.5-5 LeftClosedMonoidalEvaluationMorphismWithGivenSource
 ‣ LeftClosedMonoidalEvaluationMorphismWithGivenSource( a, b, s ) ( operation )

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

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

##### 1.5-6 LeftClosedMonoidalCoevaluationMorphism
 ‣ LeftClosedMonoidalCoevaluationMorphism( a, b ) ( operation )

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

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

##### 1.5-7 LeftClosedMonoidalCoevaluationMorphismWithGivenRange
 ‣ LeftClosedMonoidalCoevaluationMorphismWithGivenRange( a, b, r ) ( operation )

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

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

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

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

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

 ‣ TensorProductToLeftInternalHomAdjunctMorphismWithGivenLeftInternalHom( a, b, f, i ) ( operation )

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

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

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

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

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

 ‣ LeftInternalHomToTensorProductAdjunctMorphismWithGivenTensorProduct( b, c, g, t ) ( operation )

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

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

##### 1.5-12 LeftClosedMonoidalPreComposeMorphism
 ‣ LeftClosedMonoidalPreComposeMorphism( a, b, c ) ( operation )

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

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

##### 1.5-13 LeftClosedMonoidalPreComposeMorphismWithGivenObjects
 ‣ LeftClosedMonoidalPreComposeMorphismWithGivenObjects( s, a, b, c, r ) ( operation )

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

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

##### 1.5-14 LeftClosedMonoidalPostComposeMorphism
 ‣ LeftClosedMonoidalPostComposeMorphism( a, b, c ) ( operation )

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

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

##### 1.5-15 LeftClosedMonoidalPostComposeMorphismWithGivenObjects
 ‣ LeftClosedMonoidalPostComposeMorphismWithGivenObjects( s, a, b, c, r ) ( operation )

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

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

##### 1.5-16 LeftDualOnObjects
 ‣ LeftDualOnObjects( a ) ( attribute )

Returns: an object

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

##### 1.5-17 LeftDualOnMorphisms
 ‣ LeftDualOnMorphisms( 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}$$.

##### 1.5-18 LeftDualOnMorphismsWithGivenLeftDuals
 ‣ LeftDualOnMorphismsWithGivenLeftDuals( s, alpha, r ) ( operation )

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

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}$$.

##### 1.5-19 LeftClosedMonoidalEvaluationForLeftDual
 ‣ LeftClosedMonoidalEvaluationForLeftDual( 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$$.

##### 1.5-20 LeftClosedMonoidalEvaluationForLeftDualWithGivenTensorProduct
 ‣ LeftClosedMonoidalEvaluationForLeftDualWithGivenTensorProduct( s, a, r ) ( operation )

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

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$$.

##### 1.5-21 MorphismToLeftBidual
 ‣ MorphismToLeftBidual( 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}$$.

##### 1.5-22 MorphismToLeftBidualWithGivenLeftBidual
 ‣ MorphismToLeftBidualWithGivenLeftBidual( a, r ) ( operation )

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

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}$$.

##### 1.5-23 TensorProductLeftInternalHomCompatibilityMorphism
 ‣ TensorProductLeftInternalHomCompatibilityMorphism( list ) ( operation )

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

The argument is a list of four objects $$[ a, a', b, b' ]$$. The output is the natural morphism $$\mathrm{TensorProductLeftInternalHomCompatibilityMorphism}_{a,a',b,b'}: \mathrm{\underline{Hom}_\ell}(a,a') \otimes \mathrm{\underline{Hom}_\ell}(b,b') \rightarrow \mathrm{\underline{Hom}_\ell}(a \otimes b,a' \otimes b')$$.

##### 1.5-24 TensorProductLeftInternalHomCompatibilityMorphismWithGivenObjects
 ‣ TensorProductLeftInternalHomCompatibilityMorphismWithGivenObjects( s, list, r ) ( operation )

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

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

##### 1.5-25 TensorProductLeftDualityCompatibilityMorphism
 ‣ TensorProductLeftDualityCompatibilityMorphism( 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{TensorProductLeftDualityCompatibilityMorphism}: a^{\vee} \otimes b^{\vee} \rightarrow (a \otimes b)^{\vee}$$.

##### 1.5-26 TensorProductLeftDualityCompatibilityMorphismWithGivenObjects
 ‣ TensorProductLeftDualityCompatibilityMorphismWithGivenObjects( s, a, b, r ) ( operation )

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

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{TensorProductLeftDualityCompatibilityMorphismWithGivenObjects}_{a,b}: a^{\vee} \otimes b^{\vee} \rightarrow (a \otimes b)^{\vee}$$.

##### 1.5-27 MorphismFromTensorProductToLeftInternalHom
 ‣ MorphismFromTensorProductToLeftInternalHom( a, b ) ( operation )

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

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

##### 1.5-28 MorphismFromTensorProductToLeftInternalHomWithGivenObjects
 ‣ MorphismFromTensorProductToLeftInternalHomWithGivenObjects( s, a, b, r ) ( operation )

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

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

##### 1.5-29 IsomorphismFromLeftDualObjectToLeftInternalHomIntoTensorUnit
 ‣ IsomorphismFromLeftDualObjectToLeftInternalHomIntoTensorUnit( a ) ( attribute )

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

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

##### 1.5-30 IsomorphismFromLeftInternalHomIntoTensorUnitToLeftDualObject
 ‣ IsomorphismFromLeftInternalHomIntoTensorUnitToLeftDualObject( a ) ( attribute )

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

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

##### 1.5-31 UniversalPropertyOfLeftDual
 ‣ UniversalPropertyOfLeftDual( 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}$$.

##### 1.5-32 LeftClosedMonoidalLambdaIntroduction
 ‣ LeftClosedMonoidalLambdaIntroduction( alpha ) ( attribute )

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

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

##### 1.5-33 LeftClosedMonoidalLambdaElimination
 ‣ LeftClosedMonoidalLambdaElimination( 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}_\ell}(a,b)$$. The output is a morphism $$a \rightarrow b$$ corresponding to $$\alpha$$ under the tensor hom adjunction.

##### 1.5-34 IsomorphismFromObjectToLeftInternalHom
 ‣ IsomorphismFromObjectToLeftInternalHom( a ) ( attribute )

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

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

##### 1.5-35 IsomorphismFromObjectToLeftInternalHomWithGivenLeftInternalHom
 ‣ IsomorphismFromObjectToLeftInternalHomWithGivenLeftInternalHom( a, r ) ( operation )

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

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

##### 1.5-36 IsomorphismFromLeftInternalHomToObject
 ‣ IsomorphismFromLeftInternalHomToObject( a ) ( attribute )

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

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

##### 1.5-37 IsomorphismFromLeftInternalHomToObjectWithGivenLeftInternalHom
 ‣ IsomorphismFromLeftInternalHomToObjectWithGivenLeftInternalHom( a, s ) ( operation )

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

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

#### 1.6 Closed Monoidal Categories

A monoidal category $$\mathbf{C}$$ which has for each functor $$- \otimes b: \mathbf{C} \rightarrow \mathbf{C}$$ a right adjoint (denoted by $$\mathrm{\underline{Hom}_\ell}(b,-)$$) is called a closed monoidal category.

If no operations involving duals are installed manually, the dual objects will be derived as $$a^\vee \coloneqq \mathrm{\underline{Hom}_\ell}(a,1)$$.

The corresponding GAP property is called IsClosedMonoidalCategory.

##### 1.6-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)$$.

##### 1.6-2 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')$$.

##### 1.6-3 InternalHomOnMorphismsWithGivenInternalHoms
 ‣ InternalHomOnMorphismsWithGivenInternalHoms( s, alpha, beta, r ) ( operation )

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

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')$$.

##### 1.6-4 ClosedMonoidalRightEvaluationMorphism
 ‣ ClosedMonoidalRightEvaluationMorphism( a, b ) ( operation )

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

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

##### 1.6-5 ClosedMonoidalRightEvaluationMorphismWithGivenSource
 ‣ ClosedMonoidalRightEvaluationMorphismWithGivenSource( a, b, s ) ( operation )

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

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

##### 1.6-6 ClosedMonoidalRightCoevaluationMorphism
 ‣ ClosedMonoidalRightCoevaluationMorphism( a, b ) ( operation )

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

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

##### 1.6-7 ClosedMonoidalRightCoevaluationMorphismWithGivenRange
 ‣ ClosedMonoidalRightCoevaluationMorphismWithGivenRange( a, b, r ) ( operation )

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

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

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

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

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

 ‣ TensorProductToInternalHomRightAdjunctMorphismWithGivenInternalHom( a, b, f, i ) ( operation )

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

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

 ‣ InternalHomToTensorProductRightAdjunctMorphism( a, c, g ) ( operation )

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

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

 ‣ InternalHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct( a, c, g, s ) ( operation )

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

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

##### 1.6-12 ClosedMonoidalLeftEvaluationMorphism
 ‣ ClosedMonoidalLeftEvaluationMorphism( 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 left evaluation morphism $$\mathrm{ev}_{a,b}: \mathrm{\underline{Hom}}(a,b) \otimes a \rightarrow b$$, i.e., the counit of the tensor hom adjunction.

##### 1.6-13 ClosedMonoidalLeftEvaluationMorphismWithGivenSource
 ‣ ClosedMonoidalLeftEvaluationMorphismWithGivenSource( a, b, s ) ( operation )

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

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

##### 1.6-14 ClosedMonoidalLeftCoevaluationMorphism
 ‣ ClosedMonoidalLeftCoevaluationMorphism( a, b ) ( operation )

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

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

##### 1.6-15 ClosedMonoidalLeftCoevaluationMorphismWithGivenRange
 ‣ ClosedMonoidalLeftCoevaluationMorphismWithGivenRange( a, b, r ) ( operation )

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

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

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

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

The arguments are two 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.

 ‣ TensorProductToInternalHomLeftAdjunctMorphismWithGivenInternalHom( a, b, f, i ) ( operation )

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

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

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

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

The arguments are two 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.

 ‣ InternalHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct( b, c, g, s ) ( operation )

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

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

##### 1.6-20 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{MonoidalPreComposeMorphism}_{a,b,c}: \mathrm{\underline{Hom}}(a,b) \otimes \mathrm{\underline{Hom}}(b,c) \rightarrow \mathrm{\underline{Hom}}(a,c)$$.

##### 1.6-21 MonoidalPreComposeMorphismWithGivenObjects
 ‣ MonoidalPreComposeMorphismWithGivenObjects( s, a, b, c, r ) ( operation )

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

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)$$.

##### 1.6-22 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{MonoidalPostComposeMorphism}_{a,b,c}: \mathrm{\underline{Hom}}(b,c) \otimes \mathrm{\underline{Hom}}(a,b) \rightarrow \mathrm{\underline{Hom}}(a,c)$$.

##### 1.6-23 MonoidalPostComposeMorphismWithGivenObjects
 ‣ MonoidalPostComposeMorphismWithGivenObjects( s, a, b, c, r ) ( operation )

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

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)$$.

##### 1.6-24 DualOnObjects
 ‣ DualOnObjects( a ) ( attribute )

Returns: an object

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

##### 1.6-25 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}$$.

##### 1.6-26 DualOnMorphismsWithGivenDuals
 ‣ DualOnMorphismsWithGivenDuals( s, alpha, r ) ( operation )

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

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}$$.

##### 1.6-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$$.

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

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

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$$.

##### 1.6-29 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}$$.

##### 1.6-30 MorphismToBidualWithGivenBidual
 ‣ MorphismToBidualWithGivenBidual( a, r ) ( operation )

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

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}$$.

##### 1.6-31 TensorProductInternalHomCompatibilityMorphism
 ‣ TensorProductInternalHomCompatibilityMorphism( list ) ( 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 argument is a list of four objects $$[ a, a', b, b' ]$$. The output is the natural morphism $$\mathrm{TensorProductInternalHomCompatibilityMorphism}_{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')$$.

##### 1.6-32 TensorProductInternalHomCompatibilityMorphismWithGivenObjects
 ‣ TensorProductInternalHomCompatibilityMorphismWithGivenObjects( s, list, r ) ( operation )

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

The arguments are a list of four objects $$[ a, a', b, b' ]$$, and two objects $$s = \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b')$$ and $$r = \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')$$.

##### 1.6-33 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{TensorProductDualityCompatibilityMorphism}: a^{\vee} \otimes b^{\vee} \rightarrow (a \otimes b)^{\vee}$$.

##### 1.6-34 TensorProductDualityCompatibilityMorphismWithGivenObjects
 ‣ TensorProductDualityCompatibilityMorphismWithGivenObjects( s, a, b, r ) ( operation )

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

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}$$.

##### 1.6-35 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{MorphismFromTensorProductToInternalHom}_{a,b}: a^{\vee} \otimes b \rightarrow \mathrm{\underline{Hom}}(a,b)$$.

##### 1.6-36 MorphismFromTensorProductToInternalHomWithGivenObjects
 ‣ MorphismFromTensorProductToInternalHomWithGivenObjects( s, a, b, r ) ( operation )

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

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)$$.

##### 1.6-37 IsomorphismFromDualObjectToInternalHomIntoTensorUnit
 ‣ IsomorphismFromDualObjectToInternalHomIntoTensorUnit( 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{IsomorphismFromDualObjectToInternalHomIntoTensorUnit}_{a}: a^{\vee} \rightarrow \mathrm{\underline{Hom}}(a,1)$$.

##### 1.6-38 IsomorphismFromInternalHomIntoTensorUnitToDualObject
 ‣ IsomorphismFromInternalHomIntoTensorUnitToDualObject( 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{IsomorphismFromInternalHomIntoTensorUnitToDualObject}_{a}: \mathrm{\underline{Hom}}(a,1) \rightarrow a^{\vee}$$.

##### 1.6-39 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}$$.

##### 1.6-40 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.

##### 1.6-41 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.

##### 1.6-42 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)$$.

##### 1.6-43 IsomorphismFromObjectToInternalHomWithGivenInternalHom
 ‣ IsomorphismFromObjectToInternalHomWithGivenInternalHom( a, r ) ( operation )

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

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)$$.

##### 1.6-44 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$$.

##### 1.6-45 IsomorphismFromInternalHomToObjectWithGivenInternalHom
 ‣ IsomorphismFromInternalHomToObjectWithGivenInternalHom( a, s ) ( operation )

Returns: a morphism in $$\mathrm{Hom}(s,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$$.

#### 1.7 Left Coclosed Monoidal Categories

A monoidal category $$\mathbf{C}$$ which has for each functor $$- \otimes b: \mathbf{C} \rightarrow \mathbf{C}$$ a left adjoint (denoted by $$\mathrm{\underline{coHom}}(-,b)$$) is called a left coclosed monoidal category.

If no operations involving left coduals are installed manually, the left codual objects will be derived as $$a_\vee \coloneqq \mathrm{\underline{coHom}}(1,a)$$.

The corresponding GAP property is called IsLeftCoclosedMonoidalCategory.

##### 1.7-1 LeftInternalCoHomOnObjects
 ‣ LeftInternalCoHomOnObjects( a, b ) ( operation )

Returns: an object

The arguments are two objects $$a,b$$. The output is the internal cohom object $$\mathrm{\underline{coHom}_\ell}(a,b)$$.

##### 1.7-2 LeftInternalCoHomOnMorphisms
 ‣ LeftInternalCoHomOnMorphisms( alpha, beta ) ( operation )

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

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

##### 1.7-3 LeftInternalCoHomOnMorphismsWithGivenLeftInternalCoHoms
 ‣ LeftInternalCoHomOnMorphismsWithGivenLeftInternalCoHoms( s, alpha, beta, r ) ( operation )

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

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

##### 1.7-4 LeftCoclosedMonoidalEvaluationMorphism
 ‣ LeftCoclosedMonoidalEvaluationMorphism( a, b ) ( operation )

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

The arguments are two objects $$a, b$$. The output is the coclosed evaluation morphism $$\mathrm{coclev}_{a,b}: b \rightarrow \mathrm{\underline{coHom}_\ell}(b,a) \otimes a$$, i.e., the unit of the cohom tensor adjunction.

##### 1.7-5 LeftCoclosedMonoidalEvaluationMorphismWithGivenRange
 ‣ LeftCoclosedMonoidalEvaluationMorphismWithGivenRange( a, b, r ) ( operation )

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

The arguments are two objects $$a,b$$ and an object $$r = \mathrm{\underline{coHom}_\ell}(b,a) \otimes a$$. The output is the coclosed evaluation morphism $$\mathrm{coclev}_{a,b}: b \rightarrow \mathrm{\underline{coHom}_\ell}(b,a) \otimes a$$, i.e., the unit of the cohom tensor adjunction.

##### 1.7-6 LeftCoclosedMonoidalCoevaluationMorphism
 ‣ LeftCoclosedMonoidalCoevaluationMorphism( a, b ) ( operation )

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

The arguments are two objects $$a,b$$. The output is the coclosed coevaluation morphism $$\mathrm{coclcoev}_{a,b}: \mathrm{\underline{coHom}_\ell}(b \otimes a, a) \rightarrow b$$, i.e., the counit of the cohom tensor adjunction.

##### 1.7-7 LeftCoclosedMonoidalCoevaluationMorphismWithGivenSource
 ‣ LeftCoclosedMonoidalCoevaluationMorphismWithGivenSource( a, b, s ) ( operation )

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

The arguments are two objects $$a,b$$ and an object $$s = \mathrm{\underline{coHom}_\ell}(b \otimes a, a)$$. The output is the coclosed coevaluation morphism $$\mathrm{coclcoev}_{a,b}: \mathrm{\underline{coHom}_\ell}(b \otimes a, a) \rightarrow b$$, i.e., the unit of the cohom tensor adjunction.

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

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

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

 ‣ TensorProductToLeftInternalCoHomAdjunctMorphismWithGivenLeftInternalCoHom( b, c, g, i ) ( operation )

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

The arguments are two objects $$b,c$$, a morphism $$g: a \rightarrow b \otimes c$$ and an object $$i = \mathrm{\underline{coHom}_\ell}(a,c)$$. The output is a morphism $$f: \mathrm{\underline{coHom}_\ell}(a,c) \rightarrow b$$ corresponding to $$g$$ under the cohom tensor adjunction.

 ‣ LeftInternalCoHomToTensorProductAdjunctMorphism( a, c, f ) ( operation )

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

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

 ‣ LeftInternalCoHomToTensorProductAdjunctMorphismWithGivenTensorProduct( a, c, f, t ) ( operation )

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

The arguments are two objects $$a,c$$, a morphism $$f: \mathrm{\underline{coHom}_\ell}(a,c) \rightarrow b$$ and an object $$t = b \otimes c$$. The output is a morphism $$g: a \rightarrow b \otimes c$$ corresponding to $$f$$ under the cohom tensor adjunction.

##### 1.7-12 LeftCoclosedMonoidalPreCoComposeMorphism
 ‣ LeftCoclosedMonoidalPreCoComposeMorphism( a, b, c ) ( operation )

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

The arguments are three objects $$a,b,c$$. The output is the precocomposition morphism $$\mathrm{LeftCoclosedMonoidalPreCoComposeMorphism}_{a,b,c}: \mathrm{\underline{coHom}_\ell}(a,c) \rightarrow \mathrm{\underline{coHom}_\ell}(b,c) \otimes \mathrm{\underline{coHom}_\ell}(a,b)$$.

##### 1.7-13 LeftCoclosedMonoidalPreCoComposeMorphismWithGivenObjects
 ‣ LeftCoclosedMonoidalPreCoComposeMorphismWithGivenObjects( s, a, b, c, r ) ( operation )

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

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

##### 1.7-14 LeftCoclosedMonoidalPostCoComposeMorphism
 ‣ LeftCoclosedMonoidalPostCoComposeMorphism( a, b, c ) ( operation )

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

The arguments are three objects $$a,b,c$$. The output is the postcocomposition morphism $$\mathrm{LeftCoclosedMonoidalPostCoComposeMorphism}_{a,b,c}: \mathrm{\underline{coHom}_\ell}(a,c) \rightarrow \mathrm{\underline{coHom}_\ell}(a,b) \otimes \mathrm{\underline{coHom}_\ell}(b,c)$$.

##### 1.7-15 LeftCoclosedMonoidalPostCoComposeMorphismWithGivenObjects
 ‣ LeftCoclosedMonoidalPostCoComposeMorphismWithGivenObjects( s, a, b, c, r ) ( operation )

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

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

##### 1.7-16 LeftCoDualOnObjects
 ‣ LeftCoDualOnObjects( a ) ( attribute )

Returns: an object

The argument is an object $$a$$. The output is its codual object $$a_{\vee}$$.

##### 1.7-17 LeftCoDualOnMorphisms
 ‣ LeftCoDualOnMorphisms( 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 codual morphism $$\alpha_{\vee}: b_{\vee} \rightarrow a_{\vee}$$.

##### 1.7-18 LeftCoDualOnMorphismsWithGivenLeftCoDuals
 ‣ LeftCoDualOnMorphismsWithGivenLeftCoDuals( s, alpha, r ) ( operation )

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

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}$$.

##### 1.7-19 LeftCoclosedMonoidalEvaluationForLeftCoDual
 ‣ LeftCoclosedMonoidalEvaluationForLeftCoDual( a ) ( attribute )

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

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

##### 1.7-20 LeftCoclosedMonoidalEvaluationForLeftCoDualWithGivenTensorProduct
 ‣ LeftCoclosedMonoidalEvaluationForLeftCoDualWithGivenTensorProduct( s, a, r ) ( operation )

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

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

##### 1.7-21 MorphismFromLeftCoBidual
 ‣ MorphismFromLeftCoBidual( a ) ( attribute )

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

The argument is an object $$a$$. The output is the morphism from the cobidual $$(a_{\vee})_{\vee} \rightarrow a$$.

##### 1.7-22 MorphismFromLeftCoBidualWithGivenLeftCoBidual
 ‣ MorphismFromLeftCoBidualWithGivenLeftCoBidual( a, s ) ( operation )

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

The arguments are an object $$a$$, and an object $$s = (a_{\vee})_{\vee}$$. The output is the morphism from the cobidual $$(a_{\vee})_{\vee} \rightarrow a$$.

##### 1.7-23 LeftInternalCoHomTensorProductCompatibilityMorphism
 ‣ LeftInternalCoHomTensorProductCompatibilityMorphism( list ) ( operation )

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

The argument is a list of four objects $$[ a, a', b, b' ]$$. The output is the natural morphism $$\mathrm{LeftInternalCoHomTensorProductCompatibilityMorphism}_{a,a',b,b'}: \mathrm{\underline{coHom}_\ell}(a \otimes a', b \otimes b') \rightarrow \mathrm{\underline{coHom}_\ell}(a,b) \otimes \mathrm{\underline{coHom}_\ell}(a',b')$$.

##### 1.7-24 LeftInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects
 ‣ LeftInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects( s, list, r ) ( operation )

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

The arguments are a list of four objects $$[ a, a', b, b' ]$$, and two objects $$s = \mathrm{\underline{coHom}_\ell}(a \otimes a', b \otimes b')$$ and $$r = \mathrm{\underline{coHom}_\ell}(a,b) \otimes \mathrm{\underline{coHom}_\ell}(a',b')$$. The output is the natural morphism $$\mathrm{LeftInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects}_{a,a',b,b'}: \mathrm{\underline{coHom}_\ell}(a \otimes a', b \otimes b') \rightarrow \mathrm{\underline{coHom}_\ell}(a,b) \otimes \mathrm{\underline{coHom}_\ell}(a',b')$$.

##### 1.7-25 LeftCoDualityTensorProductCompatibilityMorphism
 ‣ LeftCoDualityTensorProductCompatibilityMorphism( a, b ) ( operation )

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

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

##### 1.7-26 LeftCoDualityTensorProductCompatibilityMorphismWithGivenObjects
 ‣ LeftCoDualityTensorProductCompatibilityMorphismWithGivenObjects( s, a, b, r ) ( operation )

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

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

##### 1.7-27 MorphismFromLeftInternalCoHomToTensorProduct
 ‣ MorphismFromLeftInternalCoHomToTensorProduct( a, b ) ( operation )

Returns: a morphism in $$\mathrm{Hom}( \mathrm{\underline{coHom}_\ell}(a,b), b_{\vee} \otimes a )$$.

The arguments are two objects $$a,b$$. The output is the natural morphism $$\mathrm{MorphismFromLeftInternalCoHomToTensorProduct}_{a,b}: \mathrm{\underline{coHom}_\ell}(a,b) \rightarrow b_{\vee} \otimes a$$.

##### 1.7-28 MorphismFromLeftInternalCoHomToTensorProductWithGivenObjects
 ‣ MorphismFromLeftInternalCoHomToTensorProductWithGivenObjects( s, a, b, r ) ( operation )

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

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

##### 1.7-29 IsomorphismFromLeftCoDualObjectToLeftInternalCoHomFromTensorUnit
 ‣ IsomorphismFromLeftCoDualObjectToLeftInternalCoHomFromTensorUnit( a ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}(a_{\vee}, \mathrm{\underline{coHom}_\ell}(1,a))$$.

The argument is an object $$a$$. The output is the isomorphism $$\mathrm{IsomorphismFromLeftCoDualObjectToLeftInternalCoHomFromTensorUnit}_{a}: a_{\vee} \rightarrow \mathrm{\underline{coHom}_\ell}(1,a)$$.

##### 1.7-30 IsomorphismFromLeftInternalCoHomFromTensorUnitToLeftCoDualObject
 ‣ IsomorphismFromLeftInternalCoHomFromTensorUnitToLeftCoDualObject( a ) ( attribute )

Returns: a morphism in $$\mathrm{Hom}(\mathrm{\underline{coHom}_\ell}(1,a), a_{\vee})$$.

The argument is an object $$a$$. The output is the isomorphism $$\mathrm{IsomorphismFromLeftInternalCoHomFromTensorUnitToLeftCoDualObject}_{a}: \mathrm{\underline{coHom}_\ell}(1,a) \rightarrow a_{\vee}$$.

##### 1.7-31 UniversalPropertyOfLeftCoDual
 ‣ UniversalPropertyOfLeftCoDual( t, a, alpha ) ( operation )

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

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

##### 1.7-32 LeftCoclosedMonoidalLambdaIntroduction
 ‣ LeftCoclosedMonoidalLambdaIntroduction( alpha ) ( attribute )

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

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

##### 1.7-33 LeftCoclosedMonoidalLambdaElimination
 ‣ LeftCoclosedMonoidalLambdaElimination( a, b, alpha ) ( operation )

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

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

##### 1.7-34 IsomorphismFromObjectToLeftInternalCoHom
 ‣ IsomorphismFromObjectToLeftInternalCoHom( a ) ( attribute )

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

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

##### 1.7-35 IsomorphismFromObjectToLeftInternalCoHomWithGivenLeftInternalCoHom
 ‣ IsomorphismFromObjectToLeftInternalCoHomWithGivenLeftInternalCoHom( a, r ) ( operation )

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

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

##### 1.7-36 IsomorphismFromLeftInternalCoHomToObject
 ‣ IsomorphismFromLeftInternalCoHomToObject( a ) ( attribute )

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

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

##### 1.7-37 IsomorphismFromLeftInternalCoHomToObjectWithGivenLeftInternalCoHom
 ‣ IsomorphismFromLeftInternalCoHomToObjectWithGivenLeftInternalCoHom( a, s ) ( operation )

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

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

#### 1.8 Coclosed Monoidal Categories

A monoidal category $$\mathbf{C}$$ which has for each functor $$- \otimes b: \mathbf{C} \rightarrow \mathbf{C}$$ a left adjoint (denoted by $$\mathrm{\underline{coHom}}(-,b)$$) is called a coclosed monoidal category.

If no operations involving coduals are installed manually, the codual objects will be derived as $$a_\vee \coloneqq \mathrm{\underline{coHom}}(1,a)$$.

The corresponding GAP property is called IsCoclosedMonoidalCategory.

##### 1.8-1 InternalCoHomOnObjects
 ‣ InternalCoHomOnObjects( a, b ) ( operation )

Returns: an object

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

##### 1.8-2 InternalCoHomOnMorphisms
 ‣ InternalCoHomOnMorphisms( alpha, beta ) ( operation )

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

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

##### 1.8-3 InternalCoHomOnMorphismsWithGivenInternalCoHoms
 ‣ InternalCoHomOnMorphismsWithGivenInternalCoHoms( s, alpha, beta, r ) ( operation )

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

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

##### 1.8-4 CoclosedMonoidalRightEvaluationMorphism
 ‣ CoclosedMonoidalRightEvaluationMorphism( a, b ) ( operation )

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

The arguments are two objects $$a, b$$. The output is the coclosed right evaluation morphism $$\mathrm{coclev}_{a,b}: b \rightarrow a \otimes \mathrm{\underline{coHom}}(b,a)$$, i.e., the unit of the cohom tensor adjunction.

##### 1.8-5 CoclosedMonoidalRightEvaluationMorphismWithGivenRange
 ‣ CoclosedMonoidalRightEvaluationMorphismWithGivenRange( a, b, r ) ( operation )

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

The arguments are two objects $$a,b$$ and an object $$r = a \otimes \mathrm{\underline{coHom}}(b,a)$$. The output is the coclosed right evaluation morphism $$\mathrm{coclev}_{a,b}: b \rightarrow a \otimes \mathrm{\underline{coHom}}(b,a)$$, i.e., the unit of the cohom tensor adjunction.

##### 1.8-6 CoclosedMonoidalRightCoevaluationMorphism
 ‣ CoclosedMonoidalRightCoevaluationMorphism( a, b ) ( operation )

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

The arguments are two objects $$a,b$$. The output is the coclosed right coevaluation morphism $$\mathrm{coclcoev}_{a,b}: \mathrm{\underline{coHom}}(a \otimes b, a) \rightarrow b$$, i.e., the counit of the cohom tensor adjunction.

##### 1.8-7 CoclosedMonoidalRightCoevaluationMorphismWithGivenSource
 ‣ CoclosedMonoidalRightCoevaluationMorphismWithGivenSource( a, b, s ) ( operation )

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

The arguments are two objects $$a,b$$ and an object $$s = \mathrm{\underline{coHom}}(a \otimes b, a)$$. The output is the coclosed right coevaluation morphism $$\mathrm{coclcoev}_{a,b}: \mathrm{\underline{coHom}}(a \otimes b, a) \rightarrow b$$, i.e., the unit of the cohom tensor adjunction.

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

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

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

 ‣ TensorProductToInternalCoHomRightAdjunctMorphismWithGivenInternalCoHom( b, c, g, i ) ( operation )

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

The arguments are two objects $$b,c$$, a morphism $$g: a \rightarrow b \otimes c$$ and an object $$i = \mathrm{\underline{coHom}}(a,b)$$. The output is a morphism $$f: \mathrm{\underline{coHom}}(a,b) \rightarrow c$$ corresponding to $$g$$ under the cohom tensor adjunction.

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

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

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

 ‣ InternalCoHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct( a, b, f, t ) ( operation )

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

The arguments are two objects $$a,b$$, a morphism $$f: \mathrm{\underline{coHom}}(a,b) \rightarrow c$$ and an object $$t = b \otimes c$$. The output is a morphism $$g: a \rightarrow t$$ corresponding to $$f$$ under the cohom tensor adjunction.

##### 1.8-12 CoclosedMonoidalLeftEvaluationMorphism
 ‣ CoclosedMonoidalLeftEvaluationMorphism( a, b ) ( operation )

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

The arguments are two objects $$a, b$$. The output is the coclosed left evaluation morphism $$\mathrm{coclev}_{a,b}: b \rightarrow \mathrm{\underline{coHom}}(b,a) \otimes a$$, i.e., the unit of the cohom tensor adjunction.

##### 1.8-13 CoclosedMonoidalLeftEvaluationMorphismWithGivenRange
 ‣ CoclosedMonoidalLeftEvaluationMorphismWithGivenRange( a, b, r ) ( operation )

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

The arguments are two objects $$a,b$$ and an object $$r = \mathrm{\underline{coHom}}(b,a) \otimes a$$. The output is the coclosed left evaluation morphism $$\mathrm{coclev}_{a,b}: b \rightarrow \mathrm{\underline{coHom}}(b,a) \otimes a$$, i.e., the unit of the cohom tensor adjunction.

##### 1.8-14 CoclosedMonoidalLeftCoevaluationMorphism
 ‣ CoclosedMonoidalLeftCoevaluationMorphism( a, b ) ( operation )

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

The arguments are two objects $$a,b$$. The output is the coclosed left coevaluation morphism $$\mathrm{coclcoev}_{a,b}: \mathrm{\underline{coHom}}(b \otimes a, a) \rightarrow b$$, i.e., the counit of the cohom tensor adjunction.

##### 1.8-15 CoclosedMonoidalLeftCoevaluationMorphismWithGivenSource
 ‣ CoclosedMonoidalLeftCoevaluationMorphismWithGivenSource( a, b, s ) ( operation )

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

The arguments are two objects $$a,b$$ and an object $$s = \mathrm{\underline{coHom}}(b \otimes a, a)$$. The output is the coclosed left coevaluation morphism $$\mathrm{coclcoev}_{a,b}: \mathrm{\underline{coHom}}(b \otimes a, a) \rightarrow b$$, i.e., the unit of the cohom tensor adjunction.

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

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

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

 ‣ TensorProductToInternalCoHomLeftAdjunctMorphismWithGivenInternalCoHom( b, c, g, i ) ( operation )

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

The arguments are two objects $$b,c$$, a morphism $$g: a \rightarrow b \otimes c$$ and an object $$i = \mathrm{\underline{coHom}}(a,c)$$. The output is a morphism $$f: \mathrm{\underline{coHom}}(a,c) \rightarrow b$$ corresponding to $$g$$ under the cohom tensor adjunction.

 ‣ InternalCoHomToTensorProductLeftAdjunctMorphism( a, c, f ) ( operation )

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

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

 ‣ InternalCoHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct( a, c, f, t ) ( operation )

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

The arguments are two objects $$a,c$$, a morphism $$f: \mathrm{\underline{coHom}}(a,c) \rightarrow b$$ and an object $$t = b \otimes c$$. The output is a morphism $$g: a \rightarrow t$$ corresponding to $$f$$ under the cohom tensor adjunction.

##### 1.8-20 MonoidalPreCoComposeMorphism
 ‣ MonoidalPreCoComposeMorphism( a, b, c ) ( operation )

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

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

##### 1.8-21 MonoidalPreCoComposeMorphismWithGivenObjects
 ‣ MonoidalPreCoComposeMorphismWithGivenObjects( s, a, b, c, r ) ( operation )

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

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

##### 1.8-22 MonoidalPostCoComposeMorphism
 ‣ MonoidalPostCoComposeMorphism( a, b, c ) ( operation )

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

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

##### 1.8-23 MonoidalPostCoComposeMorphismWithGivenObjects
 ‣ MonoidalPostCoComposeMorphismWithGivenObjects( s, a, b, c, r ) ( operation )

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

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

##### 1.8-24 CoDualOnObjects
 ‣ CoDualOnObjects( a ) ( attribute )

Returns: an object

The argument is an object $$a$$. The output is its codual object $$a_{\vee}$$.

##### 1.8-25 CoDualOnMorphisms
 ‣ CoDualOnMorphisms( 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 codual morphism $$\alpha_{\vee}: b_{\vee} \rightarrow a_{\vee}$$.

##### 1.8-26 CoDualOnMorphismsWithGivenCoDuals
 ‣ CoDualOnMorphismsWithGivenCoDuals( s, alpha, r ) ( operation )

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

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}$$.

##### 1.8-27 CoclosedEvaluationForCoDual
 ‣ CoclosedEvaluationForCoDual( a ) ( attribute )

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

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

##### 1.8-28 CoclosedEvaluationForCoDualWithGivenTensorProduct
 ‣ CoclosedEvaluationForCoDualWithGivenTensorProduct( s, a, r ) ( operation )

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

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

##### 1.8-29 MorphismFromCoBidual
 ‣ MorphismFromCoBidual( a ) ( attribute )

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

The argument is an object $$a$$. The output is the morphism from the cobidual $$(a_{\vee})_{\vee} \rightarrow a$$.

##### 1.8-30 MorphismFromCoBidualWithGivenCoBidual
 ‣ MorphismFromCoBidualWithGivenCoBidual( a, s ) ( operation )

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

The arguments are an object $$a$$, and an object $$s = (a_{\vee})_{\vee}$$. The output is the morphism from the cobidual $$(a_{\vee})_{\vee} \rightarrow a$$.

##### 1.8-31 InternalCoHomTensorProductCompatibilityMorphism
 ‣ InternalCoHomTensorProductCompatibilityMorphism( list ) ( operation )

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

The argument is a list of four objects $$[ a, a', b, b' ]$$. The output is the natural morphism $$\mathrm{InternalCoHomTensorProductCompatibilityMorphism}_{a,a',b,b'}: \mathrm{\underline{coHom}}(a \otimes a', b \otimes b') \rightarrow \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(a',b')$$.

##### 1.8-32 InternalCoHomTensorProductCompatibilityMorphismWithGivenObjects
 ‣ InternalCoHomTensorProductCompatibilityMorphismWithGivenObjects( s, list, r ) ( operation )

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

The arguments are a list of four objects $$[ a, a', b, b' ]$$, and two objects $$s = \mathrm{\underline{coHom}}(a \otimes a', b \otimes b')$$ and $$r = \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(a',b')$$. The output is the natural morphism $$\mathrm{InternalCoHomTensorProductCompatibilityMorphismWithGivenObjects}_{a,a',b,b'}: \mathrm{\underline{coHom}}(a \otimes a', b \otimes b') \rightarrow \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(a',b')$$.

##### 1.8-33 CoDualityTensorProductCompatibilityMorphism
 ‣ CoDualityTensorProductCompatibilityMorphism( a, b ) ( operation )

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

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

##### 1.8-34 CoDualityTensorProductCompatibilityMorphismWithGivenObjects
 ‣ CoDualityTensorProductCompatibilityMorphismWithGivenObjects( s, a, b, r ) ( operation )

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

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

##### 1.8-35 MorphismFromInternalCoHomToTensorProduct
 ‣ MorphismFromInternalCoHomToTensorProduct( a, b ) ( operation )

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

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

##### 1.8-36 MorphismFromInternalCoHomToTensorProductWithGivenObjects
 ‣ MorphismFromInternalCoHomToTensorProductWithGivenObjects( s, a, b, r ) ( operation )

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

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

##### 1.8-37 IsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit
 ‣ IsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit( a ) ( attribute )

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

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

##### 1.8-38 IsomorphismFromInternalCoHomFromTensorUnitToCoDualObject
 ‣ IsomorphismFromInternalCoHomFromTensorUnitToCoDualObject( a ) ( attribute )

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

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

##### 1.8-39 UniversalPropertyOfCoDual
 ‣ UniversalPropertyOfCoDual( t, a, alpha ) ( operation )

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

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

##### 1.8-40 CoLambdaIntroduction
 ‣ CoLambdaIntroduction( alpha ) ( attribute )

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

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

##### 1.8-41 CoLambdaElimination
 ‣ CoLambdaElimination( a, b, alpha ) ( operation )

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

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

##### 1.8-42 IsomorphismFromObjectToInternalCoHom
 ‣ IsomorphismFromObjectToInternalCoHom( a ) ( attribute )

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

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

##### 1.8-43 IsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom
 ‣ IsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom( a, r ) ( operation )

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

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

##### 1.8-44 IsomorphismFromInternalCoHomToObject
 ‣ IsomorphismFromInternalCoHomToObject( a ) ( attribute )

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

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

##### 1.8-45 IsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom
 ‣ IsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom( a, s ) ( operation )

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

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

#### 1.9 Symmetric Closed Monoidal Categories

A monoidal category $$\mathbf{C}$$ which is symmetric and closed is called a symmetric closed monoidal category.

The corresponding GAP property is given by IsSymmetricClosedMonoidalCategory.

#### 1.10 Symmetric Coclosed Monoidal Categories

A monoidal category $$\mathbf{C}$$ which is symmetric and coclosed is called a symmetric coclosed monoidal category.

The corresponding GAP property is given by IsSymmetricCoclosedMonoidalCategory.

#### 1.11 Rigid Symmetric Closed Monoidal Categories

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

• the natural morphism

$$\mathrm{\underline{Hom}_\ell}(a, a') \otimes \mathrm{\underline{Hom}_\ell}(b, b') \rightarrow \mathrm{\underline{Hom}_\ell}(a \otimes b, a' \otimes b')$$ is an isomorphism,

• the natural morphism

$$a \rightarrow \mathrm{\underline{Hom}_\ell}(\mathrm{\underline{Hom}_\ell}(a, 1), 1)$$ is an isomorphism is called a rigid symmetric closed monoidal category.

If no operations involving the closed structure are installed manually, the internal hom objects will be derived as $$\mathrm{\underline{Hom}_\ell}(a,b) \coloneqq a^\vee \otimes b$$ and, in particular, $$\mathrm{\underline{Hom}_\ell}(a,1) \coloneqq a^\vee \otimes 1$$.

The corresponding GAP property is given by IsRigidSymmetricClosedMonoidalCategory.

##### 1.11-1 IsomorphismFromTensorProductWithDualObjectToInternalHom
 ‣ IsomorphismFromTensorProductWithDualObjectToInternalHom( 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{IsomorphismFromTensorProductWithDualObjectToInternalHom}_{a,b}: a^{\vee} \otimes b \rightarrow \mathrm{\underline{Hom}}(a,b)$$.

##### 1.11-2 IsomorphismFromInternalHomToTensorProductWithDualObject
 ‣ IsomorphismFromInternalHomToTensorProductWithDualObject( 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{IsomorphismFromTensorProductWithDualObjectToInternalHom}$$, namely $$\mathrm{IsomorphismFromInternalHomToTensorProductWithDualObject}_{a,b}: \mathrm{\underline{Hom}}(a,b) \rightarrow a^{\vee} \otimes b$$.

##### 1.11-3 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$$.

##### 1.11-4 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$$.

##### 1.11-5 TensorProductInternalHomCompatibilityMorphismInverse
 ‣ TensorProductInternalHomCompatibilityMorphismInverse( list ) ( 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 argument is a list of 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')$$.

##### 1.11-6 TensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects
 ‣ TensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects( s, list, r ) ( 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 a list of four objects $$[ a, a', b, b' ]$$, and two objects $$s = \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b')$$ and $$r = \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(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')$$.

##### 1.11-7 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}$$.

##### 1.11-8 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}$$.

##### 1.11-9 TraceMap
 ‣ TraceMap( alpha ) ( attribute )

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

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

##### 1.11-10 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$$.

##### 1.11-11 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$$.

##### 1.11-12 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$$.

#### 1.12 Rigid Symmetric Coclosed Monoidal Categories

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

• the natural morphism

$$\mathrm{\underline{coHom}}(a \otimes a', b \otimes b') \rightarrow \mathrm{\underline{coHom}}(a, b) \otimes \mathrm{\underline{coHom}}(a', b')$$ is an isomorphism,

• the natural morphism

$$\mathrm{\underline{coHom}}(1, \mathrm{\underline{coHom}}(1, a)) \rightarrow a$$ is an isomorphism is called a rigid symmetric coclosed monoidal category.

If no operations involving the coclosed structure are installed manually, the internal cohom objects will be derived as $$\mathrm{\underline{coHom}}(a,b) \coloneqq a \otimes b_\vee$$ and, in particular, $$\mathrm{\underline{coHom}}(1,a) \coloneqq 1 \otimes a_\vee$$.

The corresponding GAP property is given by IsRigidSymmetricCoclosedMonoidalCategory.

##### 1.12-1 IsomorphismFromInternalCoHomToTensorProductWithCoDualObject
 ‣ IsomorphismFromInternalCoHomToTensorProductWithCoDualObject( a, b ) ( operation )

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

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

##### 1.12-2 IsomorphismFromTensorProductWithCoDualObjectToInternalCoHom
 ‣ IsomorphismFromTensorProductWithCoDualObjectToInternalCoHom( a, b ) ( operation )

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

The arguments are two objects $$a,b$$. The output is the inverse of $$\mathrm{IsomorphismFromInternalCoHomToTensorProductWithCoDualObject}$$, namely $$\mathrm{IsomorphismFromTensorProductWithCoDualObjectToInternalCoHom}_{a,b}: a_{\vee} \otimes b \rightarrow \mathrm{\underline{coHom}}(b,a)$$.

##### 1.12-3 MorphismFromTensorProductToInternalCoHom
 ‣ MorphismFromTensorProductToInternalCoHom( a, b ) ( operation )

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

The arguments are two objects $$a,b$$. The output is the inverse of $$\mathrm{MorphismFromInternalCoHomToTensorProductWithGivenObjects}$$, namely $$\mathrm{MorphismFromTensorProductToInternalCoHomWithGivenObjects}_{a,b}: a_{\vee} \otimes b \rightarrow \mathrm{\underline{coHom}}(b,a)$$.

##### 1.12-4 MorphismFromTensorProductToInternalCoHomWithGivenObjects
 ‣ MorphismFromTensorProductToInternalCoHomWithGivenObjects( s, a, b, r ) ( operation )

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

The arguments are an object $$s_{\vee} = a \otimes b$$, two objects $$a,b$$, and an object $$r = \mathrm{\underline{coHom}}(b,a)$$. The output is the inverse of $$\mathrm{MorphismFromInternalCoHomToTensorProductWithGivenObjects}$$, namely $$\mathrm{MorphismFromTensorProductToInternalCoHomWithGivenObjects}_{a,b}: a_{\vee} \otimes b \rightarrow \mathrm{\underline{coHom}}(b,a)$$.

##### 1.12-5 InternalCoHomTensorProductCompatibilityMorphismInverse
 ‣ InternalCoHomTensorProductCompatibilityMorphismInverse( list ) ( operation )

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

The argument is a list of four objects $$[ a, a', b, b' ]$$. The output is the natural morphism $$\mathrm{InternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects}_{a,a',b,b'}: \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(a',b') \rightarrow \mathrm{\underline{coHom}}(a \otimes a', b \otimes b')$$.

##### 1.12-6 InternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects
 ‣ InternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects( s, list, r ) ( operation )

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

The arguments are a list of four objects $$[ a, a', b, b' ]$$, and two objects $$s = \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(a',b')$$ and $$r = \mathrm{\underline{coHom}}(a \otimes a', b \otimes b')$$. The output is the natural morphism $$\mathrm{InternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects}_{a,a',b,b'}: \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(a',b') \rightarrow \mathrm{\underline{coHom}}(a \otimes a', b \otimes b')$$.

##### 1.12-7 CoclosedCoevaluationForCoDual
 ‣ CoclosedCoevaluationForCoDual( a ) ( attribute )

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

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

##### 1.12-8 CoclosedCoevaluationForCoDualWithGivenTensorProduct
 ‣ CoclosedCoevaluationForCoDualWithGivenTensorProduct( s, a, r ) ( operation )

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

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

##### 1.12-9 CoTraceMap
 ‣ CoTraceMap( alpha ) ( attribute )

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

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

##### 1.12-10 CoRankMorphism
 ‣ CoRankMorphism( a ) ( attribute )

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

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

##### 1.12-11 MorphismToCoBidual
 ‣ MorphismToCoBidual( a ) ( attribute )

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

The argument is an object $$a$$. The output is the inverse of the morphism from the cobidual $$a \rightarrow (a_{\vee})_{\vee}$$.

##### 1.12-12 MorphismToCoBidualWithGivenCoBidual
 ‣ MorphismToCoBidualWithGivenCoBidual( a, r ) ( operation )

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

The argument is an object $$a$$, and an object $$r = (a_{\vee})_{\vee}$$. The output is the inverse of the morphism from the cobidual $$a \rightarrow (a_{\vee})_{\vee}$$.

#### 1.13 Convenience Methods

##### 1.13-1 InternalHom
 ‣ InternalHom( a, b ) ( operation )

Returns: a cell

This is a convenience method. The arguments are two cells $$a,b$$. The output is the internal hom cell. If $$a,b$$ are two CAP objects the output is the internal Hom object $$\mathrm{\underline{Hom}}(a,b)$$. If at least one of the arguments is a CAP morphism the output is a CAP morphism, namely the internal hom on morphisms, where any object is replaced by its identity morphism.

##### 1.13-2 InternalCoHom
 ‣ InternalCoHom( a, b ) ( operation )

Returns: a cell

This is a convenience method. The arguments are two cells $$a,b$$. The output is the internal cohom cell. If $$a,b$$ are two CAP objects the output is the internal cohom object $$\mathrm{\underline{coHom}}(a,b)$$. If at least one of the arguments is a CAP morphism the output is a CAP morphism, namely the internal cohom on morphisms, where any object is replaced by its identity morphism.

##### 1.13-3 LeftInternalHom
 ‣ LeftInternalHom( a, b ) ( operation )

Returns: a cell

This is a convenience method. The arguments are two cells $$a,b$$. The output is the internal hom cell. If $$a,b$$ are two CAP objects the output is the internal Hom object $$\mathrm{\underline{Hom}_\ell}(a,b)$$. If at least one of the arguments is a CAP morphism the output is a CAP morphism, namely the internal hom on morphisms, where any object is replaced by its identity morphism.

##### 1.13-4 LeftInternalCoHom
 ‣ LeftInternalCoHom( a, b ) ( operation )

Returns: a cell

This is a convenience method. The arguments are two cells $$a,b$$. The output is the internal cohom cell. If $$a,b$$ are two CAP objects the output is the internal cohom object $$\mathrm{\underline{coHom}_\ell}(a,b)$$. If at least one of the arguments is a CAP morphism the output is a CAP morphism, namely the internal cohom on morphisms, where any object is replaced by its identity morphism.

 ‣ AddLeftDistributivityExpanding( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LeftDistributivityExpanding. $$F: ( a, L ) \mapsto \mathtt{LeftDistributivityExpanding}(a, L)$$.

 ‣ AddLeftDistributivityExpandingWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LeftDistributivityExpandingWithGivenObjects. $$F: ( s, a, L, r ) \mapsto \mathtt{LeftDistributivityExpandingWithGivenObjects}(s, a, L, r)$$.

 ‣ AddLeftDistributivityFactoring( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LeftDistributivityFactoring. $$F: ( a, L ) \mapsto \mathtt{LeftDistributivityFactoring}(a, L)$$.

 ‣ AddLeftDistributivityFactoringWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LeftDistributivityFactoringWithGivenObjects. $$F: ( s, a, L, r ) \mapsto \mathtt{LeftDistributivityFactoringWithGivenObjects}(s, a, L, r)$$.

 ‣ AddRightDistributivityExpanding( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation RightDistributivityExpanding. $$F: ( L, a ) \mapsto \mathtt{RightDistributivityExpanding}(L, a)$$.

 ‣ AddRightDistributivityExpandingWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation RightDistributivityExpandingWithGivenObjects. $$F: ( s, L, a, r ) \mapsto \mathtt{RightDistributivityExpandingWithGivenObjects}(s, L, a, r)$$.

 ‣ AddRightDistributivityFactoring( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation RightDistributivityFactoring. $$F: ( L, a ) \mapsto \mathtt{RightDistributivityFactoring}(L, a)$$.

 ‣ AddRightDistributivityFactoringWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation RightDistributivityFactoringWithGivenObjects. $$F: ( s, L, a, r ) \mapsto \mathtt{RightDistributivityFactoringWithGivenObjects}(s, L, a, r)$$.

 ‣ AddBraiding( C, F ) ( operation )

Returns: nothing

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

 ‣ AddBraidingInverse( C, F ) ( operation )

Returns: nothing

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

 ‣ AddBraidingInverseWithGivenTensorProducts( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation BraidingInverseWithGivenTensorProducts. $$F: ( s, a, b, r ) \mapsto \mathtt{BraidingInverseWithGivenTensorProducts}(s, a, b, r)$$.

 ‣ AddBraidingWithGivenTensorProducts( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation BraidingWithGivenTensorProducts. $$F: ( s, a, b, r ) \mapsto \mathtt{BraidingWithGivenTensorProducts}(s, a, b, r)$$.

 ‣ AddClosedMonoidalLeftCoevaluationMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddClosedMonoidalLeftCoevaluationMorphismWithGivenRange( C, F ) ( operation )

Returns: nothing

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

 ‣ AddClosedMonoidalLeftEvaluationMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddClosedMonoidalLeftEvaluationMorphismWithGivenSource( C, F ) ( operation )

Returns: nothing

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

 ‣ AddClosedMonoidalRightCoevaluationMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddClosedMonoidalRightCoevaluationMorphismWithGivenRange( C, F ) ( operation )

Returns: nothing

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

 ‣ AddClosedMonoidalRightEvaluationMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddClosedMonoidalRightEvaluationMorphismWithGivenSource( C, F ) ( operation )

Returns: nothing

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

 ‣ AddDualOnMorphisms( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation DualOnMorphisms. $$F: ( alpha ) \mapsto \mathtt{DualOnMorphisms}(alpha)$$.

 ‣ AddDualOnMorphismsWithGivenDuals( C, F ) ( operation )

Returns: nothing

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

 ‣ AddDualOnObjects( C, F ) ( operation )

Returns: nothing

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

 ‣ AddEvaluationForDual( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation EvaluationForDual. $$F: ( a ) \mapsto \mathtt{EvaluationForDual}(a)$$.

 ‣ AddEvaluationForDualWithGivenTensorProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation EvaluationForDualWithGivenTensorProduct. $$F: ( s, a, r ) \mapsto \mathtt{EvaluationForDualWithGivenTensorProduct}(s, a, r)$$.

 ‣ AddInternalHomOnMorphisms( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation InternalHomOnMorphisms. $$F: ( alpha, beta ) \mapsto \mathtt{InternalHomOnMorphisms}(alpha, beta)$$.

 ‣ AddInternalHomOnMorphismsWithGivenInternalHoms( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation InternalHomOnMorphismsWithGivenInternalHoms. $$F: ( s, alpha, beta, r ) \mapsto \mathtt{InternalHomOnMorphismsWithGivenInternalHoms}(s, alpha, beta, r)$$.

 ‣ AddInternalHomOnObjects( C, F ) ( operation )

Returns: nothing

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

 ‣ AddInternalHomToTensorProductLeftAdjunctMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddInternalHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation InternalHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct. $$F: ( b, c, g, s ) \mapsto \mathtt{InternalHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct}(b, c, g, s)$$.

 ‣ AddInternalHomToTensorProductRightAdjunctMorphism( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation InternalHomToTensorProductRightAdjunctMorphism. $$F: ( a, c, g ) \mapsto \mathtt{InternalHomToTensorProductRightAdjunctMorphism}(a, c, g)$$.

 ‣ AddInternalHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation InternalHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct. $$F: ( a, c, g, s ) \mapsto \mathtt{InternalHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct}(a, c, g, s)$$.

 ‣ AddIsomorphismFromDualObjectToInternalHomIntoTensorUnit( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation IsomorphismFromDualObjectToInternalHomIntoTensorUnit. $$F: ( a ) \mapsto \mathtt{IsomorphismFromDualObjectToInternalHomIntoTensorUnit}(a)$$.

 ‣ AddIsomorphismFromInternalHomIntoTensorUnitToDualObject( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation IsomorphismFromInternalHomIntoTensorUnitToDualObject. $$F: ( a ) \mapsto \mathtt{IsomorphismFromInternalHomIntoTensorUnitToDualObject}(a)$$.

 ‣ AddIsomorphismFromInternalHomToObject( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation IsomorphismFromInternalHomToObject. $$F: ( a ) \mapsto \mathtt{IsomorphismFromInternalHomToObject}(a)$$.

 ‣ AddIsomorphismFromInternalHomToObjectWithGivenInternalHom( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation IsomorphismFromInternalHomToObjectWithGivenInternalHom. $$F: ( a, s ) \mapsto \mathtt{IsomorphismFromInternalHomToObjectWithGivenInternalHom}(a, s)$$.

 ‣ AddIsomorphismFromObjectToInternalHom( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation IsomorphismFromObjectToInternalHom. $$F: ( a ) \mapsto \mathtt{IsomorphismFromObjectToInternalHom}(a)$$.

 ‣ AddIsomorphismFromObjectToInternalHomWithGivenInternalHom( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation IsomorphismFromObjectToInternalHomWithGivenInternalHom. $$F: ( a, r ) \mapsto \mathtt{IsomorphismFromObjectToInternalHomWithGivenInternalHom}(a, r)$$.

 ‣ AddLambdaElimination( C, F ) ( operation )

Returns: nothing

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

 ‣ AddLambdaIntroduction( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LambdaIntroduction. $$F: ( alpha ) \mapsto \mathtt{LambdaIntroduction}(alpha)$$.

 ‣ AddMonoidalPostComposeMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddMonoidalPostComposeMorphismWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation MonoidalPostComposeMorphismWithGivenObjects. $$F: ( s, a, b, c, r ) \mapsto \mathtt{MonoidalPostComposeMorphismWithGivenObjects}(s, a, b, c, r)$$.

 ‣ AddMonoidalPreComposeMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddMonoidalPreComposeMorphismWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation MonoidalPreComposeMorphismWithGivenObjects. $$F: ( s, a, b, c, r ) \mapsto \mathtt{MonoidalPreComposeMorphismWithGivenObjects}(s, a, b, c, r)$$.

 ‣ AddMorphismFromTensorProductToInternalHom( C, F ) ( operation )

Returns: nothing

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

 ‣ AddMorphismFromTensorProductToInternalHomWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation MorphismFromTensorProductToInternalHomWithGivenObjects. $$F: ( s, a, b, r ) \mapsto \mathtt{MorphismFromTensorProductToInternalHomWithGivenObjects}(s, a, b, r)$$.

 ‣ AddMorphismToBidual( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation MorphismToBidual. $$F: ( a ) \mapsto \mathtt{MorphismToBidual}(a)$$.

 ‣ AddMorphismToBidualWithGivenBidual( C, F ) ( operation )

Returns: nothing

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

 ‣ AddTensorProductDualityCompatibilityMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddTensorProductDualityCompatibilityMorphismWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation TensorProductDualityCompatibilityMorphismWithGivenObjects. $$F: ( s, a, b, r ) \mapsto \mathtt{TensorProductDualityCompatibilityMorphismWithGivenObjects}(s, a, b, r)$$.

 ‣ AddTensorProductInternalHomCompatibilityMorphism( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation TensorProductInternalHomCompatibilityMorphism. $$F: ( list ) \mapsto \mathtt{TensorProductInternalHomCompatibilityMorphism}(list)$$.

 ‣ AddTensorProductInternalHomCompatibilityMorphismWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation TensorProductInternalHomCompatibilityMorphismWithGivenObjects. $$F: ( source, list, range ) \mapsto \mathtt{TensorProductInternalHomCompatibilityMorphismWithGivenObjects}(source, list, range)$$.

 ‣ AddTensorProductToInternalHomLeftAdjunctMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddTensorProductToInternalHomLeftAdjunctMorphismWithGivenInternalHom( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation TensorProductToInternalHomLeftAdjunctMorphismWithGivenInternalHom. $$F: ( a, b, f, i ) \mapsto \mathtt{TensorProductToInternalHomLeftAdjunctMorphismWithGivenInternalHom}(a, b, f, i)$$.

 ‣ AddTensorProductToInternalHomRightAdjunctMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddTensorProductToInternalHomRightAdjunctMorphismWithGivenInternalHom( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation TensorProductToInternalHomRightAdjunctMorphismWithGivenInternalHom. $$F: ( a, b, f, i ) \mapsto \mathtt{TensorProductToInternalHomRightAdjunctMorphismWithGivenInternalHom}(a, b, f, i)$$.

 ‣ AddUniversalPropertyOfDual( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCoDualOnMorphisms( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation CoDualOnMorphisms. $$F: ( alpha ) \mapsto \mathtt{CoDualOnMorphisms}(alpha)$$.

 ‣ AddCoDualOnMorphismsWithGivenCoDuals( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation CoDualOnMorphismsWithGivenCoDuals. $$F: ( s, alpha, r ) \mapsto \mathtt{CoDualOnMorphismsWithGivenCoDuals}(s, alpha, r)$$.

 ‣ AddCoDualOnObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation CoDualOnObjects. $$F: ( a ) \mapsto \mathtt{CoDualOnObjects}(a)$$.

 ‣ AddCoDualityTensorProductCompatibilityMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCoDualityTensorProductCompatibilityMorphismWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation CoDualityTensorProductCompatibilityMorphismWithGivenObjects. $$F: ( s, a, b, r ) \mapsto \mathtt{CoDualityTensorProductCompatibilityMorphismWithGivenObjects}(s, a, b, r)$$.

 ‣ AddCoLambdaElimination( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCoLambdaIntroduction( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation CoLambdaIntroduction. $$F: ( alpha ) \mapsto \mathtt{CoLambdaIntroduction}(alpha)$$.

 ‣ AddCoclosedEvaluationForCoDual( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation CoclosedEvaluationForCoDual. $$F: ( a ) \mapsto \mathtt{CoclosedEvaluationForCoDual}(a)$$.

 ‣ AddCoclosedEvaluationForCoDualWithGivenTensorProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation CoclosedEvaluationForCoDualWithGivenTensorProduct. $$F: ( s, a, r ) \mapsto \mathtt{CoclosedEvaluationForCoDualWithGivenTensorProduct}(s, a, r)$$.

 ‣ AddCoclosedMonoidalLeftCoevaluationMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCoclosedMonoidalLeftCoevaluationMorphismWithGivenSource( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCoclosedMonoidalLeftEvaluationMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCoclosedMonoidalLeftEvaluationMorphismWithGivenRange( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCoclosedMonoidalRightCoevaluationMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCoclosedMonoidalRightCoevaluationMorphismWithGivenSource( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCoclosedMonoidalRightEvaluationMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCoclosedMonoidalRightEvaluationMorphismWithGivenRange( C, F ) ( operation )

Returns: nothing

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

 ‣ AddInternalCoHomOnMorphisms( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation InternalCoHomOnMorphisms. $$F: ( alpha, beta ) \mapsto \mathtt{InternalCoHomOnMorphisms}(alpha, beta)$$.

 ‣ AddInternalCoHomOnMorphismsWithGivenInternalCoHoms( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation InternalCoHomOnMorphismsWithGivenInternalCoHoms. $$F: ( s, alpha, beta, r ) \mapsto \mathtt{InternalCoHomOnMorphismsWithGivenInternalCoHoms}(s, alpha, beta, r)$$.

 ‣ AddInternalCoHomOnObjects( C, F ) ( operation )

Returns: nothing

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

 ‣ AddInternalCoHomTensorProductCompatibilityMorphism( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation InternalCoHomTensorProductCompatibilityMorphism. $$F: ( list ) \mapsto \mathtt{InternalCoHomTensorProductCompatibilityMorphism}(list)$$.

 ‣ AddInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation InternalCoHomTensorProductCompatibilityMorphismWithGivenObjects. $$F: ( source, list, range ) \mapsto \mathtt{InternalCoHomTensorProductCompatibilityMorphismWithGivenObjects}(source, list, range)$$.

 ‣ AddInternalCoHomToTensorProductLeftAdjunctMorphism( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation InternalCoHomToTensorProductLeftAdjunctMorphism. $$F: ( a, c, f ) \mapsto \mathtt{InternalCoHomToTensorProductLeftAdjunctMorphism}(a, c, f)$$.

 ‣ AddInternalCoHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation InternalCoHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct. $$F: ( a, c, f, t ) \mapsto \mathtt{InternalCoHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct}(a, c, f, t)$$.

 ‣ AddInternalCoHomToTensorProductRightAdjunctMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddInternalCoHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation InternalCoHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct. $$F: ( a, b, f, t ) \mapsto \mathtt{InternalCoHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct}(a, b, f, t)$$.

 ‣ AddIsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation IsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit. $$F: ( a ) \mapsto \mathtt{IsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit}(a)$$.

 ‣ AddIsomorphismFromInternalCoHomFromTensorUnitToCoDualObject( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation IsomorphismFromInternalCoHomFromTensorUnitToCoDualObject. $$F: ( a ) \mapsto \mathtt{IsomorphismFromInternalCoHomFromTensorUnitToCoDualObject}(a)$$.

 ‣ AddIsomorphismFromInternalCoHomToObject( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation IsomorphismFromInternalCoHomToObject. $$F: ( a ) \mapsto \mathtt{IsomorphismFromInternalCoHomToObject}(a)$$.

 ‣ AddIsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation IsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom. $$F: ( a, s ) \mapsto \mathtt{IsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom}(a, s)$$.

 ‣ AddIsomorphismFromObjectToInternalCoHom( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation IsomorphismFromObjectToInternalCoHom. $$F: ( a ) \mapsto \mathtt{IsomorphismFromObjectToInternalCoHom}(a)$$.

 ‣ AddIsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation IsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom. $$F: ( a, r ) \mapsto \mathtt{IsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom}(a, r)$$.

 ‣ AddMonoidalPostCoComposeMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddMonoidalPostCoComposeMorphismWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation MonoidalPostCoComposeMorphismWithGivenObjects. $$F: ( s, a, b, c, r ) \mapsto \mathtt{MonoidalPostCoComposeMorphismWithGivenObjects}(s, a, b, c, r)$$.

 ‣ AddMonoidalPreCoComposeMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddMonoidalPreCoComposeMorphismWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation MonoidalPreCoComposeMorphismWithGivenObjects. $$F: ( s, a, b, c, r ) \mapsto \mathtt{MonoidalPreCoComposeMorphismWithGivenObjects}(s, a, b, c, r)$$.

 ‣ AddMorphismFromCoBidual( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation MorphismFromCoBidual. $$F: ( a ) \mapsto \mathtt{MorphismFromCoBidual}(a)$$.

 ‣ AddMorphismFromCoBidualWithGivenCoBidual( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation MorphismFromCoBidualWithGivenCoBidual. $$F: ( a, s ) \mapsto \mathtt{MorphismFromCoBidualWithGivenCoBidual}(a, s)$$.

 ‣ AddMorphismFromInternalCoHomToTensorProduct( C, F ) ( operation )

Returns: nothing

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

 ‣ AddMorphismFromInternalCoHomToTensorProductWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation MorphismFromInternalCoHomToTensorProductWithGivenObjects. $$F: ( s, a, b, r ) \mapsto \mathtt{MorphismFromInternalCoHomToTensorProductWithGivenObjects}(s, a, b, r)$$.

 ‣ AddTensorProductToInternalCoHomLeftAdjunctMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddTensorProductToInternalCoHomLeftAdjunctMorphismWithGivenInternalCoHom( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation TensorProductToInternalCoHomLeftAdjunctMorphismWithGivenInternalCoHom. $$F: ( b, c, g, i ) \mapsto \mathtt{TensorProductToInternalCoHomLeftAdjunctMorphismWithGivenInternalCoHom}(b, c, g, i)$$.

 ‣ AddTensorProductToInternalCoHomRightAdjunctMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddTensorProductToInternalCoHomRightAdjunctMorphismWithGivenInternalCoHom( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation TensorProductToInternalCoHomRightAdjunctMorphismWithGivenInternalCoHom. $$F: ( b, c, g, i ) \mapsto \mathtt{TensorProductToInternalCoHomRightAdjunctMorphismWithGivenInternalCoHom}(b, c, g, i)$$.

 ‣ AddUniversalPropertyOfCoDual( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation UniversalPropertyOfCoDual. $$F: ( t, a, alpha ) \mapsto \mathtt{UniversalPropertyOfCoDual}(t, a, alpha)$$.

 ‣ AddIsomorphismFromLeftDualObjectToLeftInternalHomIntoTensorUnit( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation IsomorphismFromLeftDualObjectToLeftInternalHomIntoTensorUnit. $$F: ( a ) \mapsto \mathtt{IsomorphismFromLeftDualObjectToLeftInternalHomIntoTensorUnit}(a)$$.

 ‣ AddIsomorphismFromLeftInternalHomIntoTensorUnitToLeftDualObject( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation IsomorphismFromLeftInternalHomIntoTensorUnitToLeftDualObject. $$F: ( a ) \mapsto \mathtt{IsomorphismFromLeftInternalHomIntoTensorUnitToLeftDualObject}(a)$$.

 ‣ AddIsomorphismFromLeftInternalHomToObject( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation IsomorphismFromLeftInternalHomToObject. $$F: ( a ) \mapsto \mathtt{IsomorphismFromLeftInternalHomToObject}(a)$$.

 ‣ AddIsomorphismFromLeftInternalHomToObjectWithGivenLeftInternalHom( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation IsomorphismFromLeftInternalHomToObjectWithGivenLeftInternalHom. $$F: ( a, s ) \mapsto \mathtt{IsomorphismFromLeftInternalHomToObjectWithGivenLeftInternalHom}(a, s)$$.

 ‣ AddIsomorphismFromObjectToLeftInternalHom( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation IsomorphismFromObjectToLeftInternalHom. $$F: ( a ) \mapsto \mathtt{IsomorphismFromObjectToLeftInternalHom}(a)$$.

 ‣ AddIsomorphismFromObjectToLeftInternalHomWithGivenLeftInternalHom( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation IsomorphismFromObjectToLeftInternalHomWithGivenLeftInternalHom. $$F: ( a, r ) \mapsto \mathtt{IsomorphismFromObjectToLeftInternalHomWithGivenLeftInternalHom}(a, r)$$.

 ‣ AddLeftClosedMonoidalCoevaluationMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddLeftClosedMonoidalCoevaluationMorphismWithGivenRange( C, F ) ( operation )

Returns: nothing

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

 ‣ AddLeftClosedMonoidalEvaluationForLeftDual( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LeftClosedMonoidalEvaluationForLeftDual. $$F: ( a ) \mapsto \mathtt{LeftClosedMonoidalEvaluationForLeftDual}(a)$$.

 ‣ AddLeftClosedMonoidalEvaluationForLeftDualWithGivenTensorProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LeftClosedMonoidalEvaluationForLeftDualWithGivenTensorProduct. $$F: ( s, a, r ) \mapsto \mathtt{LeftClosedMonoidalEvaluationForLeftDualWithGivenTensorProduct}(s, a, r)$$.

 ‣ AddLeftClosedMonoidalEvaluationMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddLeftClosedMonoidalEvaluationMorphismWithGivenSource( C, F ) ( operation )

Returns: nothing

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

 ‣ AddLeftClosedMonoidalLambdaElimination( C, F ) ( operation )

Returns: nothing

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

 ‣ AddLeftClosedMonoidalLambdaIntroduction( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LeftClosedMonoidalLambdaIntroduction. $$F: ( alpha ) \mapsto \mathtt{LeftClosedMonoidalLambdaIntroduction}(alpha)$$.

 ‣ AddLeftClosedMonoidalPostComposeMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddLeftClosedMonoidalPostComposeMorphismWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LeftClosedMonoidalPostComposeMorphismWithGivenObjects. $$F: ( s, a, b, c, r ) \mapsto \mathtt{LeftClosedMonoidalPostComposeMorphismWithGivenObjects}(s, a, b, c, r)$$.

 ‣ AddLeftClosedMonoidalPreComposeMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddLeftClosedMonoidalPreComposeMorphismWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LeftClosedMonoidalPreComposeMorphismWithGivenObjects. $$F: ( s, a, b, c, r ) \mapsto \mathtt{LeftClosedMonoidalPreComposeMorphismWithGivenObjects}(s, a, b, c, r)$$.

 ‣ AddLeftDualOnMorphisms( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LeftDualOnMorphisms. $$F: ( alpha ) \mapsto \mathtt{LeftDualOnMorphisms}(alpha)$$.

 ‣ AddLeftDualOnMorphismsWithGivenLeftDuals( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LeftDualOnMorphismsWithGivenLeftDuals. $$F: ( s, alpha, r ) \mapsto \mathtt{LeftDualOnMorphismsWithGivenLeftDuals}(s, alpha, r)$$.

 ‣ AddLeftDualOnObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LeftDualOnObjects. $$F: ( a ) \mapsto \mathtt{LeftDualOnObjects}(a)$$.

 ‣ AddLeftInternalHomOnMorphisms( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LeftInternalHomOnMorphisms. $$F: ( alpha, beta ) \mapsto \mathtt{LeftInternalHomOnMorphisms}(alpha, beta)$$.

 ‣ AddLeftInternalHomOnMorphismsWithGivenLeftInternalHoms( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LeftInternalHomOnMorphismsWithGivenLeftInternalHoms. $$F: ( s, alpha, beta, r ) \mapsto \mathtt{LeftInternalHomOnMorphismsWithGivenLeftInternalHoms}(s, alpha, beta, r)$$.

 ‣ AddLeftInternalHomOnObjects( C, F ) ( operation )

Returns: nothing

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

 ‣ AddLeftInternalHomToTensorProductAdjunctMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddLeftInternalHomToTensorProductAdjunctMorphismWithGivenTensorProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LeftInternalHomToTensorProductAdjunctMorphismWithGivenTensorProduct. $$F: ( b, c, g, t ) \mapsto \mathtt{LeftInternalHomToTensorProductAdjunctMorphismWithGivenTensorProduct}(b, c, g, t)$$.

 ‣ AddMorphismFromTensorProductToLeftInternalHom( C, F ) ( operation )

Returns: nothing

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

 ‣ AddMorphismFromTensorProductToLeftInternalHomWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation MorphismFromTensorProductToLeftInternalHomWithGivenObjects. $$F: ( s, a, b, r ) \mapsto \mathtt{MorphismFromTensorProductToLeftInternalHomWithGivenObjects}(s, a, b, r)$$.

 ‣ AddMorphismToLeftBidual( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation MorphismToLeftBidual. $$F: ( a ) \mapsto \mathtt{MorphismToLeftBidual}(a)$$.

 ‣ AddMorphismToLeftBidualWithGivenLeftBidual( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation MorphismToLeftBidualWithGivenLeftBidual. $$F: ( a, r ) \mapsto \mathtt{MorphismToLeftBidualWithGivenLeftBidual}(a, r)$$.

 ‣ AddTensorProductLeftDualityCompatibilityMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddTensorProductLeftDualityCompatibilityMorphismWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation TensorProductLeftDualityCompatibilityMorphismWithGivenObjects. $$F: ( s, a, b, r ) \mapsto \mathtt{TensorProductLeftDualityCompatibilityMorphismWithGivenObjects}(s, a, b, r)$$.

 ‣ AddTensorProductLeftInternalHomCompatibilityMorphism( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation TensorProductLeftInternalHomCompatibilityMorphism. $$F: ( list ) \mapsto \mathtt{TensorProductLeftInternalHomCompatibilityMorphism}(list)$$.

 ‣ AddTensorProductLeftInternalHomCompatibilityMorphismWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation TensorProductLeftInternalHomCompatibilityMorphismWithGivenObjects. $$F: ( source, list, range ) \mapsto \mathtt{TensorProductLeftInternalHomCompatibilityMorphismWithGivenObjects}(source, list, range)$$.

 ‣ AddTensorProductToLeftInternalHomAdjunctMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddTensorProductToLeftInternalHomAdjunctMorphismWithGivenLeftInternalHom( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation TensorProductToLeftInternalHomAdjunctMorphismWithGivenLeftInternalHom. $$F: ( a, b, f, i ) \mapsto \mathtt{TensorProductToLeftInternalHomAdjunctMorphismWithGivenLeftInternalHom}(a, b, f, i)$$.

 ‣ AddUniversalPropertyOfLeftDual( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation UniversalPropertyOfLeftDual. $$F: ( t, a, alpha ) \mapsto \mathtt{UniversalPropertyOfLeftDual}(t, a, alpha)$$.

 ‣ AddIsomorphismFromLeftCoDualObjectToLeftInternalCoHomFromTensorUnit( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation IsomorphismFromLeftCoDualObjectToLeftInternalCoHomFromTensorUnit. $$F: ( a ) \mapsto \mathtt{IsomorphismFromLeftCoDualObjectToLeftInternalCoHomFromTensorUnit}(a)$$.

 ‣ AddIsomorphismFromLeftInternalCoHomFromTensorUnitToLeftCoDualObject( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation IsomorphismFromLeftInternalCoHomFromTensorUnitToLeftCoDualObject. $$F: ( a ) \mapsto \mathtt{IsomorphismFromLeftInternalCoHomFromTensorUnitToLeftCoDualObject}(a)$$.

 ‣ AddIsomorphismFromLeftInternalCoHomToObject( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation IsomorphismFromLeftInternalCoHomToObject. $$F: ( a ) \mapsto \mathtt{IsomorphismFromLeftInternalCoHomToObject}(a)$$.

 ‣ AddIsomorphismFromLeftInternalCoHomToObjectWithGivenLeftInternalCoHom( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation IsomorphismFromLeftInternalCoHomToObjectWithGivenLeftInternalCoHom. $$F: ( a, s ) \mapsto \mathtt{IsomorphismFromLeftInternalCoHomToObjectWithGivenLeftInternalCoHom}(a, s)$$.

 ‣ AddIsomorphismFromObjectToLeftInternalCoHom( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation IsomorphismFromObjectToLeftInternalCoHom. $$F: ( a ) \mapsto \mathtt{IsomorphismFromObjectToLeftInternalCoHom}(a)$$.

 ‣ AddIsomorphismFromObjectToLeftInternalCoHomWithGivenLeftInternalCoHom( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation IsomorphismFromObjectToLeftInternalCoHomWithGivenLeftInternalCoHom. $$F: ( a, r ) \mapsto \mathtt{IsomorphismFromObjectToLeftInternalCoHomWithGivenLeftInternalCoHom}(a, r)$$.

 ‣ AddLeftCoDualOnMorphisms( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LeftCoDualOnMorphisms. $$F: ( alpha ) \mapsto \mathtt{LeftCoDualOnMorphisms}(alpha)$$.

 ‣ AddLeftCoDualOnMorphismsWithGivenLeftCoDuals( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LeftCoDualOnMorphismsWithGivenLeftCoDuals. $$F: ( s, alpha, r ) \mapsto \mathtt{LeftCoDualOnMorphismsWithGivenLeftCoDuals}(s, alpha, r)$$.

 ‣ AddLeftCoDualOnObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LeftCoDualOnObjects. $$F: ( a ) \mapsto \mathtt{LeftCoDualOnObjects}(a)$$.

 ‣ AddLeftCoDualityTensorProductCompatibilityMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddLeftCoDualityTensorProductCompatibilityMorphismWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LeftCoDualityTensorProductCompatibilityMorphismWithGivenObjects. $$F: ( s, a, b, r ) \mapsto \mathtt{LeftCoDualityTensorProductCompatibilityMorphismWithGivenObjects}(s, a, b, r)$$.

 ‣ AddLeftCoclosedMonoidalCoevaluationMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddLeftCoclosedMonoidalCoevaluationMorphismWithGivenSource( C, F ) ( operation )

Returns: nothing

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

 ‣ AddLeftCoclosedMonoidalEvaluationForLeftCoDual( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LeftCoclosedMonoidalEvaluationForLeftCoDual. $$F: ( a ) \mapsto \mathtt{LeftCoclosedMonoidalEvaluationForLeftCoDual}(a)$$.

 ‣ AddLeftCoclosedMonoidalEvaluationForLeftCoDualWithGivenTensorProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LeftCoclosedMonoidalEvaluationForLeftCoDualWithGivenTensorProduct. $$F: ( s, a, r ) \mapsto \mathtt{LeftCoclosedMonoidalEvaluationForLeftCoDualWithGivenTensorProduct}(s, a, r)$$.

 ‣ AddLeftCoclosedMonoidalEvaluationMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddLeftCoclosedMonoidalEvaluationMorphismWithGivenRange( C, F ) ( operation )

Returns: nothing

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

 ‣ AddLeftCoclosedMonoidalLambdaElimination( C, F ) ( operation )

Returns: nothing

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

 ‣ AddLeftCoclosedMonoidalLambdaIntroduction( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LeftCoclosedMonoidalLambdaIntroduction. $$F: ( alpha ) \mapsto \mathtt{LeftCoclosedMonoidalLambdaIntroduction}(alpha)$$.

 ‣ AddLeftCoclosedMonoidalPostCoComposeMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddLeftCoclosedMonoidalPostCoComposeMorphismWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LeftCoclosedMonoidalPostCoComposeMorphismWithGivenObjects. $$F: ( s, a, b, c, r ) \mapsto \mathtt{LeftCoclosedMonoidalPostCoComposeMorphismWithGivenObjects}(s, a, b, c, r)$$.

 ‣ AddLeftCoclosedMonoidalPreCoComposeMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddLeftCoclosedMonoidalPreCoComposeMorphismWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LeftCoclosedMonoidalPreCoComposeMorphismWithGivenObjects. $$F: ( s, a, b, c, r ) \mapsto \mathtt{LeftCoclosedMonoidalPreCoComposeMorphismWithGivenObjects}(s, a, b, c, r)$$.

 ‣ AddLeftInternalCoHomOnMorphisms( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LeftInternalCoHomOnMorphisms. $$F: ( alpha, beta ) \mapsto \mathtt{LeftInternalCoHomOnMorphisms}(alpha, beta)$$.

 ‣ AddLeftInternalCoHomOnMorphismsWithGivenLeftInternalCoHoms( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LeftInternalCoHomOnMorphismsWithGivenLeftInternalCoHoms. $$F: ( s, alpha, beta, r ) \mapsto \mathtt{LeftInternalCoHomOnMorphismsWithGivenLeftInternalCoHoms}(s, alpha, beta, r)$$.

 ‣ AddLeftInternalCoHomOnObjects( C, F ) ( operation )

Returns: nothing

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

 ‣ AddLeftInternalCoHomTensorProductCompatibilityMorphism( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LeftInternalCoHomTensorProductCompatibilityMorphism. $$F: ( list ) \mapsto \mathtt{LeftInternalCoHomTensorProductCompatibilityMorphism}(list)$$.

 ‣ AddLeftInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LeftInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects. $$F: ( source, list, range ) \mapsto \mathtt{LeftInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects}(source, list, range)$$.

 ‣ AddLeftInternalCoHomToTensorProductAdjunctMorphism( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LeftInternalCoHomToTensorProductAdjunctMorphism. $$F: ( a, c, f ) \mapsto \mathtt{LeftInternalCoHomToTensorProductAdjunctMorphism}(a, c, f)$$.

 ‣ AddLeftInternalCoHomToTensorProductAdjunctMorphismWithGivenTensorProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LeftInternalCoHomToTensorProductAdjunctMorphismWithGivenTensorProduct. $$F: ( a, c, f, t ) \mapsto \mathtt{LeftInternalCoHomToTensorProductAdjunctMorphismWithGivenTensorProduct}(a, c, f, t)$$.

 ‣ AddMorphismFromLeftCoBidual( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation MorphismFromLeftCoBidual. $$F: ( a ) \mapsto \mathtt{MorphismFromLeftCoBidual}(a)$$.

 ‣ AddMorphismFromLeftCoBidualWithGivenLeftCoBidual( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation MorphismFromLeftCoBidualWithGivenLeftCoBidual. $$F: ( a, s ) \mapsto \mathtt{MorphismFromLeftCoBidualWithGivenLeftCoBidual}(a, s)$$.

 ‣ AddMorphismFromLeftInternalCoHomToTensorProduct( C, F ) ( operation )

Returns: nothing

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

 ‣ AddMorphismFromLeftInternalCoHomToTensorProductWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation MorphismFromLeftInternalCoHomToTensorProductWithGivenObjects. $$F: ( s, a, b, r ) \mapsto \mathtt{MorphismFromLeftInternalCoHomToTensorProductWithGivenObjects}(s, a, b, r)$$.

 ‣ AddTensorProductToLeftInternalCoHomAdjunctMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddTensorProductToLeftInternalCoHomAdjunctMorphismWithGivenLeftInternalCoHom( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation TensorProductToLeftInternalCoHomAdjunctMorphismWithGivenLeftInternalCoHom. $$F: ( b, c, g, i ) \mapsto \mathtt{TensorProductToLeftInternalCoHomAdjunctMorphismWithGivenLeftInternalCoHom}(b, c, g, i)$$.

 ‣ AddUniversalPropertyOfLeftCoDual( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation UniversalPropertyOfLeftCoDual. $$F: ( t, a, alpha ) \mapsto \mathtt{UniversalPropertyOfLeftCoDual}(t, a, alpha)$$.

 ‣ AddAssociatorLeftToRight( C, F ) ( operation )

Returns: nothing

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

 ‣ AddAssociatorLeftToRightWithGivenTensorProducts( C, F ) ( operation )

Returns: nothing

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

 ‣ AddAssociatorRightToLeft( C, F ) ( operation )

Returns: nothing

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

 ‣ AddAssociatorRightToLeftWithGivenTensorProducts( C, F ) ( operation )

Returns: nothing

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

 ‣ AddLeftUnitor( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LeftUnitor. $$F: ( a ) \mapsto \mathtt{LeftUnitor}(a)$$.

 ‣ AddLeftUnitorInverse( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LeftUnitorInverse. $$F: ( a ) \mapsto \mathtt{LeftUnitorInverse}(a)$$.

 ‣ AddLeftUnitorInverseWithGivenTensorProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LeftUnitorInverseWithGivenTensorProduct. $$F: ( a, r ) \mapsto \mathtt{LeftUnitorInverseWithGivenTensorProduct}(a, r)$$.

 ‣ AddLeftUnitorWithGivenTensorProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation LeftUnitorWithGivenTensorProduct. $$F: ( a, s ) \mapsto \mathtt{LeftUnitorWithGivenTensorProduct}(a, s)$$.

 ‣ AddRightUnitor( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation RightUnitor. $$F: ( a ) \mapsto \mathtt{RightUnitor}(a)$$.

 ‣ AddRightUnitorInverse( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation RightUnitorInverse. $$F: ( a ) \mapsto \mathtt{RightUnitorInverse}(a)$$.

 ‣ AddRightUnitorInverseWithGivenTensorProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation RightUnitorInverseWithGivenTensorProduct. $$F: ( a, r ) \mapsto \mathtt{RightUnitorInverseWithGivenTensorProduct}(a, r)$$.

 ‣ AddRightUnitorWithGivenTensorProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation RightUnitorWithGivenTensorProduct. $$F: ( a, s ) \mapsto \mathtt{RightUnitorWithGivenTensorProduct}(a, s)$$.

 ‣ AddTensorProductOnMorphisms( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation TensorProductOnMorphisms. $$F: ( alpha, beta ) \mapsto \mathtt{TensorProductOnMorphisms}(alpha, beta)$$.

 ‣ AddTensorProductOnMorphismsWithGivenTensorProducts( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation TensorProductOnMorphismsWithGivenTensorProducts. $$F: ( s, alpha, beta, r ) \mapsto \mathtt{TensorProductOnMorphismsWithGivenTensorProducts}(s, alpha, beta, r)$$.

 ‣ AddCoevaluationForDual( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation CoevaluationForDual. $$F: ( a ) \mapsto \mathtt{CoevaluationForDual}(a)$$.

 ‣ AddCoevaluationForDualWithGivenTensorProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation CoevaluationForDualWithGivenTensorProduct. $$F: ( s, a, r ) \mapsto \mathtt{CoevaluationForDualWithGivenTensorProduct}(s, a, r)$$.

 ‣ AddIsomorphismFromInternalHomToTensorProductWithDualObject( C, F ) ( operation )

Returns: nothing

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

 ‣ AddIsomorphismFromTensorProductWithDualObjectToInternalHom( C, F ) ( operation )

Returns: nothing

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

 ‣ AddMorphismFromBidual( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation MorphismFromBidual. $$F: ( a ) \mapsto \mathtt{MorphismFromBidual}(a)$$.

 ‣ AddMorphismFromBidualWithGivenBidual( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation MorphismFromBidualWithGivenBidual. $$F: ( a, s ) \mapsto \mathtt{MorphismFromBidualWithGivenBidual}(a, s)$$.

 ‣ AddMorphismFromInternalHomToTensorProduct( C, F ) ( operation )

Returns: nothing

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

 ‣ AddMorphismFromInternalHomToTensorProductWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation MorphismFromInternalHomToTensorProductWithGivenObjects. $$F: ( s, a, b, r ) \mapsto \mathtt{MorphismFromInternalHomToTensorProductWithGivenObjects}(s, a, b, r)$$.

 ‣ AddRankMorphism( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation RankMorphism. $$F: ( a ) \mapsto \mathtt{RankMorphism}(a)$$.

 ‣ AddTensorProductInternalHomCompatibilityMorphismInverse( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation TensorProductInternalHomCompatibilityMorphismInverse. $$F: ( list ) \mapsto \mathtt{TensorProductInternalHomCompatibilityMorphismInverse}(list)$$.

 ‣ AddTensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation TensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects. $$F: ( source, list, range ) \mapsto \mathtt{TensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects}(source, list, range)$$.

 ‣ AddTraceMap( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation TraceMap. $$F: ( alpha ) \mapsto \mathtt{TraceMap}(alpha)$$.

 ‣ AddCoRankMorphism( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation CoRankMorphism. $$F: ( a ) \mapsto \mathtt{CoRankMorphism}(a)$$.

 ‣ AddCoTraceMap( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation CoTraceMap. $$F: ( alpha ) \mapsto \mathtt{CoTraceMap}(alpha)$$.

 ‣ AddCoclosedCoevaluationForCoDual( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation CoclosedCoevaluationForCoDual. $$F: ( a ) \mapsto \mathtt{CoclosedCoevaluationForCoDual}(a)$$.

 ‣ AddCoclosedCoevaluationForCoDualWithGivenTensorProduct( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation CoclosedCoevaluationForCoDualWithGivenTensorProduct. $$F: ( s, a, r ) \mapsto \mathtt{CoclosedCoevaluationForCoDualWithGivenTensorProduct}(s, a, r)$$.

 ‣ AddInternalCoHomTensorProductCompatibilityMorphismInverse( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation InternalCoHomTensorProductCompatibilityMorphismInverse. $$F: ( list ) \mapsto \mathtt{InternalCoHomTensorProductCompatibilityMorphismInverse}(list)$$.

 ‣ AddInternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation InternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects. $$F: ( source, list, range ) \mapsto \mathtt{InternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects}(source, list, range)$$.

 ‣ AddIsomorphismFromInternalCoHomToTensorProductWithCoDualObject( C, F ) ( operation )

Returns: nothing

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

 ‣ AddIsomorphismFromTensorProductWithCoDualObjectToInternalCoHom( C, F ) ( operation )

Returns: nothing

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

 ‣ AddMorphismFromTensorProductToInternalCoHom( C, F ) ( operation )

Returns: nothing

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

 ‣ AddMorphismFromTensorProductToInternalCoHomWithGivenObjects( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation MorphismFromTensorProductToInternalCoHomWithGivenObjects. $$F: ( s, a, b, r ) \mapsto \mathtt{MorphismFromTensorProductToInternalCoHomWithGivenObjects}(s, a, b, r)$$.

 ‣ AddMorphismToCoBidual( C, F ) ( operation )

Returns: nothing

The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation MorphismToCoBidual. $$F: ( a ) \mapsto \mathtt{MorphismToCoBidual}(a)$$.

 ‣ AddMorphismToCoBidualWithGivenCoBidual( C, F ) ( operation )
The arguments are a category $$C$$ and a function $$F$$. This operation adds the given function $$F$$ to the category for the basic operation MorphismToCoBidualWithGivenCoBidual. $$F: ( a, r ) \mapsto \mathtt{MorphismToCoBidualWithGivenCoBidual}(a, r)$$.