Goto Chapter: Top 1 2 3 4 5 Ind
 [Top of Book]  [Contents]   [Previous Chapter]   [Next Chapter] 

1 Monoidal Categories
 1.1 Monoidal Categories
 1.2 Additive Monoidal Categories
 1.3 Braided Monoidal Categories
 1.4 Symmetric Monoidal Categories
 1.5 Closed Monoidal Categories

  1.5-1 InternalHomOnObjects

  1.5-2 InternalHomOnMorphisms

  1.5-3 InternalHomOnMorphismsWithGivenInternalHoms

  1.5-4 EvaluationMorphism

  1.5-5 EvaluationMorphismWithGivenSource

  1.5-6 CoevaluationMorphism

  1.5-7 CoevaluationMorphismWithGivenRange

  1.5-8 TensorProductToInternalHomAdjunctionMap

  1.5-9 TensorProductToInternalHomAdjunctionMapWithGivenInternalHom

  1.5-10 InternalHomToTensorProductAdjunctionMap

  1.5-11 InternalHomToTensorProductAdjunctionMapWithGivenTensorProduct

  1.5-12 MonoidalPreComposeMorphism

  1.5-13 MonoidalPreComposeMorphismWithGivenObjects

  1.5-14 MonoidalPostComposeMorphism

  1.5-15 MonoidalPostComposeMorphismWithGivenObjects

  1.5-16 DualOnObjects

  1.5-17 DualOnMorphisms

  1.5-18 DualOnMorphismsWithGivenDuals

  1.5-19 EvaluationForDual

  1.5-20 EvaluationForDualWithGivenTensorProduct

  1.5-21 MorphismToBidual

  1.5-22 MorphismToBidualWithGivenBidual

  1.5-23 TensorProductInternalHomCompatibilityMorphism

  1.5-24 TensorProductInternalHomCompatibilityMorphismWithGivenObjects

  1.5-25 TensorProductDualityCompatibilityMorphism

  1.5-26 TensorProductDualityCompatibilityMorphismWithGivenObjects

  1.5-27 MorphismFromTensorProductToInternalHom

  1.5-28 MorphismFromTensorProductToInternalHomWithGivenObjects

  1.5-29 IsomorphismFromDualObjectToInternalHomIntoTensorUnit

  1.5-30 IsomorphismFromInternalHomIntoTensorUnitToDualObject

  1.5-31 UniversalPropertyOfDual

  1.5-32 LambdaIntroduction

  1.5-33 LambdaElimination

  1.5-34 IsomorphismFromObjectToInternalHom

  1.5-35 IsomorphismFromObjectToInternalHomWithGivenInternalHom

  1.5-36 IsomorphismFromInternalHomToObject

  1.5-37 IsomorphismFromInternalHomToObjectWithGivenInternalHom
 1.6 Coclosed Monoidal Categories

  1.6-1 InternalCoHomOnObjects

  1.6-2 InternalCoHomOnMorphisms

  1.6-3 InternalCoHomOnMorphismsWithGivenInternalCoHoms

  1.6-4 CoclosedEvaluationMorphism

  1.6-5 CoclosedEvaluationMorphismWithGivenRange

  1.6-6 CoclosedCoevaluationMorphism

  1.6-7 CoclosedCoevaluationMorphismWithGivenSource

  1.6-8 TensorProductToInternalCoHomAdjunctionMap

  1.6-9 TensorProductToInternalCoHomAdjunctionMapWithGivenInternalCoHom

  1.6-10 InternalCoHomToTensorProductAdjunctionMap

  1.6-11 InternalCoHomToTensorProductAdjunctionMapWithGivenTensorProduct

  1.6-12 MonoidalPreCoComposeMorphism

  1.6-13 MonoidalPreCoComposeMorphismWithGivenObjects

  1.6-14 MonoidalPostCoComposeMorphism

  1.6-15 MonoidalPostCoComposeMorphismWithGivenObjects

  1.6-16 CoDualOnObjects

  1.6-17 CoDualOnMorphisms

  1.6-18 CoDualOnMorphismsWithGivenCoDuals

  1.6-19 CoclosedEvaluationForCoDual

  1.6-20 CoclosedEvaluationForCoDualWithGivenTensorProduct

  1.6-21 MorphismFromCoBidual

  1.6-22 MorphismFromCoBidualWithGivenCoBidual

  1.6-23 InternalCoHomTensorProductCompatibilityMorphism

  1.6-24 InternalCoHomTensorProductCompatibilityMorphismWithGivenObjects

  1.6-25 CoDualityTensorProductCompatibilityMorphism

  1.6-26 CoDualityTensorProductCompatibilityMorphismWithGivenObjects

  1.6-27 MorphismFromInternalCoHomToTensorProduct

  1.6-28 MorphismFromInternalCoHomToTensorProductWithGivenObjects

  1.6-29 IsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit

  1.6-30 IsomorphismFromInternalCoHomFromTensorUnitToCoDualObject

  1.6-31 UniversalPropertyOfCoDual

  1.6-32 CoLambdaIntroduction

  1.6-33 CoLambdaElimination

  1.6-34 IsomorphismFromObjectToInternalCoHom

  1.6-35 IsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom

  1.6-36 IsomorphismFromInternalCoHomToObject

  1.6-37 IsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom
 1.7 Symmetric Closed Monoidal Categories
 1.8 Symmetric Coclosed Monoidal Categories
 1.9 Rigid Symmetric Closed Monoidal Categories
 1.10 Rigid Symmetric Coclosed Monoidal Categories
 1.11 Convenience Methods
 1.12 Add-methods

  1.12-1 AddLeftDistributivityExpanding

  1.12-2 AddLeftDistributivityExpandingWithGivenObjects

  1.12-3 AddLeftDistributivityFactoring

  1.12-4 AddLeftDistributivityFactoringWithGivenObjects

  1.12-5 AddRightDistributivityExpanding

  1.12-6 AddRightDistributivityExpandingWithGivenObjects

  1.12-7 AddRightDistributivityFactoring

  1.12-8 AddRightDistributivityFactoringWithGivenObjects

  1.12-9 AddBraiding

  1.12-10 AddBraidingInverse

  1.12-11 AddBraidingInverseWithGivenTensorProducts

  1.12-12 AddBraidingWithGivenTensorProducts

  1.12-13 AddCoevaluationMorphism

  1.12-14 AddCoevaluationMorphismWithGivenRange

  1.12-15 AddDualOnMorphisms

  1.12-16 AddDualOnMorphismsWithGivenDuals

  1.12-17 AddDualOnObjects

  1.12-18 AddEvaluationForDual

  1.12-19 AddEvaluationForDualWithGivenTensorProduct

  1.12-20 AddEvaluationMorphism

  1.12-21 AddEvaluationMorphismWithGivenSource

  1.12-22 AddInternalHomOnMorphisms

  1.12-23 AddInternalHomOnMorphismsWithGivenInternalHoms

  1.12-24 AddInternalHomOnObjects

  1.12-25 AddInternalHomToTensorProductAdjunctionMap

  1.12-26 AddInternalHomToTensorProductAdjunctionMapWithGivenTensorProduct

  1.12-27 AddIsomorphismFromDualObjectToInternalHomIntoTensorUnit

  1.12-28 AddIsomorphismFromInternalHomIntoTensorUnitToDualObject

  1.12-29 AddIsomorphismFromInternalHomToObject

  1.12-30 AddIsomorphismFromInternalHomToObjectWithGivenInternalHom

  1.12-31 AddIsomorphismFromObjectToInternalHom

  1.12-32 AddIsomorphismFromObjectToInternalHomWithGivenInternalHom

  1.12-33 AddLambdaElimination

  1.12-34 AddLambdaIntroduction

  1.12-35 AddMonoidalPostComposeMorphism

  1.12-36 AddMonoidalPostComposeMorphismWithGivenObjects

  1.12-37 AddMonoidalPreComposeMorphism

  1.12-38 AddMonoidalPreComposeMorphismWithGivenObjects

  1.12-39 AddMorphismFromTensorProductToInternalHom

  1.12-40 AddMorphismFromTensorProductToInternalHomWithGivenObjects

  1.12-41 AddMorphismToBidual

  1.12-42 AddMorphismToBidualWithGivenBidual

  1.12-43 AddTensorProductDualityCompatibilityMorphism

  1.12-44 AddTensorProductDualityCompatibilityMorphismWithGivenObjects

  1.12-45 AddTensorProductInternalHomCompatibilityMorphism

  1.12-46 AddTensorProductInternalHomCompatibilityMorphismWithGivenObjects

  1.12-47 AddTensorProductToInternalHomAdjunctionMap

  1.12-48 AddTensorProductToInternalHomAdjunctionMapWithGivenInternalHom

  1.12-49 AddUniversalPropertyOfDual

  1.12-50 AddCoDualOnMorphisms

  1.12-51 AddCoDualOnMorphismsWithGivenCoDuals

  1.12-52 AddCoDualOnObjects

  1.12-53 AddCoDualityTensorProductCompatibilityMorphism

  1.12-54 AddCoDualityTensorProductCompatibilityMorphismWithGivenObjects

  1.12-55 AddCoLambdaElimination

  1.12-56 AddCoLambdaIntroduction

  1.12-57 AddCoclosedCoevaluationMorphism

  1.12-58 AddCoclosedCoevaluationMorphismWithGivenSource

  1.12-59 AddCoclosedEvaluationForCoDual

  1.12-60 AddCoclosedEvaluationForCoDualWithGivenTensorProduct

  1.12-61 AddCoclosedEvaluationMorphism

  1.12-62 AddCoclosedEvaluationMorphismWithGivenRange

  1.12-63 AddInternalCoHomOnMorphisms

  1.12-64 AddInternalCoHomOnMorphismsWithGivenInternalCoHoms

  1.12-65 AddInternalCoHomOnObjects

  1.12-66 AddInternalCoHomTensorProductCompatibilityMorphism

  1.12-67 AddInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects

  1.12-68 AddInternalCoHomToTensorProductAdjunctionMap

  1.12-69 AddInternalCoHomToTensorProductAdjunctionMapWithGivenTensorProduct

  1.12-70 AddIsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit

  1.12-71 AddIsomorphismFromInternalCoHomFromTensorUnitToCoDualObject

  1.12-72 AddIsomorphismFromInternalCoHomToObject

  1.12-73 AddIsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom

  1.12-74 AddIsomorphismFromObjectToInternalCoHom

  1.12-75 AddIsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom

  1.12-76 AddMonoidalPostCoComposeMorphism

  1.12-77 AddMonoidalPostCoComposeMorphismWithGivenObjects

  1.12-78 AddMonoidalPreCoComposeMorphism

  1.12-79 AddMonoidalPreCoComposeMorphismWithGivenObjects

  1.12-80 AddMorphismFromCoBidual

  1.12-81 AddMorphismFromCoBidualWithGivenCoBidual

  1.12-82 AddMorphismFromInternalCoHomToTensorProduct

  1.12-83 AddMorphismFromInternalCoHomToTensorProductWithGivenObjects

  1.12-84 AddTensorProductToInternalCoHomAdjunctionMap

  1.12-85 AddTensorProductToInternalCoHomAdjunctionMapWithGivenInternalCoHom

  1.12-86 AddUniversalPropertyOfCoDual

  1.12-87 AddAssociatorLeftToRight

  1.12-88 AddAssociatorLeftToRightWithGivenTensorProducts

  1.12-89 AddAssociatorRightToLeft

  1.12-90 AddAssociatorRightToLeftWithGivenTensorProducts

  1.12-91 AddLeftUnitor

  1.12-92 AddLeftUnitorInverse

  1.12-93 AddLeftUnitorInverseWithGivenTensorProduct

  1.12-94 AddLeftUnitorWithGivenTensorProduct

  1.12-95 AddRightUnitor

  1.12-96 AddRightUnitorInverse

  1.12-97 AddRightUnitorInverseWithGivenTensorProduct

  1.12-98 AddRightUnitorWithGivenTensorProduct

  1.12-99 AddTensorProductOnMorphisms

  1.12-100 AddTensorProductOnMorphismsWithGivenTensorProducts

  1.12-101 AddCoevaluationForDual

  1.12-102 AddCoevaluationForDualWithGivenTensorProduct

  1.12-103 AddIsomorphismFromInternalHomToTensorProductWithDualObject

  1.12-104 AddIsomorphismFromTensorProductWithDualObjectToInternalHom

  1.12-105 AddMorphismFromBidual

  1.12-106 AddMorphismFromBidualWithGivenBidual

  1.12-107 AddMorphismFromInternalHomToTensorProduct

  1.12-108 AddMorphismFromInternalHomToTensorProductWithGivenObjects

  1.12-109 AddRankMorphism

  1.12-110 AddTensorProductInternalHomCompatibilityMorphismInverse

  1.12-111 AddTensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects

  1.12-112 AddTraceMap

  1.12-113 AddCoRankMorphism

  1.12-114 AddCoTraceMap

  1.12-115 AddCoclosedCoevaluationForCoDual

  1.12-116 AddCoclosedCoevaluationForCoDualWithGivenTensorProduct

  1.12-117 AddInternalCoHomTensorProductCompatibilityMorphismInverse

  1.12-118 AddInternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects

  1.12-119 AddIsomorphismFromInternalCoHomToTensorProductWithCoDualObject

  1.12-120 AddIsomorphismFromTensorProductWithCoDualObjectToInternalCoHom

  1.12-121 AddMorphismFromTensorProductToInternalCoHom

  1.12-122 AddMorphismFromTensorProductToInternalCoHomWithGivenObjects

  1.12-123 AddMorphismToCoBidual

  1.12-124 AddMorphismToCoBidualWithGivenCoBidual

