Goto Chapter: Top 1 2 3 4 5 6 Ind

### 2 Cocartesian Categories

#### 2.1 Cocartesian Categories

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

• a category \mathbf{C},

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

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

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

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

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

is called a cocartesian category, if

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

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

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

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

The corresponding GAP property is given by IsCocartesianCategory.

##### 2.1-1 CocartesianBraiding
 ‣ CocartesianBraiding( a, b ) ( operation )

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

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

##### 2.1-2 CocartesianBraidingWithGivenCoproducts
 ‣ CocartesianBraidingWithGivenCoproducts( s, a, b, r ) ( operation )

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

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

##### 2.1-3 CocartesianBraidingInverse
 ‣ CocartesianBraidingInverse( a, b ) ( operation )

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

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

##### 2.1-4 CocartesianBraidingInverseWithGivenCoproducts
 ‣ CocartesianBraidingInverseWithGivenCoproducts( s, a, b, r ) ( operation )

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

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

##### 2.1-5 CoproductOnMorphisms
 ‣ CoproductOnMorphisms( alpha, beta ) ( operation )

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

The arguments are two morphisms \alpha: a \rightarrow a', \beta: b \rightarrow b'. The output is the coproduct \alpha \sqcup \beta.

##### 2.1-6 CoproductOnMorphismsWithGivenCoproducts
 ‣ CoproductOnMorphismsWithGivenCoproducts( s, alpha, beta, r ) ( operation )

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

The arguments are an object s = a \sqcup b, two morphisms \alpha: a \rightarrow a', \beta: b \rightarrow b', and an object r = a' \sqcup b'. The output is the coproduct \alpha \sqcup \beta.

##### 2.1-7 CocartesianAssociatorRightToLeft
 ‣ CocartesianAssociatorRightToLeft( a, b, c ) ( operation )

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

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

##### 2.1-8 CocartesianAssociatorRightToLeftWithGivenCoproducts
 ‣ CocartesianAssociatorRightToLeftWithGivenCoproducts( s, a, b, c, r ) ( operation )

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

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

##### 2.1-9 CocartesianAssociatorLeftToRight
 ‣ CocartesianAssociatorLeftToRight( a, b, c ) ( operation )

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

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

##### 2.1-10 CocartesianAssociatorLeftToRightWithGivenCoproducts
 ‣ CocartesianAssociatorLeftToRightWithGivenCoproducts( s, a, b, c, r ) ( operation )

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

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

##### 2.1-11 CocartesianLeftUnitor
 ‣ CocartesianLeftUnitor( a ) ( attribute )

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

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

##### 2.1-12 CocartesianLeftUnitorWithGivenCoproduct
 ‣ CocartesianLeftUnitorWithGivenCoproduct( a, s ) ( operation )

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

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

##### 2.1-13 CocartesianLeftUnitorInverse
 ‣ CocartesianLeftUnitorInverse( a ) ( attribute )

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

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

##### 2.1-14 CocartesianLeftUnitorInverseWithGivenCoproduct
 ‣ CocartesianLeftUnitorInverseWithGivenCoproduct( a, r ) ( operation )

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

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

##### 2.1-15 CocartesianRightUnitor
 ‣ CocartesianRightUnitor( a ) ( attribute )

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

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

##### 2.1-16 CocartesianRightUnitorWithGivenCoproduct
 ‣ CocartesianRightUnitorWithGivenCoproduct( a, s ) ( operation )

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

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

##### 2.1-17 CocartesianRightUnitorInverse
 ‣ CocartesianRightUnitorInverse( a ) ( attribute )

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

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

##### 2.1-18 CocartesianRightUnitorInverseWithGivenCoproduct
 ‣ CocartesianRightUnitorInverseWithGivenCoproduct( a, r ) ( operation )

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

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

##### 2.1-19 CocartesianCodiagonal
 ‣ CocartesianCodiagonal( a, n ) ( operation )

Returns: a morphism in \mathrm{Hom}(\sqcup_{i=1}^n a, a).

