Goto Chapter: Top 1 2 3 4 5 6 Ind

### 1 Cartesian Categories

#### 1.1 Cartesian Categories

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

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

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

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

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

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

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

is called a cartesian category, if

• for all objects $$a,b,c,d$$, the pentagon identity holds:

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

• for all objects $$a,c$$, the triangle identity holds:

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

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

 ‣ 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 \mathrm{Exponential}(a,c)$$ corresponding to $$f$$ under the direct product-exponential adjunction.

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

 ‣ 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-12 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-13 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-14 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-15 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.

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

 ‣ 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 \mathrm{Exponential}(b,c)$$ corresponding to $$f$$ under the direct product-exponential adjunction.

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

 ‣ 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-20 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-21 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-22 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-23 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-24 CartesianDualOnObjects
 ‣ CartesianDualOnObjects( a ) ( attribute )

Returns: an object

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

##### 1.2-25 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-26 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-27 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-28 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-29 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-30 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-31 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-32 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-33 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-34 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-35 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-36 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-37 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-38 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-39 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-40 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-41 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-42 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-43 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-44 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-45 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.

 ‣ AddCartesianBraiding( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, b ) \mapsto \mathtt{CartesianBraiding}(a, b)$$.

 ‣ AddCartesianBraidingInverse( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, b ) \mapsto \mathtt{CartesianBraidingInverse}(a, b)$$.

 ‣ AddCartesianBraidingInverseWithGivenDirectProducts( C, F ) ( operation )

Returns: nothing

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. $$F: ( s, a, b, r ) \mapsto \mathtt{CartesianBraidingInverseWithGivenDirectProducts}(s, a, b, r)$$.

 ‣ AddCartesianBraidingWithGivenDirectProducts( C, F ) ( operation )

Returns: nothing

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. $$F: ( s, a, b, r ) \mapsto \mathtt{CartesianBraidingWithGivenDirectProducts}(s, a, b, r)$$.

 ‣ AddCartesianAssociatorLeftToRight( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, b, c ) \mapsto \mathtt{CartesianAssociatorLeftToRight}(a, b, c)$$.

 ‣ AddCartesianAssociatorLeftToRightWithGivenDirectProducts( C, F ) ( operation )

Returns: nothing

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. $$F: ( s, a, b, c, r ) \mapsto \mathtt{CartesianAssociatorLeftToRightWithGivenDirectProducts}(s, a, b, c, r)$$.

 ‣ AddCartesianAssociatorRightToLeft( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, b, c ) \mapsto \mathtt{CartesianAssociatorRightToLeft}(a, b, c)$$.

 ‣ AddCartesianAssociatorRightToLeftWithGivenDirectProducts( C, F ) ( operation )

Returns: nothing

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. $$F: ( s, a, b, c, r ) \mapsto \mathtt{CartesianAssociatorRightToLeftWithGivenDirectProducts}(s, a, b, c, r)$$.

 ‣ AddCartesianDiagonal( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, n ) \mapsto \mathtt{CartesianDiagonal}(a, n)$$.

 ‣ AddCartesianDiagonalWithGivenCartesianPower( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, n, cartesian_power ) \mapsto \mathtt{CartesianDiagonalWithGivenCartesianPower}(a, n, cartesian_power)$$.

 ‣ AddCartesianLeftUnitor( C, F ) ( operation )

Returns: nothing

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. $$F: ( a ) \mapsto \mathtt{CartesianLeftUnitor}(a)$$.

 ‣ AddCartesianLeftUnitorInverse( C, F ) ( operation )

Returns: nothing

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. $$F: ( a ) \mapsto \mathtt{CartesianLeftUnitorInverse}(a)$$.

 ‣ AddCartesianLeftUnitorInverseWithGivenDirectProduct( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, r ) \mapsto \mathtt{CartesianLeftUnitorInverseWithGivenDirectProduct}(a, r)$$.

 ‣ AddCartesianLeftUnitorWithGivenDirectProduct( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, s ) \mapsto \mathtt{CartesianLeftUnitorWithGivenDirectProduct}(a, s)$$.

 ‣ AddCartesianRightUnitor( C, F ) ( operation )

Returns: nothing

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. $$F: ( a ) \mapsto \mathtt{CartesianRightUnitor}(a)$$.

 ‣ AddCartesianRightUnitorInverse( C, F ) ( operation )