1 Monoidal Categories

1.1 Monoidal Categories

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

is called a monoidal category, if

\((\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}\),

\(( \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\).

1.1-16 AddTensorProductOnObjects
‣ 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}\).

1.1-18 AddTensorUnit
‣ 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 Additive Monoidal Categories

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

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 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}}(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}}(a,1)\).

The corresponding GAP property is called IsClosedMonoidalCategory.

1.5-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.5-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.5-3 InternalHomOnMorphismsWithGivenInternalHoms
‣ InternalHomOnMorphismsWithGivenInternalHoms( s, alpha, beta, r )( operation )

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

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

1.5-4 EvaluationMorphism
‣ EvaluationMorphism( a, b )( operation )

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

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

1.5-5 EvaluationMorphismWithGivenSource
‣ EvaluationMorphismWithGivenSource( a, b, s )( operation )

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

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

1.5-6 CoevaluationMorphism
‣ CoevaluationMorphism( a, b )( operation )

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

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

1.5-7 CoevaluationMorphismWithGivenRange
‣ CoevaluationMorphismWithGivenRange( a, b, r )( operation )

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

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

1.5-8 TensorProductToInternalHomAdjunctionMap
‣ TensorProductToInternalHomAdjunctionMap( 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.

1.5-9 TensorProductToInternalHomAdjunctionMapWithGivenInternalHom
‣ TensorProductToInternalHomAdjunctionMapWithGivenInternalHom( a, b, f, i )( operation )

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

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.

1.5-10 InternalHomToTensorProductAdjunctionMap
‣ InternalHomToTensorProductAdjunctionMap( 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.

1.5-11 InternalHomToTensorProductAdjunctionMapWithGivenTensorProduct
‣ InternalHomToTensorProductAdjunctionMapWithGivenTensorProduct( b, c, g, t )( operation )

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

The arguments are two objects \(b,c\), a morphism \(g: a \rightarrow \mathrm{\underline{Hom}}(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 MonoidalPreComposeMorphism
‣ MonoidalPreComposeMorphism( a, b, c )( operation )

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

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

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

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

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

1.5-14 MonoidalPostComposeMorphism
‣ MonoidalPostComposeMorphism( a, b, c )( operation )

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

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

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

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

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

1.5-16 DualOnObjects
‣ DualOnObjects( a )( attribute )

Returns: an object

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

1.5-17 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.5-18 DualOnMorphismsWithGivenDuals
‣ DualOnMorphismsWithGivenDuals( s, alpha, r )( operation )

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

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

1.5-19 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.5-20 EvaluationForDualWithGivenTensorProduct
‣ EvaluationForDualWithGivenTensorProduct( s, a, r )( operation )

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

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

1.5-21 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.5-22 MorphismToBidualWithGivenBidual
‣ MorphismToBidualWithGivenBidual( a, r )( operation )

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

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

1.5-23 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{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.5-24 TensorProductInternalHomCompatibilityMorphismWithGivenObjects
‣ TensorProductInternalHomCompatibilityMorphismWithGivenObjects( s, list, r )( operation )

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

The arguments are 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.5-25 TensorProductDualityCompatibilityMorphism
‣ TensorProductDualityCompatibilityMorphism( a, b )( operation )

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

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

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

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

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

1.5-27 MorphismFromTensorProductToInternalHom
‣ MorphismFromTensorProductToInternalHom( a, b )( operation )

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

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

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

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

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

1.5-29 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.5-30 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.5-31 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.5-32 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.5-33 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.5-34 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.5-35 IsomorphismFromObjectToInternalHomWithGivenInternalHom
‣ IsomorphismFromObjectToInternalHomWithGivenInternalHom( a, r )( operation )

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

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

1.5-36 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.5-37 IsomorphismFromInternalHomToObjectWithGivenInternalHom
‣ IsomorphismFromInternalHomToObjectWithGivenInternalHom( a, s )( operation )

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

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

1.6 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.6-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.6-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.6-3 InternalCoHomOnMorphismsWithGivenInternalCoHoms
‣ InternalCoHomOnMorphismsWithGivenInternalCoHoms( s, alpha, beta, r )( operation )

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

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.6-4 CoclosedEvaluationMorphism
‣ CoclosedEvaluationMorphism( a, b )( operation )

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

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

1.6-5 CoclosedEvaluationMorphismWithGivenRange
‣ CoclosedEvaluationMorphismWithGivenRange( a, b, r )( operation )

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

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

1.6-6 CoclosedCoevaluationMorphism
‣ CoclosedCoevaluationMorphism( a, b )( operation )

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

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

1.6-7 CoclosedCoevaluationMorphismWithGivenSource
‣ CoclosedCoevaluationMorphismWithGivenSource( a, b, s )( operation )

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

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

1.6-8 TensorProductToInternalCoHomAdjunctionMap
‣ TensorProductToInternalCoHomAdjunctionMap( c, b, g )( operation )

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

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

1.6-9 TensorProductToInternalCoHomAdjunctionMapWithGivenInternalCoHom
‣ TensorProductToInternalCoHomAdjunctionMapWithGivenInternalCoHom( c, b, g, i )( operation )

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

The arguments are two objects \(c,b\), a morphism \(g: a \rightarrow c \otimes b\) 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.

1.6-10 InternalCoHomToTensorProductAdjunctionMap
‣ InternalCoHomToTensorProductAdjunctionMap( a, b, f )( operation )

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

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 c \otimes b\) corresponding to \(f\) under the cohom tensor adjunction.

1.6-11 InternalCoHomToTensorProductAdjunctionMapWithGivenTensorProduct
‣ InternalCoHomToTensorProductAdjunctionMapWithGivenTensorProduct( a, b, f, t )( operation )

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

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

1.6-12 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{MonoidalPreCoComposeMorphismWithGivenObjects}_{a,b,c}: \mathrm{\underline{coHom}}(a,c) \rightarrow \mathrm{\underline{coHom}}(b,c) \otimes \mathrm{\underline{coHom}}(a,b)\).

1.6-13 MonoidalPreCoComposeMorphismWithGivenObjects
‣ MonoidalPreCoComposeMorphismWithGivenObjects( s, a, b, c, r )( 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 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.6-14 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{MonoidalPostCoComposeMorphismWithGivenObjects}_{a,b,c}: \mathrm{\underline{coHom}}(a,c) \rightarrow \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(b,c)\).

1.6-15 MonoidalPostCoComposeMorphismWithGivenObjects
‣ MonoidalPostCoComposeMorphismWithGivenObjects( s, a, b, c, r )( 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 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.6-16 CoDualOnObjects
‣ CoDualOnObjects( a )( attribute )

Returns: an object

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

1.6-17 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.6-18 CoDualOnMorphismsWithGivenCoDuals
‣ CoDualOnMorphismsWithGivenCoDuals( s, alpha, r )( operation )

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

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

1.6-19 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.6-20 CoclosedEvaluationForCoDualWithGivenTensorProduct
‣ CoclosedEvaluationForCoDualWithGivenTensorProduct( s, a, r )( operation )

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

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.6-21 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.6-22 MorphismFromCoBidualWithGivenCoBidual
‣ MorphismFromCoBidualWithGivenCoBidual( a, s )( operation )

Returns: a morphism in \(\mathrm{Hom}((a_{\vee})_{\vee}, 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.6-23 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{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.6-24 InternalCoHomTensorProductCompatibilityMorphismWithGivenObjects
‣ InternalCoHomTensorProductCompatibilityMorphismWithGivenObjects( s, list, r )( 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 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.6-25 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{CoDualityTensorProductCompatibilityMorphismWithGivenObjects}: (a \otimes b)_{\vee} \rightarrow a_{\vee} \otimes b_{\vee}\).

1.6-26 CoDualityTensorProductCompatibilityMorphismWithGivenObjects
‣ CoDualityTensorProductCompatibilityMorphismWithGivenObjects( s, a, b, r )( operation )

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

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.6-27 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{MorphismFromInternalCoHomToTensorProductWithGivenObjects}_{a,b}: \mathrm{\underline{coHom}}(a,b) \rightarrow b_{\vee} \otimes a\).

1.6-28 MorphismFromInternalCoHomToTensorProductWithGivenObjects
‣ MorphismFromInternalCoHomToTensorProductWithGivenObjects( s, a, b, r )( operation )

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

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.6-29 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.6-30 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.6-31 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.6-32 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.6-33 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.6-34 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.6-35 IsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom
‣ IsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom( a, r )( operation )

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

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.6-36 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.6-37 IsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom
‣ IsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom( a, s )( operation )

Returns: a morphism in \(\mathrm{Hom}(\mathrm{\underline{coHom}}(a,1), 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.7 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.8 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.9 Rigid Symmetric Closed Monoidal Categories

A symmetric closed monoidal category \(\mathbf{C}\) satisfying

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

\(a \rightarrow \mathrm{\underline{Hom}}(\mathrm{\underline{Hom}}(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}}(a,b) \coloneqq a^\vee \otimes b\) and, in particular, \(\mathrm{\underline{Hom}}(a,1) \coloneqq a^\vee \otimes 1\).

The corresponding GAP property is given by IsRigidSymmetricClosedMonoidalCategory.

1.9-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.9-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.9-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.9-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.9-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.9-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.9-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.9-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.9-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.9-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.9-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.9-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.10 Rigid Symmetric Coclosed Monoidal Categories

A symmetric coclosed monoidal category \(\mathbf{C}\) satisfying

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

\(\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.10-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.10-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.10-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.10-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.10-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.10-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.10-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.10-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.10-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.10-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.10-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.10-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.11 Convenience Methods

1.11-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.11-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.12 Add-methods

1.12-1 AddLeftDistributivityExpanding
‣ 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)\).

1.12-2 AddLeftDistributivityExpandingWithGivenObjects
‣ 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)\).

1.12-3 AddLeftDistributivityFactoring
‣ 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)\).

1.12-4 AddLeftDistributivityFactoringWithGivenObjects
‣ 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)\).

1.12-5 AddRightDistributivityExpanding
‣ 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)\).

