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

2 Cocartesian Categories
 2.1 Cocartesian Categories
 2.2 Cocartesian Coclosed Categories

  2.2-1 CoexponentialOnObjects

  2.2-2 CoexponentialOnMorphisms

  2.2-3 CoexponentialOnMorphismsWithGivenCoexponentials

  2.2-4 CocartesianRightEvaluationMorphism

  2.2-5 CocartesianRightEvaluationMorphismWithGivenRange

  2.2-6 CocartesianRightCoevaluationMorphism

  2.2-7 CocartesianRightCoevaluationMorphismWithGivenSource

  2.2-8 CoproductToCoexponentialRightAdjunctMorphism

  2.2-9 CoproductToCoexponentialRightAdjunctMorphismWithGivenCoexponential

  2.2-10 CoexponentialToCoproductRightAdjunctMorphism

  2.2-11 CoexponentialToCoproductRightAdjunctMorphismWithGivenCoproduct

  2.2-12 CocartesianLeftEvaluationMorphism

  2.2-13 CocartesianLeftEvaluationMorphismWithGivenRange

  2.2-14 CocartesianLeftCoevaluationMorphism

  2.2-15 CocartesianLeftCoevaluationMorphismWithGivenSource

  2.2-16 CoproductToCoexponentialLeftAdjunctMorphism

  2.2-17 CoproductToCoexponentialLeftAdjunctMorphismWithGivenCoexponential

  2.2-18 CoexponentialToCoproductLeftAdjunctMorphism

  2.2-19 CoexponentialToCoproductLeftAdjunctMorphismWithGivenCoproduct

  2.2-20 CocartesianPreCoComposeMorphism

  2.2-21 CocartesianPreCoComposeMorphismWithGivenObjects

  2.2-22 CocartesianPostCoComposeMorphism

  2.2-23 CocartesianPostCoComposeMorphismWithGivenObjects

  2.2-24 CocartesianDualOnObjects

  2.2-25 CocartesianDualOnMorphisms

  2.2-26 CocartesianDualOnMorphismsWithGivenCocartesianDuals

  2.2-27 CocartesianEvaluationForCocartesianDual

  2.2-28 CocartesianEvaluationForCocartesianDualWithGivenCoproduct

  2.2-29 MorphismFromCocartesianBidual

  2.2-30 MorphismFromCocartesianBidualWithGivenCocartesianBidual

  2.2-31 CoexponentialCoproductCompatibilityMorphism

  2.2-32 CoexponentialCoproductCompatibilityMorphismWithGivenObjects

  2.2-33 CocartesianDualityCoproductCompatibilityMorphism

  2.2-34 CocartesianDualityCoproductCompatibilityMorphismWithGivenObjects

  2.2-35 MorphismFromCoexponentialToCoproduct

  2.2-36 MorphismFromCoexponentialToCoproductWithGivenObjects

  2.2-37 IsomorphismFromCocartesianDualObjectToCoexponentialFromInitialObject

  2.2-38 IsomorphismFromCoexponentialFromInitialObjectToCocartesianDualObject

  2.2-39 UniversalPropertyOfCocartesianDual

  2.2-40 CocartesianLambdaIntroduction

  2.2-41 CocartesianLambdaElimination

  2.2-42 IsomorphismFromObjectToCoexponential

  2.2-43 IsomorphismFromObjectToCoexponentialWithGivenCoexponential

  2.2-44 IsomorphismFromCoexponentialToObject

  2.2-45 IsomorphismFromCoexponentialToObjectWithGivenCoexponential
 2.3 Convenience Methods
 2.4 Add-methods

  2.4-1 AddCocartesianBraiding

  2.4-2 AddCocartesianBraidingInverse

  2.4-3 AddCocartesianBraidingInverseWithGivenCoproducts

  2.4-4 AddCocartesianBraidingWithGivenCoproducts

  2.4-5 AddCocartesianAssociatorLeftToRight

  2.4-6 AddCocartesianAssociatorLeftToRightWithGivenCoproducts

  2.4-7 AddCocartesianAssociatorRightToLeft

  2.4-8 AddCocartesianAssociatorRightToLeftWithGivenCoproducts

  2.4-9 AddCocartesianCodiagonal

  2.4-10 AddCocartesianCodiagonalWithGivenCocartesianMultiple

  2.4-11 AddCocartesianLeftUnitor

  2.4-12 AddCocartesianLeftUnitorInverse

  2.4-13 AddCocartesianLeftUnitorInverseWithGivenCoproduct

  2.4-14 AddCocartesianLeftUnitorWithGivenCoproduct

  2.4-15 AddCocartesianRightUnitor

  2.4-16 AddCocartesianRightUnitorInverse

  2.4-17 AddCocartesianRightUnitorInverseWithGivenCoproduct

  2.4-18 AddCocartesianRightUnitorWithGivenCoproduct

  2.4-19 AddCoproductOnMorphisms

  2.4-20 AddCoproductOnMorphismsWithGivenCoproducts

  2.4-21 AddCocartesianDualOnMorphisms

  2.4-22 AddCocartesianDualOnMorphismsWithGivenCocartesianDuals

  2.4-23 AddCocartesianDualOnObjects

  2.4-24 AddCocartesianDualityCoproductCompatibilityMorphism

  2.4-25 AddCocartesianDualityCoproductCompatibilityMorphismWithGivenObjects

  2.4-26 AddCocartesianEvaluationForCocartesianDual

  2.4-27 AddCocartesianEvaluationForCocartesianDualWithGivenCoproduct

  2.4-28 AddCocartesianLambdaElimination

  2.4-29 AddCocartesianLambdaIntroduction

  2.4-30 AddCocartesianLeftCoevaluationMorphism

  2.4-31 AddCocartesianLeftCoevaluationMorphismWithGivenSource

  2.4-32 AddCocartesianLeftEvaluationMorphism

  2.4-33 AddCocartesianLeftEvaluationMorphismWithGivenRange

  2.4-34 AddCocartesianPostCoComposeMorphism

  2.4-35 AddCocartesianPostCoComposeMorphismWithGivenObjects

  2.4-36 AddCocartesianPreCoComposeMorphism

  2.4-37 AddCocartesianPreCoComposeMorphismWithGivenObjects

  2.4-38 AddCocartesianRightCoevaluationMorphism

  2.4-39 AddCocartesianRightCoevaluationMorphismWithGivenSource

  2.4-40 AddCocartesianRightEvaluationMorphism

  2.4-41 AddCocartesianRightEvaluationMorphismWithGivenRange

  2.4-42 AddCoexponentialCoproductCompatibilityMorphism

  2.4-43 AddCoexponentialCoproductCompatibilityMorphismWithGivenObjects

  2.4-44 AddCoexponentialOnMorphisms

  2.4-45 AddCoexponentialOnMorphismsWithGivenCoexponentials

  2.4-46 AddCoexponentialOnObjects

  2.4-47 AddCoexponentialToCoproductLeftAdjunctMorphism

  2.4-48 AddCoexponentialToCoproductLeftAdjunctMorphismWithGivenCoproduct

  2.4-49 AddCoexponentialToCoproductRightAdjunctMorphism

  2.4-50 AddCoexponentialToCoproductRightAdjunctMorphismWithGivenCoproduct

  2.4-51 AddCoproductToCoexponentialLeftAdjunctMorphism

  2.4-52 AddCoproductToCoexponentialLeftAdjunctMorphismWithGivenCoexponential

  2.4-53 AddCoproductToCoexponentialRightAdjunctMorphism

  2.4-54 AddCoproductToCoexponentialRightAdjunctMorphismWithGivenCoexponential

  2.4-55 AddIsomorphismFromCocartesianDualObjectToCoexponentialFromInitialObject

  2.4-56 AddIsomorphismFromCoexponentialFromInitialObjectToCocartesianDualObject

  2.4-57 AddIsomorphismFromCoexponentialToObject

  2.4-58 AddIsomorphismFromCoexponentialToObjectWithGivenCoexponential

  2.4-59 AddIsomorphismFromObjectToCoexponential

  2.4-60 AddIsomorphismFromObjectToCoexponentialWithGivenCoexponential

  2.4-61 AddMorphismFromCocartesianBidual

  2.4-62 AddMorphismFromCocartesianBidualWithGivenCocartesianBidual

  2.4-63 AddMorphismFromCoexponentialToCoproduct

  2.4-64 AddMorphismFromCoexponentialToCoproductWithGivenObjects

  2.4-65 AddUniversalPropertyOfCocartesianDual

  2.4-66 AddLeftCocartesianCodistributivityExpanding

  2.4-67 AddLeftCocartesianCodistributivityExpandingWithGivenObjects

  2.4-68 AddLeftCocartesianCodistributivityFactoring

  2.4-69 AddLeftCocartesianCodistributivityFactoringWithGivenObjects

  2.4-70 AddRightCocartesianCodistributivityExpanding

  2.4-71 AddRightCocartesianCodistributivityExpandingWithGivenObjects

  2.4-72 AddRightCocartesianCodistributivityFactoring

  2.4-73 AddRightCocartesianCodistributivityFactoringWithGivenObjects