The arguments are an object a and an integer n \geq 0. The output is the codiagonal morphism from the n-fold cocartesian multiple \sqcup_{i=1}^n a to a. If the category does not support empty limits, n must be not be 0.

##### 2.1-20 CocartesianCodiagonalWithGivenCocartesianMultiple
 ‣ CocartesianCodiagonalWithGivenCocartesianMultiple( a, n, b ) ( operation )

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

The arguments are an object a, an integer n, and an object b equal to the n-fold cocartesian multiple \sqcup_{i=1}^n a of a. The output is the codiagonal morphism from b to a.

##### 2.1-21 LeftCocartesianCodistributivityExpanding
 ‣ LeftCocartesianCodistributivityExpanding( a, L ) ( operation )

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

##### 2.1-22 LeftCocartesianCodistributivityExpandingWithGivenObjects
 ‣ LeftCocartesianCodistributivityExpandingWithGivenObjects( s, a, L, r ) ( operation )

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

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

##### 2.1-23 LeftCocartesianCodistributivityFactoring
 ‣ LeftCocartesianCodistributivityFactoring( a, L ) ( operation )

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

##### 2.1-24 LeftCocartesianCodistributivityFactoringWithGivenObjects
 ‣ LeftCocartesianCodistributivityFactoringWithGivenObjects( s, a, L, r ) ( operation )

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

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

##### 2.1-25 RightCocartesianCodistributivityExpanding
 ‣ RightCocartesianCodistributivityExpanding( L, a ) ( operation )

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

##### 2.1-26 RightCocartesianCodistributivityExpandingWithGivenObjects
 ‣ RightCocartesianCodistributivityExpandingWithGivenObjects( s, L, a, r ) ( operation )

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

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

##### 2.1-27 RightCocartesianCodistributivityFactoring
 ‣ RightCocartesianCodistributivityFactoring( L, a ) ( operation )

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

##### 2.1-28 RightCocartesianCodistributivityFactoringWithGivenObjects
 ‣ RightCocartesianCodistributivityFactoringWithGivenObjects( s, L, a, r ) ( operation )

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

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

#### 2.2 Cocartesian Coclosed Categories

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

The corresponding GAP property is called IsCocartesianCoclosedCategory.

##### 2.2-1 CoexponentialOnObjects
 ‣ CoexponentialOnObjects( a, b ) ( operation )

Returns: an object

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

##### 2.2-2 CoexponentialOnMorphisms
 ‣ CoexponentialOnMorphisms( alpha, beta ) ( operation )

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

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

##### 2.2-3 CoexponentialOnMorphismsWithGivenCoexponentials
 ‣ CoexponentialOnMorphismsWithGivenCoexponentials( s, alpha, beta, r ) ( operation )

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

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

##### 2.2-4 CocartesianRightEvaluationMorphism
 ‣ CocartesianRightEvaluationMorphism( a, b ) ( operation )

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

The arguments are two objects a, b. The output is the coclosed right evaluation morphism \mathrm{cocaev}_{a,b}: b \rightarrow a \sqcup \mathrm{Coexponential}(b,a), i.e., the unit of the coexponential-coproduct adjunction.

##### 2.2-5 CocartesianRightEvaluationMorphismWithGivenRange
 ‣ CocartesianRightEvaluationMorphismWithGivenRange( a, b, r ) ( operation )

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

The arguments are two objects a,b and an object r = a \sqcup \mathrm{Coexponential}(b,a). The output is the coclosed right evaluation morphism \mathrm{cocaev}_{a,b}: b \rightarrow a \sqcup \mathrm{Coexponential}(b,a), i.e., the unit of the coexponential-coproduct adjunction.

##### 2.2-6 CocartesianRightCoevaluationMorphism
 ‣ CocartesianRightCoevaluationMorphism( a, b ) ( operation )

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

The arguments are two objects a,b. The output is the coclosed right coevaluation morphism \mathrm{cocacoev}_{a,b}: \mathrm{Coexponential}(a \sqcup b, a) \rightarrow b, i.e., the counit of the coexponential-coproduct adjunction.

