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

1 Cartesian Categories
 1.1 Cartesian Categories
 1.2 Cartesian Closed Categories

  1.2-1 ExponentialOnObjects

  1.2-2 ExponentialOnMorphisms

  1.2-3 ExponentialOnMorphismsWithGivenExponentials

  1.2-4 CartesianRightEvaluationMorphism

  1.2-5 CartesianRightEvaluationMorphismWithGivenSource

  1.2-6 CartesianRightCoevaluationMorphism

  1.2-7 CartesianRightCoevaluationMorphismWithGivenRange

  1.2-8 DirectProductToExponentialRightAdjunctMorphism

  1.2-9 DirectProductToExponentialRightAdjunctMorphismWithGivenExponential

  1.2-10 DirectProductToExponentialRightAdjunctionIsomorphism

  1.2-11 DirectProductToExponentialRightAdjunctionIsomorphismWithGivenObjects

  1.2-12 ExponentialToDirectProductRightAdjunctMorphism

  1.2-13 ExponentialToDirectProductRightAdjunctMorphismWithGivenDirectProduct

  1.2-14 ExponentialToDirectProductRightAdjunctionIsomorphism

  1.2-15 ExponentialToDirectProductRightAdjunctionIsomorphismWithGivenObjects

  1.2-16 CartesianLeftEvaluationMorphism

  1.2-17 CartesianLeftEvaluationMorphismWithGivenSource

  1.2-18 CartesianLeftCoevaluationMorphism

  1.2-19 CartesianLeftCoevaluationMorphismWithGivenRange

  1.2-20 DirectProductToExponentialLeftAdjunctMorphism

  1.2-21 DirectProductToExponentialLeftAdjunctMorphismWithGivenExponential

  1.2-22 DirectProductToExponentialLeftAdjunctionIsomorphism

  1.2-23 DirectProductToExponentialLeftAdjunctionIsomorphismWithGivenObjects

  1.2-24 ExponentialToDirectProductLeftAdjunctMorphism

  1.2-25 ExponentialToDirectProductLeftAdjunctMorphismWithGivenDirectProduct

  1.2-26 ExponentialToDirectProductLeftAdjunctionIsomorphism

  1.2-27 ExponentialToDirectProductLeftAdjunctionIsomorphismWithGivenObjects

  1.2-28 CartesianPreComposeMorphism

  1.2-29 CartesianPreComposeMorphismWithGivenObjects

  1.2-30 CartesianPostComposeMorphism

  1.2-31 CartesianPostComposeMorphismWithGivenObjects

  1.2-32 CartesianDualOnObjects

  1.2-33 CartesianDualOnMorphisms

  1.2-34 CartesianDualOnMorphismsWithGivenCartesianDuals

  1.2-35 CartesianEvaluationForCartesianDual

  1.2-36 CartesianEvaluationForCartesianDualWithGivenDirectProduct

  1.2-37 MorphismToCartesianBidual

  1.2-38 MorphismToCartesianBidualWithGivenCartesianBidual

  1.2-39 DirectProductExponentialCompatibilityMorphism

  1.2-40 DirectProductExponentialCompatibilityMorphismWithGivenObjects

  1.2-41 DirectProductCartesianDualityCompatibilityMorphism

  1.2-42 DirectProductCartesianDualityCompatibilityMorphismWithGivenObjects

  1.2-43 MorphismFromDirectProductToExponential

  1.2-44 MorphismFromDirectProductToExponentialWithGivenObjects

  1.2-45 IsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject

  1.2-46 IsomorphismFromExponentialIntoTerminalObjectToCartesianDualObject

  1.2-47 UniversalPropertyOfCartesianDual

  1.2-48 CartesianLambdaIntroduction

  1.2-49 CartesianLambdaElimination

  1.2-50 IsomorphismFromObjectToExponential

  1.2-51 IsomorphismFromObjectToExponentialWithGivenExponential

  1.2-52 IsomorphismFromExponentialToObject

  1.2-53 IsomorphismFromExponentialToObjectWithGivenExponential
 1.3 Convenience Methods
 1.4 Add-methods

  1.4-1 AddCartesianBraiding

  1.4-2 AddCartesianBraidingInverse

  1.4-3 AddCartesianBraidingInverseWithGivenDirectProducts

  1.4-4 AddCartesianBraidingWithGivenDirectProducts

  1.4-5 AddCartesianAssociatorLeftToRight

  1.4-6 AddCartesianAssociatorLeftToRightWithGivenDirectProducts

  1.4-7 AddCartesianAssociatorRightToLeft

  1.4-8 AddCartesianAssociatorRightToLeftWithGivenDirectProducts

  1.4-9 AddCartesianDiagonal

  1.4-10 AddCartesianDiagonalWithGivenCartesianPower

  1.4-11 AddCartesianLeftUnitor

  1.4-12 AddCartesianLeftUnitorInverse

  1.4-13 AddCartesianLeftUnitorInverseWithGivenDirectProduct

  1.4-14 AddCartesianLeftUnitorWithGivenDirectProduct

  1.4-15 AddCartesianRightUnitor

  1.4-16 AddCartesianRightUnitorInverse

  1.4-17 AddCartesianRightUnitorInverseWithGivenDirectProduct

  1.4-18 AddCartesianRightUnitorWithGivenDirectProduct

  1.4-19 AddDirectProductOnMorphisms

  1.4-20 AddDirectProductOnMorphismsWithGivenDirectProducts

  1.4-21 AddCartesianDualOnMorphisms

  1.4-22 AddCartesianDualOnMorphismsWithGivenCartesianDuals

  1.4-23 AddCartesianDualOnObjects

  1.4-24 AddCartesianEvaluationForCartesianDual

  1.4-25 AddCartesianEvaluationForCartesianDualWithGivenDirectProduct

  1.4-26 AddCartesianLambdaElimination

  1.4-27 AddCartesianLambdaIntroduction

  1.4-28 AddCartesianLeftCoevaluationMorphism

  1.4-29 AddCartesianLeftCoevaluationMorphismWithGivenRange

  1.4-30 AddCartesianLeftEvaluationMorphism

  1.4-31 AddCartesianLeftEvaluationMorphismWithGivenSource

  1.4-32 AddCartesianPostComposeMorphism

  1.4-33 AddCartesianPostComposeMorphismWithGivenObjects

  1.4-34 AddCartesianPreComposeMorphism

  1.4-35 AddCartesianPreComposeMorphismWithGivenObjects

  1.4-36 AddCartesianRightCoevaluationMorphism

  1.4-37 AddCartesianRightCoevaluationMorphismWithGivenRange

  1.4-38 AddCartesianRightEvaluationMorphism

  1.4-39 AddCartesianRightEvaluationMorphismWithGivenSource

  1.4-40 AddDirectProductCartesianDualityCompatibilityMorphism

  1.4-41 AddDirectProductCartesianDualityCompatibilityMorphismWithGivenObjects

  1.4-42 AddDirectProductExponentialCompatibilityMorphism

  1.4-43 AddDirectProductExponentialCompatibilityMorphismWithGivenObjects

  1.4-44 AddDirectProductToExponentialLeftAdjunctMorphism

  1.4-45 AddDirectProductToExponentialLeftAdjunctMorphismWithGivenExponential

  1.4-46 AddDirectProductToExponentialLeftAdjunctionIsomorphism

  1.4-47 AddDirectProductToExponentialLeftAdjunctionIsomorphismWithGivenObjects

  1.4-48 AddDirectProductToExponentialRightAdjunctMorphism

  1.4-49 AddDirectProductToExponentialRightAdjunctMorphismWithGivenExponential

  1.4-50 AddDirectProductToExponentialRightAdjunctionIsomorphism

  1.4-51 AddDirectProductToExponentialRightAdjunctionIsomorphismWithGivenObjects

  1.4-52 AddExponentialOnMorphisms

  1.4-53 AddExponentialOnMorphismsWithGivenExponentials

  1.4-54 AddExponentialOnObjects

  1.4-55 AddExponentialToDirectProductLeftAdjunctMorphism

  1.4-56 AddExponentialToDirectProductLeftAdjunctMorphismWithGivenDirectProduct

  1.4-57 AddExponentialToDirectProductLeftAdjunctionIsomorphism

  1.4-58 AddExponentialToDirectProductLeftAdjunctionIsomorphismWithGivenObjects

  1.4-59 AddExponentialToDirectProductRightAdjunctMorphism

  1.4-60 AddExponentialToDirectProductRightAdjunctMorphismWithGivenDirectProduct

  1.4-61 AddExponentialToDirectProductRightAdjunctionIsomorphism

  1.4-62 AddExponentialToDirectProductRightAdjunctionIsomorphismWithGivenObjects

  1.4-63 AddIsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject

  1.4-64 AddIsomorphismFromExponentialIntoTerminalObjectToCartesianDualObject

  1.4-65 AddIsomorphismFromExponentialToObject

  1.4-66 AddIsomorphismFromExponentialToObjectWithGivenExponential

  1.4-67 AddIsomorphismFromObjectToExponential

  1.4-68 AddIsomorphismFromObjectToExponentialWithGivenExponential

  1.4-69 AddMorphismFromDirectProductToExponential

  1.4-70 AddMorphismFromDirectProductToExponentialWithGivenObjects

  1.4-71 AddMorphismToCartesianBidual

  1.4-72 AddMorphismToCartesianBidualWithGivenCartesianBidual

  1.4-73 AddUniversalPropertyOfCartesianDual

  1.4-74 AddLeftCartesianDistributivityExpanding

  1.4-75 AddLeftCartesianDistributivityExpandingWithGivenObjects

  1.4-76 AddLeftCartesianDistributivityFactoring

  1.4-77 AddLeftCartesianDistributivityFactoringWithGivenObjects

  1.4-78 AddRightCartesianDistributivityExpanding

  1.4-79 AddRightCartesianDistributivityExpandingWithGivenObjects

  1.4-80 AddRightCartesianDistributivityFactoring

  1.4-81 AddRightCartesianDistributivityFactoringWithGivenObjects