2 Cocartesian Categories

2.1 Cocartesian Categories

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

is called a cocartesian category, if

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

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

2.2-8 CoproductToCoexponentialRightAdjunctMorphism
‣ 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.

2.2-9 CoproductToCoexponentialRightAdjunctMorphismWithGivenCoexponential
‣ 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.

2.2-10 CoexponentialToCoproductRightAdjunctMorphism
‣ 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.

2.2-11 CoexponentialToCoproductRightAdjunctMorphismWithGivenCoproduct
‣ 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.

2.2-16 CoproductToCoexponentialLeftAdjunctMorphism
‣ 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.

2.2-17 CoproductToCoexponentialLeftAdjunctMorphismWithGivenCoexponential
‣ 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.

2.2-18 CoexponentialToCoproductLeftAdjunctMorphism
‣ 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.

2.2-19 CoexponentialToCoproductLeftAdjunctMorphismWithGivenCoproduct
‣ 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.

2.4 Add-methods

2.4-1 AddCocartesianBraiding
‣ AddCocartesianBraiding( C, F )( operation )
‣ AddCocartesianBraiding( C, F, weight )( operation )

Returns: nothing

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

2.4-2 AddCocartesianBraidingInverse
‣ AddCocartesianBraidingInverse( C, F )( operation )
‣ AddCocartesianBraidingInverse( C, F, weight )( operation )

