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
.
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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)\).
‣ 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)\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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.
‣ 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\).
‣ 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)\).
‣ 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\).
‣ 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)\).
‣ 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\).
‣ 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)\).
‣ 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\).
‣ 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 \).
‣ 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\).
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
.
‣ CoexponentialOnObjects ( a, b ) | ( operation ) |
Returns: an object
The arguments are two objects \(a,b\). The output is the coexponential object \(\mathrm{Coexponential}(a,b)\).
‣ 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)\).
‣ 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)\).
‣ 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.
‣ 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.
‣ 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.
‣ 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.
‣ 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.
‣ 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.
‣ 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.
‣ 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.
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ CocartesianDualOnObjects ( a ) | ( attribute ) |
Returns: an object
The argument is an object \(a\). The output is its codual object \(a_{\vee}\).
‣ 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}\).
‣ 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}\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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\).
‣ 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')\).
‣ 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')\).
‣ 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}\).
‣ 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}\).
‣ 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\).
‣ 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}\).
‣ 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)\).
‣ 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}\).
‣ 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}\).
‣ 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.
‣ 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.
‣ 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)\).
‣ 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)\).
‣ 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\).
‣ 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\).
‣ 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 ) |
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
‣ 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)\).
generated by GAPDoc2HTML