Goto Chapter: Top 1 2 3 4 5 6 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 Left Closed Monoidal Categories

  1.5-1 LeftInternalHomOnObjects

  1.5-2 LeftInternalHomOnMorphisms

  1.5-3 LeftInternalHomOnMorphismsWithGivenLeftInternalHoms

  1.5-4 LeftClosedMonoidalEvaluationMorphism

  1.5-5 LeftClosedMonoidalEvaluationMorphismWithGivenSource

  1.5-6 LeftClosedMonoidalCoevaluationMorphism

  1.5-7 LeftClosedMonoidalCoevaluationMorphismWithGivenRange

  1.5-8 TensorProductToLeftInternalHomAdjunctMorphism

  1.5-9 TensorProductToLeftInternalHomAdjunctMorphismWithGivenLeftInternalHom

  1.5-10 LeftInternalHomToTensorProductAdjunctMorphism

  1.5-11 LeftInternalHomToTensorProductAdjunctMorphismWithGivenTensorProduct

  1.5-12 LeftClosedMonoidalPreComposeMorphism

  1.5-13 LeftClosedMonoidalPreComposeMorphismWithGivenObjects

  1.5-14 LeftClosedMonoidalPostComposeMorphism

  1.5-15 LeftClosedMonoidalPostComposeMorphismWithGivenObjects

  1.5-16 LeftDualOnObjects

  1.5-17 LeftDualOnMorphisms

  1.5-18 LeftDualOnMorphismsWithGivenLeftDuals

  1.5-19 LeftClosedMonoidalEvaluationForLeftDual

  1.5-20 LeftClosedMonoidalEvaluationForLeftDualWithGivenTensorProduct

  1.5-21 MorphismToLeftBidual

  1.5-22 MorphismToLeftBidualWithGivenLeftBidual

  1.5-23 TensorProductLeftInternalHomCompatibilityMorphism

  1.5-24 TensorProductLeftInternalHomCompatibilityMorphismWithGivenObjects

  1.5-25 TensorProductLeftDualityCompatibilityMorphism

  1.5-26 TensorProductLeftDualityCompatibilityMorphismWithGivenObjects

  1.5-27 MorphismFromTensorProductToLeftInternalHom

  1.5-28 MorphismFromTensorProductToLeftInternalHomWithGivenObjects

  1.5-29 IsomorphismFromLeftDualObjectToLeftInternalHomIntoTensorUnit

  1.5-30 IsomorphismFromLeftInternalHomIntoTensorUnitToLeftDualObject

  1.5-31 UniversalPropertyOfLeftDual

  1.5-32 LeftClosedMonoidalLambdaIntroduction

  1.5-33 LeftClosedMonoidalLambdaElimination

  1.5-34 IsomorphismFromObjectToLeftInternalHom

  1.5-35 IsomorphismFromObjectToLeftInternalHomWithGivenLeftInternalHom

  1.5-36 IsomorphismFromLeftInternalHomToObject

  1.5-37 IsomorphismFromLeftInternalHomToObjectWithGivenLeftInternalHom
 1.6 Closed Monoidal Categories

  1.6-1 InternalHomOnObjects

  1.6-2 InternalHomOnMorphisms

  1.6-3 InternalHomOnMorphismsWithGivenInternalHoms

  1.6-4 ClosedMonoidalRightEvaluationMorphism

  1.6-5 ClosedMonoidalRightEvaluationMorphismWithGivenSource

  1.6-6 ClosedMonoidalRightCoevaluationMorphism

  1.6-7 ClosedMonoidalRightCoevaluationMorphismWithGivenRange

  1.6-8 TensorProductToInternalHomRightAdjunctMorphism

  1.6-9 TensorProductToInternalHomRightAdjunctMorphismWithGivenInternalHom

  1.6-10 TensorProductToInternalHomRightAdjunctionIsomorphism

  1.6-11 TensorProductToInternalHomRightAdjunctionIsomorphismWithGivenObjects

  1.6-12 InternalHomToTensorProductRightAdjunctMorphism

  1.6-13 InternalHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct

  1.6-14 InternalHomToTensorProductRightAdjunctionIsomorphism

  1.6-15 InternalHomToTensorProductRightAdjunctionIsomorphismWithGivenObjects

  1.6-16 ClosedMonoidalLeftEvaluationMorphism

  1.6-17 ClosedMonoidalLeftEvaluationMorphismWithGivenSource

  1.6-18 ClosedMonoidalLeftCoevaluationMorphism

  1.6-19 ClosedMonoidalLeftCoevaluationMorphismWithGivenRange

  1.6-20 TensorProductToInternalHomLeftAdjunctMorphism

  1.6-21 TensorProductToInternalHomLeftAdjunctMorphismWithGivenInternalHom

  1.6-22 TensorProductToInternalHomLeftAdjunctionIsomorphism

  1.6-23 TensorProductToInternalHomLeftAdjunctionIsomorphismWithGivenObjects

  1.6-24 InternalHomToTensorProductLeftAdjunctMorphism

  1.6-25 InternalHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct

  1.6-26 InternalHomToTensorProductLeftAdjunctionIsomorphism

  1.6-27 InternalHomToTensorProductLeftAdjunctionIsomorphismWithGivenObjects

  1.6-28 MonoidalPreComposeMorphism

  1.6-29 MonoidalPreComposeMorphismWithGivenObjects

  1.6-30 MonoidalPostComposeMorphism

  1.6-31 MonoidalPostComposeMorphismWithGivenObjects

  1.6-32 DualOnObjects

  1.6-33 DualOnMorphisms

  1.6-34 DualOnMorphismsWithGivenDuals

  1.6-35 EvaluationForDual

  1.6-36 EvaluationForDualWithGivenTensorProduct

  1.6-37 MorphismToBidual

  1.6-38 MorphismToBidualWithGivenBidual

  1.6-39 TensorProductInternalHomCompatibilityMorphism

  1.6-40 TensorProductInternalHomCompatibilityMorphismWithGivenObjects

  1.6-41 TensorProductDualityCompatibilityMorphism

  1.6-42 TensorProductDualityCompatibilityMorphismWithGivenObjects

  1.6-43 MorphismFromTensorProductToInternalHom

  1.6-44 MorphismFromTensorProductToInternalHomWithGivenObjects

  1.6-45 IsomorphismFromDualObjectToInternalHomIntoTensorUnit

  1.6-46 IsomorphismFromInternalHomIntoTensorUnitToDualObject

  1.6-47 UniversalPropertyOfDual

  1.6-48 LambdaIntroduction

  1.6-49 LambdaElimination

  1.6-50 IsomorphismFromObjectToInternalHom

  1.6-51 IsomorphismFromObjectToInternalHomWithGivenInternalHom

  1.6-52 IsomorphismFromInternalHomToObject

  1.6-53 IsomorphismFromInternalHomToObjectWithGivenInternalHom
 1.7 Left Coclosed Monoidal Categories

  1.7-1 LeftInternalCoHomOnObjects

  1.7-2 LeftInternalCoHomOnMorphisms

  1.7-3 LeftInternalCoHomOnMorphismsWithGivenLeftInternalCoHoms

  1.7-4 LeftCoclosedMonoidalEvaluationMorphism

  1.7-5 LeftCoclosedMonoidalEvaluationMorphismWithGivenRange

  1.7-6 LeftCoclosedMonoidalCoevaluationMorphism

  1.7-7 LeftCoclosedMonoidalCoevaluationMorphismWithGivenSource

  1.7-8 TensorProductToLeftInternalCoHomAdjunctMorphism

  1.7-9 TensorProductToLeftInternalCoHomAdjunctMorphismWithGivenLeftInternalCoHom

  1.7-10 LeftInternalCoHomToTensorProductAdjunctMorphism

  1.7-11 LeftInternalCoHomToTensorProductAdjunctMorphismWithGivenTensorProduct

  1.7-12 LeftCoclosedMonoidalPreCoComposeMorphism

  1.7-13 LeftCoclosedMonoidalPreCoComposeMorphismWithGivenObjects

  1.7-14 LeftCoclosedMonoidalPostCoComposeMorphism

  1.7-15 LeftCoclosedMonoidalPostCoComposeMorphismWithGivenObjects

  1.7-16 LeftCoDualOnObjects

  1.7-17 LeftCoDualOnMorphisms

  1.7-18 LeftCoDualOnMorphismsWithGivenLeftCoDuals

  1.7-19 LeftCoclosedMonoidalEvaluationForLeftCoDual

  1.7-20 LeftCoclosedMonoidalEvaluationForLeftCoDualWithGivenTensorProduct

  1.7-21 MorphismFromLeftCoBidual

  1.7-22 MorphismFromLeftCoBidualWithGivenLeftCoBidual

  1.7-23 LeftInternalCoHomTensorProductCompatibilityMorphism

  1.7-24 LeftInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects

  1.7-25 LeftCoDualityTensorProductCompatibilityMorphism

  1.7-26 LeftCoDualityTensorProductCompatibilityMorphismWithGivenObjects

  1.7-27 MorphismFromLeftInternalCoHomToTensorProduct

  1.7-28 MorphismFromLeftInternalCoHomToTensorProductWithGivenObjects

  1.7-29 IsomorphismFromLeftCoDualObjectToLeftInternalCoHomFromTensorUnit

  1.7-30 IsomorphismFromLeftInternalCoHomFromTensorUnitToLeftCoDualObject

  1.7-31 UniversalPropertyOfLeftCoDual

  1.7-32 LeftCoclosedMonoidalLambdaIntroduction

  1.7-33 LeftCoclosedMonoidalLambdaElimination

  1.7-34 IsomorphismFromObjectToLeftInternalCoHom

  1.7-35 IsomorphismFromObjectToLeftInternalCoHomWithGivenLeftInternalCoHom

  1.7-36 IsomorphismFromLeftInternalCoHomToObject

  1.7-37 IsomorphismFromLeftInternalCoHomToObjectWithGivenLeftInternalCoHom
 1.8 Coclosed Monoidal Categories

  1.8-1 InternalCoHomOnObjects

  1.8-2 InternalCoHomOnMorphisms

  1.8-3 InternalCoHomOnMorphismsWithGivenInternalCoHoms

  1.8-4 CoclosedMonoidalRightEvaluationMorphism

  1.8-5 CoclosedMonoidalRightEvaluationMorphismWithGivenRange

  1.8-6 CoclosedMonoidalRightCoevaluationMorphism

  1.8-7 CoclosedMonoidalRightCoevaluationMorphismWithGivenSource

  1.8-8 TensorProductToInternalCoHomRightAdjunctMorphism

  1.8-9 TensorProductToInternalCoHomRightAdjunctMorphismWithGivenInternalCoHom

  1.8-10 InternalCoHomToTensorProductRightAdjunctMorphism

  1.8-11 InternalCoHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct

  1.8-12 CoclosedMonoidalLeftEvaluationMorphism

  1.8-13 CoclosedMonoidalLeftEvaluationMorphismWithGivenRange

  1.8-14 CoclosedMonoidalLeftCoevaluationMorphism

  1.8-15 CoclosedMonoidalLeftCoevaluationMorphismWithGivenSource

  1.8-16 TensorProductToInternalCoHomLeftAdjunctMorphism

  1.8-17 TensorProductToInternalCoHomLeftAdjunctMorphismWithGivenInternalCoHom

  1.8-18 InternalCoHomToTensorProductLeftAdjunctMorphism

  1.8-19 InternalCoHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct

  1.8-20 MonoidalPreCoComposeMorphism

  1.8-21 MonoidalPreCoComposeMorphismWithGivenObjects

  1.8-22 MonoidalPostCoComposeMorphism

  1.8-23 MonoidalPostCoComposeMorphismWithGivenObjects

  1.8-24 CoDualOnObjects

  1.8-25 CoDualOnMorphisms

  1.8-26 CoDualOnMorphismsWithGivenCoDuals

  1.8-27 CoclosedEvaluationForCoDual

  1.8-28 CoclosedEvaluationForCoDualWithGivenTensorProduct

  1.8-29 MorphismFromCoBidual

  1.8-30 MorphismFromCoBidualWithGivenCoBidual

  1.8-31 InternalCoHomTensorProductCompatibilityMorphism

  1.8-32 InternalCoHomTensorProductCompatibilityMorphismWithGivenObjects

  1.8-33 CoDualityTensorProductCompatibilityMorphism

  1.8-34 CoDualityTensorProductCompatibilityMorphismWithGivenObjects

  1.8-35 MorphismFromInternalCoHomToTensorProduct

  1.8-36 MorphismFromInternalCoHomToTensorProductWithGivenObjects

  1.8-37 IsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit

  1.8-38 IsomorphismFromInternalCoHomFromTensorUnitToCoDualObject

  1.8-39 UniversalPropertyOfCoDual

  1.8-40 CoLambdaIntroduction

  1.8-41 CoLambdaElimination

  1.8-42 IsomorphismFromObjectToInternalCoHom

  1.8-43 IsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom

  1.8-44 IsomorphismFromInternalCoHomToObject

  1.8-45 IsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom
 1.9 Symmetric Closed Monoidal Categories
 1.10 Symmetric Coclosed Monoidal Categories
 1.11 Rigid Symmetric Closed Monoidal Categories
 1.12 Rigid Symmetric Coclosed Monoidal Categories
 1.13 Convenience Methods
 1.14 Add-methods

  1.14-1 AddLeftDistributivityExpanding

  1.14-2 AddLeftDistributivityExpandingWithGivenObjects

  1.14-3 AddLeftDistributivityFactoring

  1.14-4 AddLeftDistributivityFactoringWithGivenObjects

  1.14-5 AddRightDistributivityExpanding

  1.14-6 AddRightDistributivityExpandingWithGivenObjects

  1.14-7 AddRightDistributivityFactoring

  1.14-8 AddRightDistributivityFactoringWithGivenObjects

  1.14-9 AddBraiding

  1.14-10 AddBraidingInverse

  1.14-11 AddBraidingInverseWithGivenTensorProducts

  1.14-12 AddBraidingWithGivenTensorProducts

  1.14-13 AddClosedMonoidalLeftCoevaluationMorphism

  1.14-14 AddClosedMonoidalLeftCoevaluationMorphismWithGivenRange

  1.14-15 AddClosedMonoidalLeftEvaluationMorphism

  1.14-16 AddClosedMonoidalLeftEvaluationMorphismWithGivenSource

  1.14-17 AddClosedMonoidalRightCoevaluationMorphism

  1.14-18 AddClosedMonoidalRightCoevaluationMorphismWithGivenRange

  1.14-19 AddClosedMonoidalRightEvaluationMorphism

  1.14-20 AddClosedMonoidalRightEvaluationMorphismWithGivenSource

  1.14-21 AddDualOnMorphisms

  1.14-22 AddDualOnMorphismsWithGivenDuals

  1.14-23 AddDualOnObjects

  1.14-24 AddEvaluationForDual

  1.14-25 AddEvaluationForDualWithGivenTensorProduct

  1.14-26 AddInternalHomOnMorphisms

  1.14-27 AddInternalHomOnMorphismsWithGivenInternalHoms

  1.14-28 AddInternalHomOnObjects

  1.14-29 AddInternalHomToTensorProductLeftAdjunctMorphism

  1.14-30 AddInternalHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct

  1.14-31 AddInternalHomToTensorProductLeftAdjunctionIsomorphism

  1.14-32 AddInternalHomToTensorProductLeftAdjunctionIsomorphismWithGivenObjects

  1.14-33 AddInternalHomToTensorProductRightAdjunctMorphism

  1.14-34 AddInternalHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct

  1.14-35 AddInternalHomToTensorProductRightAdjunctionIsomorphism

  1.14-36 AddInternalHomToTensorProductRightAdjunctionIsomorphismWithGivenObjects

  1.14-37 AddIsomorphismFromDualObjectToInternalHomIntoTensorUnit

  1.14-38 AddIsomorphismFromInternalHomIntoTensorUnitToDualObject

  1.14-39 AddIsomorphismFromInternalHomToObject

  1.14-40 AddIsomorphismFromInternalHomToObjectWithGivenInternalHom

  1.14-41 AddIsomorphismFromObjectToInternalHom

  1.14-42 AddIsomorphismFromObjectToInternalHomWithGivenInternalHom

  1.14-43 AddLambdaElimination

  1.14-44 AddLambdaIntroduction

  1.14-45 AddMonoidalPostComposeMorphism

  1.14-46 AddMonoidalPostComposeMorphismWithGivenObjects

  1.14-47 AddMonoidalPreComposeMorphism

  1.14-48 AddMonoidalPreComposeMorphismWithGivenObjects

  1.14-49 AddMorphismFromTensorProductToInternalHom

  1.14-50 AddMorphismFromTensorProductToInternalHomWithGivenObjects

  1.14-51 AddMorphismToBidual

  1.14-52 AddMorphismToBidualWithGivenBidual

  1.14-53 AddTensorProductDualityCompatibilityMorphism

  1.14-54 AddTensorProductDualityCompatibilityMorphismWithGivenObjects

  1.14-55 AddTensorProductInternalHomCompatibilityMorphism

  1.14-56 AddTensorProductInternalHomCompatibilityMorphismWithGivenObjects

  1.14-57 AddTensorProductToInternalHomLeftAdjunctMorphism

  1.14-58 AddTensorProductToInternalHomLeftAdjunctMorphismWithGivenInternalHom

  1.14-59 AddTensorProductToInternalHomLeftAdjunctionIsomorphism

  1.14-60 AddTensorProductToInternalHomLeftAdjunctionIsomorphismWithGivenObjects

  1.14-61 AddTensorProductToInternalHomRightAdjunctMorphism

  1.14-62 AddTensorProductToInternalHomRightAdjunctMorphismWithGivenInternalHom

  1.14-63 AddTensorProductToInternalHomRightAdjunctionIsomorphism

  1.14-64 AddTensorProductToInternalHomRightAdjunctionIsomorphismWithGivenObjects

  1.14-65 AddUniversalPropertyOfDual

  1.14-66 AddCoDualOnMorphisms

  1.14-67 AddCoDualOnMorphismsWithGivenCoDuals

  1.14-68 AddCoDualOnObjects

  1.14-69 AddCoDualityTensorProductCompatibilityMorphism

  1.14-70 AddCoDualityTensorProductCompatibilityMorphismWithGivenObjects

  1.14-71 AddCoLambdaElimination

  1.14-72 AddCoLambdaIntroduction

  1.14-73 AddCoclosedEvaluationForCoDual

  1.14-74 AddCoclosedEvaluationForCoDualWithGivenTensorProduct

  1.14-75 AddCoclosedMonoidalLeftCoevaluationMorphism

  1.14-76 AddCoclosedMonoidalLeftCoevaluationMorphismWithGivenSource

  1.14-77 AddCoclosedMonoidalLeftEvaluationMorphism

  1.14-78 AddCoclosedMonoidalLeftEvaluationMorphismWithGivenRange

  1.14-79 AddCoclosedMonoidalRightCoevaluationMorphism

  1.14-80 AddCoclosedMonoidalRightCoevaluationMorphismWithGivenSource

  1.14-81 AddCoclosedMonoidalRightEvaluationMorphism

  1.14-82 AddCoclosedMonoidalRightEvaluationMorphismWithGivenRange

  1.14-83 AddInternalCoHomOnMorphisms

  1.14-84 AddInternalCoHomOnMorphismsWithGivenInternalCoHoms

  1.14-85 AddInternalCoHomOnObjects

  1.14-86 AddInternalCoHomTensorProductCompatibilityMorphism

  1.14-87 AddInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects

  1.14-88 AddInternalCoHomToTensorProductLeftAdjunctMorphism

  1.14-89 AddInternalCoHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct

  1.14-90 AddInternalCoHomToTensorProductRightAdjunctMorphism

  1.14-91 AddInternalCoHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct

  1.14-92 AddIsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit

  1.14-93 AddIsomorphismFromInternalCoHomFromTensorUnitToCoDualObject

  1.14-94 AddIsomorphismFromInternalCoHomToObject

  1.14-95 AddIsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom

  1.14-96 AddIsomorphismFromObjectToInternalCoHom

  1.14-97 AddIsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom

  1.14-98 AddMonoidalPostCoComposeMorphism

  1.14-99 AddMonoidalPostCoComposeMorphismWithGivenObjects

  1.14-100 AddMonoidalPreCoComposeMorphism

  1.14-101 AddMonoidalPreCoComposeMorphismWithGivenObjects

  1.14-102 AddMorphismFromCoBidual

  1.14-103 AddMorphismFromCoBidualWithGivenCoBidual

  1.14-104 AddMorphismFromInternalCoHomToTensorProduct

  1.14-105 AddMorphismFromInternalCoHomToTensorProductWithGivenObjects

  1.14-106 AddTensorProductToInternalCoHomLeftAdjunctMorphism

  1.14-107 AddTensorProductToInternalCoHomLeftAdjunctMorphismWithGivenInternalCoHom

  1.14-108 AddTensorProductToInternalCoHomRightAdjunctMorphism

  1.14-109 AddTensorProductToInternalCoHomRightAdjunctMorphismWithGivenInternalCoHom

  1.14-110 AddUniversalPropertyOfCoDual

  1.14-111 AddIsomorphismFromLeftDualObjectToLeftInternalHomIntoTensorUnit

  1.14-112 AddIsomorphismFromLeftInternalHomIntoTensorUnitToLeftDualObject

  1.14-113 AddIsomorphismFromLeftInternalHomToObject

  1.14-114 AddIsomorphismFromLeftInternalHomToObjectWithGivenLeftInternalHom

  1.14-115 AddIsomorphismFromObjectToLeftInternalHom

  1.14-116 AddIsomorphismFromObjectToLeftInternalHomWithGivenLeftInternalHom

  1.14-117 AddLeftClosedMonoidalCoevaluationMorphism

  1.14-118 AddLeftClosedMonoidalCoevaluationMorphismWithGivenRange

  1.14-119 AddLeftClosedMonoidalEvaluationForLeftDual

  1.14-120 AddLeftClosedMonoidalEvaluationForLeftDualWithGivenTensorProduct

  1.14-121 AddLeftClosedMonoidalEvaluationMorphism

  1.14-122 AddLeftClosedMonoidalEvaluationMorphismWithGivenSource

  1.14-123 AddLeftClosedMonoidalLambdaElimination

  1.14-124 AddLeftClosedMonoidalLambdaIntroduction

  1.14-125 AddLeftClosedMonoidalPostComposeMorphism

  1.14-126 AddLeftClosedMonoidalPostComposeMorphismWithGivenObjects

  1.14-127 AddLeftClosedMonoidalPreComposeMorphism

  1.14-128 AddLeftClosedMonoidalPreComposeMorphismWithGivenObjects

  1.14-129 AddLeftDualOnMorphisms

  1.14-130 AddLeftDualOnMorphismsWithGivenLeftDuals

  1.14-131 AddLeftDualOnObjects

  1.14-132 AddLeftInternalHomOnMorphisms

  1.14-133 AddLeftInternalHomOnMorphismsWithGivenLeftInternalHoms

  1.14-134 AddLeftInternalHomOnObjects

  1.14-135 AddLeftInternalHomToTensorProductAdjunctMorphism

  1.14-136 AddLeftInternalHomToTensorProductAdjunctMorphismWithGivenTensorProduct

  1.14-137 AddMorphismFromTensorProductToLeftInternalHom

  1.14-138 AddMorphismFromTensorProductToLeftInternalHomWithGivenObjects

  1.14-139 AddMorphismToLeftBidual

  1.14-140 AddMorphismToLeftBidualWithGivenLeftBidual

  1.14-141 AddTensorProductLeftDualityCompatibilityMorphism

  1.14-142 AddTensorProductLeftDualityCompatibilityMorphismWithGivenObjects

  1.14-143 AddTensorProductLeftInternalHomCompatibilityMorphism

  1.14-144 AddTensorProductLeftInternalHomCompatibilityMorphismWithGivenObjects

  1.14-145 AddTensorProductToLeftInternalHomAdjunctMorphism

  1.14-146 AddTensorProductToLeftInternalHomAdjunctMorphismWithGivenLeftInternalHom

  1.14-147 AddUniversalPropertyOfLeftDual

  1.14-148 AddIsomorphismFromLeftCoDualObjectToLeftInternalCoHomFromTensorUnit

  1.14-149 AddIsomorphismFromLeftInternalCoHomFromTensorUnitToLeftCoDualObject

  1.14-150 AddIsomorphismFromLeftInternalCoHomToObject

  1.14-151 AddIsomorphismFromLeftInternalCoHomToObjectWithGivenLeftInternalCoHom

  1.14-152 AddIsomorphismFromObjectToLeftInternalCoHom

  1.14-153 AddIsomorphismFromObjectToLeftInternalCoHomWithGivenLeftInternalCoHom

  1.14-154 AddLeftCoDualOnMorphisms

  1.14-155 AddLeftCoDualOnMorphismsWithGivenLeftCoDuals

  1.14-156 AddLeftCoDualOnObjects

  1.14-157 AddLeftCoDualityTensorProductCompatibilityMorphism

  1.14-158 AddLeftCoDualityTensorProductCompatibilityMorphismWithGivenObjects

  1.14-159 AddLeftCoclosedMonoidalCoevaluationMorphism

  1.14-160 AddLeftCoclosedMonoidalCoevaluationMorphismWithGivenSource

  1.14-161 AddLeftCoclosedMonoidalEvaluationForLeftCoDual

  1.14-162 AddLeftCoclosedMonoidalEvaluationForLeftCoDualWithGivenTensorProduct

  1.14-163 AddLeftCoclosedMonoidalEvaluationMorphism

  1.14-164 AddLeftCoclosedMonoidalEvaluationMorphismWithGivenRange

  1.14-165 AddLeftCoclosedMonoidalLambdaElimination

  1.14-166 AddLeftCoclosedMonoidalLambdaIntroduction

  1.14-167 AddLeftCoclosedMonoidalPostCoComposeMorphism

  1.14-168 AddLeftCoclosedMonoidalPostCoComposeMorphismWithGivenObjects

  1.14-169 AddLeftCoclosedMonoidalPreCoComposeMorphism

  1.14-170 AddLeftCoclosedMonoidalPreCoComposeMorphismWithGivenObjects

  1.14-171 AddLeftInternalCoHomOnMorphisms

  1.14-172 AddLeftInternalCoHomOnMorphismsWithGivenLeftInternalCoHoms

  1.14-173 AddLeftInternalCoHomOnObjects

  1.14-174 AddLeftInternalCoHomTensorProductCompatibilityMorphism

  1.14-175 AddLeftInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects

  1.14-176 AddLeftInternalCoHomToTensorProductAdjunctMorphism

  1.14-177 AddLeftInternalCoHomToTensorProductAdjunctMorphismWithGivenTensorProduct

  1.14-178 AddMorphismFromLeftCoBidual

  1.14-179 AddMorphismFromLeftCoBidualWithGivenLeftCoBidual

  1.14-180 AddMorphismFromLeftInternalCoHomToTensorProduct

  1.14-181 AddMorphismFromLeftInternalCoHomToTensorProductWithGivenObjects

  1.14-182 AddTensorProductToLeftInternalCoHomAdjunctMorphism

  1.14-183 AddTensorProductToLeftInternalCoHomAdjunctMorphismWithGivenLeftInternalCoHom

  1.14-184 AddUniversalPropertyOfLeftCoDual

  1.14-185 AddAssociatorLeftToRight

  1.14-186 AddAssociatorLeftToRightWithGivenTensorProducts

  1.14-187 AddAssociatorRightToLeft

  1.14-188 AddAssociatorRightToLeftWithGivenTensorProducts

  1.14-189 AddLeftUnitor

  1.14-190 AddLeftUnitorInverse

  1.14-191 AddLeftUnitorInverseWithGivenTensorProduct

  1.14-192 AddLeftUnitorWithGivenTensorProduct

  1.14-193 AddRightUnitor

  1.14-194 AddRightUnitorInverse

  1.14-195 AddRightUnitorInverseWithGivenTensorProduct

  1.14-196 AddRightUnitorWithGivenTensorProduct

  1.14-197 AddTensorProductOnMorphisms

  1.14-198 AddTensorProductOnMorphismsWithGivenTensorProducts

  1.14-199 AddTensorProductOnObjects

  1.14-200 AddTensorUnit

  1.14-201 AddCoevaluationForDual

  1.14-202 AddCoevaluationForDualWithGivenTensorProduct

  1.14-203 AddIsomorphismFromInternalHomToTensorProductWithDualObject

  1.14-204 AddIsomorphismFromTensorProductWithDualObjectToInternalHom

  1.14-205 AddMorphismFromBidual

  1.14-206 AddMorphismFromBidualWithGivenBidual

  1.14-207 AddMorphismFromInternalHomToTensorProduct

  1.14-208 AddMorphismFromInternalHomToTensorProductWithGivenObjects

  1.14-209 AddRankMorphism

  1.14-210 AddTensorProductInternalHomCompatibilityMorphismInverse

  1.14-211 AddTensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects

  1.14-212 AddTraceMap

  1.14-213 AddCoRankMorphism

  1.14-214 AddCoTraceMap

  1.14-215 AddCoclosedCoevaluationForCoDual

  1.14-216 AddCoclosedCoevaluationForCoDualWithGivenTensorProduct

  1.14-217 AddInternalCoHomTensorProductCompatibilityMorphismInverse

  1.14-218 AddInternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects

  1.14-219 AddIsomorphismFromInternalCoHomToTensorProductWithCoDualObject

  1.14-220 AddIsomorphismFromTensorProductWithCoDualObjectToInternalCoHom

  1.14-221 AddMorphismFromTensorProductToInternalCoHom

  1.14-222 AddMorphismFromTensorProductToInternalCoHomWithGivenObjects

  1.14-223 AddMorphismToCoBidual

  1.14-224 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 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.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 Left Closed Monoidal Categories

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

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