Returns: nothing

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

2.4-3 AddCocartesianBraidingInverseWithGivenCoproducts
‣ AddCocartesianBraidingInverseWithGivenCoproducts( C, F )( operation )
‣ AddCocartesianBraidingInverseWithGivenCoproducts( C, F, weight )( operation )

Returns: nothing

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

2.4-4 AddCocartesianBraidingWithGivenCoproducts
‣ AddCocartesianBraidingWithGivenCoproducts( C, F )( operation )
‣ AddCocartesianBraidingWithGivenCoproducts( C, F, weight )( operation )

Returns: nothing

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

2.4-5 AddCocartesianAssociatorLeftToRight
‣ AddCocartesianAssociatorLeftToRight( C, F )( operation )
‣ AddCocartesianAssociatorLeftToRight( C, F, weight )( operation )

Returns: nothing

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

2.4-6 AddCocartesianAssociatorLeftToRightWithGivenCoproducts
‣ AddCocartesianAssociatorLeftToRightWithGivenCoproducts( C, F )( operation )
‣ AddCocartesianAssociatorLeftToRightWithGivenCoproducts( C, F, weight )( operation )

Returns: nothing

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

2.4-7 AddCocartesianAssociatorRightToLeft
‣ AddCocartesianAssociatorRightToLeft( C, F )( operation )
‣ AddCocartesianAssociatorRightToLeft( C, F, weight )( operation )