1 Cartesian Categories

1.1 Cartesian Categories

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

is called a cartesian category, if

\((\alpha_{a,b,c} \times \mathrm{id}_d) \circ \alpha_{a,b \times c, d} \circ ( \mathrm{id}_a \times \alpha_{b,c,d} ) = \alpha_{a \times b, c, d} \circ \alpha_{a,b,c \times d}\),

\(( \rho_a \times \mathrm{id}_c ) \circ \alpha_{a,1,c} = \mathrm{id}_a \times \lambda_c\).

The corresponding GAP property is given by IsCartesianCategory.

1.1-1 CartesianBraiding
‣ CartesianBraiding( a, b )( operation )

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

The arguments are two objects \(a,b\). The output is the braiding \( B_{a,b}: a \times b \rightarrow b \times a\).

1.1-2 CartesianBraidingWithGivenDirectProducts
‣ CartesianBraidingWithGivenDirectProducts( s, a, b, r )( operation )

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

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

1.1-3 CartesianBraidingInverse
‣ CartesianBraidingInverse( a, b )( operation )

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

The arguments are two objects \(a,b\). The output is the inverse braiding \( B_{a,b}^{-1}: b \times a \rightarrow a \times b\).

1.1-4 CartesianBraidingInverseWithGivenDirectProducts
‣ CartesianBraidingInverseWithGivenDirectProducts( s, a, b, r )( operation )

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

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

1.1-5 DirectProductOnMorphisms
‣ DirectProductOnMorphisms( alpha, beta )( operation )

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

The arguments are two morphisms \(\alpha: a \rightarrow a', \beta: b \rightarrow b'\). The output is the direct product \(\alpha \times \beta\).

1.1-6 DirectProductOnMorphismsWithGivenDirectProducts
‣ DirectProductOnMorphismsWithGivenDirectProducts( s, alpha, beta, r )( operation )

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

The arguments are an object \(s = a \times b\), two morphisms \(\alpha: a \rightarrow a', \beta: b \rightarrow b'\), and an object \(r = a' \times b'\). The output is the direct product \(\alpha \times \beta\).

1.1-7 CartesianAssociatorRightToLeft
‣ CartesianAssociatorRightToLeft( a, b, c )( operation )

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

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

1.1-8 CartesianAssociatorRightToLeftWithGivenDirectProducts
‣ CartesianAssociatorRightToLeftWithGivenDirectProducts( s, a, b, c, r )( operation )

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

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

1.1-9 CartesianAssociatorLeftToRight
‣ CartesianAssociatorLeftToRight( a, b, c )( operation )

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

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

1.1-10 CartesianAssociatorLeftToRightWithGivenDirectProducts
‣ CartesianAssociatorLeftToRightWithGivenDirectProducts( s, a, b, c, r )( operation )

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

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

1.1-11 CartesianLeftUnitor
‣ CartesianLeftUnitor( a )( attribute )

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

The argument is an object \(a\). The output is the left unitor \(\lambda_a: 1 \times a \rightarrow a\).

1.1-12 CartesianLeftUnitorWithGivenDirectProduct
‣ CartesianLeftUnitorWithGivenDirectProduct( a, s )( operation )

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

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

1.1-13 CartesianLeftUnitorInverse
‣ CartesianLeftUnitorInverse( a )( attribute )

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

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

1.1-14 CartesianLeftUnitorInverseWithGivenDirectProduct
‣ CartesianLeftUnitorInverseWithGivenDirectProduct( a, r )( operation )

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

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

1.1-15 CartesianRightUnitor
‣ CartesianRightUnitor( a )( attribute )

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

The argument is an object \(a\). The output is the right unitor \(\rho_a: a \times 1 \rightarrow a\).

1.1-16 CartesianRightUnitorWithGivenDirectProduct
‣ CartesianRightUnitorWithGivenDirectProduct( a, s )( operation )

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

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

1.1-17 CartesianRightUnitorInverse
‣ CartesianRightUnitorInverse( a )( attribute )

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

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

1.1-18 CartesianRightUnitorInverseWithGivenDirectProduct
‣ CartesianRightUnitorInverseWithGivenDirectProduct( a, r )( operation )

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

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

1.1-19 CartesianDiagonal
‣ CartesianDiagonal( a, n )( operation )

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

The arguments are an object \(a\) and an integer \(n \geq 0\). The output is the diagonal morphism from \(a\) to the \(n\)-fold cartesian power \(a^{\times n}\). If the category does not support empty limits, \(n\) must be not be 0.

1.1-20 CartesianDiagonalWithGivenCartesianPower
‣ CartesianDiagonalWithGivenCartesianPower( a, n, b )( operation )

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

The arguments are an object \(a\), an integer \(n\), and an object \(b\) equal to the \(n\)-fold cartesian power \(a^{\times n}\) of \(a\). The output is the diagonal morphism from \(a\) to \(b\).

1.1-21 LeftCartesianDistributivityExpanding
‣ LeftCartesianDistributivityExpanding( a, L )( operation )