1.12-6 AddRightDistributivityExpandingWithGivenObjects
‣ 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)\).

1.12-7 AddRightDistributivityFactoring
‣ 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)\).

1.12-8 AddRightDistributivityFactoringWithGivenObjects
‣ 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)\).

1.12-9 AddBraiding
‣ 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)\).

1.12-10 AddBraidingInverse
‣ 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)\).

1.12-11 AddBraidingInverseWithGivenTensorProducts
‣ 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)\).

1.12-12 AddBraidingWithGivenTensorProducts
‣ 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)\).

1.12-13 AddCoevaluationMorphism
‣ AddCoevaluationMorphism( 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 CoevaluationMorphism. \(F: ( a, b ) \mapsto \mathtt{CoevaluationMorphism}(a, b)\).

1.12-14 AddCoevaluationMorphismWithGivenRange
‣ AddCoevaluationMorphismWithGivenRange( 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 CoevaluationMorphismWithGivenRange. \(F: ( a, b, r ) \mapsto \mathtt{CoevaluationMorphismWithGivenRange}(a, b, r)\).

1.12-15 AddDualOnMorphisms
‣ 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)\).

1.12-16 AddDualOnMorphismsWithGivenDuals
‣ 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)\).

1.12-17 AddDualOnObjects
‣ 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)\).