##### 2.2-7 CocartesianRightCoevaluationMorphismWithGivenSource
 ‣ CocartesianRightCoevaluationMorphismWithGivenSource( a, b, s ) ( operation )

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

The arguments are two objects a,b and an object s = \mathrm{Coexponential}(a \sqcup b, a). The output is the coclosed right coevaluation morphism \mathrm{cocacoev}_{a,b}: \mathrm{Coexponential}(a \sqcup b, a) \rightarrow b, i.e., the unit of the coexponential-coproduct adjunction.

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

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

The arguments are two objects b,c and a morphism g: a \rightarrow b \sqcup c. The output is a morphism f: \mathrm{Coexponential}(a,b) \rightarrow c corresponding to g under the coexponential-coproduct adjunction.

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

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

The arguments are two objects b,c, a morphism g: a \rightarrow b \sqcup c and an object i = \mathrm{Coexponential}(a,b). The output is a morphism f: \mathrm{Coexponential}(a,b) \rightarrow c corresponding to g under the coexponential-coproduct adjunction.

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

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

The arguments are two objects a,b and a morphism f: \mathrm{Coexponential}(a,b) \rightarrow c. The output is a morphism g: a \rightarrow b \sqcup c corresponding to f under the coexponential-coproduct adjunction.

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

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

The arguments are two objects a,b, a morphism f: \mathrm{Coexponential}(a,b) \rightarrow c and an object t = b \sqcup c. The output is a morphism g: a \rightarrow t corresponding to f under the coexponential-coproduct adjunction.

##### 2.2-12 CocartesianLeftEvaluationMorphism
 ‣ CocartesianLeftEvaluationMorphism( a, b ) ( operation )

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

The arguments are two objects a, b. The output is the coclosed left evaluation morphism \mathrm{cocaev}_{a,b}: b \rightarrow \mathrm{Coexponential}(b,a) \sqcup a, i.e., the unit of the coexponential-coproduct adjunction.

##### 2.2-13 CocartesianLeftEvaluationMorphismWithGivenRange
 ‣ CocartesianLeftEvaluationMorphismWithGivenRange( a, b, r ) ( operation )

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

The arguments are two objects a,b and an object r = \mathrm{Coexponential}(b,a) \sqcup a. The output is the coclosed left evaluation morphism \mathrm{cocaev}_{a,b}: b \rightarrow \mathrm{Coexponential}(b,a) \sqcup a, i.e., the unit of the coexponential-coproduct adjunction.

##### 2.2-14 CocartesianLeftCoevaluationMorphism
 ‣ CocartesianLeftCoevaluationMorphism( a, b ) ( operation )

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

The arguments are two objects a,b. The output is the coclosed left coevaluation morphism \mathrm{cocacoev}_{a,b}: \mathrm{Coexponential}(b \sqcup a, a) \rightarrow b, i.e., the counit of the coexponential-coproduct adjunction.

##### 2.2-15 CocartesianLeftCoevaluationMorphismWithGivenSource
 ‣ CocartesianLeftCoevaluationMorphismWithGivenSource( a, b, s ) ( operation )

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

The arguments are two objects a,b and an object s = \mathrm{Coexponential}(b \sqcup a, a). The output is the coclosed left coevaluation morphism \mathrm{cocacoev}_{a,b}: \mathrm{Coexponential}(b \sqcup a, a) \rightarrow b, i.e., the unit of the coexponential-coproduct adjunction.

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

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

The arguments are two objects b,c and a morphism g: a \rightarrow b \sqcup c. The output is a morphism f: \mathrm{Coexponential}(a,c) \rightarrow b corresponding to g under the coexponential-coproduct adjunction.

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

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

The arguments are two objects b,c, a morphism g: a \rightarrow b \sqcup c and an object i = \mathrm{Coexponential}(a,c). The output is a morphism f: \mathrm{Coexponential}(a,c) \rightarrow b corresponding to g under the coexponential-coproduct adjunction.

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

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

The arguments are two objects a,c and a morphism f: \mathrm{Coexponential}(a,c) \rightarrow b. The output is a morphism g: a \rightarrow b \sqcup c corresponding to f under the coexponential-coproduct adjunction.

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

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