Returns: a morphism in \(\mathrm{Hom}( a \times (b_1 \sqcup \dots \sqcup b_n), (a \times b_1) \sqcup \dots \sqcup (a \times 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 \times (b_1 \sqcup \dots \sqcup b_n) \rightarrow (a \times b_1) \sqcup \dots \sqcup (a \times b_n)\).

1.1-22 LeftCartesianDistributivityExpandingWithGivenObjects
‣ LeftCartesianDistributivityExpandingWithGivenObjects( s, a, L, r )( operation )

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

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

1.1-23 LeftCartesianDistributivityFactoring
‣ LeftCartesianDistributivityFactoring( a, L )( operation )

Returns: a morphism in \(\mathrm{Hom}( (a \times b_1) \sqcup \dots \sqcup (a \times b_n), a \times (b_1 \sqcup \dots \sqcup 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 \times b_1) \sqcup \dots \sqcup (a \times b_n) \rightarrow a \times (b_1 \sqcup \dots \sqcup b_n)\).

1.1-24 LeftCartesianDistributivityFactoringWithGivenObjects
‣ LeftCartesianDistributivityFactoringWithGivenObjects( s, a, L, r )( operation )

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

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

1.1-25 RightCartesianDistributivityExpanding
‣ RightCartesianDistributivityExpanding( L, a )( operation )

Returns: a morphism in \(\mathrm{Hom}( (b_1 \sqcup \dots \sqcup b_n) \times a, (b_1 \times a) \sqcup \dots \sqcup (b_n \times 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 \sqcup \dots \sqcup b_n) \times a \rightarrow (b_1 \times a) \sqcup \dots \sqcup (b_n \times a)\).

1.1-26 RightCartesianDistributivityExpandingWithGivenObjects
‣ RightCartesianDistributivityExpandingWithGivenObjects( s, L, a, r )( operation )

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

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

1.1-27 RightCartesianDistributivityFactoring
‣ RightCartesianDistributivityFactoring( L, a )( operation )

Returns: a morphism in \(\mathrm{Hom}( (b_1 \times a) \sqcup \dots \sqcup (b_n \times a), (b_1 \sqcup \dots \sqcup b_n) \times 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 \times a) \sqcup \dots \sqcup (b_n \times a) \rightarrow (b_1 \sqcup \dots \sqcup b_n) \times a \).

1.1-28 RightCartesianDistributivityFactoringWithGivenObjects
‣ RightCartesianDistributivityFactoringWithGivenObjects( s, L, a, r )( operation )

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

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

1.2 Cartesian Closed Categories

A cartesian category \(\mathbf{C}\) which has for each functor \(- \times b: \mathbf{C} \rightarrow \mathbf{C}\) a right adjoint (denoted by \(\mathrm{Exponential}(b,-)\)) is called a closed cartesian category.

The corresponding GAP property is called IsCartesianClosedCategory.

1.2-1 ExponentialOnObjects
‣ ExponentialOnObjects( a, b )( operation )

Returns: an object

The arguments are two objects \(a,b\). The output is the exponential object \(\mathrm{Exponential}(a,b)\).

1.2-2 ExponentialOnMorphisms
‣ ExponentialOnMorphisms( alpha, beta )( operation )

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

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

1.2-3 ExponentialOnMorphismsWithGivenExponentials
‣ ExponentialOnMorphismsWithGivenExponentials( s, alpha, beta, r )( operation )

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

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

1.2-4 CartesianRightEvaluationMorphism
‣ CartesianRightEvaluationMorphism( a, b )( operation )

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

The arguments are two objects \(a, b\). The output is the right evaluation morphism \(\mathrm{ev}_{a,b}:a \times \mathrm{Exponential}(a,b) \rightarrow b\), i.e., the counit of the direct product-exponential adjunction.

1.2-5 CartesianRightEvaluationMorphismWithGivenSource
‣ CartesianRightEvaluationMorphismWithGivenSource( a, b, s )( operation )

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

The arguments are two objects \(a,b\) and an object \(s = a \times \mathrm{Exponential}(a,b)\). The output is the right evaluation morphism \(\mathrm{ev}_{a,b}: a \times \mathrm{Exponential}(a,b) \rightarrow b\), i.e., the counit of the direct product-exponential adjunction.

1.2-6 CartesianRightCoevaluationMorphism
‣ CartesianRightCoevaluationMorphism( a, b )( operation )

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

The arguments are two objects \(a,b\). The output is the right coevaluation morphism \(\mathrm{coev}_{a,b}: b \rightarrow \mathrm{Exponential}(a, a \times b)\), i.e., the unit of the direct product-exponential adjunction.

1.2-7 CartesianRightCoevaluationMorphismWithGivenRange
‣ CartesianRightCoevaluationMorphismWithGivenRange( a, b, r )( operation )

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

The arguments are two objects \(a,b\) and an object \(r = \mathrm{Exponential}(a, a \times b)\). The output is the right coevaluation morphism \(\mathrm{coev}_{a,b}: b \rightarrow \mathrm{Exponential}(a, a \times b)\), i.e., the unit of the direct product-exponential adjunction.

1.2-8 DirectProductToExponentialRightAdjunctMorphism
‣ DirectProductToExponentialRightAdjunctMorphism( a, b, f )( operation )

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

The arguments are two objects \(a,b\) and a morphism \(f: a \times b \rightarrow c\). The output is a morphism \(g: b \rightarrow \mathrm{Exponential}(a,c)\) corresponding to \(f\) under the direct product-exponential adjunction.

1.2-9 DirectProductToExponentialRightAdjunctMorphismWithGivenExponential
‣ DirectProductToExponentialRightAdjunctMorphismWithGivenExponential( a, b, f, i )( operation )

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

The arguments are two objects \(a,b\), a morphism \(f: a \times b \rightarrow c\) and an object \(i = \mathrm{Exponential}(a,c)\). The output is a morphism \(g: b \rightarrow i\) corresponding to \(f\) under the direct product-exponential adjunction.

1.2-10 DirectProductToExponentialRightAdjunctionIsomorphism
‣ DirectProductToExponentialRightAdjunctionIsomorphism( a, b, c )( operation )

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

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

1.2-11 DirectProductToExponentialRightAdjunctionIsomorphismWithGivenObjects
‣ DirectProductToExponentialRightAdjunctionIsomorphismWithGivenObjects( 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 \times b, c)\) and \(r = H(b, \mathrm{Exponential}(a,c))\). The output is the tri-natural isomorphism \(s \to r\) in the range category of the homomorphism structure \(H\).

1.2-12 ExponentialToDirectProductRightAdjunctMorphism
‣ ExponentialToDirectProductRightAdjunctMorphism( a, c, g )( operation )

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

The arguments are two objects \(a,c\) and a morphism \(g: b \rightarrow \mathrm{Exponential}(a,c)\). The output is a morphism \(f: a \times b \rightarrow c\) corresponding to \(g\) under the direct product-exponential adjunction.

1.2-13 ExponentialToDirectProductRightAdjunctMorphismWithGivenDirectProduct
‣ ExponentialToDirectProductRightAdjunctMorphismWithGivenDirectProduct( 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{Exponential}(a,c)\) and an object \(s = a \times b\). The output is a morphism \(f: s \rightarrow c\) corresponding to \(g\) under the direct product-exponential adjunction.

1.2-14 ExponentialToDirectProductRightAdjunctionIsomorphism
‣ ExponentialToDirectProductRightAdjunctionIsomorphism( a, b, c )( operation )

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

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

1.2-15 ExponentialToDirectProductRightAdjunctionIsomorphismWithGivenObjects
‣ ExponentialToDirectProductRightAdjunctionIsomorphismWithGivenObjects( 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{Exponential}(a,c))\) and \(r = H(a \times b, c)\). The output is the tri-natural isomorphism \(s \to r\) in the range category of the homomorphism structure \(H\).

1.2-16 CartesianLeftEvaluationMorphism
‣ CartesianLeftEvaluationMorphism( a, b )( operation )

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

The arguments are two objects \(a, b\). The output is the left evaluation morphism \(\mathrm{ev}_{a,b}: \mathrm{Exponential}(a,b) \times a \rightarrow b\), i.e., the counit of the direct product-exponential adjunction.

1.2-17 CartesianLeftEvaluationMorphismWithGivenSource
‣ CartesianLeftEvaluationMorphismWithGivenSource( a, b, s )( operation )

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

The arguments are two objects \(a,b\) and an object \(s = \mathrm{Exponential}(a,b) \times a\). The output is the left evaluation morphism \(\mathrm{ev}_{a,b}: \mathrm{Exponential}(a,b) \times a \rightarrow b\), i.e., the counit of the direct product-exponential adjunction.

1.2-18 CartesianLeftCoevaluationMorphism
‣ CartesianLeftCoevaluationMorphism( a, b )( operation )

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

The arguments are two objects \(a,b\). The output is the left coevaluation morphism \(\mathrm{coev}_{a,b}: b \rightarrow \mathrm{Exponential}(a, b \times a)\), i.e., the unit of the direct product-exponential adjunction.

1.2-19 CartesianLeftCoevaluationMorphismWithGivenRange
‣ CartesianLeftCoevaluationMorphismWithGivenRange( a, b, r )( operation )

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

The arguments are two objects \(a,b\) and an object \(r = \mathrm{Exponential}(a, b \times a)\). The output is the left coevaluation morphism \(\mathrm{coev}_{a,b}: b \rightarrow \mathrm{Exponential}(a, b \times a)\), i.e., the unit of the direct product-exponential adjunction.

1.2-20 DirectProductToExponentialLeftAdjunctMorphism
‣ DirectProductToExponentialLeftAdjunctMorphism( a, b, f )( operation )

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

The arguments are two objects \(a,b\) and a morphism \(f: a \times b \rightarrow c\). The output is a morphism \(g: a \rightarrow \mathrm{Exponential}(b,c)\) corresponding to \(f\) under the direct product-exponential adjunction.

1.2-21 DirectProductToExponentialLeftAdjunctMorphismWithGivenExponential
‣ DirectProductToExponentialLeftAdjunctMorphismWithGivenExponential( a, b, f, i )( operation )

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

The arguments are two objects \(a,b\), a morphism \(f: a \times b \rightarrow c\) and an object \(i = \mathrm{Exponential}(b,c)\). The output is a morphism \(g: a \rightarrow i\) corresponding to \(f\) under the direct product-exponential adjunction.

1.2-22 DirectProductToExponentialLeftAdjunctionIsomorphism
‣ DirectProductToExponentialLeftAdjunctionIsomorphism( a, b, c )( operation )

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

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

1.2-23 DirectProductToExponentialLeftAdjunctionIsomorphismWithGivenObjects
‣ DirectProductToExponentialLeftAdjunctionIsomorphismWithGivenObjects( 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 \times b, c)\) and \(r = H(a, \mathrm{Exponential}(b,c))\). The output is the tri-natural isomorphism \(s \to r\) in the range category of the homomorphism structure \(H\).

1.2-24 ExponentialToDirectProductLeftAdjunctMorphism
‣ ExponentialToDirectProductLeftAdjunctMorphism( b, c, g )( operation )

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

The arguments are two objects \(b,c\) and a morphism \(g: a \rightarrow \mathrm{Exponential}(b,c)\). The output is a morphism \(f: a \times b \rightarrow c\) corresponding to \(g\) under the direct product-exponential adjunction.

1.2-25 ExponentialToDirectProductLeftAdjunctMorphismWithGivenDirectProduct
‣ ExponentialToDirectProductLeftAdjunctMorphismWithGivenDirectProduct( 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{Exponential}(b,c)\) and an object \(s = a \times b\). The output is a morphism \(f: s \rightarrow c\) corresponding to \(g\) under the direct product-exponential adjunction.

1.2-26 ExponentialToDirectProductLeftAdjunctionIsomorphism
‣ ExponentialToDirectProductLeftAdjunctionIsomorphism( a, b, c )( operation )

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

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

1.2-27 ExponentialToDirectProductLeftAdjunctionIsomorphismWithGivenObjects
‣ ExponentialToDirectProductLeftAdjunctionIsomorphismWithGivenObjects( 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{Exponential}(b,c))\) and \(r = H(a \times b, c)\). The output is the tri-natural isomorphism \(s \to r\) in the range category of the homomorphism structure \(H\).