The corresponding GAP property is called IsLeftClosedMonoidalCategory.

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

Returns: an object

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1.5-8 TensorProductToLeftInternalHomAdjunctMorphism
‣ TensorProductToLeftInternalHomAdjunctMorphism( a, b, f )( operation )

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

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

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

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

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

1.5-10 LeftInternalHomToTensorProductAdjunctMorphism
‣ LeftInternalHomToTensorProductAdjunctMorphism( b, c, g )( operation )

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Returns: an object

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

1.5-17 LeftDualOnMorphisms
‣ LeftDualOnMorphisms( alpha )( attribute )

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

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

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

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

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

1.5-19 LeftClosedMonoidalEvaluationForLeftDual
‣ LeftClosedMonoidalEvaluationForLeftDual( a )( attribute )

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

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

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

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

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

1.5-21 MorphismToLeftBidual
‣ MorphismToLeftBidual( a )( attribute )

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

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

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

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

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

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

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

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

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

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

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

1.5-25 TensorProductLeftDualityCompatibilityMorphism
‣ TensorProductLeftDualityCompatibilityMorphism( a, b )( operation )

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1.5-31 UniversalPropertyOfLeftDual
‣ UniversalPropertyOfLeftDual( t, a, alpha )( operation )

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

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

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

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

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

1.5-33 LeftClosedMonoidalLambdaElimination
‣ LeftClosedMonoidalLambdaElimination( a, b, alpha )( operation )

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1.6 Closed Monoidal Categories

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

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

The corresponding GAP property is called IsClosedMonoidalCategory.