1.12-18 AddEvaluationForDual
‣ 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)\).

1.12-19 AddEvaluationForDualWithGivenTensorProduct
‣ 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)\).

1.12-20 AddEvaluationMorphism
‣ AddEvaluationMorphism( 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 EvaluationMorphism. \(F: ( a, b ) \mapsto \mathtt{EvaluationMorphism}(a, b)\).

1.12-21 AddEvaluationMorphismWithGivenSource
‣ AddEvaluationMorphismWithGivenSource( 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 EvaluationMorphismWithGivenSource. \(F: ( a, b, s ) \mapsto \mathtt{EvaluationMorphismWithGivenSource}(a, b, s)\).

1.12-22 AddInternalHomOnMorphisms
‣ 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)\).

1.12-23 AddInternalHomOnMorphismsWithGivenInternalHoms
‣ 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)\).

1.12-24 AddInternalHomOnObjects
‣ 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)\).

1.12-25 AddInternalHomToTensorProductAdjunctionMap
‣ AddInternalHomToTensorProductAdjunctionMap( 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 InternalHomToTensorProductAdjunctionMap. \(F: ( b, c, g ) \mapsto \mathtt{InternalHomToTensorProductAdjunctionMap}(b, c, g)\).

1.12-26 AddInternalHomToTensorProductAdjunctionMapWithGivenTensorProduct
‣ AddInternalHomToTensorProductAdjunctionMapWithGivenTensorProduct( 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 InternalHomToTensorProductAdjunctionMapWithGivenTensorProduct. \(F: ( b, c, g, t ) \mapsto \mathtt{InternalHomToTensorProductAdjunctionMapWithGivenTensorProduct}(b, c, g, t)\).

1.12-27 AddIsomorphismFromDualObjectToInternalHomIntoTensorUnit
‣ 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)\).