Returns: nothing

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. $$F: ( a ) \mapsto \mathtt{CartesianRightUnitorInverse}(a)$$.

 ‣ AddCartesianRightUnitorInverseWithGivenDirectProduct( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, r ) \mapsto \mathtt{CartesianRightUnitorInverseWithGivenDirectProduct}(a, r)$$.

 ‣ AddCartesianRightUnitorWithGivenDirectProduct( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, s ) \mapsto \mathtt{CartesianRightUnitorWithGivenDirectProduct}(a, s)$$.

 ‣ AddDirectProductOnMorphisms( C, F ) ( operation )

Returns: nothing

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. $$F: ( alpha, beta ) \mapsto \mathtt{DirectProductOnMorphisms}(alpha, beta)$$.

 ‣ AddDirectProductOnMorphismsWithGivenDirectProducts( C, F ) ( operation )

Returns: nothing

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. $$F: ( s, alpha, beta, r ) \mapsto \mathtt{DirectProductOnMorphismsWithGivenDirectProducts}(s, alpha, beta, r)$$.

 ‣ AddCartesianDualOnMorphisms( C, F ) ( operation )

Returns: nothing

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. $$F: ( alpha ) \mapsto \mathtt{CartesianDualOnMorphisms}(alpha)$$.

 ‣ AddCartesianDualOnMorphismsWithGivenCartesianDuals( C, F ) ( operation )

Returns: nothing

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. $$F: ( s, alpha, r ) \mapsto \mathtt{CartesianDualOnMorphismsWithGivenCartesianDuals}(s, alpha, r)$$.

 ‣ AddCartesianDualOnObjects( C, F ) ( operation )

Returns: nothing

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. $$F: ( a ) \mapsto \mathtt{CartesianDualOnObjects}(a)$$.

 ‣ AddCartesianEvaluationForCartesianDual( C, F ) ( operation )

Returns: nothing

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. $$F: ( a ) \mapsto \mathtt{CartesianEvaluationForCartesianDual}(a)$$.

 ‣ AddCartesianEvaluationForCartesianDualWithGivenDirectProduct( C, F ) ( operation )

Returns: nothing

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. $$F: ( s, a, r ) \mapsto \mathtt{CartesianEvaluationForCartesianDualWithGivenDirectProduct}(s, a, r)$$.

 ‣ AddCartesianLambdaElimination( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, b, alpha ) \mapsto \mathtt{CartesianLambdaElimination}(a, b, alpha)$$.

 ‣ AddCartesianLambdaIntroduction( C, F ) ( operation )

Returns: nothing

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. $$F: ( alpha ) \mapsto \mathtt{CartesianLambdaIntroduction}(alpha)$$.

 ‣ AddCartesianLeftCoevaluationMorphism( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, b ) \mapsto \mathtt{CartesianLeftCoevaluationMorphism}(a, b)$$.

 ‣ AddCartesianLeftCoevaluationMorphismWithGivenRange( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, b, r ) \mapsto \mathtt{CartesianLeftCoevaluationMorphismWithGivenRange}(a, b, r)$$.

 ‣ AddCartesianLeftEvaluationMorphism( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, b ) \mapsto \mathtt{CartesianLeftEvaluationMorphism}(a, b)$$.

 ‣ AddCartesianLeftEvaluationMorphismWithGivenSource( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, b, s ) \mapsto \mathtt{CartesianLeftEvaluationMorphismWithGivenSource}(a, b, s)$$.

 ‣ AddCartesianPostComposeMorphism( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, b, c ) \mapsto \mathtt{CartesianPostComposeMorphism}(a, b, c)$$.

 ‣ AddCartesianPostComposeMorphismWithGivenObjects( C, F ) ( operation )

Returns: nothing

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. $$F: ( s, a, b, c, r ) \mapsto \mathtt{CartesianPostComposeMorphismWithGivenObjects}(s, a, b, c, r)$$.

 ‣ AddCartesianPreComposeMorphism( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, b, c ) \mapsto \mathtt{CartesianPreComposeMorphism}(a, b, c)$$.

 ‣ AddCartesianPreComposeMorphismWithGivenObjects( C, F ) ( operation )