Returns: nothing

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

2.4-8 AddCocartesianAssociatorRightToLeftWithGivenCoproducts
‣ AddCocartesianAssociatorRightToLeftWithGivenCoproducts( C, F )( operation )
‣ AddCocartesianAssociatorRightToLeftWithGivenCoproducts( C, F, weight )( operation )

Returns: nothing

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

2.4-9 AddCocartesianCodiagonal
‣ AddCocartesianCodiagonal( C, F )( operation )
‣ AddCocartesianCodiagonal( C, F, weight )( operation )

Returns: nothing

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

2.4-10 AddCocartesianCodiagonalWithGivenCocartesianMultiple
‣ AddCocartesianCodiagonalWithGivenCocartesianMultiple( C, F )( operation )
‣ AddCocartesianCodiagonalWithGivenCocartesianMultiple( C, F, weight )( operation )

Returns: nothing

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

2.4-11 AddCocartesianLeftUnitor
‣ AddCocartesianLeftUnitor( C, F )( operation )
‣ AddCocartesianLeftUnitor( C, F, weight )( operation )

Returns: nothing

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

2.4-12 AddCocartesianLeftUnitorInverse
‣ AddCocartesianLeftUnitorInverse( C, F )( operation )
‣ AddCocartesianLeftUnitorInverse( C, F, weight )( operation )

Returns: nothing

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

2.4-13 AddCocartesianLeftUnitorInverseWithGivenCoproduct
‣ AddCocartesianLeftUnitorInverseWithGivenCoproduct( C, F )( operation )
‣ AddCocartesianLeftUnitorInverseWithGivenCoproduct( C, F, weight )( operation )

Returns: nothing

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

2.4-14 AddCocartesianLeftUnitorWithGivenCoproduct
‣ AddCocartesianLeftUnitorWithGivenCoproduct( C, F )( operation )
‣ AddCocartesianLeftUnitorWithGivenCoproduct( C, F, weight )( operation )

Returns: nothing

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

2.4-15 AddCocartesianRightUnitor
‣ AddCocartesianRightUnitor( C, F )( operation )
‣ AddCocartesianRightUnitor( C, F, weight )( operation )

Returns: nothing

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

2.4-16 AddCocartesianRightUnitorInverse
‣ AddCocartesianRightUnitorInverse( C, F )( operation )
‣ AddCocartesianRightUnitorInverse( C, F, weight )( operation )

Returns: nothing

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

2.4-17 AddCocartesianRightUnitorInverseWithGivenCoproduct
‣ AddCocartesianRightUnitorInverseWithGivenCoproduct( C, F )( operation )
‣ AddCocartesianRightUnitorInverseWithGivenCoproduct( C, F, weight )( operation )

Returns: nothing

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

2.4-18 AddCocartesianRightUnitorWithGivenCoproduct
‣ AddCocartesianRightUnitorWithGivenCoproduct( C, F )( operation )
‣ AddCocartesianRightUnitorWithGivenCoproduct( C, F, weight )( operation )

Returns: nothing

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

2.4-19 AddCoproductOnMorphisms
‣ AddCoproductOnMorphisms( C, F )( operation )
‣ AddCoproductOnMorphisms( C, F, weight )( operation )

Returns: nothing

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

2.4-20 AddCoproductOnMorphismsWithGivenCoproducts
‣ AddCoproductOnMorphismsWithGivenCoproducts( C, F )( operation )
‣ AddCoproductOnMorphismsWithGivenCoproducts( C, F, weight )( operation )

Returns: nothing

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

2.4-21 AddCocartesianDualOnMorphisms
‣ AddCocartesianDualOnMorphisms( C, F )( operation )
‣ AddCocartesianDualOnMorphisms( C, F, weight )( operation )