1.12-28 AddIsomorphismFromInternalHomIntoTensorUnitToDualObject
‣ 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)\).

1.12-29 AddIsomorphismFromInternalHomToObject
‣ 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)\).

1.12-30 AddIsomorphismFromInternalHomToObjectWithGivenInternalHom
‣ 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)\).

1.12-31 AddIsomorphismFromObjectToInternalHom
‣ 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)\).

1.12-32 AddIsomorphismFromObjectToInternalHomWithGivenInternalHom
‣ 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)\).

1.12-33 AddLambdaElimination
‣ 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)\).

1.12-34 AddLambdaIntroduction
‣ 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)\).

1.12-35 AddMonoidalPostComposeMorphism
‣ 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)\).

1.12-36 AddMonoidalPostComposeMorphismWithGivenObjects
‣ 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)\).

1.12-37 AddMonoidalPreComposeMorphism
‣ 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)\).

1.12-38 AddMonoidalPreComposeMorphismWithGivenObjects
‣ 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)\).

1.12-39 AddMorphismFromTensorProductToInternalHom
‣ 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)\).

1.12-40 AddMorphismFromTensorProductToInternalHomWithGivenObjects
‣ 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)\).

1.12-41 AddMorphismToBidual
‣ 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)\).

1.12-42 AddMorphismToBidualWithGivenBidual
‣ 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)\).