Returns: nothing

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. $$F: ( s, a, b, c, r ) \mapsto \mathtt{CartesianPreComposeMorphismWithGivenObjects}(s, a, b, c, r)$$.

 ‣ AddCartesianRightCoevaluationMorphism( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, b ) \mapsto \mathtt{CartesianRightCoevaluationMorphism}(a, b)$$.

 ‣ AddCartesianRightCoevaluationMorphismWithGivenRange( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, b, r ) \mapsto \mathtt{CartesianRightCoevaluationMorphismWithGivenRange}(a, b, r)$$.

 ‣ AddCartesianRightEvaluationMorphism( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, b ) \mapsto \mathtt{CartesianRightEvaluationMorphism}(a, b)$$.

 ‣ AddCartesianRightEvaluationMorphismWithGivenSource( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, b, s ) \mapsto \mathtt{CartesianRightEvaluationMorphismWithGivenSource}(a, b, s)$$.

 ‣ AddDirectProductCartesianDualityCompatibilityMorphism( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, b ) \mapsto \mathtt{DirectProductCartesianDualityCompatibilityMorphism}(a, b)$$.

 ‣ AddDirectProductCartesianDualityCompatibilityMorphismWithGivenObjects( C, F ) ( operation )

Returns: nothing

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. $$F: ( s, a, b, r ) \mapsto \mathtt{DirectProductCartesianDualityCompatibilityMorphismWithGivenObjects}(s, a, b, r)$$.

 ‣ AddDirectProductExponentialCompatibilityMorphism( C, F ) ( operation )

Returns: nothing

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. $$F: ( list ) \mapsto \mathtt{DirectProductExponentialCompatibilityMorphism}(list)$$.

 ‣ AddDirectProductExponentialCompatibilityMorphismWithGivenObjects( C, F ) ( operation )

Returns: nothing

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. $$F: ( source, list, range ) \mapsto \mathtt{DirectProductExponentialCompatibilityMorphismWithGivenObjects}(source, list, range)$$.

 ‣ AddDirectProductToExponentialLeftAdjunctMorphism( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, b, f ) \mapsto \mathtt{DirectProductToExponentialLeftAdjunctMorphism}(a, b, f)$$.

 ‣ AddDirectProductToExponentialLeftAdjunctMorphismWithGivenExponential( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, b, f, i ) \mapsto \mathtt{DirectProductToExponentialLeftAdjunctMorphismWithGivenExponential}(a, b, f, i)$$.

 ‣ AddDirectProductToExponentialRightAdjunctMorphism( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, b, f ) \mapsto \mathtt{DirectProductToExponentialRightAdjunctMorphism}(a, b, f)$$.

 ‣ AddDirectProductToExponentialRightAdjunctMorphismWithGivenExponential( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, b, f, i ) \mapsto \mathtt{DirectProductToExponentialRightAdjunctMorphismWithGivenExponential}(a, b, f, i)$$.

 ‣ AddExponentialOnMorphisms( C, F ) ( operation )

Returns: nothing

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. $$F: ( alpha, beta ) \mapsto \mathtt{ExponentialOnMorphisms}(alpha, beta)$$.

 ‣ AddExponentialOnMorphismsWithGivenExponentials( C, F ) ( operation )

Returns: nothing

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. $$F: ( s, alpha, beta, r ) \mapsto \mathtt{ExponentialOnMorphismsWithGivenExponentials}(s, alpha, beta, r)$$.

 ‣ AddExponentialOnObjects( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, b ) \mapsto \mathtt{ExponentialOnObjects}(a, b)$$.

 ‣ AddExponentialToDirectProductLeftAdjunctMorphism( C, F ) ( operation )

Returns: nothing

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. $$F: ( b, c, g ) \mapsto \mathtt{ExponentialToDirectProductLeftAdjunctMorphism}(b, c, g)$$.

 ‣ AddExponentialToDirectProductLeftAdjunctMorphismWithGivenDirectProduct( C, F ) ( operation )

Returns: nothing

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. $$F: ( b, c, g, s ) \mapsto \mathtt{ExponentialToDirectProductLeftAdjunctMorphismWithGivenDirectProduct}(b, c, g, s)$$.

 ‣ AddExponentialToDirectProductRightAdjunctMorphism( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, c, g ) \mapsto \mathtt{ExponentialToDirectProductRightAdjunctMorphism}(a, c, g)$$.

 ‣ AddExponentialToDirectProductRightAdjunctMorphismWithGivenDirectProduct( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, c, g, s ) \mapsto \mathtt{ExponentialToDirectProductRightAdjunctMorphismWithGivenDirectProduct}(a, c, g, s)$$.

 ‣ AddIsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject( C, F ) ( operation )