Returns: nothing

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

2.4-22 AddCocartesianDualOnMorphismsWithGivenCocartesianDuals
‣ AddCocartesianDualOnMorphismsWithGivenCocartesianDuals( C, F )( operation )
‣ AddCocartesianDualOnMorphismsWithGivenCocartesianDuals( C, F, weight )( operation )

Returns: nothing

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

2.4-23 AddCocartesianDualOnObjects
‣ AddCocartesianDualOnObjects( C, F )( operation )
‣ AddCocartesianDualOnObjects( C, F, weight )( operation )

Returns: nothing

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

2.4-24 AddCocartesianDualityCoproductCompatibilityMorphism
‣ AddCocartesianDualityCoproductCompatibilityMorphism( C, F )( operation )
‣ AddCocartesianDualityCoproductCompatibilityMorphism( C, F, weight )( operation )

Returns: nothing

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

2.4-25 AddCocartesianDualityCoproductCompatibilityMorphismWithGivenObjects
‣ AddCocartesianDualityCoproductCompatibilityMorphismWithGivenObjects( C, F )( operation )
‣ AddCocartesianDualityCoproductCompatibilityMorphismWithGivenObjects( C, F, weight )( operation )

Returns: nothing

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

2.4-26 AddCocartesianEvaluationForCocartesianDual
‣ AddCocartesianEvaluationForCocartesianDual( C, F )( operation )
‣ AddCocartesianEvaluationForCocartesianDual( C, F, weight )( operation )

Returns: nothing

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

2.4-27 AddCocartesianEvaluationForCocartesianDualWithGivenCoproduct
‣ AddCocartesianEvaluationForCocartesianDualWithGivenCoproduct( C, F )( operation )
‣ AddCocartesianEvaluationForCocartesianDualWithGivenCoproduct( C, F, weight )( operation )

Returns: nothing

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

2.4-28 AddCocartesianLambdaElimination
‣ AddCocartesianLambdaElimination( C, F )( operation )
‣ AddCocartesianLambdaElimination( C, F, weight )( operation )

Returns: nothing

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

2.4-29 AddCocartesianLambdaIntroduction
‣ AddCocartesianLambdaIntroduction( C, F )( operation )
‣ AddCocartesianLambdaIntroduction( C, F, weight )( operation )

Returns: nothing

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

2.4-30 AddCocartesianLeftCoevaluationMorphism
‣ AddCocartesianLeftCoevaluationMorphism( C, F )( operation )
‣ AddCocartesianLeftCoevaluationMorphism( C, F, weight )( operation )

Returns: nothing

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

2.4-31 AddCocartesianLeftCoevaluationMorphismWithGivenSource
‣ AddCocartesianLeftCoevaluationMorphismWithGivenSource( C, F )( operation )
‣ AddCocartesianLeftCoevaluationMorphismWithGivenSource( C, F, weight )( operation )

Returns: nothing

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

2.4-32 AddCocartesianLeftEvaluationMorphism
‣ AddCocartesianLeftEvaluationMorphism( C, F )( operation )
‣ AddCocartesianLeftEvaluationMorphism( C, F, weight )( operation )

Returns: nothing

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

2.4-33 AddCocartesianLeftEvaluationMorphismWithGivenRange
‣ AddCocartesianLeftEvaluationMorphismWithGivenRange( C, F )( operation )
‣ AddCocartesianLeftEvaluationMorphismWithGivenRange( C, F, weight )( operation )

Returns: nothing

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

2.4-34 AddCocartesianPostCoComposeMorphism
‣ AddCocartesianPostCoComposeMorphism( C, F )( operation )
‣ AddCocartesianPostCoComposeMorphism( C, F, weight )( operation )

Returns: nothing

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