1.6-1 InternalHomOnObjects
‣ InternalHomOnObjects( a, b )( operation )

Returns: an object

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

1.6-2 InternalHomOnMorphisms
‣ InternalHomOnMorphisms( alpha, beta )( operation )

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1.6-8 TensorProductToInternalHomRightAdjunctMorphism
‣ TensorProductToInternalHomRightAdjunctMorphism( a, b, f )( operation )

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

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

1.6-9 TensorProductToInternalHomRightAdjunctMorphismWithGivenInternalHom
‣ TensorProductToInternalHomRightAdjunctMorphismWithGivenInternalHom( a, b, f, i )( operation )

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

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

1.6-10 TensorProductToInternalHomRightAdjunctionIsomorphism
‣ TensorProductToInternalHomRightAdjunctionIsomorphism( a, b, c )( operation )

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

The arguments are three objects a,b,c. The output is the tri-natural isomorphism H(a \otimes b, c) \to H(b, \mathrm{\underline{Hom}}(a,c)) in the range category of the homomorphism structure H.

1.6-11 TensorProductToInternalHomRightAdjunctionIsomorphismWithGivenObjects
‣ TensorProductToInternalHomRightAdjunctionIsomorphismWithGivenObjects( s, a, b, c, r )( operation )

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

The arguments are fives objects s,a,b,c,r where s = H(a \otimes b, c) and r = H(b, \mathrm{\underline{Hom}}(a,c)). The output is the tri-natural isomorphism s \to r in the range category of the homomorphism structure H.

1.6-12 InternalHomToTensorProductRightAdjunctMorphism
‣ InternalHomToTensorProductRightAdjunctMorphism( a, c, g )( operation )

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

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

1.6-13 InternalHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct
‣ InternalHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct( a, c, g, s )( operation )

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

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

1.6-14 InternalHomToTensorProductRightAdjunctionIsomorphism
‣ InternalHomToTensorProductRightAdjunctionIsomorphism( a, b, c )( operation )

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

The arguments are three objects a,b,c. The output is the tri-natural isomorphism H(b, \mathrm{\underline{Hom}}(a,c)) \to H(a \otimes b, c) in the range category of the homomorphism structure H.

1.6-15 InternalHomToTensorProductRightAdjunctionIsomorphismWithGivenObjects
‣ InternalHomToTensorProductRightAdjunctionIsomorphismWithGivenObjects( s, a, b, c, r )( operation )

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

The arguments are fives objects s,a,b,c,r where s = H(b, \mathrm{\underline{Hom}}(a,c)) and r = H(a \otimes b, c). The output is the tri-natural isomorphism s \to r in the range category of the homomorphism structure H.

1.6-16 ClosedMonoidalLeftEvaluationMorphism
‣ ClosedMonoidalLeftEvaluationMorphism( a, b )( operation )

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

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

1.6-17 ClosedMonoidalLeftEvaluationMorphismWithGivenSource
‣ ClosedMonoidalLeftEvaluationMorphismWithGivenSource( a, b, s )( operation )

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

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

1.6-18 ClosedMonoidalLeftCoevaluationMorphism
‣ ClosedMonoidalLeftCoevaluationMorphism( a, b )( operation )

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

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

1.6-19 ClosedMonoidalLeftCoevaluationMorphismWithGivenRange
‣ ClosedMonoidalLeftCoevaluationMorphismWithGivenRange( a, b, r )( operation )

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

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

1.6-20 TensorProductToInternalHomLeftAdjunctMorphism
‣ TensorProductToInternalHomLeftAdjunctMorphism( a, b, f )( operation )

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

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

1.6-21 TensorProductToInternalHomLeftAdjunctMorphismWithGivenInternalHom
‣ TensorProductToInternalHomLeftAdjunctMorphismWithGivenInternalHom( a, b, f, i )( operation )

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

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

1.6-22 TensorProductToInternalHomLeftAdjunctionIsomorphism
‣ TensorProductToInternalHomLeftAdjunctionIsomorphism( a, b, c )( operation )

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

The arguments are three objects a,b,c. The output is the tri-natural isomorphism H(a \otimes b, c) \to H(a, \mathrm{\underline{Hom}}(b,c)) in the range category of the homomorphism structure H.

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

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

The arguments are fives objects s,a,b,c,r where s = H(a \otimes b, c) and r = H(a, \mathrm{\underline{Hom}}(b,c)). The output is the tri-natural isomorphism s \to r in the range category of the homomorphism structure H.

1.6-24 InternalHomToTensorProductLeftAdjunctMorphism
‣ InternalHomToTensorProductLeftAdjunctMorphism( b, c, g )( operation )

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

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

1.6-25 InternalHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct
‣ InternalHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct( b, c, g, s )( operation )

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

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

1.6-26 InternalHomToTensorProductLeftAdjunctionIsomorphism
‣ InternalHomToTensorProductLeftAdjunctionIsomorphism( a, b, c )( operation )

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

The arguments are three objects a,b,c. The output is the tri-natural isomorphism H(a, \mathrm{\underline{Hom}}(b,c)) \to H(a \otimes b, c) in the range category of the homomorphism structure H.

1.6-27 InternalHomToTensorProductLeftAdjunctionIsomorphismWithGivenObjects
‣ InternalHomToTensorProductLeftAdjunctionIsomorphismWithGivenObjects( s, a, b, c, r )( operation )

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

The arguments are fives objects s,a,b,c,r where s = H(a, \mathrm{\underline{Hom}}(b,c)) and r = H(a \otimes b, c). The output is the tri-natural isomorphism s \to r in the range category of the homomorphism structure H.

1.6-28 MonoidalPreComposeMorphism
‣ MonoidalPreComposeMorphism( a, b, c )( operation )

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

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

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

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

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

1.6-30 MonoidalPostComposeMorphism
‣ MonoidalPostComposeMorphism( a, b, c )( operation )

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

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

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

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

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

1.6-32 DualOnObjects
‣ DualOnObjects( a )( attribute )

Returns: an object

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

1.6-33 DualOnMorphisms
‣ DualOnMorphisms( alpha )( attribute )

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

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

1.6-34 DualOnMorphismsWithGivenDuals
‣ DualOnMorphismsWithGivenDuals( s, alpha, r )( operation )

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

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

1.6-35 EvaluationForDual
‣ EvaluationForDual( a )( attribute )

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

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

1.6-36 EvaluationForDualWithGivenTensorProduct
‣ EvaluationForDualWithGivenTensorProduct( s, a, r )( operation )

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

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

1.6-37 MorphismToBidual
‣ MorphismToBidual( a )( attribute )

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

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

1.6-38 MorphismToBidualWithGivenBidual
‣ MorphismToBidualWithGivenBidual( a, r )( operation )

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

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

1.6-39 TensorProductInternalHomCompatibilityMorphism
‣ TensorProductInternalHomCompatibilityMorphism( list )( operation )

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

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

1.6-40 TensorProductInternalHomCompatibilityMorphismWithGivenObjects
‣ TensorProductInternalHomCompatibilityMorphismWithGivenObjects( s, list, r )( operation )

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

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

1.6-41 TensorProductDualityCompatibilityMorphism
‣ TensorProductDualityCompatibilityMorphism( a, b )( operation )

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

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

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

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

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

1.6-43 MorphismFromTensorProductToInternalHom
‣ MorphismFromTensorProductToInternalHom( a, b )( operation )

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

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

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

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

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

1.6-45 IsomorphismFromDualObjectToInternalHomIntoTensorUnit
‣ IsomorphismFromDualObjectToInternalHomIntoTensorUnit( a )( attribute )

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

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

1.6-46 IsomorphismFromInternalHomIntoTensorUnitToDualObject
‣ IsomorphismFromInternalHomIntoTensorUnitToDualObject( a )( attribute )

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

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

1.6-47 UniversalPropertyOfDual
‣ UniversalPropertyOfDual( t, a, alpha )( operation )

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

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

1.6-48 LambdaIntroduction
‣ LambdaIntroduction( alpha )( attribute )

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

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

1.6-49 LambdaElimination
‣ LambdaElimination( a, b, alpha )( operation )

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

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

1.6-50 IsomorphismFromObjectToInternalHom
‣ IsomorphismFromObjectToInternalHom( a )( attribute )

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

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

1.6-51 IsomorphismFromObjectToInternalHomWithGivenInternalHom
‣ IsomorphismFromObjectToInternalHomWithGivenInternalHom( a, r )( operation )

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

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

1.6-52 IsomorphismFromInternalHomToObject
‣ IsomorphismFromInternalHomToObject( a )( attribute )

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

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

1.6-53 IsomorphismFromInternalHomToObjectWithGivenInternalHom
‣ IsomorphismFromInternalHomToObjectWithGivenInternalHom( a, s )( operation )

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

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

1.7 Left Coclosed Monoidal Categories

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

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

The corresponding GAP property is called IsLeftCoclosedMonoidalCategory.

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

Returns: an object

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1.7-8 TensorProductToLeftInternalCoHomAdjunctMorphism
‣ TensorProductToLeftInternalCoHomAdjunctMorphism( b, c, g )( operation )

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

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

1.7-9 TensorProductToLeftInternalCoHomAdjunctMorphismWithGivenLeftInternalCoHom
‣ TensorProductToLeftInternalCoHomAdjunctMorphismWithGivenLeftInternalCoHom( b, c, g, i )( operation )

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

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

1.7-10 LeftInternalCoHomToTensorProductAdjunctMorphism
‣ LeftInternalCoHomToTensorProductAdjunctMorphism( a, c, f )( operation )

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

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

1.7-11 LeftInternalCoHomToTensorProductAdjunctMorphismWithGivenTensorProduct
‣ LeftInternalCoHomToTensorProductAdjunctMorphismWithGivenTensorProduct( a, c, f, t )( operation )

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Returns: an object

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

1.7-17 LeftCoDualOnMorphisms
‣ LeftCoDualOnMorphisms( alpha )( attribute )

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

The argument is a morphism \alpha: a \rightarrow b. The output is its codual morphism \alpha_{\vee}: b_{\vee} \rightarrow a_{\vee}.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1.8 Coclosed Monoidal Categories

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

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

The corresponding GAP property is called IsCoclosedMonoidalCategory.

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

Returns: an object

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1.8-8 TensorProductToInternalCoHomRightAdjunctMorphism
‣ TensorProductToInternalCoHomRightAdjunctMorphism( b, c, g )( operation )

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

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

1.8-9 TensorProductToInternalCoHomRightAdjunctMorphismWithGivenInternalCoHom
‣ TensorProductToInternalCoHomRightAdjunctMorphismWithGivenInternalCoHom( b, c, g, i )( operation )

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

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

1.8-10 InternalCoHomToTensorProductRightAdjunctMorphism
‣ InternalCoHomToTensorProductRightAdjunctMorphism( a, b, f )( operation )

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

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

1.8-11 InternalCoHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct
‣ InternalCoHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct( a, b, f, t )( operation )

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1.8-16 TensorProductToInternalCoHomLeftAdjunctMorphism
‣ TensorProductToInternalCoHomLeftAdjunctMorphism( b, c, g )( operation )

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

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

1.8-17 TensorProductToInternalCoHomLeftAdjunctMorphismWithGivenInternalCoHom
‣ TensorProductToInternalCoHomLeftAdjunctMorphismWithGivenInternalCoHom( b, c, g, i )( operation )

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

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

1.8-18 InternalCoHomToTensorProductLeftAdjunctMorphism
‣ InternalCoHomToTensorProductLeftAdjunctMorphism( a, c, f )( operation )

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

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

1.8-19 InternalCoHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct
‣ InternalCoHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct( a, c, f, t )( operation )

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Returns: an object

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

1.8-25 CoDualOnMorphisms
‣ CoDualOnMorphisms( alpha )( attribute )

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

The argument is a morphism \alpha: a \rightarrow b. The output is its codual morphism \alpha_{\vee}: b_{\vee} \rightarrow a_{\vee}.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1.9 Symmetric Closed Monoidal Categories

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

The corresponding GAP property is given by IsSymmetricClosedMonoidalCategory.

1.10 Symmetric Coclosed Monoidal Categories

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

The corresponding GAP property is given by IsSymmetricCoclosedMonoidalCategory.

1.11 Rigid Symmetric Closed Monoidal Categories

A symmetric closed monoidal category \mathbf{C} satisfying

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

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

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

The corresponding GAP property is given by IsRigidSymmetricClosedMonoidalCategory.

1.11-1 IsomorphismFromTensorProductWithDualObjectToInternalHom
‣ IsomorphismFromTensorProductWithDualObjectToInternalHom( a, b )( operation )

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

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

1.11-2 IsomorphismFromInternalHomToTensorProductWithDualObject
‣ IsomorphismFromInternalHomToTensorProductWithDualObject( a, b )( operation )

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

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

1.11-3 MorphismFromInternalHomToTensorProduct
‣ MorphismFromInternalHomToTensorProduct( a, b )( operation )

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

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

1.11-4 MorphismFromInternalHomToTensorProductWithGivenObjects
‣ MorphismFromInternalHomToTensorProductWithGivenObjects( s, a, b, r )( operation )

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

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

1.11-5 TensorProductInternalHomCompatibilityMorphismInverse
‣ TensorProductInternalHomCompatibilityMorphismInverse( list )( operation )

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

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

1.11-6 TensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects
‣ TensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects( s, list, r )( operation )

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

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

1.11-7 CoevaluationForDual
‣ CoevaluationForDual( a )( attribute )

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

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

1.11-8 CoevaluationForDualWithGivenTensorProduct
‣ CoevaluationForDualWithGivenTensorProduct( s, a, r )( operation )

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

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

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

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

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

1.11-10 RankMorphism
‣ RankMorphism( a )( attribute )

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

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

1.11-11 MorphismFromBidual
‣ MorphismFromBidual( a )( attribute )

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

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

1.11-12 MorphismFromBidualWithGivenBidual
‣ MorphismFromBidualWithGivenBidual( a, s )( operation )

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

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

1.12 Rigid Symmetric Coclosed Monoidal Categories

A symmetric coclosed monoidal category \mathbf{C} satisfying

\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.12-1 IsomorphismFromInternalCoHomToTensorProductWithCoDualObject
‣ IsomorphismFromInternalCoHomToTensorProductWithCoDualObject( a, b )( operation )

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1.13 Convenience Methods

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

Returns: a cell

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

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

Returns: a cell

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

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

Returns: a cell

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

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

Returns: a cell

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

1.14 Add-methods

1.14-1 AddLeftDistributivityExpanding
‣ AddLeftDistributivityExpanding( C, F )( operation )
‣ AddLeftDistributivityExpanding( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, L ) \mapsto \mathtt{LeftDistributivityExpanding}(a, L).

1.14-2 AddLeftDistributivityExpandingWithGivenObjects
‣ AddLeftDistributivityExpandingWithGivenObjects( C, F )( operation )
‣ AddLeftDistributivityExpandingWithGivenObjects( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, L, r ) \mapsto \mathtt{LeftDistributivityExpandingWithGivenObjects}(s, a, L, r).

1.14-3 AddLeftDistributivityFactoring
‣ AddLeftDistributivityFactoring( C, F )( operation )
‣ AddLeftDistributivityFactoring( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, L ) \mapsto \mathtt{LeftDistributivityFactoring}(a, L).

1.14-4 AddLeftDistributivityFactoringWithGivenObjects
‣ AddLeftDistributivityFactoringWithGivenObjects( C, F )( operation )
‣ AddLeftDistributivityFactoringWithGivenObjects( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, L, r ) \mapsto \mathtt{LeftDistributivityFactoringWithGivenObjects}(s, a, L, r).