1.2-28 CartesianPreComposeMorphism
‣ CartesianPreComposeMorphism( a, b, c )( operation )

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

The arguments are three objects \(a,b,c\). The output is the precomposition morphism \(\mathrm{CartesianPreComposeMorphism}_{a,b,c}: \mathrm{Exponential}(a,b) \times \mathrm{Exponential}(b,c) \rightarrow \mathrm{Exponential}(a,c)\).

1.2-29 CartesianPreComposeMorphismWithGivenObjects
‣ CartesianPreComposeMorphismWithGivenObjects( s, a, b, c, r )( operation )

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

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

1.2-30 CartesianPostComposeMorphism
‣ CartesianPostComposeMorphism( a, b, c )( operation )

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

The arguments are three objects \(a,b,c\). The output is the postcomposition morphism \(\mathrm{CartesianPostComposeMorphism}_{a,b,c}: \mathrm{Exponential}(b,c) \times \mathrm{Exponential}(a,b) \rightarrow \mathrm{Exponential}(a,c)\).

1.2-31 CartesianPostComposeMorphismWithGivenObjects
‣ CartesianPostComposeMorphismWithGivenObjects( s, a, b, c, r )( operation )

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

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

1.2-32 CartesianDualOnObjects
‣ CartesianDualOnObjects( a )( attribute )

Returns: an object

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