2.4-35 AddCocartesianPostCoComposeMorphismWithGivenObjects
‣ AddCocartesianPostCoComposeMorphismWithGivenObjects( C, F )( operation )
‣ AddCocartesianPostCoComposeMorphismWithGivenObjects( C, F, weight )( operation )

Returns: nothing

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

2.4-36 AddCocartesianPreCoComposeMorphism
‣ AddCocartesianPreCoComposeMorphism( C, F )( operation )
‣ AddCocartesianPreCoComposeMorphism( C, F, weight )( operation )

Returns: nothing

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

2.4-37 AddCocartesianPreCoComposeMorphismWithGivenObjects
‣ AddCocartesianPreCoComposeMorphismWithGivenObjects( C, F )( operation )
‣ AddCocartesianPreCoComposeMorphismWithGivenObjects( C, F, weight )( operation )

Returns: nothing

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

2.4-38 AddCocartesianRightCoevaluationMorphism
‣ AddCocartesianRightCoevaluationMorphism( C, F )( operation )
‣ AddCocartesianRightCoevaluationMorphism( C, F, weight )( operation )

Returns: nothing

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

2.4-39 AddCocartesianRightCoevaluationMorphismWithGivenSource
‣ AddCocartesianRightCoevaluationMorphismWithGivenSource( C, F )( operation )
‣ AddCocartesianRightCoevaluationMorphismWithGivenSource( C, F, weight )( operation )

Returns: nothing

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

2.4-40 AddCocartesianRightEvaluationMorphism
‣ AddCocartesianRightEvaluationMorphism( C, F )( operation )
‣ AddCocartesianRightEvaluationMorphism( C, F, weight )( operation )

Returns: nothing

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

2.4-41 AddCocartesianRightEvaluationMorphismWithGivenRange
‣ AddCocartesianRightEvaluationMorphismWithGivenRange( C, F )( operation )
‣ AddCocartesianRightEvaluationMorphismWithGivenRange( C, F, weight )( operation )

Returns: nothing

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

2.4-42 AddCoexponentialCoproductCompatibilityMorphism
‣ AddCoexponentialCoproductCompatibilityMorphism( C, F )( operation )
‣ AddCoexponentialCoproductCompatibilityMorphism( C, F, weight )( operation )

Returns: nothing

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

2.4-43 AddCoexponentialCoproductCompatibilityMorphismWithGivenObjects
‣ AddCoexponentialCoproductCompatibilityMorphismWithGivenObjects( C, F )( operation )
‣ AddCoexponentialCoproductCompatibilityMorphismWithGivenObjects( C, F, weight )( operation )

Returns: nothing

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

2.4-44 AddCoexponentialOnMorphisms
‣ AddCoexponentialOnMorphisms( C, F )( operation )
‣ AddCoexponentialOnMorphisms( C, F, weight )( operation )

Returns: nothing

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

2.4-45 AddCoexponentialOnMorphismsWithGivenCoexponentials
‣ AddCoexponentialOnMorphismsWithGivenCoexponentials( C, F )( operation )
‣ AddCoexponentialOnMorphismsWithGivenCoexponentials( C, F, weight )( operation )

Returns: nothing

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

2.4-46 AddCoexponentialOnObjects
‣ AddCoexponentialOnObjects( C, F )( operation )
‣ AddCoexponentialOnObjects( C, F, weight )( operation )

Returns: nothing

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

2.4-47 AddCoexponentialToCoproductLeftAdjunctMorphism
‣ AddCoexponentialToCoproductLeftAdjunctMorphism( C, F )( operation )
‣ AddCoexponentialToCoproductLeftAdjunctMorphism( C, F, weight )( operation )

Returns: nothing

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

2.4-48 AddCoexponentialToCoproductLeftAdjunctMorphismWithGivenCoproduct
‣ AddCoexponentialToCoproductLeftAdjunctMorphismWithGivenCoproduct( C, F )( operation )
‣ AddCoexponentialToCoproductLeftAdjunctMorphismWithGivenCoproduct( C, F, weight )( operation )