1.12-43 AddTensorProductDualityCompatibilityMorphism
‣ 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)\).

1.12-44 AddTensorProductDualityCompatibilityMorphismWithGivenObjects
‣ 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)\).

1.12-45 AddTensorProductInternalHomCompatibilityMorphism
‣ 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)\).

1.12-46 AddTensorProductInternalHomCompatibilityMorphismWithGivenObjects
‣ 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)\).

1.12-47 AddTensorProductToInternalHomAdjunctionMap
‣ AddTensorProductToInternalHomAdjunctionMap( 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 TensorProductToInternalHomAdjunctionMap. \(F: ( a, b, f ) \mapsto \mathtt{TensorProductToInternalHomAdjunctionMap}(a, b, f)\).

1.12-48 AddTensorProductToInternalHomAdjunctionMapWithGivenInternalHom
‣ AddTensorProductToInternalHomAdjunctionMapWithGivenInternalHom( 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 TensorProductToInternalHomAdjunctionMapWithGivenInternalHom. \(F: ( a, b, f, i ) \mapsto \mathtt{TensorProductToInternalHomAdjunctionMapWithGivenInternalHom}(a, b, f, i)\).

1.12-49 AddUniversalPropertyOfDual
‣ 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)\).

1.12-50 AddCoDualOnMorphisms
‣ 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)\).