The arguments are two objects a,c, a morphism f: \mathrm{Coexponential}(a,c) \rightarrow b and an object t = b \sqcup c. The output is a morphism g: a \rightarrow t corresponding to f under the coexponential-coproduct adjunction.

##### 2.2-20 CocartesianPreCoComposeMorphism
 ‣ CocartesianPreCoComposeMorphism( a, b, c ) ( operation )

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

The arguments are three objects a,b,c. The output is the precocomposition morphism \mathrm{CocartesianPreCoComposeMorphism}_{a,b,c}: \mathrm{Coexponential}(a,c) \rightarrow \mathrm{Coexponential}(b,c) \sqcup \mathrm{Coexponential}(a,b).

##### 2.2-21 CocartesianPreCoComposeMorphismWithGivenObjects
 ‣ CocartesianPreCoComposeMorphismWithGivenObjects( s, a, b, c, r ) ( operation )

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

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

##### 2.2-22 CocartesianPostCoComposeMorphism
 ‣ CocartesianPostCoComposeMorphism( a, b, c ) ( operation )

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

The arguments are three objects a,b,c. The output is the postcocomposition morphism \mathrm{CocartesianPostCoComposeMorphism}_{a,b,c}: \mathrm{Coexponential}(a,c) \rightarrow \mathrm{Coexponential}(a,b) \sqcup \mathrm{Coexponential}(b,c).

##### 2.2-23 CocartesianPostCoComposeMorphismWithGivenObjects
 ‣ CocartesianPostCoComposeMorphismWithGivenObjects( s, a, b, c, r ) ( operation )

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

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

##### 2.2-24 CocartesianDualOnObjects
 ‣ CocartesianDualOnObjects( a ) ( attribute )

Returns: an object

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

##### 2.2-25 CocartesianDualOnMorphisms
 ‣ CocartesianDualOnMorphisms( alpha ) ( attribute )

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

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

##### 2.2-26 CocartesianDualOnMorphismsWithGivenCocartesianDuals
 ‣ CocartesianDualOnMorphismsWithGivenCocartesianDuals( 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}.

##### 2.2-27 CocartesianEvaluationForCocartesianDual
 ‣ CocartesianEvaluationForCocartesianDual( a ) ( attribute )

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

The argument is an object a. The output is the cocartesian evaluation morphism \mathrm{cocaev}_{a}: 1 \rightarrow a_{\vee} \sqcup a.

##### 2.2-28 CocartesianEvaluationForCocartesianDualWithGivenCoproduct
 ‣ CocartesianEvaluationForCocartesianDualWithGivenCoproduct( s, a, r ) ( operation )

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

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

##### 2.2-29 MorphismFromCocartesianBidual
 ‣ MorphismFromCocartesianBidual( a ) ( attribute )

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

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

##### 2.2-30 MorphismFromCocartesianBidualWithGivenCocartesianBidual
 ‣ MorphismFromCocartesianBidualWithGivenCocartesianBidual( a, s ) ( operation )

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

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

##### 2.2-31 CoexponentialCoproductCompatibilityMorphism
 ‣ CoexponentialCoproductCompatibilityMorphism( list ) ( operation )

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

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