Returns: nothing

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

2.4-49 AddCoexponentialToCoproductRightAdjunctMorphism
‣ AddCoexponentialToCoproductRightAdjunctMorphism( C, F )( operation )
‣ AddCoexponentialToCoproductRightAdjunctMorphism( C, F, weight )( operation )

Returns: nothing

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

2.4-50 AddCoexponentialToCoproductRightAdjunctMorphismWithGivenCoproduct
‣ AddCoexponentialToCoproductRightAdjunctMorphismWithGivenCoproduct( C, F )( operation )
‣ AddCoexponentialToCoproductRightAdjunctMorphismWithGivenCoproduct( C, F, weight )( operation )

Returns: nothing

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

2.4-51 AddCoproductToCoexponentialLeftAdjunctMorphism
‣ AddCoproductToCoexponentialLeftAdjunctMorphism( C, F )( operation )
‣ AddCoproductToCoexponentialLeftAdjunctMorphism( C, F, weight )( operation )

Returns: nothing

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

2.4-52 AddCoproductToCoexponentialLeftAdjunctMorphismWithGivenCoexponential
‣ AddCoproductToCoexponentialLeftAdjunctMorphismWithGivenCoexponential( C, F )( operation )
‣ AddCoproductToCoexponentialLeftAdjunctMorphismWithGivenCoexponential( C, F, weight )( operation )

Returns: nothing

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

2.4-53 AddCoproductToCoexponentialRightAdjunctMorphism
‣ AddCoproductToCoexponentialRightAdjunctMorphism( C, F )( operation )
‣ AddCoproductToCoexponentialRightAdjunctMorphism( C, F, weight )( operation )

Returns: nothing

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

2.4-54 AddCoproductToCoexponentialRightAdjunctMorphismWithGivenCoexponential
‣ AddCoproductToCoexponentialRightAdjunctMorphismWithGivenCoexponential( C, F )( operation )
‣ AddCoproductToCoexponentialRightAdjunctMorphismWithGivenCoexponential( C, F, weight )( operation )

Returns: nothing

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

2.4-55 AddIsomorphismFromCocartesianDualObjectToCoexponentialFromInitialObject
‣ AddIsomorphismFromCocartesianDualObjectToCoexponentialFromInitialObject( C, F )( operation )
‣ AddIsomorphismFromCocartesianDualObjectToCoexponentialFromInitialObject( C, F, weight )( operation )

Returns: nothing

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

2.4-56 AddIsomorphismFromCoexponentialFromInitialObjectToCocartesianDualObject
‣ AddIsomorphismFromCoexponentialFromInitialObjectToCocartesianDualObject( C, F )( operation )
‣ AddIsomorphismFromCoexponentialFromInitialObjectToCocartesianDualObject( C, F, weight )( operation )

Returns: nothing

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

2.4-57 AddIsomorphismFromCoexponentialToObject
‣ AddIsomorphismFromCoexponentialToObject( C, F )( operation )
‣ AddIsomorphismFromCoexponentialToObject( C, F, weight )( operation )

Returns: nothing

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

2.4-58 AddIsomorphismFromCoexponentialToObjectWithGivenCoexponential
‣ AddIsomorphismFromCoexponentialToObjectWithGivenCoexponential( C, F )( operation )
‣ AddIsomorphismFromCoexponentialToObjectWithGivenCoexponential( C, F, weight )( operation )

Returns: nothing

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

2.4-59 AddIsomorphismFromObjectToCoexponential
‣ AddIsomorphismFromObjectToCoexponential( C, F )( operation )
‣ AddIsomorphismFromObjectToCoexponential( C, F, weight )( operation )

Returns: nothing

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

2.4-60 AddIsomorphismFromObjectToCoexponentialWithGivenCoexponential
‣ AddIsomorphismFromObjectToCoexponentialWithGivenCoexponential( C, F )( operation )
‣ AddIsomorphismFromObjectToCoexponentialWithGivenCoexponential( C, F, weight )( operation )