1.2-33 CartesianDualOnMorphisms
‣ CartesianDualOnMorphisms( 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.2-34 CartesianDualOnMorphismsWithGivenCartesianDuals
‣ CartesianDualOnMorphismsWithGivenCartesianDuals( 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.2-35 CartesianEvaluationForCartesianDual
‣ CartesianEvaluationForCartesianDual( a )( attribute )

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

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

1.2-36 CartesianEvaluationForCartesianDualWithGivenDirectProduct
‣ CartesianEvaluationForCartesianDualWithGivenDirectProduct( s, a, r )( operation )

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

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

1.2-37 MorphismToCartesianBidual
‣ MorphismToCartesianBidual( 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.2-38 MorphismToCartesianBidualWithGivenCartesianBidual
‣ MorphismToCartesianBidualWithGivenCartesianBidual( 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.2-39 DirectProductExponentialCompatibilityMorphism
‣ DirectProductExponentialCompatibilityMorphism( list )( operation )

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

The argument is a list of four objects \([ a, a', b, b' ]\). The output is the natural morphism \(\mathrm{DirectProductExponentialCompatibilityMorphism}_{a,a',b,b'}: \mathrm{Exponential}(a,a') \times \mathrm{Exponential}(b,b') \rightarrow \mathrm{Exponential}(a \times b,a' \times b')\).

1.2-40 DirectProductExponentialCompatibilityMorphismWithGivenObjects
‣ DirectProductExponentialCompatibilityMorphismWithGivenObjects( 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{Exponential}(a,a') \times \mathrm{Exponential}(b,b')\) and \(r = \mathrm{Exponential}(a \times b,a' \times b')\). The output is the natural morphism \(\mathrm{DirectProductExponentialCompatibilityMorphismWithGivenObjects}_{a,a',b,b'}: \mathrm{Exponential}(a,a') \times \mathrm{Exponential}(b,b') \rightarrow \mathrm{Exponential}(a \times b,a' \times b')\).

1.2-41 DirectProductCartesianDualityCompatibilityMorphism
‣ DirectProductCartesianDualityCompatibilityMorphism( a, b )( operation )

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

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

1.2-42 DirectProductCartesianDualityCompatibilityMorphismWithGivenObjects
‣ DirectProductCartesianDualityCompatibilityMorphismWithGivenObjects( s, a, b, r )( operation )

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

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

1.2-43 MorphismFromDirectProductToExponential
‣ MorphismFromDirectProductToExponential( a, b )( operation )

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

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

1.2-44 MorphismFromDirectProductToExponentialWithGivenObjects
‣ MorphismFromDirectProductToExponentialWithGivenObjects( s, a, b, r )( operation )

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

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

1.2-45 IsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject
‣ IsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject( a )( attribute )

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

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

1.2-46 IsomorphismFromExponentialIntoTerminalObjectToCartesianDualObject
‣ IsomorphismFromExponentialIntoTerminalObjectToCartesianDualObject( a )( attribute )

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

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

1.2-47 UniversalPropertyOfCartesianDual
‣ UniversalPropertyOfCartesianDual( 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 \times a \rightarrow 1\). The output is the morphism \(t \rightarrow a^{\vee}\) given by the universal property of \(a^{\vee}\).

1.2-48 CartesianLambdaIntroduction
‣ CartesianLambdaIntroduction( alpha )( attribute )

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

The argument is a morphism \(\alpha: a \rightarrow b\). The output is the corresponding morphism \(1 \rightarrow \mathrm{Exponential}(a,b)\) under the direct product-exponential adjunction.

1.2-49 CartesianLambdaElimination
‣ CartesianLambdaElimination( 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{Exponential}(a,b)\). The output is a morphism \(a \rightarrow b\) corresponding to \(\alpha\) under the direct product-exponential adjunction.

1.2-50 IsomorphismFromObjectToExponential
‣ IsomorphismFromObjectToExponential( a )( attribute )

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

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

1.2-51 IsomorphismFromObjectToExponentialWithGivenExponential
‣ IsomorphismFromObjectToExponentialWithGivenExponential( a, r )( operation )

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

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

1.2-52 IsomorphismFromExponentialToObject
‣ IsomorphismFromExponentialToObject( a )( attribute )

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

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

1.2-53 IsomorphismFromExponentialToObjectWithGivenExponential
‣ IsomorphismFromExponentialToObjectWithGivenExponential( a, s )( operation )

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

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

1.3 Convenience Methods

1.3-1 Exponential
‣ Exponential( a, b )( operation )

Returns: a cell

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

1.4 Add-methods

1.4-1 AddCartesianBraiding
‣ AddCartesianBraiding( C, F )( operation )
‣ AddCartesianBraiding( 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 CartesianBraiding. 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{CartesianBraiding}(a, b)\).

1.4-2 AddCartesianBraidingInverse
‣ AddCartesianBraidingInverse( C, F )( operation )
‣ AddCartesianBraidingInverse( 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 CartesianBraidingInverse. 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{CartesianBraidingInverse}(a, b)\).

1.4-3 AddCartesianBraidingInverseWithGivenDirectProducts
‣ AddCartesianBraidingInverseWithGivenDirectProducts( C, F )( operation )
‣ AddCartesianBraidingInverseWithGivenDirectProducts( 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 CartesianBraidingInverseWithGivenDirectProducts. 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{CartesianBraidingInverseWithGivenDirectProducts}(s, a, b, r)\).

1.4-4 AddCartesianBraidingWithGivenDirectProducts
‣ AddCartesianBraidingWithGivenDirectProducts( C, F )( operation )
‣ AddCartesianBraidingWithGivenDirectProducts( 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 CartesianBraidingWithGivenDirectProducts. 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{CartesianBraidingWithGivenDirectProducts}(s, a, b, r)\).

1.4-5 AddCartesianAssociatorLeftToRight
‣ AddCartesianAssociatorLeftToRight( C, F )( operation )
‣ AddCartesianAssociatorLeftToRight( 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 CartesianAssociatorLeftToRight. 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{CartesianAssociatorLeftToRight}(a, b, c)\).

1.4-6 AddCartesianAssociatorLeftToRightWithGivenDirectProducts
‣ AddCartesianAssociatorLeftToRightWithGivenDirectProducts( C, F )( operation )
‣ AddCartesianAssociatorLeftToRightWithGivenDirectProducts( 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 CartesianAssociatorLeftToRightWithGivenDirectProducts. 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{CartesianAssociatorLeftToRightWithGivenDirectProducts}(s, a, b, c, r)\).

1.4-7 AddCartesianAssociatorRightToLeft
‣ AddCartesianAssociatorRightToLeft( C, F )( operation )
‣ AddCartesianAssociatorRightToLeft( 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 CartesianAssociatorRightToLeft. 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{CartesianAssociatorRightToLeft}(a, b, c)\).

1.4-8 AddCartesianAssociatorRightToLeftWithGivenDirectProducts
‣ AddCartesianAssociatorRightToLeftWithGivenDirectProducts( C, F )( operation )
‣ AddCartesianAssociatorRightToLeftWithGivenDirectProducts( 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 CartesianAssociatorRightToLeftWithGivenDirectProducts. 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{CartesianAssociatorRightToLeftWithGivenDirectProducts}(s, a, b, c, r)\).

1.4-9 AddCartesianDiagonal
‣ AddCartesianDiagonal( C, F )( operation )
‣ AddCartesianDiagonal( 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 CartesianDiagonal. 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, n ) \mapsto \mathtt{CartesianDiagonal}(a, n)\).

1.4-10 AddCartesianDiagonalWithGivenCartesianPower
‣ AddCartesianDiagonalWithGivenCartesianPower( C, F )( operation )
‣ AddCartesianDiagonalWithGivenCartesianPower( 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 CartesianDiagonalWithGivenCartesianPower. 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, n, cartesian_power ) \mapsto \mathtt{CartesianDiagonalWithGivenCartesianPower}(a, n, cartesian_power)\).

1.4-11 AddCartesianLeftUnitor
‣ AddCartesianLeftUnitor( C, F )( operation )
‣ AddCartesianLeftUnitor( 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 CartesianLeftUnitor. 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{CartesianLeftUnitor}(a)\).

1.4-12 AddCartesianLeftUnitorInverse
‣ AddCartesianLeftUnitorInverse( C, F )( operation )
‣ AddCartesianLeftUnitorInverse( 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 CartesianLeftUnitorInverse. 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{CartesianLeftUnitorInverse}(a)\).

1.4-13 AddCartesianLeftUnitorInverseWithGivenDirectProduct
‣ AddCartesianLeftUnitorInverseWithGivenDirectProduct( C, F )( operation )
‣ AddCartesianLeftUnitorInverseWithGivenDirectProduct( 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 CartesianLeftUnitorInverseWithGivenDirectProduct. 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{CartesianLeftUnitorInverseWithGivenDirectProduct}(a, r)\).

1.4-14 AddCartesianLeftUnitorWithGivenDirectProduct
‣ AddCartesianLeftUnitorWithGivenDirectProduct( C, F )( operation )
‣ AddCartesianLeftUnitorWithGivenDirectProduct( 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 CartesianLeftUnitorWithGivenDirectProduct. 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{CartesianLeftUnitorWithGivenDirectProduct}(a, s)\).

1.4-15 AddCartesianRightUnitor
‣ AddCartesianRightUnitor( C, F )( operation )
‣ AddCartesianRightUnitor( 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 CartesianRightUnitor. 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{CartesianRightUnitor}(a)\).

1.4-16 AddCartesianRightUnitorInverse
‣ AddCartesianRightUnitorInverse( C, F )( operation )
‣ AddCartesianRightUnitorInverse( 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 CartesianRightUnitorInverse. 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{CartesianRightUnitorInverse}(a)\).

1.4-17 AddCartesianRightUnitorInverseWithGivenDirectProduct
‣ AddCartesianRightUnitorInverseWithGivenDirectProduct( C, F )( operation )
‣ AddCartesianRightUnitorInverseWithGivenDirectProduct( 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 CartesianRightUnitorInverseWithGivenDirectProduct. 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{CartesianRightUnitorInverseWithGivenDirectProduct}(a, r)\).

1.4-18 AddCartesianRightUnitorWithGivenDirectProduct
‣ AddCartesianRightUnitorWithGivenDirectProduct( C, F )( operation )
‣ AddCartesianRightUnitorWithGivenDirectProduct( 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 CartesianRightUnitorWithGivenDirectProduct. 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{CartesianRightUnitorWithGivenDirectProduct}(a, s)\).

1.4-19 AddDirectProductOnMorphisms
‣ AddDirectProductOnMorphisms( C, F )( operation )
‣ AddDirectProductOnMorphisms( 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 DirectProductOnMorphisms. 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{DirectProductOnMorphisms}(alpha, beta)\).

1.4-20 AddDirectProductOnMorphismsWithGivenDirectProducts
‣ AddDirectProductOnMorphismsWithGivenDirectProducts( C, F )( operation )
‣ AddDirectProductOnMorphismsWithGivenDirectProducts( 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 DirectProductOnMorphismsWithGivenDirectProducts. 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{DirectProductOnMorphismsWithGivenDirectProducts}(s, alpha, beta, r)\).

1.4-21 AddCartesianDualOnMorphisms
‣ AddCartesianDualOnMorphisms( C, F )( operation )
‣ AddCartesianDualOnMorphisms( 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 CartesianDualOnMorphisms. 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{CartesianDualOnMorphisms}(alpha)\).

1.4-22 AddCartesianDualOnMorphismsWithGivenCartesianDuals
‣ AddCartesianDualOnMorphismsWithGivenCartesianDuals( C, F )( operation )
‣ AddCartesianDualOnMorphismsWithGivenCartesianDuals( 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 CartesianDualOnMorphismsWithGivenCartesianDuals. 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{CartesianDualOnMorphismsWithGivenCartesianDuals}(s, alpha, r)\).

1.4-23 AddCartesianDualOnObjects
‣ AddCartesianDualOnObjects( C, F )( operation )
‣ AddCartesianDualOnObjects( 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 CartesianDualOnObjects. 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{CartesianDualOnObjects}(a)\).

1.4-24 AddCartesianEvaluationForCartesianDual
‣ AddCartesianEvaluationForCartesianDual( C, F )( operation )
‣ AddCartesianEvaluationForCartesianDual( 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 CartesianEvaluationForCartesianDual. 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{CartesianEvaluationForCartesianDual}(a)\).

1.4-25 AddCartesianEvaluationForCartesianDualWithGivenDirectProduct
‣ AddCartesianEvaluationForCartesianDualWithGivenDirectProduct( C, F )( operation )
‣ AddCartesianEvaluationForCartesianDualWithGivenDirectProduct( 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 CartesianEvaluationForCartesianDualWithGivenDirectProduct. 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{CartesianEvaluationForCartesianDualWithGivenDirectProduct}(s, a, r)\).

1.4-26 AddCartesianLambdaElimination
‣ AddCartesianLambdaElimination( C, F )( operation )
‣ AddCartesianLambdaElimination( 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 CartesianLambdaElimination. 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{CartesianLambdaElimination}(a, b, alpha)\).

1.4-27 AddCartesianLambdaIntroduction
‣ AddCartesianLambdaIntroduction( C, F )( operation )
‣ AddCartesianLambdaIntroduction( 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 CartesianLambdaIntroduction. 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{CartesianLambdaIntroduction}(alpha)\).

1.4-28 AddCartesianLeftCoevaluationMorphism
‣ AddCartesianLeftCoevaluationMorphism( C, F )( operation )
‣ AddCartesianLeftCoevaluationMorphism( 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 CartesianLeftCoevaluationMorphism. 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{CartesianLeftCoevaluationMorphism}(a, b)\).

1.4-29 AddCartesianLeftCoevaluationMorphismWithGivenRange
‣ AddCartesianLeftCoevaluationMorphismWithGivenRange( C, F )( operation )
‣ AddCartesianLeftCoevaluationMorphismWithGivenRange( 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 CartesianLeftCoevaluationMorphismWithGivenRange. 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{CartesianLeftCoevaluationMorphismWithGivenRange}(a, b, r)\).

1.4-30 AddCartesianLeftEvaluationMorphism
‣ AddCartesianLeftEvaluationMorphism( C, F )( operation )
‣ AddCartesianLeftEvaluationMorphism( 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 CartesianLeftEvaluationMorphism. 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{CartesianLeftEvaluationMorphism}(a, b)\).

1.4-31 AddCartesianLeftEvaluationMorphismWithGivenSource
‣ AddCartesianLeftEvaluationMorphismWithGivenSource( C, F )( operation )
‣ AddCartesianLeftEvaluationMorphismWithGivenSource( 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 CartesianLeftEvaluationMorphismWithGivenSource. 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{CartesianLeftEvaluationMorphismWithGivenSource}(a, b, s)\).

1.4-32 AddCartesianPostComposeMorphism
‣ AddCartesianPostComposeMorphism( C, F )( operation )
‣ AddCartesianPostComposeMorphism( 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 CartesianPostComposeMorphism. 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{CartesianPostComposeMorphism}(a, b, c)\).

1.4-33 AddCartesianPostComposeMorphismWithGivenObjects
‣ AddCartesianPostComposeMorphismWithGivenObjects( C, F )( operation )
‣ AddCartesianPostComposeMorphismWithGivenObjects( 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 CartesianPostComposeMorphismWithGivenObjects. 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{CartesianPostComposeMorphismWithGivenObjects}(s, a, b, c, r)\).

1.4-34 AddCartesianPreComposeMorphism
‣ AddCartesianPreComposeMorphism( C, F )( operation )
‣ AddCartesianPreComposeMorphism( 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 CartesianPreComposeMorphism. 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{CartesianPreComposeMorphism}(a, b, c)\).

1.4-35 AddCartesianPreComposeMorphismWithGivenObjects
‣ AddCartesianPreComposeMorphismWithGivenObjects( C, F )( operation )
‣ AddCartesianPreComposeMorphismWithGivenObjects( 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 CartesianPreComposeMorphismWithGivenObjects. 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{CartesianPreComposeMorphismWithGivenObjects}(s, a, b, c, r)\).

1.4-36 AddCartesianRightCoevaluationMorphism
‣ AddCartesianRightCoevaluationMorphism( C, F )( operation )
‣ AddCartesianRightCoevaluationMorphism( 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 CartesianRightCoevaluationMorphism. 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{CartesianRightCoevaluationMorphism}(a, b)\).

1.4-37 AddCartesianRightCoevaluationMorphismWithGivenRange
‣ AddCartesianRightCoevaluationMorphismWithGivenRange( C, F )( operation )
‣ AddCartesianRightCoevaluationMorphismWithGivenRange( 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 CartesianRightCoevaluationMorphismWithGivenRange. 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{CartesianRightCoevaluationMorphismWithGivenRange}(a, b, r)\).

1.4-38 AddCartesianRightEvaluationMorphism
‣ AddCartesianRightEvaluationMorphism( C, F )( operation )
‣ AddCartesianRightEvaluationMorphism( 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 CartesianRightEvaluationMorphism. 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{CartesianRightEvaluationMorphism}(a, b)\).

1.4-39 AddCartesianRightEvaluationMorphismWithGivenSource
‣ AddCartesianRightEvaluationMorphismWithGivenSource( C, F )( operation )
‣ AddCartesianRightEvaluationMorphismWithGivenSource( 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 CartesianRightEvaluationMorphismWithGivenSource. 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{CartesianRightEvaluationMorphismWithGivenSource}(a, b, s)\).

1.4-40 AddDirectProductCartesianDualityCompatibilityMorphism
‣ AddDirectProductCartesianDualityCompatibilityMorphism( C, F )( operation )
‣ AddDirectProductCartesianDualityCompatibilityMorphism( 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 DirectProductCartesianDualityCompatibilityMorphism. 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{DirectProductCartesianDualityCompatibilityMorphism}(a, b)\).

1.4-41 AddDirectProductCartesianDualityCompatibilityMorphismWithGivenObjects
‣ AddDirectProductCartesianDualityCompatibilityMorphismWithGivenObjects( C, F )( operation )
‣ AddDirectProductCartesianDualityCompatibilityMorphismWithGivenObjects( 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 DirectProductCartesianDualityCompatibilityMorphismWithGivenObjects. 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{DirectProductCartesianDualityCompatibilityMorphismWithGivenObjects}(s, a, b, r)\).

1.4-42 AddDirectProductExponentialCompatibilityMorphism
‣ AddDirectProductExponentialCompatibilityMorphism( C, F )( operation )
‣ AddDirectProductExponentialCompatibilityMorphism( 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 DirectProductExponentialCompatibilityMorphism. 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{DirectProductExponentialCompatibilityMorphism}(list)\).

1.4-43 AddDirectProductExponentialCompatibilityMorphismWithGivenObjects
‣ AddDirectProductExponentialCompatibilityMorphismWithGivenObjects( C, F )( operation )
‣ AddDirectProductExponentialCompatibilityMorphismWithGivenObjects( 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 DirectProductExponentialCompatibilityMorphismWithGivenObjects. 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{DirectProductExponentialCompatibilityMorphismWithGivenObjects}(source, list, range)\).

1.4-44 AddDirectProductToExponentialLeftAdjunctMorphism
‣ AddDirectProductToExponentialLeftAdjunctMorphism( C, F )( operation )
‣ AddDirectProductToExponentialLeftAdjunctMorphism( 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 DirectProductToExponentialLeftAdjunctMorphism. 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{DirectProductToExponentialLeftAdjunctMorphism}(a, b, f)\).

1.4-45 AddDirectProductToExponentialLeftAdjunctMorphismWithGivenExponential
‣ AddDirectProductToExponentialLeftAdjunctMorphismWithGivenExponential( C, F )( operation )
‣ AddDirectProductToExponentialLeftAdjunctMorphismWithGivenExponential( 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 DirectProductToExponentialLeftAdjunctMorphismWithGivenExponential. 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{DirectProductToExponentialLeftAdjunctMorphismWithGivenExponential}(a, b, f, i)\).

1.4-46 AddDirectProductToExponentialLeftAdjunctionIsomorphism
‣ AddDirectProductToExponentialLeftAdjunctionIsomorphism( C, F )( operation )
‣ AddDirectProductToExponentialLeftAdjunctionIsomorphism( 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 DirectProductToExponentialLeftAdjunctionIsomorphism. 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{DirectProductToExponentialLeftAdjunctionIsomorphism}(a, b, c)\).

1.4-47 AddDirectProductToExponentialLeftAdjunctionIsomorphismWithGivenObjects
‣ AddDirectProductToExponentialLeftAdjunctionIsomorphismWithGivenObjects( C, F )( operation )
‣ AddDirectProductToExponentialLeftAdjunctionIsomorphismWithGivenObjects( 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 DirectProductToExponentialLeftAdjunctionIsomorphismWithGivenObjects. 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{DirectProductToExponentialLeftAdjunctionIsomorphismWithGivenObjects}(s, a, b, c, r)\).

1.4-48 AddDirectProductToExponentialRightAdjunctMorphism
‣ AddDirectProductToExponentialRightAdjunctMorphism( C, F )( operation )
‣ AddDirectProductToExponentialRightAdjunctMorphism( 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 DirectProductToExponentialRightAdjunctMorphism. 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{DirectProductToExponentialRightAdjunctMorphism}(a, b, f)\).

1.4-49 AddDirectProductToExponentialRightAdjunctMorphismWithGivenExponential
‣ AddDirectProductToExponentialRightAdjunctMorphismWithGivenExponential( C, F )( operation )
‣ AddDirectProductToExponentialRightAdjunctMorphismWithGivenExponential( 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 DirectProductToExponentialRightAdjunctMorphismWithGivenExponential. 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{DirectProductToExponentialRightAdjunctMorphismWithGivenExponential}(a, b, f, i)\).

1.4-50 AddDirectProductToExponentialRightAdjunctionIsomorphism
‣ AddDirectProductToExponentialRightAdjunctionIsomorphism( C, F )( operation )
‣ AddDirectProductToExponentialRightAdjunctionIsomorphism( 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 DirectProductToExponentialRightAdjunctionIsomorphism. 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{DirectProductToExponentialRightAdjunctionIsomorphism}(a, b, c)\).

1.4-51 AddDirectProductToExponentialRightAdjunctionIsomorphismWithGivenObjects
‣ AddDirectProductToExponentialRightAdjunctionIsomorphismWithGivenObjects( C, F )( operation )
‣ AddDirectProductToExponentialRightAdjunctionIsomorphismWithGivenObjects( 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 DirectProductToExponentialRightAdjunctionIsomorphismWithGivenObjects. 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{DirectProductToExponentialRightAdjunctionIsomorphismWithGivenObjects}(s, a, b, c, r)\).

1.4-52 AddExponentialOnMorphisms
‣ AddExponentialOnMorphisms( C, F )( operation )
‣ AddExponentialOnMorphisms( 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 ExponentialOnMorphisms. 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{ExponentialOnMorphisms}(alpha, beta)\).

1.4-53 AddExponentialOnMorphismsWithGivenExponentials
‣ AddExponentialOnMorphismsWithGivenExponentials( C, F )( operation )
‣ AddExponentialOnMorphismsWithGivenExponentials( 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 ExponentialOnMorphismsWithGivenExponentials. 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{ExponentialOnMorphismsWithGivenExponentials}(s, alpha, beta, r)\).

1.4-54 AddExponentialOnObjects
‣ AddExponentialOnObjects( C, F )( operation )
‣ AddExponentialOnObjects( 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 ExponentialOnObjects. 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{ExponentialOnObjects}(a, b)\).

1.4-55 AddExponentialToDirectProductLeftAdjunctMorphism
‣ AddExponentialToDirectProductLeftAdjunctMorphism( C, F )( operation )
‣ AddExponentialToDirectProductLeftAdjunctMorphism( 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 ExponentialToDirectProductLeftAdjunctMorphism. 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{ExponentialToDirectProductLeftAdjunctMorphism}(b, c, g)\).

1.4-56 AddExponentialToDirectProductLeftAdjunctMorphismWithGivenDirectProduct
‣ AddExponentialToDirectProductLeftAdjunctMorphismWithGivenDirectProduct( C, F )( operation )
‣ AddExponentialToDirectProductLeftAdjunctMorphismWithGivenDirectProduct( 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 ExponentialToDirectProductLeftAdjunctMorphismWithGivenDirectProduct. 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{ExponentialToDirectProductLeftAdjunctMorphismWithGivenDirectProduct}(b, c, g, s)\).

1.4-57 AddExponentialToDirectProductLeftAdjunctionIsomorphism
‣ AddExponentialToDirectProductLeftAdjunctionIsomorphism( C, F )( operation )
‣ AddExponentialToDirectProductLeftAdjunctionIsomorphism( 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 ExponentialToDirectProductLeftAdjunctionIsomorphism. 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{ExponentialToDirectProductLeftAdjunctionIsomorphism}(a, b, c)\).

1.4-58 AddExponentialToDirectProductLeftAdjunctionIsomorphismWithGivenObjects
‣ AddExponentialToDirectProductLeftAdjunctionIsomorphismWithGivenObjects( C, F )( operation )
‣ AddExponentialToDirectProductLeftAdjunctionIsomorphismWithGivenObjects( 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 ExponentialToDirectProductLeftAdjunctionIsomorphismWithGivenObjects. 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{ExponentialToDirectProductLeftAdjunctionIsomorphismWithGivenObjects}(s, a, b, c, r)\).

1.4-59 AddExponentialToDirectProductRightAdjunctMorphism
‣ AddExponentialToDirectProductRightAdjunctMorphism( C, F )( operation )
‣ AddExponentialToDirectProductRightAdjunctMorphism( 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 ExponentialToDirectProductRightAdjunctMorphism. 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{ExponentialToDirectProductRightAdjunctMorphism}(a, c, g)\).

1.4-60 AddExponentialToDirectProductRightAdjunctMorphismWithGivenDirectProduct
‣ AddExponentialToDirectProductRightAdjunctMorphismWithGivenDirectProduct( C, F )( operation )
‣ AddExponentialToDirectProductRightAdjunctMorphismWithGivenDirectProduct( 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 ExponentialToDirectProductRightAdjunctMorphismWithGivenDirectProduct. 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{ExponentialToDirectProductRightAdjunctMorphismWithGivenDirectProduct}(a, c, g, s)\).

1.4-61 AddExponentialToDirectProductRightAdjunctionIsomorphism
‣ AddExponentialToDirectProductRightAdjunctionIsomorphism( C, F )( operation )
‣ AddExponentialToDirectProductRightAdjunctionIsomorphism( 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 ExponentialToDirectProductRightAdjunctionIsomorphism. 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{ExponentialToDirectProductRightAdjunctionIsomorphism}(a, b, c)\).

1.4-62 AddExponentialToDirectProductRightAdjunctionIsomorphismWithGivenObjects
‣ AddExponentialToDirectProductRightAdjunctionIsomorphismWithGivenObjects( C, F )( operation )
‣ AddExponentialToDirectProductRightAdjunctionIsomorphismWithGivenObjects( 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 ExponentialToDirectProductRightAdjunctionIsomorphismWithGivenObjects. 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{ExponentialToDirectProductRightAdjunctionIsomorphismWithGivenObjects}(s, a, b, c, r)\).

1.4-63 AddIsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject
‣ AddIsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject( C, F )( operation )
‣ AddIsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject( 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 IsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject. 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{IsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject}(a)\).

1.4-64 AddIsomorphismFromExponentialIntoTerminalObjectToCartesianDualObject
‣ AddIsomorphismFromExponentialIntoTerminalObjectToCartesianDualObject( C, F )( operation )
‣ AddIsomorphismFromExponentialIntoTerminalObjectToCartesianDualObject( 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 IsomorphismFromExponentialIntoTerminalObjectToCartesianDualObject. 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{IsomorphismFromExponentialIntoTerminalObjectToCartesianDualObject}(a)\).

1.4-65 AddIsomorphismFromExponentialToObject
‣ AddIsomorphismFromExponentialToObject( C, F )( operation )
‣ AddIsomorphismFromExponentialToObject( 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 IsomorphismFromExponentialToObject. 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{IsomorphismFromExponentialToObject}(a)\).

1.4-66 AddIsomorphismFromExponentialToObjectWithGivenExponential
‣ AddIsomorphismFromExponentialToObjectWithGivenExponential( C, F )( operation )
‣ AddIsomorphismFromExponentialToObjectWithGivenExponential( 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 IsomorphismFromExponentialToObjectWithGivenExponential. 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{IsomorphismFromExponentialToObjectWithGivenExponential}(a, s)\).

1.4-67 AddIsomorphismFromObjectToExponential
‣ AddIsomorphismFromObjectToExponential( C, F )( operation )
‣ AddIsomorphismFromObjectToExponential( 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 IsomorphismFromObjectToExponential. 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{IsomorphismFromObjectToExponential}(a)\).

1.4-68 AddIsomorphismFromObjectToExponentialWithGivenExponential
‣ AddIsomorphismFromObjectToExponentialWithGivenExponential( C, F )( operation )
‣ AddIsomorphismFromObjectToExponentialWithGivenExponential( 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 IsomorphismFromObjectToExponentialWithGivenExponential. 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{IsomorphismFromObjectToExponentialWithGivenExponential}(a, r)\).

1.4-69 AddMorphismFromDirectProductToExponential
‣ AddMorphismFromDirectProductToExponential( C, F )( operation )
‣ AddMorphismFromDirectProductToExponential( 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 MorphismFromDirectProductToExponential. 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{MorphismFromDirectProductToExponential}(a, b)\).

1.4-70 AddMorphismFromDirectProductToExponentialWithGivenObjects
‣ AddMorphismFromDirectProductToExponentialWithGivenObjects( C, F )( operation )
‣ AddMorphismFromDirectProductToExponentialWithGivenObjects( 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 MorphismFromDirectProductToExponentialWithGivenObjects. 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{MorphismFromDirectProductToExponentialWithGivenObjects}(s, a, b, r)\).

1.4-71 AddMorphismToCartesianBidual
‣ AddMorphismToCartesianBidual( C, F )( operation )
‣ AddMorphismToCartesianBidual( 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 MorphismToCartesianBidual. 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{MorphismToCartesianBidual}(a)\).

1.4-72 AddMorphismToCartesianBidualWithGivenCartesianBidual
‣ AddMorphismToCartesianBidualWithGivenCartesianBidual( C, F )( operation )
‣ AddMorphismToCartesianBidualWithGivenCartesianBidual( 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 MorphismToCartesianBidualWithGivenCartesianBidual. 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{MorphismToCartesianBidualWithGivenCartesianBidual}(a, r)\).

1.4-73 AddUniversalPropertyOfCartesianDual
‣ AddUniversalPropertyOfCartesianDual( C, F )( operation )
‣ AddUniversalPropertyOfCartesianDual( 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 UniversalPropertyOfCartesianDual. 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{UniversalPropertyOfCartesianDual}(t, a, alpha)\).

1.4-74 AddLeftCartesianDistributivityExpanding
‣ AddLeftCartesianDistributivityExpanding( C, F )( operation )
‣ AddLeftCartesianDistributivityExpanding( 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 LeftCartesianDistributivityExpanding. 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{LeftCartesianDistributivityExpanding}(a, L)\).

1.4-75 AddLeftCartesianDistributivityExpandingWithGivenObjects
‣ AddLeftCartesianDistributivityExpandingWithGivenObjects( C, F )( operation )
‣ AddLeftCartesianDistributivityExpandingWithGivenObjects( 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 LeftCartesianDistributivityExpandingWithGivenObjects. 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{LeftCartesianDistributivityExpandingWithGivenObjects}(s, a, L, r)\).

1.4-76 AddLeftCartesianDistributivityFactoring
‣ AddLeftCartesianDistributivityFactoring( C, F )( operation )
‣ AddLeftCartesianDistributivityFactoring( 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 LeftCartesianDistributivityFactoring. 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{LeftCartesianDistributivityFactoring}(a, L)\).

1.4-77 AddLeftCartesianDistributivityFactoringWithGivenObjects
‣ AddLeftCartesianDistributivityFactoringWithGivenObjects( C, F )( operation )
‣ AddLeftCartesianDistributivityFactoringWithGivenObjects( 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 LeftCartesianDistributivityFactoringWithGivenObjects. 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{LeftCartesianDistributivityFactoringWithGivenObjects}(s, a, L, r)\).

1.4-78 AddRightCartesianDistributivityExpanding
‣ AddRightCartesianDistributivityExpanding( C, F )( operation )
‣ AddRightCartesianDistributivityExpanding( 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 RightCartesianDistributivityExpanding. 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{RightCartesianDistributivityExpanding}(L, a)\).

1.4-79 AddRightCartesianDistributivityExpandingWithGivenObjects
‣ AddRightCartesianDistributivityExpandingWithGivenObjects( C, F )( operation )
‣ AddRightCartesianDistributivityExpandingWithGivenObjects( 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 RightCartesianDistributivityExpandingWithGivenObjects. 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{RightCartesianDistributivityExpandingWithGivenObjects}(s, L, a, r)\).

1.4-80 AddRightCartesianDistributivityFactoring
‣ AddRightCartesianDistributivityFactoring( C, F )( operation )
‣ AddRightCartesianDistributivityFactoring( 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 RightCartesianDistributivityFactoring. 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{RightCartesianDistributivityFactoring}(L, a)\).

1.4-81 AddRightCartesianDistributivityFactoringWithGivenObjects
‣ AddRightCartesianDistributivityFactoringWithGivenObjects( C, F )( operation )
‣ AddRightCartesianDistributivityFactoringWithGivenObjects( 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 RightCartesianDistributivityFactoringWithGivenObjects. 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{RightCartesianDistributivityFactoringWithGivenObjects}(s, L, a, r)\).

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

generated by GAPDoc2HTML