##### 2.2-32 CoexponentialCoproductCompatibilityMorphismWithGivenObjects
 ‣ CoexponentialCoproductCompatibilityMorphismWithGivenObjects( 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{Coexponential}(a \sqcup a', b \sqcup b') and r = \mathrm{Coexponential}(a,b) \sqcup \mathrm{Coexponential}(a',b'). The output is the natural morphism \mathrm{CoexponentialCoproductCompatibilityMorphismWithGivenObjects}_{a,a',b,b'}: \mathrm{Coexponential}(a \sqcup a', b \sqcup b') \rightarrow \mathrm{Coexponential}(a,b) \sqcup \mathrm{Coexponential}(a',b').

##### 2.2-33 CocartesianDualityCoproductCompatibilityMorphism
 ‣ CocartesianDualityCoproductCompatibilityMorphism( a, b ) ( operation )

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

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

##### 2.2-34 CocartesianDualityCoproductCompatibilityMorphismWithGivenObjects
 ‣ CocartesianDualityCoproductCompatibilityMorphismWithGivenObjects( s, a, b, r ) ( operation )

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

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

##### 2.2-35 MorphismFromCoexponentialToCoproduct
 ‣ MorphismFromCoexponentialToCoproduct( a, b ) ( operation )

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

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

##### 2.2-36 MorphismFromCoexponentialToCoproductWithGivenObjects
 ‣ MorphismFromCoexponentialToCoproductWithGivenObjects( s, a, b, r ) ( operation )

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

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

##### 2.2-37 IsomorphismFromCocartesianDualObjectToCoexponentialFromInitialObject
 ‣ IsomorphismFromCocartesianDualObjectToCoexponentialFromInitialObject( a ) ( attribute )

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

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

##### 2.2-38 IsomorphismFromCoexponentialFromInitialObjectToCocartesianDualObject
 ‣ IsomorphismFromCoexponentialFromInitialObjectToCocartesianDualObject( a ) ( attribute )

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

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

##### 2.2-39 UniversalPropertyOfCocartesianDual
 ‣ UniversalPropertyOfCocartesianDual( t, a, alpha ) ( operation )

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

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

##### 2.2-40 CocartesianLambdaIntroduction
 ‣ CocartesianLambdaIntroduction( alpha ) ( attribute )

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

The argument is a morphism \alpha: a \rightarrow b. The output is the corresponding morphism \mathrm{Coexponential}(a,b) \rightarrow 1 under the coexponential-coproduct adjunction.

##### 2.2-41 CocartesianLambdaElimination
 ‣ CocartesianLambdaElimination( a, b, alpha ) ( operation )

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

The arguments are two objects a,b, and a morphism \alpha: \mathrm{Coexponential}(a,b) \rightarrow 1. The output is a morphism a \rightarrow b corresponding to \alpha under the coexponential-coproduct adjunction.

##### 2.2-42 IsomorphismFromObjectToCoexponential
 ‣ IsomorphismFromObjectToCoexponential( a ) ( attribute )

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

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

##### 2.2-43 IsomorphismFromObjectToCoexponentialWithGivenCoexponential
 ‣ IsomorphismFromObjectToCoexponentialWithGivenCoexponential( a, r ) ( operation )

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

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

##### 2.2-44 IsomorphismFromCoexponentialToObject
 ‣ IsomorphismFromCoexponentialToObject( a ) ( attribute )

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

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

##### 2.2-45 IsomorphismFromCoexponentialToObjectWithGivenCoexponential
 ‣ IsomorphismFromCoexponentialToObjectWithGivenCoexponential( a, s ) ( operation )

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

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

#### 2.3 Convenience Methods

##### 2.3-1 Coexponential
 ‣ Coexponential( a, b ) ( operation )

Returns: a cell

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

 ‣ AddCocartesianBraiding( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianBraidingInverse( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianBraidingInverseWithGivenCoproducts( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianBraidingWithGivenCoproducts( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianAssociatorLeftToRight( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianAssociatorLeftToRightWithGivenCoproducts( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianAssociatorRightToLeft( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianAssociatorRightToLeftWithGivenCoproducts( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianCodiagonal( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianCodiagonalWithGivenCocartesianMultiple( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianLeftUnitor( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianLeftUnitorInverse( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianLeftUnitorInverseWithGivenCoproduct( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianLeftUnitorWithGivenCoproduct( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianRightUnitor( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianRightUnitorInverse( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianRightUnitorInverseWithGivenCoproduct( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianRightUnitorWithGivenCoproduct( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCoproductOnMorphisms( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCoproductOnMorphismsWithGivenCoproducts( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianDualOnMorphisms( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianDualOnMorphismsWithGivenCocartesianDuals( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianDualOnObjects( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianDualityCoproductCompatibilityMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianDualityCoproductCompatibilityMorphismWithGivenObjects( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianEvaluationForCocartesianDual( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianEvaluationForCocartesianDualWithGivenCoproduct( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianLambdaElimination( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianLambdaIntroduction( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianLeftCoevaluationMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianLeftCoevaluationMorphismWithGivenSource( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianLeftEvaluationMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianLeftEvaluationMorphismWithGivenRange( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianPostCoComposeMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianPostCoComposeMorphismWithGivenObjects( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianPreCoComposeMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianPreCoComposeMorphismWithGivenObjects( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianRightCoevaluationMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianRightCoevaluationMorphismWithGivenSource( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianRightEvaluationMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCocartesianRightEvaluationMorphismWithGivenRange( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCoexponentialCoproductCompatibilityMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCoexponentialCoproductCompatibilityMorphismWithGivenObjects( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCoexponentialOnMorphisms( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCoexponentialOnMorphismsWithGivenCoexponentials( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCoexponentialOnObjects( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCoexponentialToCoproductLeftAdjunctMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCoexponentialToCoproductLeftAdjunctMorphismWithGivenCoproduct( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCoexponentialToCoproductRightAdjunctMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCoexponentialToCoproductRightAdjunctMorphismWithGivenCoproduct( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCoproductToCoexponentialLeftAdjunctMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCoproductToCoexponentialLeftAdjunctMorphismWithGivenCoexponential( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCoproductToCoexponentialRightAdjunctMorphism( C, F ) ( operation )

Returns: nothing

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

 ‣ AddCoproductToCoexponentialRightAdjunctMorphismWithGivenCoexponential( C, F ) ( operation )

Returns: nothing

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

 ‣ AddIsomorphismFromCocartesianDualObjectToCoexponentialFromInitialObject( C, F ) ( operation )

Returns: nothing

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

 ‣ AddIsomorphismFromCoexponentialFromInitialObjectToCocartesianDualObject( C, F ) ( operation )

Returns: nothing

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

 ‣ AddIsomorphismFromCoexponentialToObject( C, F ) ( operation )

Returns: nothing

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

 ‣ AddIsomorphismFromCoexponentialToObjectWithGivenCoexponential( C, F ) ( operation )

Returns: nothing

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

 ‣ AddIsomorphismFromObjectToCoexponential( C, F ) ( operation )

Returns: nothing

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

 ‣ AddIsomorphismFromObjectToCoexponentialWithGivenCoexponential( C, F ) ( operation )

Returns: nothing

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

 ‣ AddMorphismFromCocartesianBidual( C, F ) ( operation )

Returns: nothing

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

 ‣ AddMorphismFromCocartesianBidualWithGivenCocartesianBidual( C, F ) ( operation )

Returns: nothing

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

 ‣ AddMorphismFromCoexponentialToCoproduct( C, F ) ( operation )

Returns: nothing

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

 ‣ AddMorphismFromCoexponentialToCoproductWithGivenObjects( C, F ) ( operation )

Returns: nothing

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

 ‣ AddUniversalPropertyOfCocartesianDual( C, F ) ( operation )

Returns: nothing

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

 ‣ AddLeftCocartesianCodistributivityExpanding( C, F ) ( operation )

Returns: nothing

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

 ‣ AddLeftCocartesianCodistributivityExpandingWithGivenObjects( C, F ) ( operation )

Returns: nothing

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

 ‣ AddLeftCocartesianCodistributivityFactoring( C, F ) ( operation )

Returns: nothing

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

 ‣ AddLeftCocartesianCodistributivityFactoringWithGivenObjects( C, F ) ( operation )

Returns: nothing

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

 ‣ AddRightCocartesianCodistributivityExpanding( C, F ) ( operation )

Returns: nothing

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

 ‣ AddRightCocartesianCodistributivityExpandingWithGivenObjects( C, F ) ( operation )

Returns: nothing

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

 ‣ AddRightCocartesianCodistributivityFactoring( C, F ) ( operation )

Returns: nothing

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

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