1.14-5 AddRightDistributivityExpanding
‣ AddRightDistributivityExpanding( C, F )( operation )
‣ AddRightDistributivityExpanding( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( L, a ) \mapsto \mathtt{RightDistributivityExpanding}(L, a).

1.14-6 AddRightDistributivityExpandingWithGivenObjects
‣ AddRightDistributivityExpandingWithGivenObjects( C, F )( operation )
‣ AddRightDistributivityExpandingWithGivenObjects( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, L, a, r ) \mapsto \mathtt{RightDistributivityExpandingWithGivenObjects}(s, L, a, r).

1.14-7 AddRightDistributivityFactoring
‣ AddRightDistributivityFactoring( C, F )( operation )
‣ AddRightDistributivityFactoring( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( L, a ) \mapsto \mathtt{RightDistributivityFactoring}(L, a).

1.14-8 AddRightDistributivityFactoringWithGivenObjects
‣ AddRightDistributivityFactoringWithGivenObjects( C, F )( operation )
‣ AddRightDistributivityFactoringWithGivenObjects( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, L, a, r ) \mapsto \mathtt{RightDistributivityFactoringWithGivenObjects}(s, L, a, r).

1.14-9 AddBraiding
‣ AddBraiding( C, F )( operation )
‣ AddBraiding( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{Braiding}(a, b).

1.14-10 AddBraidingInverse
‣ AddBraidingInverse( C, F )( operation )
‣ AddBraidingInverse( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{BraidingInverse}(a, b).

1.14-11 AddBraidingInverseWithGivenTensorProducts
‣ AddBraidingInverseWithGivenTensorProducts( C, F )( operation )
‣ AddBraidingInverseWithGivenTensorProducts( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, r ) \mapsto \mathtt{BraidingInverseWithGivenTensorProducts}(s, a, b, r).

1.14-12 AddBraidingWithGivenTensorProducts
‣ AddBraidingWithGivenTensorProducts( C, F )( operation )
‣ AddBraidingWithGivenTensorProducts( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, r ) \mapsto \mathtt{BraidingWithGivenTensorProducts}(s, a, b, r).

1.14-13 AddClosedMonoidalLeftCoevaluationMorphism
‣ AddClosedMonoidalLeftCoevaluationMorphism( C, F )( operation )
‣ AddClosedMonoidalLeftCoevaluationMorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation ClosedMonoidalLeftCoevaluationMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{ClosedMonoidalLeftCoevaluationMorphism}(a, b).

1.14-14 AddClosedMonoidalLeftCoevaluationMorphismWithGivenRange
‣ AddClosedMonoidalLeftCoevaluationMorphismWithGivenRange( C, F )( operation )
‣ AddClosedMonoidalLeftCoevaluationMorphismWithGivenRange( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation ClosedMonoidalLeftCoevaluationMorphismWithGivenRange. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, r ) \mapsto \mathtt{ClosedMonoidalLeftCoevaluationMorphismWithGivenRange}(a, b, r).

1.14-15 AddClosedMonoidalLeftEvaluationMorphism
‣ AddClosedMonoidalLeftEvaluationMorphism( C, F )( operation )
‣ AddClosedMonoidalLeftEvaluationMorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation ClosedMonoidalLeftEvaluationMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{ClosedMonoidalLeftEvaluationMorphism}(a, b).

1.14-16 AddClosedMonoidalLeftEvaluationMorphismWithGivenSource
‣ AddClosedMonoidalLeftEvaluationMorphismWithGivenSource( C, F )( operation )
‣ AddClosedMonoidalLeftEvaluationMorphismWithGivenSource( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation ClosedMonoidalLeftEvaluationMorphismWithGivenSource. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, s ) \mapsto \mathtt{ClosedMonoidalLeftEvaluationMorphismWithGivenSource}(a, b, s).

1.14-17 AddClosedMonoidalRightCoevaluationMorphism
‣ AddClosedMonoidalRightCoevaluationMorphism( C, F )( operation )
‣ AddClosedMonoidalRightCoevaluationMorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation ClosedMonoidalRightCoevaluationMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{ClosedMonoidalRightCoevaluationMorphism}(a, b).

1.14-18 AddClosedMonoidalRightCoevaluationMorphismWithGivenRange
‣ AddClosedMonoidalRightCoevaluationMorphismWithGivenRange( C, F )( operation )
‣ AddClosedMonoidalRightCoevaluationMorphismWithGivenRange( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation ClosedMonoidalRightCoevaluationMorphismWithGivenRange. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, r ) \mapsto \mathtt{ClosedMonoidalRightCoevaluationMorphismWithGivenRange}(a, b, r).

1.14-19 AddClosedMonoidalRightEvaluationMorphism
‣ AddClosedMonoidalRightEvaluationMorphism( C, F )( operation )
‣ AddClosedMonoidalRightEvaluationMorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation ClosedMonoidalRightEvaluationMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{ClosedMonoidalRightEvaluationMorphism}(a, b).

1.14-20 AddClosedMonoidalRightEvaluationMorphismWithGivenSource
‣ AddClosedMonoidalRightEvaluationMorphismWithGivenSource( C, F )( operation )
‣ AddClosedMonoidalRightEvaluationMorphismWithGivenSource( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation ClosedMonoidalRightEvaluationMorphismWithGivenSource. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, s ) \mapsto \mathtt{ClosedMonoidalRightEvaluationMorphismWithGivenSource}(a, b, s).

1.14-21 AddDualOnMorphisms
‣ AddDualOnMorphisms( C, F )( operation )
‣ AddDualOnMorphisms( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( alpha ) \mapsto \mathtt{DualOnMorphisms}(alpha).

1.14-22 AddDualOnMorphismsWithGivenDuals
‣ AddDualOnMorphismsWithGivenDuals( C, F )( operation )
‣ AddDualOnMorphismsWithGivenDuals( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, alpha, r ) \mapsto \mathtt{DualOnMorphismsWithGivenDuals}(s, alpha, r).

1.14-23 AddDualOnObjects
‣ AddDualOnObjects( C, F )( operation )
‣ AddDualOnObjects( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{DualOnObjects}(a).

1.14-24 AddEvaluationForDual
‣ AddEvaluationForDual( C, F )( operation )
‣ AddEvaluationForDual( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{EvaluationForDual}(a).

1.14-25 AddEvaluationForDualWithGivenTensorProduct
‣ AddEvaluationForDualWithGivenTensorProduct( C, F )( operation )
‣ AddEvaluationForDualWithGivenTensorProduct( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, r ) \mapsto \mathtt{EvaluationForDualWithGivenTensorProduct}(s, a, r).

1.14-26 AddInternalHomOnMorphisms
‣ AddInternalHomOnMorphisms( C, F )( operation )
‣ AddInternalHomOnMorphisms( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( alpha, beta ) \mapsto \mathtt{InternalHomOnMorphisms}(alpha, beta).

1.14-27 AddInternalHomOnMorphismsWithGivenInternalHoms
‣ AddInternalHomOnMorphismsWithGivenInternalHoms( C, F )( operation )
‣ AddInternalHomOnMorphismsWithGivenInternalHoms( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, alpha, beta, r ) \mapsto \mathtt{InternalHomOnMorphismsWithGivenInternalHoms}(s, alpha, beta, r).

1.14-28 AddInternalHomOnObjects
‣ AddInternalHomOnObjects( C, F )( operation )
‣ AddInternalHomOnObjects( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{InternalHomOnObjects}(a, b).

1.14-29 AddInternalHomToTensorProductLeftAdjunctMorphism
‣ AddInternalHomToTensorProductLeftAdjunctMorphism( C, F )( operation )
‣ AddInternalHomToTensorProductLeftAdjunctMorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation InternalHomToTensorProductLeftAdjunctMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( b, c, g ) \mapsto \mathtt{InternalHomToTensorProductLeftAdjunctMorphism}(b, c, g).

1.14-30 AddInternalHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct
‣ AddInternalHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct( C, F )( operation )
‣ AddInternalHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation InternalHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( b, c, g, s ) \mapsto \mathtt{InternalHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct}(b, c, g, s).

1.14-31 AddInternalHomToTensorProductLeftAdjunctionIsomorphism
‣ AddInternalHomToTensorProductLeftAdjunctionIsomorphism( C, F )( operation )
‣ AddInternalHomToTensorProductLeftAdjunctionIsomorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation InternalHomToTensorProductLeftAdjunctionIsomorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, c ) \mapsto \mathtt{InternalHomToTensorProductLeftAdjunctionIsomorphism}(a, b, c).

1.14-32 AddInternalHomToTensorProductLeftAdjunctionIsomorphismWithGivenObjects
‣ AddInternalHomToTensorProductLeftAdjunctionIsomorphismWithGivenObjects( C, F )( operation )
‣ AddInternalHomToTensorProductLeftAdjunctionIsomorphismWithGivenObjects( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation InternalHomToTensorProductLeftAdjunctionIsomorphismWithGivenObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, c, r ) \mapsto \mathtt{InternalHomToTensorProductLeftAdjunctionIsomorphismWithGivenObjects}(s, a, b, c, r).

1.14-33 AddInternalHomToTensorProductRightAdjunctMorphism
‣ AddInternalHomToTensorProductRightAdjunctMorphism( C, F )( operation )
‣ AddInternalHomToTensorProductRightAdjunctMorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation InternalHomToTensorProductRightAdjunctMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, c, g ) \mapsto \mathtt{InternalHomToTensorProductRightAdjunctMorphism}(a, c, g).

1.14-34 AddInternalHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct
‣ AddInternalHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct( C, F )( operation )
‣ AddInternalHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation InternalHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, c, g, s ) \mapsto \mathtt{InternalHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct}(a, c, g, s).

1.14-35 AddInternalHomToTensorProductRightAdjunctionIsomorphism
‣ AddInternalHomToTensorProductRightAdjunctionIsomorphism( C, F )( operation )
‣ AddInternalHomToTensorProductRightAdjunctionIsomorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation InternalHomToTensorProductRightAdjunctionIsomorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, c ) \mapsto \mathtt{InternalHomToTensorProductRightAdjunctionIsomorphism}(a, b, c).

1.14-36 AddInternalHomToTensorProductRightAdjunctionIsomorphismWithGivenObjects
‣ AddInternalHomToTensorProductRightAdjunctionIsomorphismWithGivenObjects( C, F )( operation )
‣ AddInternalHomToTensorProductRightAdjunctionIsomorphismWithGivenObjects( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation InternalHomToTensorProductRightAdjunctionIsomorphismWithGivenObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, c, r ) \mapsto \mathtt{InternalHomToTensorProductRightAdjunctionIsomorphismWithGivenObjects}(s, a, b, c, r).

1.14-37 AddIsomorphismFromDualObjectToInternalHomIntoTensorUnit
‣ AddIsomorphismFromDualObjectToInternalHomIntoTensorUnit( C, F )( operation )
‣ AddIsomorphismFromDualObjectToInternalHomIntoTensorUnit( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{IsomorphismFromDualObjectToInternalHomIntoTensorUnit}(a).

1.14-38 AddIsomorphismFromInternalHomIntoTensorUnitToDualObject
‣ AddIsomorphismFromInternalHomIntoTensorUnitToDualObject( C, F )( operation )
‣ AddIsomorphismFromInternalHomIntoTensorUnitToDualObject( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{IsomorphismFromInternalHomIntoTensorUnitToDualObject}(a).

1.14-39 AddIsomorphismFromInternalHomToObject
‣ AddIsomorphismFromInternalHomToObject( C, F )( operation )
‣ AddIsomorphismFromInternalHomToObject( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{IsomorphismFromInternalHomToObject}(a).

1.14-40 AddIsomorphismFromInternalHomToObjectWithGivenInternalHom
‣ AddIsomorphismFromInternalHomToObjectWithGivenInternalHom( C, F )( operation )
‣ AddIsomorphismFromInternalHomToObjectWithGivenInternalHom( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, s ) \mapsto \mathtt{IsomorphismFromInternalHomToObjectWithGivenInternalHom}(a, s).

1.14-41 AddIsomorphismFromObjectToInternalHom
‣ AddIsomorphismFromObjectToInternalHom( C, F )( operation )
‣ AddIsomorphismFromObjectToInternalHom( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{IsomorphismFromObjectToInternalHom}(a).

1.14-42 AddIsomorphismFromObjectToInternalHomWithGivenInternalHom
‣ AddIsomorphismFromObjectToInternalHomWithGivenInternalHom( C, F )( operation )
‣ AddIsomorphismFromObjectToInternalHomWithGivenInternalHom( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, r ) \mapsto \mathtt{IsomorphismFromObjectToInternalHomWithGivenInternalHom}(a, r).

1.14-43 AddLambdaElimination
‣ AddLambdaElimination( C, F )( operation )
‣ AddLambdaElimination( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, alpha ) \mapsto \mathtt{LambdaElimination}(a, b, alpha).

1.14-44 AddLambdaIntroduction
‣ AddLambdaIntroduction( C, F )( operation )
‣ AddLambdaIntroduction( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( alpha ) \mapsto \mathtt{LambdaIntroduction}(alpha).

1.14-45 AddMonoidalPostComposeMorphism
‣ AddMonoidalPostComposeMorphism( C, F )( operation )
‣ AddMonoidalPostComposeMorphism( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, c ) \mapsto \mathtt{MonoidalPostComposeMorphism}(a, b, c).

1.14-46 AddMonoidalPostComposeMorphismWithGivenObjects
‣ AddMonoidalPostComposeMorphismWithGivenObjects( C, F )( operation )
‣ AddMonoidalPostComposeMorphismWithGivenObjects( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, c, r ) \mapsto \mathtt{MonoidalPostComposeMorphismWithGivenObjects}(s, a, b, c, r).

1.14-47 AddMonoidalPreComposeMorphism
‣ AddMonoidalPreComposeMorphism( C, F )( operation )
‣ AddMonoidalPreComposeMorphism( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, c ) \mapsto \mathtt{MonoidalPreComposeMorphism}(a, b, c).

1.14-48 AddMonoidalPreComposeMorphismWithGivenObjects
‣ AddMonoidalPreComposeMorphismWithGivenObjects( C, F )( operation )
‣ AddMonoidalPreComposeMorphismWithGivenObjects( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, c, r ) \mapsto \mathtt{MonoidalPreComposeMorphismWithGivenObjects}(s, a, b, c, r).

1.14-49 AddMorphismFromTensorProductToInternalHom
‣ AddMorphismFromTensorProductToInternalHom( C, F )( operation )
‣ AddMorphismFromTensorProductToInternalHom( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{MorphismFromTensorProductToInternalHom}(a, b).

1.14-50 AddMorphismFromTensorProductToInternalHomWithGivenObjects
‣ AddMorphismFromTensorProductToInternalHomWithGivenObjects( C, F )( operation )
‣ AddMorphismFromTensorProductToInternalHomWithGivenObjects( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, r ) \mapsto \mathtt{MorphismFromTensorProductToInternalHomWithGivenObjects}(s, a, b, r).

1.14-51 AddMorphismToBidual
‣ AddMorphismToBidual( C, F )( operation )
‣ AddMorphismToBidual( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{MorphismToBidual}(a).

1.14-52 AddMorphismToBidualWithGivenBidual
‣ AddMorphismToBidualWithGivenBidual( C, F )( operation )
‣ AddMorphismToBidualWithGivenBidual( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, r ) \mapsto \mathtt{MorphismToBidualWithGivenBidual}(a, r).

1.14-53 AddTensorProductDualityCompatibilityMorphism
‣ AddTensorProductDualityCompatibilityMorphism( C, F )( operation )
‣ AddTensorProductDualityCompatibilityMorphism( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{TensorProductDualityCompatibilityMorphism}(a, b).

1.14-54 AddTensorProductDualityCompatibilityMorphismWithGivenObjects
‣ AddTensorProductDualityCompatibilityMorphismWithGivenObjects( C, F )( operation )
‣ AddTensorProductDualityCompatibilityMorphismWithGivenObjects( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, r ) \mapsto \mathtt{TensorProductDualityCompatibilityMorphismWithGivenObjects}(s, a, b, r).

1.14-55 AddTensorProductInternalHomCompatibilityMorphism
‣ AddTensorProductInternalHomCompatibilityMorphism( C, F )( operation )
‣ AddTensorProductInternalHomCompatibilityMorphism( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( list ) \mapsto \mathtt{TensorProductInternalHomCompatibilityMorphism}(list).

1.14-56 AddTensorProductInternalHomCompatibilityMorphismWithGivenObjects
‣ AddTensorProductInternalHomCompatibilityMorphismWithGivenObjects( C, F )( operation )
‣ AddTensorProductInternalHomCompatibilityMorphismWithGivenObjects( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( source, list, range ) \mapsto \mathtt{TensorProductInternalHomCompatibilityMorphismWithGivenObjects}(source, list, range).

1.14-57 AddTensorProductToInternalHomLeftAdjunctMorphism
‣ AddTensorProductToInternalHomLeftAdjunctMorphism( C, F )( operation )
‣ AddTensorProductToInternalHomLeftAdjunctMorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation TensorProductToInternalHomLeftAdjunctMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, f ) \mapsto \mathtt{TensorProductToInternalHomLeftAdjunctMorphism}(a, b, f).

1.14-58 AddTensorProductToInternalHomLeftAdjunctMorphismWithGivenInternalHom
‣ AddTensorProductToInternalHomLeftAdjunctMorphismWithGivenInternalHom( C, F )( operation )
‣ AddTensorProductToInternalHomLeftAdjunctMorphismWithGivenInternalHom( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation TensorProductToInternalHomLeftAdjunctMorphismWithGivenInternalHom. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, f, i ) \mapsto \mathtt{TensorProductToInternalHomLeftAdjunctMorphismWithGivenInternalHom}(a, b, f, i).

1.14-59 AddTensorProductToInternalHomLeftAdjunctionIsomorphism
‣ AddTensorProductToInternalHomLeftAdjunctionIsomorphism( C, F )( operation )
‣ AddTensorProductToInternalHomLeftAdjunctionIsomorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation TensorProductToInternalHomLeftAdjunctionIsomorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, c ) \mapsto \mathtt{TensorProductToInternalHomLeftAdjunctionIsomorphism}(a, b, c).

1.14-60 AddTensorProductToInternalHomLeftAdjunctionIsomorphismWithGivenObjects
‣ AddTensorProductToInternalHomLeftAdjunctionIsomorphismWithGivenObjects( C, F )( operation )
‣ AddTensorProductToInternalHomLeftAdjunctionIsomorphismWithGivenObjects( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation TensorProductToInternalHomLeftAdjunctionIsomorphismWithGivenObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, c, r ) \mapsto \mathtt{TensorProductToInternalHomLeftAdjunctionIsomorphismWithGivenObjects}(s, a, b, c, r).

1.14-61 AddTensorProductToInternalHomRightAdjunctMorphism
‣ AddTensorProductToInternalHomRightAdjunctMorphism( C, F )( operation )
‣ AddTensorProductToInternalHomRightAdjunctMorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation TensorProductToInternalHomRightAdjunctMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, f ) \mapsto \mathtt{TensorProductToInternalHomRightAdjunctMorphism}(a, b, f).

1.14-62 AddTensorProductToInternalHomRightAdjunctMorphismWithGivenInternalHom
‣ AddTensorProductToInternalHomRightAdjunctMorphismWithGivenInternalHom( C, F )( operation )
‣ AddTensorProductToInternalHomRightAdjunctMorphismWithGivenInternalHom( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation TensorProductToInternalHomRightAdjunctMorphismWithGivenInternalHom. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, f, i ) \mapsto \mathtt{TensorProductToInternalHomRightAdjunctMorphismWithGivenInternalHom}(a, b, f, i).

1.14-63 AddTensorProductToInternalHomRightAdjunctionIsomorphism
‣ AddTensorProductToInternalHomRightAdjunctionIsomorphism( C, F )( operation )
‣ AddTensorProductToInternalHomRightAdjunctionIsomorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation TensorProductToInternalHomRightAdjunctionIsomorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, c ) \mapsto \mathtt{TensorProductToInternalHomRightAdjunctionIsomorphism}(a, b, c).

1.14-64 AddTensorProductToInternalHomRightAdjunctionIsomorphismWithGivenObjects
‣ AddTensorProductToInternalHomRightAdjunctionIsomorphismWithGivenObjects( C, F )( operation )
‣ AddTensorProductToInternalHomRightAdjunctionIsomorphismWithGivenObjects( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation TensorProductToInternalHomRightAdjunctionIsomorphismWithGivenObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, c, r ) \mapsto \mathtt{TensorProductToInternalHomRightAdjunctionIsomorphismWithGivenObjects}(s, a, b, c, r).

1.14-65 AddUniversalPropertyOfDual
‣ AddUniversalPropertyOfDual( C, F )( operation )
‣ AddUniversalPropertyOfDual( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( t, a, alpha ) \mapsto \mathtt{UniversalPropertyOfDual}(t, a, alpha).

1.14-66 AddCoDualOnMorphisms
‣ AddCoDualOnMorphisms( C, F )( operation )
‣ AddCoDualOnMorphisms( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( alpha ) \mapsto \mathtt{CoDualOnMorphisms}(alpha).

1.14-67 AddCoDualOnMorphismsWithGivenCoDuals
‣ AddCoDualOnMorphismsWithGivenCoDuals( C, F )( operation )
‣ AddCoDualOnMorphismsWithGivenCoDuals( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, alpha, r ) \mapsto \mathtt{CoDualOnMorphismsWithGivenCoDuals}(s, alpha, r).

1.14-68 AddCoDualOnObjects
‣ AddCoDualOnObjects( C, F )( operation )
‣ AddCoDualOnObjects( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{CoDualOnObjects}(a).

1.14-69 AddCoDualityTensorProductCompatibilityMorphism
‣ AddCoDualityTensorProductCompatibilityMorphism( C, F )( operation )
‣ AddCoDualityTensorProductCompatibilityMorphism( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{CoDualityTensorProductCompatibilityMorphism}(a, b).

1.14-70 AddCoDualityTensorProductCompatibilityMorphismWithGivenObjects
‣ AddCoDualityTensorProductCompatibilityMorphismWithGivenObjects( C, F )( operation )
‣ AddCoDualityTensorProductCompatibilityMorphismWithGivenObjects( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, r ) \mapsto \mathtt{CoDualityTensorProductCompatibilityMorphismWithGivenObjects}(s, a, b, r).

1.14-71 AddCoLambdaElimination
‣ AddCoLambdaElimination( C, F )( operation )
‣ AddCoLambdaElimination( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, alpha ) \mapsto \mathtt{CoLambdaElimination}(a, b, alpha).

1.14-72 AddCoLambdaIntroduction
‣ AddCoLambdaIntroduction( C, F )( operation )
‣ AddCoLambdaIntroduction( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( alpha ) \mapsto \mathtt{CoLambdaIntroduction}(alpha).

1.14-73 AddCoclosedEvaluationForCoDual
‣ AddCoclosedEvaluationForCoDual( C, F )( operation )
‣ AddCoclosedEvaluationForCoDual( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{CoclosedEvaluationForCoDual}(a).

1.14-74 AddCoclosedEvaluationForCoDualWithGivenTensorProduct
‣ AddCoclosedEvaluationForCoDualWithGivenTensorProduct( C, F )( operation )
‣ AddCoclosedEvaluationForCoDualWithGivenTensorProduct( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, r ) \mapsto \mathtt{CoclosedEvaluationForCoDualWithGivenTensorProduct}(s, a, r).

1.14-75 AddCoclosedMonoidalLeftCoevaluationMorphism
‣ AddCoclosedMonoidalLeftCoevaluationMorphism( C, F )( operation )
‣ AddCoclosedMonoidalLeftCoevaluationMorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CoclosedMonoidalLeftCoevaluationMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{CoclosedMonoidalLeftCoevaluationMorphism}(a, b).

1.14-76 AddCoclosedMonoidalLeftCoevaluationMorphismWithGivenSource
‣ AddCoclosedMonoidalLeftCoevaluationMorphismWithGivenSource( C, F )( operation )
‣ AddCoclosedMonoidalLeftCoevaluationMorphismWithGivenSource( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CoclosedMonoidalLeftCoevaluationMorphismWithGivenSource. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, s ) \mapsto \mathtt{CoclosedMonoidalLeftCoevaluationMorphismWithGivenSource}(a, b, s).

1.14-77 AddCoclosedMonoidalLeftEvaluationMorphism
‣ AddCoclosedMonoidalLeftEvaluationMorphism( C, F )( operation )
‣ AddCoclosedMonoidalLeftEvaluationMorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CoclosedMonoidalLeftEvaluationMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{CoclosedMonoidalLeftEvaluationMorphism}(a, b).

1.14-78 AddCoclosedMonoidalLeftEvaluationMorphismWithGivenRange
‣ AddCoclosedMonoidalLeftEvaluationMorphismWithGivenRange( C, F )( operation )
‣ AddCoclosedMonoidalLeftEvaluationMorphismWithGivenRange( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CoclosedMonoidalLeftEvaluationMorphismWithGivenRange. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, r ) \mapsto \mathtt{CoclosedMonoidalLeftEvaluationMorphismWithGivenRange}(a, b, r).

1.14-79 AddCoclosedMonoidalRightCoevaluationMorphism
‣ AddCoclosedMonoidalRightCoevaluationMorphism( C, F )( operation )
‣ AddCoclosedMonoidalRightCoevaluationMorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CoclosedMonoidalRightCoevaluationMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{CoclosedMonoidalRightCoevaluationMorphism}(a, b).

1.14-80 AddCoclosedMonoidalRightCoevaluationMorphismWithGivenSource
‣ AddCoclosedMonoidalRightCoevaluationMorphismWithGivenSource( C, F )( operation )
‣ AddCoclosedMonoidalRightCoevaluationMorphismWithGivenSource( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CoclosedMonoidalRightCoevaluationMorphismWithGivenSource. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, s ) \mapsto \mathtt{CoclosedMonoidalRightCoevaluationMorphismWithGivenSource}(a, b, s).

1.14-81 AddCoclosedMonoidalRightEvaluationMorphism
‣ AddCoclosedMonoidalRightEvaluationMorphism( C, F )( operation )
‣ AddCoclosedMonoidalRightEvaluationMorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CoclosedMonoidalRightEvaluationMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{CoclosedMonoidalRightEvaluationMorphism}(a, b).

1.14-82 AddCoclosedMonoidalRightEvaluationMorphismWithGivenRange
‣ AddCoclosedMonoidalRightEvaluationMorphismWithGivenRange( C, F )( operation )
‣ AddCoclosedMonoidalRightEvaluationMorphismWithGivenRange( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CoclosedMonoidalRightEvaluationMorphismWithGivenRange. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, r ) \mapsto \mathtt{CoclosedMonoidalRightEvaluationMorphismWithGivenRange}(a, b, r).

1.14-83 AddInternalCoHomOnMorphisms
‣ AddInternalCoHomOnMorphisms( C, F )( operation )
‣ AddInternalCoHomOnMorphisms( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( alpha, beta ) \mapsto \mathtt{InternalCoHomOnMorphisms}(alpha, beta).

1.14-84 AddInternalCoHomOnMorphismsWithGivenInternalCoHoms
‣ AddInternalCoHomOnMorphismsWithGivenInternalCoHoms( C, F )( operation )
‣ AddInternalCoHomOnMorphismsWithGivenInternalCoHoms( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, alpha, beta, r ) \mapsto \mathtt{InternalCoHomOnMorphismsWithGivenInternalCoHoms}(s, alpha, beta, r).

1.14-85 AddInternalCoHomOnObjects
‣ AddInternalCoHomOnObjects( C, F )( operation )
‣ AddInternalCoHomOnObjects( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{InternalCoHomOnObjects}(a, b).

1.14-86 AddInternalCoHomTensorProductCompatibilityMorphism
‣ AddInternalCoHomTensorProductCompatibilityMorphism( C, F )( operation )
‣ AddInternalCoHomTensorProductCompatibilityMorphism( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( list ) \mapsto \mathtt{InternalCoHomTensorProductCompatibilityMorphism}(list).

1.14-87 AddInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects
‣ AddInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects( C, F )( operation )
‣ AddInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( source, list, range ) \mapsto \mathtt{InternalCoHomTensorProductCompatibilityMorphismWithGivenObjects}(source, list, range).

1.14-88 AddInternalCoHomToTensorProductLeftAdjunctMorphism
‣ AddInternalCoHomToTensorProductLeftAdjunctMorphism( C, F )( operation )
‣ AddInternalCoHomToTensorProductLeftAdjunctMorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation InternalCoHomToTensorProductLeftAdjunctMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, c, f ) \mapsto \mathtt{InternalCoHomToTensorProductLeftAdjunctMorphism}(a, c, f).

1.14-89 AddInternalCoHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct
‣ AddInternalCoHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct( C, F )( operation )
‣ AddInternalCoHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation InternalCoHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, c, f, t ) \mapsto \mathtt{InternalCoHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct}(a, c, f, t).

1.14-90 AddInternalCoHomToTensorProductRightAdjunctMorphism
‣ AddInternalCoHomToTensorProductRightAdjunctMorphism( C, F )( operation )
‣ AddInternalCoHomToTensorProductRightAdjunctMorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation InternalCoHomToTensorProductRightAdjunctMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, f ) \mapsto \mathtt{InternalCoHomToTensorProductRightAdjunctMorphism}(a, b, f).

1.14-91 AddInternalCoHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct
‣ AddInternalCoHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct( C, F )( operation )
‣ AddInternalCoHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation InternalCoHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, f, t ) \mapsto \mathtt{InternalCoHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct}(a, b, f, t).

1.14-92 AddIsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit
‣ AddIsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit( C, F )( operation )
‣ AddIsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{IsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit}(a).

1.14-93 AddIsomorphismFromInternalCoHomFromTensorUnitToCoDualObject
‣ AddIsomorphismFromInternalCoHomFromTensorUnitToCoDualObject( C, F )( operation )
‣ AddIsomorphismFromInternalCoHomFromTensorUnitToCoDualObject( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{IsomorphismFromInternalCoHomFromTensorUnitToCoDualObject}(a).

1.14-94 AddIsomorphismFromInternalCoHomToObject
‣ AddIsomorphismFromInternalCoHomToObject( C, F )( operation )
‣ AddIsomorphismFromInternalCoHomToObject( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{IsomorphismFromInternalCoHomToObject}(a).

1.14-95 AddIsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom
‣ AddIsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom( C, F )( operation )
‣ AddIsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, s ) \mapsto \mathtt{IsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom}(a, s).

1.14-96 AddIsomorphismFromObjectToInternalCoHom
‣ AddIsomorphismFromObjectToInternalCoHom( C, F )( operation )
‣ AddIsomorphismFromObjectToInternalCoHom( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{IsomorphismFromObjectToInternalCoHom}(a).

1.14-97 AddIsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom
‣ AddIsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom( C, F )( operation )
‣ AddIsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, r ) \mapsto \mathtt{IsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom}(a, r).

1.14-98 AddMonoidalPostCoComposeMorphism
‣ AddMonoidalPostCoComposeMorphism( C, F )( operation )
‣ AddMonoidalPostCoComposeMorphism( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, c ) \mapsto \mathtt{MonoidalPostCoComposeMorphism}(a, b, c).

1.14-99 AddMonoidalPostCoComposeMorphismWithGivenObjects
‣ AddMonoidalPostCoComposeMorphismWithGivenObjects( C, F )( operation )
‣ AddMonoidalPostCoComposeMorphismWithGivenObjects( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, c, r ) \mapsto \mathtt{MonoidalPostCoComposeMorphismWithGivenObjects}(s, a, b, c, r).

1.14-100 AddMonoidalPreCoComposeMorphism
‣ AddMonoidalPreCoComposeMorphism( C, F )( operation )
‣ AddMonoidalPreCoComposeMorphism( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, c ) \mapsto \mathtt{MonoidalPreCoComposeMorphism}(a, b, c).

1.14-101 AddMonoidalPreCoComposeMorphismWithGivenObjects
‣ AddMonoidalPreCoComposeMorphismWithGivenObjects( C, F )( operation )
‣ AddMonoidalPreCoComposeMorphismWithGivenObjects( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, c, r ) \mapsto \mathtt{MonoidalPreCoComposeMorphismWithGivenObjects}(s, a, b, c, r).

1.14-102 AddMorphismFromCoBidual
‣ AddMorphismFromCoBidual( C, F )( operation )
‣ AddMorphismFromCoBidual( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{MorphismFromCoBidual}(a).

1.14-103 AddMorphismFromCoBidualWithGivenCoBidual
‣ AddMorphismFromCoBidualWithGivenCoBidual( C, F )( operation )
‣ AddMorphismFromCoBidualWithGivenCoBidual( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, s ) \mapsto \mathtt{MorphismFromCoBidualWithGivenCoBidual}(a, s).

1.14-104 AddMorphismFromInternalCoHomToTensorProduct
‣ AddMorphismFromInternalCoHomToTensorProduct( C, F )( operation )
‣ AddMorphismFromInternalCoHomToTensorProduct( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{MorphismFromInternalCoHomToTensorProduct}(a, b).

1.14-105 AddMorphismFromInternalCoHomToTensorProductWithGivenObjects
‣ AddMorphismFromInternalCoHomToTensorProductWithGivenObjects( C, F )( operation )
‣ AddMorphismFromInternalCoHomToTensorProductWithGivenObjects( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, r ) \mapsto \mathtt{MorphismFromInternalCoHomToTensorProductWithGivenObjects}(s, a, b, r).

1.14-106 AddTensorProductToInternalCoHomLeftAdjunctMorphism
‣ AddTensorProductToInternalCoHomLeftAdjunctMorphism( C, F )( operation )
‣ AddTensorProductToInternalCoHomLeftAdjunctMorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation TensorProductToInternalCoHomLeftAdjunctMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( b, c, g ) \mapsto \mathtt{TensorProductToInternalCoHomLeftAdjunctMorphism}(b, c, g).

1.14-107 AddTensorProductToInternalCoHomLeftAdjunctMorphismWithGivenInternalCoHom
‣ AddTensorProductToInternalCoHomLeftAdjunctMorphismWithGivenInternalCoHom( C, F )( operation )
‣ AddTensorProductToInternalCoHomLeftAdjunctMorphismWithGivenInternalCoHom( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation TensorProductToInternalCoHomLeftAdjunctMorphismWithGivenInternalCoHom. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( b, c, g, i ) \mapsto \mathtt{TensorProductToInternalCoHomLeftAdjunctMorphismWithGivenInternalCoHom}(b, c, g, i).

1.14-108 AddTensorProductToInternalCoHomRightAdjunctMorphism
‣ AddTensorProductToInternalCoHomRightAdjunctMorphism( C, F )( operation )
‣ AddTensorProductToInternalCoHomRightAdjunctMorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation TensorProductToInternalCoHomRightAdjunctMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( b, c, g ) \mapsto \mathtt{TensorProductToInternalCoHomRightAdjunctMorphism}(b, c, g).

1.14-109 AddTensorProductToInternalCoHomRightAdjunctMorphismWithGivenInternalCoHom
‣ AddTensorProductToInternalCoHomRightAdjunctMorphismWithGivenInternalCoHom( C, F )( operation )
‣ AddTensorProductToInternalCoHomRightAdjunctMorphismWithGivenInternalCoHom( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation TensorProductToInternalCoHomRightAdjunctMorphismWithGivenInternalCoHom. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( b, c, g, i ) \mapsto \mathtt{TensorProductToInternalCoHomRightAdjunctMorphismWithGivenInternalCoHom}(b, c, g, i).

1.14-110 AddUniversalPropertyOfCoDual
‣ AddUniversalPropertyOfCoDual( C, F )( operation )
‣ AddUniversalPropertyOfCoDual( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( t, a, alpha ) \mapsto \mathtt{UniversalPropertyOfCoDual}(t, a, alpha).

1.14-111 AddIsomorphismFromLeftDualObjectToLeftInternalHomIntoTensorUnit
‣ AddIsomorphismFromLeftDualObjectToLeftInternalHomIntoTensorUnit( C, F )( operation )
‣ AddIsomorphismFromLeftDualObjectToLeftInternalHomIntoTensorUnit( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation IsomorphismFromLeftDualObjectToLeftInternalHomIntoTensorUnit. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{IsomorphismFromLeftDualObjectToLeftInternalHomIntoTensorUnit}(a).

1.14-112 AddIsomorphismFromLeftInternalHomIntoTensorUnitToLeftDualObject
‣ AddIsomorphismFromLeftInternalHomIntoTensorUnitToLeftDualObject( C, F )( operation )
‣ AddIsomorphismFromLeftInternalHomIntoTensorUnitToLeftDualObject( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation IsomorphismFromLeftInternalHomIntoTensorUnitToLeftDualObject. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{IsomorphismFromLeftInternalHomIntoTensorUnitToLeftDualObject}(a).

1.14-113 AddIsomorphismFromLeftInternalHomToObject
‣ AddIsomorphismFromLeftInternalHomToObject( C, F )( operation )
‣ AddIsomorphismFromLeftInternalHomToObject( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation IsomorphismFromLeftInternalHomToObject. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{IsomorphismFromLeftInternalHomToObject}(a).

1.14-114 AddIsomorphismFromLeftInternalHomToObjectWithGivenLeftInternalHom
‣ AddIsomorphismFromLeftInternalHomToObjectWithGivenLeftInternalHom( C, F )( operation )
‣ AddIsomorphismFromLeftInternalHomToObjectWithGivenLeftInternalHom( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation IsomorphismFromLeftInternalHomToObjectWithGivenLeftInternalHom. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, s ) \mapsto \mathtt{IsomorphismFromLeftInternalHomToObjectWithGivenLeftInternalHom}(a, s).

1.14-115 AddIsomorphismFromObjectToLeftInternalHom
‣ AddIsomorphismFromObjectToLeftInternalHom( C, F )( operation )
‣ AddIsomorphismFromObjectToLeftInternalHom( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation IsomorphismFromObjectToLeftInternalHom. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{IsomorphismFromObjectToLeftInternalHom}(a).

1.14-116 AddIsomorphismFromObjectToLeftInternalHomWithGivenLeftInternalHom
‣ AddIsomorphismFromObjectToLeftInternalHomWithGivenLeftInternalHom( C, F )( operation )
‣ AddIsomorphismFromObjectToLeftInternalHomWithGivenLeftInternalHom( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation IsomorphismFromObjectToLeftInternalHomWithGivenLeftInternalHom. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, r ) \mapsto \mathtt{IsomorphismFromObjectToLeftInternalHomWithGivenLeftInternalHom}(a, r).

1.14-117 AddLeftClosedMonoidalCoevaluationMorphism
‣ AddLeftClosedMonoidalCoevaluationMorphism( C, F )( operation )
‣ AddLeftClosedMonoidalCoevaluationMorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftClosedMonoidalCoevaluationMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{LeftClosedMonoidalCoevaluationMorphism}(a, b).

1.14-118 AddLeftClosedMonoidalCoevaluationMorphismWithGivenRange
‣ AddLeftClosedMonoidalCoevaluationMorphismWithGivenRange( C, F )( operation )
‣ AddLeftClosedMonoidalCoevaluationMorphismWithGivenRange( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftClosedMonoidalCoevaluationMorphismWithGivenRange. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, r ) \mapsto \mathtt{LeftClosedMonoidalCoevaluationMorphismWithGivenRange}(a, b, r).

1.14-119 AddLeftClosedMonoidalEvaluationForLeftDual
‣ AddLeftClosedMonoidalEvaluationForLeftDual( C, F )( operation )
‣ AddLeftClosedMonoidalEvaluationForLeftDual( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftClosedMonoidalEvaluationForLeftDual. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{LeftClosedMonoidalEvaluationForLeftDual}(a).

1.14-120 AddLeftClosedMonoidalEvaluationForLeftDualWithGivenTensorProduct
‣ AddLeftClosedMonoidalEvaluationForLeftDualWithGivenTensorProduct( C, F )( operation )
‣ AddLeftClosedMonoidalEvaluationForLeftDualWithGivenTensorProduct( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftClosedMonoidalEvaluationForLeftDualWithGivenTensorProduct. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, r ) \mapsto \mathtt{LeftClosedMonoidalEvaluationForLeftDualWithGivenTensorProduct}(s, a, r).

1.14-121 AddLeftClosedMonoidalEvaluationMorphism
‣ AddLeftClosedMonoidalEvaluationMorphism( C, F )( operation )
‣ AddLeftClosedMonoidalEvaluationMorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftClosedMonoidalEvaluationMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{LeftClosedMonoidalEvaluationMorphism}(a, b).

1.14-122 AddLeftClosedMonoidalEvaluationMorphismWithGivenSource
‣ AddLeftClosedMonoidalEvaluationMorphismWithGivenSource( C, F )( operation )
‣ AddLeftClosedMonoidalEvaluationMorphismWithGivenSource( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftClosedMonoidalEvaluationMorphismWithGivenSource. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, s ) \mapsto \mathtt{LeftClosedMonoidalEvaluationMorphismWithGivenSource}(a, b, s).

1.14-123 AddLeftClosedMonoidalLambdaElimination
‣ AddLeftClosedMonoidalLambdaElimination( C, F )( operation )
‣ AddLeftClosedMonoidalLambdaElimination( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftClosedMonoidalLambdaElimination. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, alpha ) \mapsto \mathtt{LeftClosedMonoidalLambdaElimination}(a, b, alpha).

1.14-124 AddLeftClosedMonoidalLambdaIntroduction
‣ AddLeftClosedMonoidalLambdaIntroduction( C, F )( operation )
‣ AddLeftClosedMonoidalLambdaIntroduction( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftClosedMonoidalLambdaIntroduction. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( alpha ) \mapsto \mathtt{LeftClosedMonoidalLambdaIntroduction}(alpha).

1.14-125 AddLeftClosedMonoidalPostComposeMorphism
‣ AddLeftClosedMonoidalPostComposeMorphism( C, F )( operation )
‣ AddLeftClosedMonoidalPostComposeMorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftClosedMonoidalPostComposeMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, c ) \mapsto \mathtt{LeftClosedMonoidalPostComposeMorphism}(a, b, c).

1.14-126 AddLeftClosedMonoidalPostComposeMorphismWithGivenObjects
‣ AddLeftClosedMonoidalPostComposeMorphismWithGivenObjects( C, F )( operation )
‣ AddLeftClosedMonoidalPostComposeMorphismWithGivenObjects( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftClosedMonoidalPostComposeMorphismWithGivenObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, c, r ) \mapsto \mathtt{LeftClosedMonoidalPostComposeMorphismWithGivenObjects}(s, a, b, c, r).

1.14-127 AddLeftClosedMonoidalPreComposeMorphism
‣ AddLeftClosedMonoidalPreComposeMorphism( C, F )( operation )
‣ AddLeftClosedMonoidalPreComposeMorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftClosedMonoidalPreComposeMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, c ) \mapsto \mathtt{LeftClosedMonoidalPreComposeMorphism}(a, b, c).

1.14-128 AddLeftClosedMonoidalPreComposeMorphismWithGivenObjects
‣ AddLeftClosedMonoidalPreComposeMorphismWithGivenObjects( C, F )( operation )
‣ AddLeftClosedMonoidalPreComposeMorphismWithGivenObjects( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftClosedMonoidalPreComposeMorphismWithGivenObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, c, r ) \mapsto \mathtt{LeftClosedMonoidalPreComposeMorphismWithGivenObjects}(s, a, b, c, r).

1.14-129 AddLeftDualOnMorphisms
‣ AddLeftDualOnMorphisms( C, F )( operation )
‣ AddLeftDualOnMorphisms( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftDualOnMorphisms. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( alpha ) \mapsto \mathtt{LeftDualOnMorphisms}(alpha).

1.14-130 AddLeftDualOnMorphismsWithGivenLeftDuals
‣ AddLeftDualOnMorphismsWithGivenLeftDuals( C, F )( operation )
‣ AddLeftDualOnMorphismsWithGivenLeftDuals( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftDualOnMorphismsWithGivenLeftDuals. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, alpha, r ) \mapsto \mathtt{LeftDualOnMorphismsWithGivenLeftDuals}(s, alpha, r).

1.14-131 AddLeftDualOnObjects
‣ AddLeftDualOnObjects( C, F )( operation )
‣ AddLeftDualOnObjects( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftDualOnObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{LeftDualOnObjects}(a).

1.14-132 AddLeftInternalHomOnMorphisms
‣ AddLeftInternalHomOnMorphisms( C, F )( operation )
‣ AddLeftInternalHomOnMorphisms( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftInternalHomOnMorphisms. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( alpha, beta ) \mapsto \mathtt{LeftInternalHomOnMorphisms}(alpha, beta).

1.14-133 AddLeftInternalHomOnMorphismsWithGivenLeftInternalHoms
‣ AddLeftInternalHomOnMorphismsWithGivenLeftInternalHoms( C, F )( operation )
‣ AddLeftInternalHomOnMorphismsWithGivenLeftInternalHoms( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftInternalHomOnMorphismsWithGivenLeftInternalHoms. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, alpha, beta, r ) \mapsto \mathtt{LeftInternalHomOnMorphismsWithGivenLeftInternalHoms}(s, alpha, beta, r).

1.14-134 AddLeftInternalHomOnObjects
‣ AddLeftInternalHomOnObjects( C, F )( operation )
‣ AddLeftInternalHomOnObjects( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftInternalHomOnObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{LeftInternalHomOnObjects}(a, b).

1.14-135 AddLeftInternalHomToTensorProductAdjunctMorphism
‣ AddLeftInternalHomToTensorProductAdjunctMorphism( C, F )( operation )
‣ AddLeftInternalHomToTensorProductAdjunctMorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftInternalHomToTensorProductAdjunctMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( b, c, g ) \mapsto \mathtt{LeftInternalHomToTensorProductAdjunctMorphism}(b, c, g).

1.14-136 AddLeftInternalHomToTensorProductAdjunctMorphismWithGivenTensorProduct
‣ AddLeftInternalHomToTensorProductAdjunctMorphismWithGivenTensorProduct( C, F )( operation )
‣ AddLeftInternalHomToTensorProductAdjunctMorphismWithGivenTensorProduct( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftInternalHomToTensorProductAdjunctMorphismWithGivenTensorProduct. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( b, c, g, t ) \mapsto \mathtt{LeftInternalHomToTensorProductAdjunctMorphismWithGivenTensorProduct}(b, c, g, t).

1.14-137 AddMorphismFromTensorProductToLeftInternalHom
‣ AddMorphismFromTensorProductToLeftInternalHom( C, F )( operation )
‣ AddMorphismFromTensorProductToLeftInternalHom( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation MorphismFromTensorProductToLeftInternalHom. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{MorphismFromTensorProductToLeftInternalHom}(a, b).

1.14-138 AddMorphismFromTensorProductToLeftInternalHomWithGivenObjects
‣ AddMorphismFromTensorProductToLeftInternalHomWithGivenObjects( C, F )( operation )
‣ AddMorphismFromTensorProductToLeftInternalHomWithGivenObjects( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation MorphismFromTensorProductToLeftInternalHomWithGivenObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, r ) \mapsto \mathtt{MorphismFromTensorProductToLeftInternalHomWithGivenObjects}(s, a, b, r).

1.14-139 AddMorphismToLeftBidual
‣ AddMorphismToLeftBidual( C, F )( operation )
‣ AddMorphismToLeftBidual( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation MorphismToLeftBidual. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{MorphismToLeftBidual}(a).

1.14-140 AddMorphismToLeftBidualWithGivenLeftBidual
‣ AddMorphismToLeftBidualWithGivenLeftBidual( C, F )( operation )
‣ AddMorphismToLeftBidualWithGivenLeftBidual( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation MorphismToLeftBidualWithGivenLeftBidual. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, r ) \mapsto \mathtt{MorphismToLeftBidualWithGivenLeftBidual}(a, r).

1.14-141 AddTensorProductLeftDualityCompatibilityMorphism
‣ AddTensorProductLeftDualityCompatibilityMorphism( C, F )( operation )
‣ AddTensorProductLeftDualityCompatibilityMorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation TensorProductLeftDualityCompatibilityMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{TensorProductLeftDualityCompatibilityMorphism}(a, b).

1.14-142 AddTensorProductLeftDualityCompatibilityMorphismWithGivenObjects
‣ AddTensorProductLeftDualityCompatibilityMorphismWithGivenObjects( C, F )( operation )
‣ AddTensorProductLeftDualityCompatibilityMorphismWithGivenObjects( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation TensorProductLeftDualityCompatibilityMorphismWithGivenObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, r ) \mapsto \mathtt{TensorProductLeftDualityCompatibilityMorphismWithGivenObjects}(s, a, b, r).

1.14-143 AddTensorProductLeftInternalHomCompatibilityMorphism
‣ AddTensorProductLeftInternalHomCompatibilityMorphism( C, F )( operation )
‣ AddTensorProductLeftInternalHomCompatibilityMorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation TensorProductLeftInternalHomCompatibilityMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( list ) \mapsto \mathtt{TensorProductLeftInternalHomCompatibilityMorphism}(list).

1.14-144 AddTensorProductLeftInternalHomCompatibilityMorphismWithGivenObjects
‣ AddTensorProductLeftInternalHomCompatibilityMorphismWithGivenObjects( C, F )( operation )
‣ AddTensorProductLeftInternalHomCompatibilityMorphismWithGivenObjects( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation TensorProductLeftInternalHomCompatibilityMorphismWithGivenObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( source, list, range ) \mapsto \mathtt{TensorProductLeftInternalHomCompatibilityMorphismWithGivenObjects}(source, list, range).

1.14-145 AddTensorProductToLeftInternalHomAdjunctMorphism
‣ AddTensorProductToLeftInternalHomAdjunctMorphism( C, F )( operation )
‣ AddTensorProductToLeftInternalHomAdjunctMorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation TensorProductToLeftInternalHomAdjunctMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, f ) \mapsto \mathtt{TensorProductToLeftInternalHomAdjunctMorphism}(a, b, f).

1.14-146 AddTensorProductToLeftInternalHomAdjunctMorphismWithGivenLeftInternalHom
‣ AddTensorProductToLeftInternalHomAdjunctMorphismWithGivenLeftInternalHom( C, F )( operation )
‣ AddTensorProductToLeftInternalHomAdjunctMorphismWithGivenLeftInternalHom( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation TensorProductToLeftInternalHomAdjunctMorphismWithGivenLeftInternalHom. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, f, i ) \mapsto \mathtt{TensorProductToLeftInternalHomAdjunctMorphismWithGivenLeftInternalHom}(a, b, f, i).

1.14-147 AddUniversalPropertyOfLeftDual
‣ AddUniversalPropertyOfLeftDual( C, F )( operation )
‣ AddUniversalPropertyOfLeftDual( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation UniversalPropertyOfLeftDual. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( t, a, alpha ) \mapsto \mathtt{UniversalPropertyOfLeftDual}(t, a, alpha).

1.14-148 AddIsomorphismFromLeftCoDualObjectToLeftInternalCoHomFromTensorUnit
‣ AddIsomorphismFromLeftCoDualObjectToLeftInternalCoHomFromTensorUnit( C, F )( operation )
‣ AddIsomorphismFromLeftCoDualObjectToLeftInternalCoHomFromTensorUnit( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation IsomorphismFromLeftCoDualObjectToLeftInternalCoHomFromTensorUnit. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{IsomorphismFromLeftCoDualObjectToLeftInternalCoHomFromTensorUnit}(a).

1.14-149 AddIsomorphismFromLeftInternalCoHomFromTensorUnitToLeftCoDualObject
‣ AddIsomorphismFromLeftInternalCoHomFromTensorUnitToLeftCoDualObject( C, F )( operation )
‣ AddIsomorphismFromLeftInternalCoHomFromTensorUnitToLeftCoDualObject( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation IsomorphismFromLeftInternalCoHomFromTensorUnitToLeftCoDualObject. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{IsomorphismFromLeftInternalCoHomFromTensorUnitToLeftCoDualObject}(a).

1.14-150 AddIsomorphismFromLeftInternalCoHomToObject
‣ AddIsomorphismFromLeftInternalCoHomToObject( C, F )( operation )
‣ AddIsomorphismFromLeftInternalCoHomToObject( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation IsomorphismFromLeftInternalCoHomToObject. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{IsomorphismFromLeftInternalCoHomToObject}(a).

1.14-151 AddIsomorphismFromLeftInternalCoHomToObjectWithGivenLeftInternalCoHom
‣ AddIsomorphismFromLeftInternalCoHomToObjectWithGivenLeftInternalCoHom( C, F )( operation )
‣ AddIsomorphismFromLeftInternalCoHomToObjectWithGivenLeftInternalCoHom( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation IsomorphismFromLeftInternalCoHomToObjectWithGivenLeftInternalCoHom. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, s ) \mapsto \mathtt{IsomorphismFromLeftInternalCoHomToObjectWithGivenLeftInternalCoHom}(a, s).

1.14-152 AddIsomorphismFromObjectToLeftInternalCoHom
‣ AddIsomorphismFromObjectToLeftInternalCoHom( C, F )( operation )
‣ AddIsomorphismFromObjectToLeftInternalCoHom( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation IsomorphismFromObjectToLeftInternalCoHom. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{IsomorphismFromObjectToLeftInternalCoHom}(a).

1.14-153 AddIsomorphismFromObjectToLeftInternalCoHomWithGivenLeftInternalCoHom
‣ AddIsomorphismFromObjectToLeftInternalCoHomWithGivenLeftInternalCoHom( C, F )( operation )
‣ AddIsomorphismFromObjectToLeftInternalCoHomWithGivenLeftInternalCoHom( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation IsomorphismFromObjectToLeftInternalCoHomWithGivenLeftInternalCoHom. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, r ) \mapsto \mathtt{IsomorphismFromObjectToLeftInternalCoHomWithGivenLeftInternalCoHom}(a, r).

1.14-154 AddLeftCoDualOnMorphisms
‣ AddLeftCoDualOnMorphisms( C, F )( operation )
‣ AddLeftCoDualOnMorphisms( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftCoDualOnMorphisms. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( alpha ) \mapsto \mathtt{LeftCoDualOnMorphisms}(alpha).

1.14-155 AddLeftCoDualOnMorphismsWithGivenLeftCoDuals
‣ AddLeftCoDualOnMorphismsWithGivenLeftCoDuals( C, F )( operation )
‣ AddLeftCoDualOnMorphismsWithGivenLeftCoDuals( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftCoDualOnMorphismsWithGivenLeftCoDuals. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, alpha, r ) \mapsto \mathtt{LeftCoDualOnMorphismsWithGivenLeftCoDuals}(s, alpha, r).

1.14-156 AddLeftCoDualOnObjects
‣ AddLeftCoDualOnObjects( C, F )( operation )
‣ AddLeftCoDualOnObjects( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftCoDualOnObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{LeftCoDualOnObjects}(a).

1.14-157 AddLeftCoDualityTensorProductCompatibilityMorphism
‣ AddLeftCoDualityTensorProductCompatibilityMorphism( C, F )( operation )
‣ AddLeftCoDualityTensorProductCompatibilityMorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftCoDualityTensorProductCompatibilityMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{LeftCoDualityTensorProductCompatibilityMorphism}(a, b).

1.14-158 AddLeftCoDualityTensorProductCompatibilityMorphismWithGivenObjects
‣ AddLeftCoDualityTensorProductCompatibilityMorphismWithGivenObjects( C, F )( operation )
‣ AddLeftCoDualityTensorProductCompatibilityMorphismWithGivenObjects( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftCoDualityTensorProductCompatibilityMorphismWithGivenObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, r ) \mapsto \mathtt{LeftCoDualityTensorProductCompatibilityMorphismWithGivenObjects}(s, a, b, r).

1.14-159 AddLeftCoclosedMonoidalCoevaluationMorphism
‣ AddLeftCoclosedMonoidalCoevaluationMorphism( C, F )( operation )
‣ AddLeftCoclosedMonoidalCoevaluationMorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftCoclosedMonoidalCoevaluationMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{LeftCoclosedMonoidalCoevaluationMorphism}(a, b).

1.14-160 AddLeftCoclosedMonoidalCoevaluationMorphismWithGivenSource
‣ AddLeftCoclosedMonoidalCoevaluationMorphismWithGivenSource( C, F )( operation )
‣ AddLeftCoclosedMonoidalCoevaluationMorphismWithGivenSource( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftCoclosedMonoidalCoevaluationMorphismWithGivenSource. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, s ) \mapsto \mathtt{LeftCoclosedMonoidalCoevaluationMorphismWithGivenSource}(a, b, s).

1.14-161 AddLeftCoclosedMonoidalEvaluationForLeftCoDual
‣ AddLeftCoclosedMonoidalEvaluationForLeftCoDual( C, F )( operation )
‣ AddLeftCoclosedMonoidalEvaluationForLeftCoDual( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftCoclosedMonoidalEvaluationForLeftCoDual. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{LeftCoclosedMonoidalEvaluationForLeftCoDual}(a).

1.14-162 AddLeftCoclosedMonoidalEvaluationForLeftCoDualWithGivenTensorProduct
‣ AddLeftCoclosedMonoidalEvaluationForLeftCoDualWithGivenTensorProduct( C, F )( operation )
‣ AddLeftCoclosedMonoidalEvaluationForLeftCoDualWithGivenTensorProduct( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftCoclosedMonoidalEvaluationForLeftCoDualWithGivenTensorProduct. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, r ) \mapsto \mathtt{LeftCoclosedMonoidalEvaluationForLeftCoDualWithGivenTensorProduct}(s, a, r).

1.14-163 AddLeftCoclosedMonoidalEvaluationMorphism
‣ AddLeftCoclosedMonoidalEvaluationMorphism( C, F )( operation )
‣ AddLeftCoclosedMonoidalEvaluationMorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftCoclosedMonoidalEvaluationMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{LeftCoclosedMonoidalEvaluationMorphism}(a, b).

1.14-164 AddLeftCoclosedMonoidalEvaluationMorphismWithGivenRange
‣ AddLeftCoclosedMonoidalEvaluationMorphismWithGivenRange( C, F )( operation )
‣ AddLeftCoclosedMonoidalEvaluationMorphismWithGivenRange( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftCoclosedMonoidalEvaluationMorphismWithGivenRange. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, r ) \mapsto \mathtt{LeftCoclosedMonoidalEvaluationMorphismWithGivenRange}(a, b, r).

1.14-165 AddLeftCoclosedMonoidalLambdaElimination
‣ AddLeftCoclosedMonoidalLambdaElimination( C, F )( operation )
‣ AddLeftCoclosedMonoidalLambdaElimination( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftCoclosedMonoidalLambdaElimination. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, alpha ) \mapsto \mathtt{LeftCoclosedMonoidalLambdaElimination}(a, b, alpha).

1.14-166 AddLeftCoclosedMonoidalLambdaIntroduction
‣ AddLeftCoclosedMonoidalLambdaIntroduction( C, F )( operation )
‣ AddLeftCoclosedMonoidalLambdaIntroduction( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftCoclosedMonoidalLambdaIntroduction. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( alpha ) \mapsto \mathtt{LeftCoclosedMonoidalLambdaIntroduction}(alpha).

1.14-167 AddLeftCoclosedMonoidalPostCoComposeMorphism
‣ AddLeftCoclosedMonoidalPostCoComposeMorphism( C, F )( operation )
‣ AddLeftCoclosedMonoidalPostCoComposeMorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftCoclosedMonoidalPostCoComposeMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, c ) \mapsto \mathtt{LeftCoclosedMonoidalPostCoComposeMorphism}(a, b, c).

1.14-168 AddLeftCoclosedMonoidalPostCoComposeMorphismWithGivenObjects
‣ AddLeftCoclosedMonoidalPostCoComposeMorphismWithGivenObjects( C, F )( operation )
‣ AddLeftCoclosedMonoidalPostCoComposeMorphismWithGivenObjects( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftCoclosedMonoidalPostCoComposeMorphismWithGivenObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, c, r ) \mapsto \mathtt{LeftCoclosedMonoidalPostCoComposeMorphismWithGivenObjects}(s, a, b, c, r).

1.14-169 AddLeftCoclosedMonoidalPreCoComposeMorphism
‣ AddLeftCoclosedMonoidalPreCoComposeMorphism( C, F )( operation )
‣ AddLeftCoclosedMonoidalPreCoComposeMorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftCoclosedMonoidalPreCoComposeMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, c ) \mapsto \mathtt{LeftCoclosedMonoidalPreCoComposeMorphism}(a, b, c).

1.14-170 AddLeftCoclosedMonoidalPreCoComposeMorphismWithGivenObjects
‣ AddLeftCoclosedMonoidalPreCoComposeMorphismWithGivenObjects( C, F )( operation )
‣ AddLeftCoclosedMonoidalPreCoComposeMorphismWithGivenObjects( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftCoclosedMonoidalPreCoComposeMorphismWithGivenObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, c, r ) \mapsto \mathtt{LeftCoclosedMonoidalPreCoComposeMorphismWithGivenObjects}(s, a, b, c, r).

1.14-171 AddLeftInternalCoHomOnMorphisms
‣ AddLeftInternalCoHomOnMorphisms( C, F )( operation )
‣ AddLeftInternalCoHomOnMorphisms( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftInternalCoHomOnMorphisms. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( alpha, beta ) \mapsto \mathtt{LeftInternalCoHomOnMorphisms}(alpha, beta).

1.14-172 AddLeftInternalCoHomOnMorphismsWithGivenLeftInternalCoHoms
‣ AddLeftInternalCoHomOnMorphismsWithGivenLeftInternalCoHoms( C, F )( operation )
‣ AddLeftInternalCoHomOnMorphismsWithGivenLeftInternalCoHoms( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftInternalCoHomOnMorphismsWithGivenLeftInternalCoHoms. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, alpha, beta, r ) \mapsto \mathtt{LeftInternalCoHomOnMorphismsWithGivenLeftInternalCoHoms}(s, alpha, beta, r).

1.14-173 AddLeftInternalCoHomOnObjects
‣ AddLeftInternalCoHomOnObjects( C, F )( operation )
‣ AddLeftInternalCoHomOnObjects( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftInternalCoHomOnObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{LeftInternalCoHomOnObjects}(a, b).

1.14-174 AddLeftInternalCoHomTensorProductCompatibilityMorphism
‣ AddLeftInternalCoHomTensorProductCompatibilityMorphism( C, F )( operation )
‣ AddLeftInternalCoHomTensorProductCompatibilityMorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftInternalCoHomTensorProductCompatibilityMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( list ) \mapsto \mathtt{LeftInternalCoHomTensorProductCompatibilityMorphism}(list).

1.14-175 AddLeftInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects
‣ AddLeftInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects( C, F )( operation )
‣ AddLeftInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( source, list, range ) \mapsto \mathtt{LeftInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects}(source, list, range).

1.14-176 AddLeftInternalCoHomToTensorProductAdjunctMorphism
‣ AddLeftInternalCoHomToTensorProductAdjunctMorphism( C, F )( operation )
‣ AddLeftInternalCoHomToTensorProductAdjunctMorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftInternalCoHomToTensorProductAdjunctMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, c, f ) \mapsto \mathtt{LeftInternalCoHomToTensorProductAdjunctMorphism}(a, c, f).

1.14-177 AddLeftInternalCoHomToTensorProductAdjunctMorphismWithGivenTensorProduct
‣ AddLeftInternalCoHomToTensorProductAdjunctMorphismWithGivenTensorProduct( C, F )( operation )
‣ AddLeftInternalCoHomToTensorProductAdjunctMorphismWithGivenTensorProduct( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftInternalCoHomToTensorProductAdjunctMorphismWithGivenTensorProduct. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, c, f, t ) \mapsto \mathtt{LeftInternalCoHomToTensorProductAdjunctMorphismWithGivenTensorProduct}(a, c, f, t).

1.14-178 AddMorphismFromLeftCoBidual
‣ AddMorphismFromLeftCoBidual( C, F )( operation )
‣ AddMorphismFromLeftCoBidual( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation MorphismFromLeftCoBidual. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{MorphismFromLeftCoBidual}(a).

1.14-179 AddMorphismFromLeftCoBidualWithGivenLeftCoBidual
‣ AddMorphismFromLeftCoBidualWithGivenLeftCoBidual( C, F )( operation )
‣ AddMorphismFromLeftCoBidualWithGivenLeftCoBidual( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation MorphismFromLeftCoBidualWithGivenLeftCoBidual. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, s ) \mapsto \mathtt{MorphismFromLeftCoBidualWithGivenLeftCoBidual}(a, s).

1.14-180 AddMorphismFromLeftInternalCoHomToTensorProduct
‣ AddMorphismFromLeftInternalCoHomToTensorProduct( C, F )( operation )
‣ AddMorphismFromLeftInternalCoHomToTensorProduct( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation MorphismFromLeftInternalCoHomToTensorProduct. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{MorphismFromLeftInternalCoHomToTensorProduct}(a, b).

1.14-181 AddMorphismFromLeftInternalCoHomToTensorProductWithGivenObjects
‣ AddMorphismFromLeftInternalCoHomToTensorProductWithGivenObjects( C, F )( operation )
‣ AddMorphismFromLeftInternalCoHomToTensorProductWithGivenObjects( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation MorphismFromLeftInternalCoHomToTensorProductWithGivenObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, r ) \mapsto \mathtt{MorphismFromLeftInternalCoHomToTensorProductWithGivenObjects}(s, a, b, r).

1.14-182 AddTensorProductToLeftInternalCoHomAdjunctMorphism
‣ AddTensorProductToLeftInternalCoHomAdjunctMorphism( C, F )( operation )
‣ AddTensorProductToLeftInternalCoHomAdjunctMorphism( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation TensorProductToLeftInternalCoHomAdjunctMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( b, c, g ) \mapsto \mathtt{TensorProductToLeftInternalCoHomAdjunctMorphism}(b, c, g).

1.14-183 AddTensorProductToLeftInternalCoHomAdjunctMorphismWithGivenLeftInternalCoHom
‣ AddTensorProductToLeftInternalCoHomAdjunctMorphismWithGivenLeftInternalCoHom( C, F )( operation )
‣ AddTensorProductToLeftInternalCoHomAdjunctMorphismWithGivenLeftInternalCoHom( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation TensorProductToLeftInternalCoHomAdjunctMorphismWithGivenLeftInternalCoHom. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( b, c, g, i ) \mapsto \mathtt{TensorProductToLeftInternalCoHomAdjunctMorphismWithGivenLeftInternalCoHom}(b, c, g, i).

1.14-184 AddUniversalPropertyOfLeftCoDual
‣ AddUniversalPropertyOfLeftCoDual( C, F )( operation )
‣ AddUniversalPropertyOfLeftCoDual( C, F, weight )( operation )

Returns: nothing

The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation UniversalPropertyOfLeftCoDual. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( t, a, alpha ) \mapsto \mathtt{UniversalPropertyOfLeftCoDual}(t, a, alpha).

1.14-185 AddAssociatorLeftToRight
‣ AddAssociatorLeftToRight( C, F )( operation )
‣ AddAssociatorLeftToRight( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, c ) \mapsto \mathtt{AssociatorLeftToRight}(a, b, c).

1.14-186 AddAssociatorLeftToRightWithGivenTensorProducts
‣ AddAssociatorLeftToRightWithGivenTensorProducts( C, F )( operation )
‣ AddAssociatorLeftToRightWithGivenTensorProducts( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, c, r ) \mapsto \mathtt{AssociatorLeftToRightWithGivenTensorProducts}(s, a, b, c, r).

1.14-187 AddAssociatorRightToLeft
‣ AddAssociatorRightToLeft( C, F )( operation )
‣ AddAssociatorRightToLeft( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b, c ) \mapsto \mathtt{AssociatorRightToLeft}(a, b, c).

1.14-188 AddAssociatorRightToLeftWithGivenTensorProducts
‣ AddAssociatorRightToLeftWithGivenTensorProducts( C, F )( operation )
‣ AddAssociatorRightToLeftWithGivenTensorProducts( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, c, r ) \mapsto \mathtt{AssociatorRightToLeftWithGivenTensorProducts}(s, a, b, c, r).

1.14-189 AddLeftUnitor
‣ AddLeftUnitor( C, F )( operation )
‣ AddLeftUnitor( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{LeftUnitor}(a).

1.14-190 AddLeftUnitorInverse
‣ AddLeftUnitorInverse( C, F )( operation )
‣ AddLeftUnitorInverse( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{LeftUnitorInverse}(a).

1.14-191 AddLeftUnitorInverseWithGivenTensorProduct
‣ AddLeftUnitorInverseWithGivenTensorProduct( C, F )( operation )
‣ AddLeftUnitorInverseWithGivenTensorProduct( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, r ) \mapsto \mathtt{LeftUnitorInverseWithGivenTensorProduct}(a, r).

1.14-192 AddLeftUnitorWithGivenTensorProduct
‣ AddLeftUnitorWithGivenTensorProduct( C, F )( operation )
‣ AddLeftUnitorWithGivenTensorProduct( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, s ) \mapsto \mathtt{LeftUnitorWithGivenTensorProduct}(a, s).

1.14-193 AddRightUnitor
‣ AddRightUnitor( C, F )( operation )
‣ AddRightUnitor( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{RightUnitor}(a).

1.14-194 AddRightUnitorInverse
‣ AddRightUnitorInverse( C, F )( operation )
‣ AddRightUnitorInverse( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{RightUnitorInverse}(a).

1.14-195 AddRightUnitorInverseWithGivenTensorProduct
‣ AddRightUnitorInverseWithGivenTensorProduct( C, F )( operation )
‣ AddRightUnitorInverseWithGivenTensorProduct( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, r ) \mapsto \mathtt{RightUnitorInverseWithGivenTensorProduct}(a, r).

1.14-196 AddRightUnitorWithGivenTensorProduct
‣ AddRightUnitorWithGivenTensorProduct( C, F )( operation )
‣ AddRightUnitorWithGivenTensorProduct( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, s ) \mapsto \mathtt{RightUnitorWithGivenTensorProduct}(a, s).

1.14-197 AddTensorProductOnMorphisms
‣ AddTensorProductOnMorphisms( C, F )( operation )
‣ AddTensorProductOnMorphisms( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( alpha, beta ) \mapsto \mathtt{TensorProductOnMorphisms}(alpha, beta).

1.14-198 AddTensorProductOnMorphismsWithGivenTensorProducts
‣ AddTensorProductOnMorphismsWithGivenTensorProducts( C, F )( operation )
‣ AddTensorProductOnMorphismsWithGivenTensorProducts( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, alpha, beta, r ) \mapsto \mathtt{TensorProductOnMorphismsWithGivenTensorProducts}(s, alpha, beta, r).

1.14-199 AddTensorProductOnObjects
‣ AddTensorProductOnObjects( C, F )( operation )
‣ AddTensorProductOnObjects( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( arg2, arg3 ) \mapsto \mathtt{TensorProductOnObjects}(arg2, arg3).

1.14-200 AddTensorUnit
‣ AddTensorUnit( C, F )( operation )
‣ AddTensorUnit( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( ) \mapsto \mathtt{TensorUnit}().

1.14-201 AddCoevaluationForDual
‣ AddCoevaluationForDual( C, F )( operation )
‣ AddCoevaluationForDual( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{CoevaluationForDual}(a).

1.14-202 AddCoevaluationForDualWithGivenTensorProduct
‣ AddCoevaluationForDualWithGivenTensorProduct( C, F )( operation )
‣ AddCoevaluationForDualWithGivenTensorProduct( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, r ) \mapsto \mathtt{CoevaluationForDualWithGivenTensorProduct}(s, a, r).

1.14-203 AddIsomorphismFromInternalHomToTensorProductWithDualObject
‣ AddIsomorphismFromInternalHomToTensorProductWithDualObject( C, F )( operation )
‣ AddIsomorphismFromInternalHomToTensorProductWithDualObject( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{IsomorphismFromInternalHomToTensorProductWithDualObject}(a, b).

1.14-204 AddIsomorphismFromTensorProductWithDualObjectToInternalHom
‣ AddIsomorphismFromTensorProductWithDualObjectToInternalHom( C, F )( operation )
‣ AddIsomorphismFromTensorProductWithDualObjectToInternalHom( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{IsomorphismFromTensorProductWithDualObjectToInternalHom}(a, b).

1.14-205 AddMorphismFromBidual
‣ AddMorphismFromBidual( C, F )( operation )
‣ AddMorphismFromBidual( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{MorphismFromBidual}(a).

1.14-206 AddMorphismFromBidualWithGivenBidual
‣ AddMorphismFromBidualWithGivenBidual( C, F )( operation )
‣ AddMorphismFromBidualWithGivenBidual( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, s ) \mapsto \mathtt{MorphismFromBidualWithGivenBidual}(a, s).

1.14-207 AddMorphismFromInternalHomToTensorProduct
‣ AddMorphismFromInternalHomToTensorProduct( C, F )( operation )
‣ AddMorphismFromInternalHomToTensorProduct( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{MorphismFromInternalHomToTensorProduct}(a, b).

1.14-208 AddMorphismFromInternalHomToTensorProductWithGivenObjects
‣ AddMorphismFromInternalHomToTensorProductWithGivenObjects( C, F )( operation )
‣ AddMorphismFromInternalHomToTensorProductWithGivenObjects( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, r ) \mapsto \mathtt{MorphismFromInternalHomToTensorProductWithGivenObjects}(s, a, b, r).

1.14-209 AddRankMorphism
‣ AddRankMorphism( C, F )( operation )
‣ AddRankMorphism( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{RankMorphism}(a).

1.14-210 AddTensorProductInternalHomCompatibilityMorphismInverse
‣ AddTensorProductInternalHomCompatibilityMorphismInverse( C, F )( operation )
‣ AddTensorProductInternalHomCompatibilityMorphismInverse( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( list ) \mapsto \mathtt{TensorProductInternalHomCompatibilityMorphismInverse}(list).

1.14-211 AddTensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects
‣ AddTensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects( C, F )( operation )
‣ AddTensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( source, list, range ) \mapsto \mathtt{TensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects}(source, list, range).

1.14-212 AddTraceMap
‣ AddTraceMap( C, F )( operation )
‣ AddTraceMap( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( alpha ) \mapsto \mathtt{TraceMap}(alpha).

1.14-213 AddCoRankMorphism
‣ AddCoRankMorphism( C, F )( operation )
‣ AddCoRankMorphism( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{CoRankMorphism}(a).

1.14-214 AddCoTraceMap
‣ AddCoTraceMap( C, F )( operation )
‣ AddCoTraceMap( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( alpha ) \mapsto \mathtt{CoTraceMap}(alpha).

1.14-215 AddCoclosedCoevaluationForCoDual
‣ AddCoclosedCoevaluationForCoDual( C, F )( operation )
‣ AddCoclosedCoevaluationForCoDual( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{CoclosedCoevaluationForCoDual}(a).

1.14-216 AddCoclosedCoevaluationForCoDualWithGivenTensorProduct
‣ AddCoclosedCoevaluationForCoDualWithGivenTensorProduct( C, F )( operation )
‣ AddCoclosedCoevaluationForCoDualWithGivenTensorProduct( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, r ) \mapsto \mathtt{CoclosedCoevaluationForCoDualWithGivenTensorProduct}(s, a, r).

1.14-217 AddInternalCoHomTensorProductCompatibilityMorphismInverse
‣ AddInternalCoHomTensorProductCompatibilityMorphismInverse( C, F )( operation )
‣ AddInternalCoHomTensorProductCompatibilityMorphismInverse( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( list ) \mapsto \mathtt{InternalCoHomTensorProductCompatibilityMorphismInverse}(list).

1.14-218 AddInternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects
‣ AddInternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects( C, F )( operation )
‣ AddInternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( source, list, range ) \mapsto \mathtt{InternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects}(source, list, range).

1.14-219 AddIsomorphismFromInternalCoHomToTensorProductWithCoDualObject
‣ AddIsomorphismFromInternalCoHomToTensorProductWithCoDualObject( C, F )( operation )
‣ AddIsomorphismFromInternalCoHomToTensorProductWithCoDualObject( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{IsomorphismFromInternalCoHomToTensorProductWithCoDualObject}(a, b).

1.14-220 AddIsomorphismFromTensorProductWithCoDualObjectToInternalCoHom
‣ AddIsomorphismFromTensorProductWithCoDualObjectToInternalCoHom( C, F )( operation )
‣ AddIsomorphismFromTensorProductWithCoDualObjectToInternalCoHom( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{IsomorphismFromTensorProductWithCoDualObjectToInternalCoHom}(a, b).

1.14-221 AddMorphismFromTensorProductToInternalCoHom
‣ AddMorphismFromTensorProductToInternalCoHom( C, F )( operation )
‣ AddMorphismFromTensorProductToInternalCoHom( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, b ) \mapsto \mathtt{MorphismFromTensorProductToInternalCoHom}(a, b).

1.14-222 AddMorphismFromTensorProductToInternalCoHomWithGivenObjects
‣ AddMorphismFromTensorProductToInternalCoHomWithGivenObjects( C, F )( operation )
‣ AddMorphismFromTensorProductToInternalCoHomWithGivenObjects( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( s, a, b, r ) \mapsto \mathtt{MorphismFromTensorProductToInternalCoHomWithGivenObjects}(s, a, b, r).

1.14-223 AddMorphismToCoBidual
‣ AddMorphismToCoBidual( C, F )( operation )
‣ AddMorphismToCoBidual( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a ) \mapsto \mathtt{MorphismToCoBidual}(a).

1.14-224 AddMorphismToCoBidualWithGivenCoBidual
‣ AddMorphismToCoBidualWithGivenCoBidual( C, F )( operation )
‣ AddMorphismToCoBidualWithGivenCoBidual( C, F, weight )( operation )

Returns: nothing

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. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). F: ( a, r ) \mapsto \mathtt{MorphismToCoBidualWithGivenCoBidual}(a, r).

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

generated by GAPDoc2HTML