1.12-51 AddCoDualOnMorphismsWithGivenCoDuals
‣ 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)\).

1.12-52 AddCoDualOnObjects
‣ 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)\).

1.12-53 AddCoDualityTensorProductCompatibilityMorphism
‣ 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)\).

1.12-54 AddCoDualityTensorProductCompatibilityMorphismWithGivenObjects
‣ 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)\).

1.12-55 AddCoLambdaElimination
‣ 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)\).

1.12-56 AddCoLambdaIntroduction
‣ 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)\).

1.12-57 AddCoclosedCoevaluationMorphism
‣ AddCoclosedCoevaluationMorphism( 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 CoclosedCoevaluationMorphism. \(F: ( a, b ) \mapsto \mathtt{CoclosedCoevaluationMorphism}(a, b)\).

1.12-58 AddCoclosedCoevaluationMorphismWithGivenSource
‣ AddCoclosedCoevaluationMorphismWithGivenSource( 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 CoclosedCoevaluationMorphismWithGivenSource. \(F: ( a, b, s ) \mapsto \mathtt{CoclosedCoevaluationMorphismWithGivenSource}(a, b, s)\).

1.12-59 AddCoclosedEvaluationForCoDual
‣ 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)\).

1.12-60 AddCoclosedEvaluationForCoDualWithGivenTensorProduct
‣ 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)\).

1.12-61 AddCoclosedEvaluationMorphism
‣ AddCoclosedEvaluationMorphism( 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 CoclosedEvaluationMorphism. \(F: ( a, b ) \mapsto \mathtt{CoclosedEvaluationMorphism}(a, b)\).

1.12-62 AddCoclosedEvaluationMorphismWithGivenRange
‣ AddCoclosedEvaluationMorphismWithGivenRange( 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 CoclosedEvaluationMorphismWithGivenRange. \(F: ( a, b, r ) \mapsto \mathtt{CoclosedEvaluationMorphismWithGivenRange}(a, b, r)\).

1.12-63 AddInternalCoHomOnMorphisms
‣ 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)\).

1.12-64 AddInternalCoHomOnMorphismsWithGivenInternalCoHoms
‣ 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)\).

1.12-65 AddInternalCoHomOnObjects
‣ 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)\).

1.12-66 AddInternalCoHomTensorProductCompatibilityMorphism
‣ 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)\).

1.12-67 AddInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects
‣ 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)\).

1.12-68 AddInternalCoHomToTensorProductAdjunctionMap
‣ AddInternalCoHomToTensorProductAdjunctionMap( 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 InternalCoHomToTensorProductAdjunctionMap. \(F: ( a, b, f ) \mapsto \mathtt{InternalCoHomToTensorProductAdjunctionMap}(a, b, f)\).

1.12-69 AddInternalCoHomToTensorProductAdjunctionMapWithGivenTensorProduct
‣ AddInternalCoHomToTensorProductAdjunctionMapWithGivenTensorProduct( 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 InternalCoHomToTensorProductAdjunctionMapWithGivenTensorProduct. \(F: ( a, b, f, t ) \mapsto \mathtt{InternalCoHomToTensorProductAdjunctionMapWithGivenTensorProduct}(a, b, f, t)\).

1.12-70 AddIsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit
‣ 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)\).

1.12-71 AddIsomorphismFromInternalCoHomFromTensorUnitToCoDualObject
‣ 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)\).

1.12-72 AddIsomorphismFromInternalCoHomToObject
‣ 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)\).

1.12-73 AddIsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom
‣ 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)\).

1.12-74 AddIsomorphismFromObjectToInternalCoHom
‣ 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)\).

1.12-75 AddIsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom
‣ 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)\).

1.12-76 AddMonoidalPostCoComposeMorphism
‣ 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)\).

1.12-77 AddMonoidalPostCoComposeMorphismWithGivenObjects
‣ 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)\).

1.12-78 AddMonoidalPreCoComposeMorphism
‣ 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)\).

1.12-79 AddMonoidalPreCoComposeMorphismWithGivenObjects
‣ 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)\).

1.12-80 AddMorphismFromCoBidual
‣ 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)\).