Returns: nothing

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

2.4-61 AddMorphismFromCocartesianBidual
‣ AddMorphismFromCocartesianBidual( C, F )( operation )
‣ AddMorphismFromCocartesianBidual( C, F, weight )( operation )

Returns: nothing

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

2.4-62 AddMorphismFromCocartesianBidualWithGivenCocartesianBidual
‣ AddMorphismFromCocartesianBidualWithGivenCocartesianBidual( C, F )( operation )
‣ AddMorphismFromCocartesianBidualWithGivenCocartesianBidual( C, F, weight )( operation )

Returns: nothing

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

2.4-63 AddMorphismFromCoexponentialToCoproduct
‣ AddMorphismFromCoexponentialToCoproduct( C, F )( operation )
‣ AddMorphismFromCoexponentialToCoproduct( C, F, weight )( operation )

Returns: nothing

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

2.4-64 AddMorphismFromCoexponentialToCoproductWithGivenObjects
‣ AddMorphismFromCoexponentialToCoproductWithGivenObjects( C, F )( operation )
‣ AddMorphismFromCoexponentialToCoproductWithGivenObjects( C, F, weight )( operation )

Returns: nothing

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

2.4-65 AddUniversalPropertyOfCocartesianDual
‣ AddUniversalPropertyOfCocartesianDual( C, F )( operation )
‣ AddUniversalPropertyOfCocartesianDual( C, F, weight )( operation )

Returns: nothing

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

2.4-66 AddLeftCocartesianCodistributivityExpanding
‣ AddLeftCocartesianCodistributivityExpanding( C, F )( operation )
‣ AddLeftCocartesianCodistributivityExpanding( C, F, weight )( operation )

Returns: nothing

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

2.4-67 AddLeftCocartesianCodistributivityExpandingWithGivenObjects
‣ AddLeftCocartesianCodistributivityExpandingWithGivenObjects( C, F )( operation )
‣ AddLeftCocartesianCodistributivityExpandingWithGivenObjects( C, F, weight )( operation )

Returns: nothing

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

2.4-68 AddLeftCocartesianCodistributivityFactoring
‣ AddLeftCocartesianCodistributivityFactoring( C, F )( operation )
‣ AddLeftCocartesianCodistributivityFactoring( C, F, weight )( operation )

Returns: nothing

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

2.4-69 AddLeftCocartesianCodistributivityFactoringWithGivenObjects
‣ AddLeftCocartesianCodistributivityFactoringWithGivenObjects( C, F )( operation )
‣ AddLeftCocartesianCodistributivityFactoringWithGivenObjects( C, F, weight )( operation )

Returns: nothing

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

2.4-70 AddRightCocartesianCodistributivityExpanding
‣ AddRightCocartesianCodistributivityExpanding( C, F )( operation )
‣ AddRightCocartesianCodistributivityExpanding( C, F, weight )( operation )

Returns: nothing

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

2.4-71 AddRightCocartesianCodistributivityExpandingWithGivenObjects
‣ AddRightCocartesianCodistributivityExpandingWithGivenObjects( C, F )( operation )
‣ AddRightCocartesianCodistributivityExpandingWithGivenObjects( C, F, weight )( operation )

Returns: nothing

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

2.4-72 AddRightCocartesianCodistributivityFactoring
‣ AddRightCocartesianCodistributivityFactoring( C, F )( operation )
‣ AddRightCocartesianCodistributivityFactoring( C, F, weight )( operation )

Returns: nothing

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

2.4-73 AddRightCocartesianCodistributivityFactoringWithGivenObjects
‣ AddRightCocartesianCodistributivityFactoringWithGivenObjects( C, F )( operation )
‣ AddRightCocartesianCodistributivityFactoringWithGivenObjects( C, F, weight )( operation )

Returns: nothing

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

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

generated by GAPDoc2HTML