Returns: nothing

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. $$F: ( a ) \mapsto \mathtt{IsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject}(a)$$.

 ‣ AddIsomorphismFromExponentialIntoTerminalObjectToCartesianDualObject( C, F ) ( operation )

Returns: nothing

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. $$F: ( a ) \mapsto \mathtt{IsomorphismFromExponentialIntoTerminalObjectToCartesianDualObject}(a)$$.

 ‣ AddIsomorphismFromExponentialToObject( C, F ) ( operation )

Returns: nothing

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. $$F: ( a ) \mapsto \mathtt{IsomorphismFromExponentialToObject}(a)$$.

 ‣ AddIsomorphismFromExponentialToObjectWithGivenExponential( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, s ) \mapsto \mathtt{IsomorphismFromExponentialToObjectWithGivenExponential}(a, s)$$.

 ‣ AddIsomorphismFromObjectToExponential( C, F ) ( operation )

Returns: nothing

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. $$F: ( a ) \mapsto \mathtt{IsomorphismFromObjectToExponential}(a)$$.

 ‣ AddIsomorphismFromObjectToExponentialWithGivenExponential( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, r ) \mapsto \mathtt{IsomorphismFromObjectToExponentialWithGivenExponential}(a, r)$$.

 ‣ AddMorphismFromDirectProductToExponential( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, b ) \mapsto \mathtt{MorphismFromDirectProductToExponential}(a, b)$$.

 ‣ AddMorphismFromDirectProductToExponentialWithGivenObjects( C, F ) ( operation )

Returns: nothing

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. $$F: ( s, a, b, r ) \mapsto \mathtt{MorphismFromDirectProductToExponentialWithGivenObjects}(s, a, b, r)$$.

 ‣ AddMorphismToCartesianBidual( C, F ) ( operation )

Returns: nothing

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. $$F: ( a ) \mapsto \mathtt{MorphismToCartesianBidual}(a)$$.

 ‣ AddMorphismToCartesianBidualWithGivenCartesianBidual( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, r ) \mapsto \mathtt{MorphismToCartesianBidualWithGivenCartesianBidual}(a, r)$$.

 ‣ AddUniversalPropertyOfCartesianDual( C, F ) ( operation )

Returns: nothing

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. $$F: ( t, a, alpha ) \mapsto \mathtt{UniversalPropertyOfCartesianDual}(t, a, alpha)$$.

 ‣ AddLeftCartesianDistributivityExpanding( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, L ) \mapsto \mathtt{LeftCartesianDistributivityExpanding}(a, L)$$.

 ‣ AddLeftCartesianDistributivityExpandingWithGivenObjects( C, F ) ( operation )

Returns: nothing

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. $$F: ( s, a, L, r ) \mapsto \mathtt{LeftCartesianDistributivityExpandingWithGivenObjects}(s, a, L, r)$$.

 ‣ AddLeftCartesianDistributivityFactoring( C, F ) ( operation )

Returns: nothing

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. $$F: ( a, L ) \mapsto \mathtt{LeftCartesianDistributivityFactoring}(a, L)$$.

 ‣ AddLeftCartesianDistributivityFactoringWithGivenObjects( C, F ) ( operation )

Returns: nothing

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. $$F: ( s, a, L, r ) \mapsto \mathtt{LeftCartesianDistributivityFactoringWithGivenObjects}(s, a, L, r)$$.

 ‣ AddRightCartesianDistributivityExpanding( C, F ) ( operation )

Returns: nothing

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. $$F: ( L, a ) \mapsto \mathtt{RightCartesianDistributivityExpanding}(L, a)$$.

 ‣ AddRightCartesianDistributivityExpandingWithGivenObjects( C, F ) ( operation )

Returns: nothing

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. $$F: ( s, L, a, r ) \mapsto \mathtt{RightCartesianDistributivityExpandingWithGivenObjects}(s, L, a, r)$$.

 ‣ AddRightCartesianDistributivityFactoring( C, F ) ( operation )

Returns: nothing

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. $$F: ( L, a ) \mapsto \mathtt{RightCartesianDistributivityFactoring}(L, a)$$.

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