1.12-81 AddMorphismFromCoBidualWithGivenCoBidual
‣ 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)\).

1.12-82 AddMorphismFromInternalCoHomToTensorProduct
‣ 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)\).

1.12-83 AddMorphismFromInternalCoHomToTensorProductWithGivenObjects
‣ 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)\).

1.12-84 AddTensorProductToInternalCoHomAdjunctionMap
‣ AddTensorProductToInternalCoHomAdjunctionMap( 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 TensorProductToInternalCoHomAdjunctionMap. \(F: ( c, b, g ) \mapsto \mathtt{TensorProductToInternalCoHomAdjunctionMap}(c, b, g)\).

1.12-85 AddTensorProductToInternalCoHomAdjunctionMapWithGivenInternalCoHom
‣ AddTensorProductToInternalCoHomAdjunctionMapWithGivenInternalCoHom( 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 TensorProductToInternalCoHomAdjunctionMapWithGivenInternalCoHom. \(F: ( c, b, g, i ) \mapsto \mathtt{TensorProductToInternalCoHomAdjunctionMapWithGivenInternalCoHom}(c, b, g, i)\).

1.12-86 AddUniversalPropertyOfCoDual
‣ 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)\).

1.12-87 AddAssociatorLeftToRight
‣ 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)\).

1.12-88 AddAssociatorLeftToRightWithGivenTensorProducts
‣ 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)\).

1.12-89 AddAssociatorRightToLeft
‣ 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)\).

1.12-90 AddAssociatorRightToLeftWithGivenTensorProducts
‣ 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)\).

1.12-91 AddLeftUnitor
‣ 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)\).

1.12-92 AddLeftUnitorInverse
‣ 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)\).

1.12-93 AddLeftUnitorInverseWithGivenTensorProduct
‣ 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)\).

1.12-94 AddLeftUnitorWithGivenTensorProduct
‣ 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)\).

1.12-95 AddRightUnitor
‣ 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)\).

1.12-96 AddRightUnitorInverse
‣ 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)\).

1.12-97 AddRightUnitorInverseWithGivenTensorProduct
‣ 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)\).

1.12-98 AddRightUnitorWithGivenTensorProduct
‣ 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)\).

1.12-99 AddTensorProductOnMorphisms
‣ 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)\).

1.12-100 AddTensorProductOnMorphismsWithGivenTensorProducts
‣ 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)\).

1.12-101 AddCoevaluationForDual
‣ 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)\).

1.12-102 AddCoevaluationForDualWithGivenTensorProduct
‣ 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)\).

1.12-103 AddIsomorphismFromInternalHomToTensorProductWithDualObject
‣ 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)\).

1.12-104 AddIsomorphismFromTensorProductWithDualObjectToInternalHom
‣ 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)\).

1.12-105 AddMorphismFromBidual
‣ 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)\).

1.12-106 AddMorphismFromBidualWithGivenBidual
‣ 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)\).

1.12-107 AddMorphismFromInternalHomToTensorProduct
‣ 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)\).

1.12-108 AddMorphismFromInternalHomToTensorProductWithGivenObjects
‣ 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)\).

1.12-109 AddRankMorphism
‣ 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)\).

1.12-110 AddTensorProductInternalHomCompatibilityMorphismInverse
‣ 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)\).

1.12-111 AddTensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects
‣ 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)\).

1.12-112 AddTraceMap
‣ 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)\).

1.12-113 AddCoRankMorphism
‣ 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)\).

1.12-114 AddCoTraceMap
‣ 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)\).

1.12-115 AddCoclosedCoevaluationForCoDual
‣ 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)\).

1.12-116 AddCoclosedCoevaluationForCoDualWithGivenTensorProduct
‣ 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)\).

1.12-117 AddInternalCoHomTensorProductCompatibilityMorphismInverse
‣ 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)\).

1.12-118 AddInternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects
‣ 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)\).

1.12-119 AddIsomorphismFromInternalCoHomToTensorProductWithCoDualObject
‣ 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)\).

1.12-120 AddIsomorphismFromTensorProductWithCoDualObjectToInternalCoHom
‣ 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)\).

1.12-121 AddMorphismFromTensorProductToInternalCoHom
‣ 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)\).

1.12-122 AddMorphismFromTensorProductToInternalCoHomWithGivenObjects
‣ 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)\).

1.12-123 AddMorphismToCoBidual
‣ 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)\).

1.12-124 AddMorphismToCoBidualWithGivenCoBidual
‣ AddMorphismToCoBidualWithGivenCoBidual( 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 MorphismToCoBidualWithGivenCoBidual. \(F: ( a, r ) \mapsto \mathtt{MorphismToCoBidualWithGivenCoBidual}(a, r)\).

 [Top of Book]  [Contents]   [Previous Chapter]   [Next Chapter] 
Goto Chapter: Top 1 2 3 4 5 Ind

generated by GAPDoc2HTML