A \(6\)-tuple \(( \mathbf{C}, \times, 1, \alpha, \lambda, \rho )\) consisting of
a category \(\mathbf{C}\),
a functor \(\times: \mathbf{C} \times \mathbf{C} \rightarrow \mathbf{C}\),
an object \(1 \in \mathbf{C}\),
a natural isomorphism \(\alpha_{a,b,c}: a \times (b \times c) \cong (a \times b) \times c\),
a natural isomorphism \(\lambda_{a}: 1 \times a \cong a\),
a natural isomorphism \(\rho_{a}: a \times 1 \cong a\),
is called a cartesian category, if
for all objects \(a,b,c,d\), the pentagon identity holds:
\((\alpha_{a,b,c} \times \mathrm{id}_d) \circ \alpha_{a,b \times c, d} \circ ( \mathrm{id}_a \times \alpha_{b,c,d} ) = \alpha_{a \times b, c, d} \circ \alpha_{a,b,c \times d}\),
for all objects \(a,c\), the triangle identity holds:
\(( \rho_a \times \mathrm{id}_c ) \circ \alpha_{a,1,c} = \mathrm{id}_a \times \lambda_c\).
The corresponding GAP property is given by IsCartesianCategory
.
‣ CartesianBraiding ( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a \times b, b \times a )\).
The arguments are two objects \(a,b\). The output is the braiding \( B_{a,b}: a \times b \rightarrow b \times a\).
‣ CartesianBraidingWithGivenDirectProducts ( s, a, b, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a \times b, b \times a )\).
The arguments are an object \(s = a \times b\), two objects \(a,b\), and an object \(r = b \times a\). The output is the braiding \( B_{a,b}: a \times b \rightarrow b \times a\).
‣ CartesianBraidingInverse ( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( b \times a, a \times b )\).
The arguments are two objects \(a,b\). The output is the inverse braiding \( B_{a,b}^{-1}: b \times a \rightarrow a \times b\).
‣ CartesianBraidingInverseWithGivenDirectProducts ( s, a, b, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( b \times a, a \times b )\).
The arguments are an object \(s = b \times a\), two objects \(a,b\), and an object \(r = a \times b\). The output is the inverse braiding \( B_{a,b}^{-1}: b \times a \rightarrow a \times b\).
‣ DirectProductOnMorphisms ( alpha, beta ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a \times b, a' \times b')\)
The arguments are two morphisms \(\alpha: a \rightarrow a', \beta: b \rightarrow b'\). The output is the direct product \(\alpha \times \beta\).
‣ DirectProductOnMorphismsWithGivenDirectProducts ( s, alpha, beta, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a \times b, a' \times b')\)
The arguments are an object \(s = a \times b\), two morphisms \(\alpha: a \rightarrow a', \beta: b \rightarrow b'\), and an object \(r = a' \times b'\). The output is the direct product \(\alpha \times \beta\).
‣ CartesianAssociatorRightToLeft ( a, b, c ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a \times (b \times c), (a \times b) \times c )\).
The arguments are three objects \(a,b,c\). The output is the associator \(\alpha_{a,(b,c)}: a \times (b \times c) \rightarrow (a \times b) \times c\).
‣ CartesianAssociatorRightToLeftWithGivenDirectProducts ( s, a, b, c, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a \times (b \times c), (a \times b) \times c )\).
The arguments are an object \(s = a \times (b \times c)\), three objects \(a,b,c\), and an object \(r = (a \times b) \times c\). The output is the associator \(\alpha_{a,(b,c)}: a \times (b \times c) \rightarrow (a \times b) \times c\).
‣ CartesianAssociatorLeftToRight ( a, b, c ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( (a \times b) \times c \rightarrow a \times (b \times c) )\).
The arguments are three objects \(a,b,c\). The output is the associator \(\alpha_{(a,b),c}: (a \times b) \times c \rightarrow a \times (b \times c)\).
‣ CartesianAssociatorLeftToRightWithGivenDirectProducts ( s, a, b, c, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( (a \times b) \times c \rightarrow a \times (b \times c) )\).
The arguments are an object \(s = (a \times b) \times c\), three objects \(a,b,c\), and an object \(r = a \times (b \times c)\). The output is the associator \(\alpha_{(a,b),c}: (a \times b) \times c \rightarrow a \times (b \times c)\).
‣ CartesianLeftUnitor ( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(1 \times a, a)\)
The argument is an object \(a\). The output is the left unitor \(\lambda_a: 1 \times a \rightarrow a\).
‣ CartesianLeftUnitorWithGivenDirectProduct ( a, s ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(1 \times a, a)\)
The arguments are an object \(a\) and an object \(s = 1 \times a\). The output is the left unitor \(\lambda_a: 1 \times a \rightarrow a\).
‣ CartesianLeftUnitorInverse ( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(a, 1 \times a)\)
The argument is an object \(a\). The output is the inverse of the left unitor \(\lambda_a^{-1}: a \rightarrow 1 \times a\).
‣ CartesianLeftUnitorInverseWithGivenDirectProduct ( a, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a, 1 \times a)\)
The argument is an object \(a\) and an object \(r = 1 \times a\). The output is the inverse of the left unitor \(\lambda_a^{-1}: a \rightarrow 1 \times a\).
‣ CartesianRightUnitor ( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(a \times 1, a)\)
The argument is an object \(a\). The output is the right unitor \(\rho_a: a \times 1 \rightarrow a\).
‣ CartesianRightUnitorWithGivenDirectProduct ( a, s ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a \times 1, a)\)
The arguments are an object \(a\) and an object \(s = a \times 1\). The output is the right unitor \(\rho_a: a \times 1 \rightarrow a\).
‣ CartesianRightUnitorInverse ( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(a, a \times 1)\)
The argument is an object \(a\). The output is the inverse of the right unitor \(\rho_a^{-1}: a \rightarrow a \times 1\).
‣ CartesianRightUnitorInverseWithGivenDirectProduct ( a, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a, a \times 1)\)
The arguments are an object \(a\) and an object \(r = a \times 1\). The output is the inverse of the right unitor \(\rho_a^{-1}: a \rightarrow a \times 1\).
‣ CartesianDiagonal ( a, n ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a, a^{\times n})\).
The arguments are an object \(a\) and an integer \(n \geq 0\). The output is the diagonal morphism from \(a\) to the \(n\)-fold cartesian power \(a^{\times n}\). If the category does not support empty limits, \(n\) must be not be 0.
‣ CartesianDiagonalWithGivenCartesianPower ( a, n, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a, b)\)
The arguments are an object \(a\), an integer \(n\), and an object \(b\) equal to the \(n\)-fold cartesian power \(a^{\times n}\) of \(a\). The output is the diagonal morphism from \(a\) to \(b\).
‣ LeftCartesianDistributivityExpanding ( a, L ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a \times (b_1 \sqcup \dots \sqcup b_n), (a \times b_1) \sqcup \dots \sqcup (a \times b_n) )\)
The arguments are an object \(a\) and a list of objects \(L = (b_1, \dots, b_n)\). The output is the left distributivity morphism \(a \times (b_1 \sqcup \dots \sqcup b_n) \rightarrow (a \times b_1) \sqcup \dots \sqcup (a \times b_n)\).
‣ LeftCartesianDistributivityExpandingWithGivenObjects ( s, a, L, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\)
The arguments are an object \(s = a \times (b_1 \sqcup \dots \sqcup b_n)\), an object \(a\), a list of objects \(L = (b_1, \dots, b_n)\), and an object \(r = (a \times b_1) \sqcup \dots \sqcup (a \times b_n)\). The output is the left distributivity morphism \(s \rightarrow r\).
‣ LeftCartesianDistributivityFactoring ( a, L ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( (a \times b_1) \sqcup \dots \sqcup (a \times b_n), a \times (b_1 \sqcup \dots \sqcup b_n) )\)
The arguments are an object \(a\) and a list of objects \(L = (b_1, \dots, b_n)\). The output is the left distributivity morphism \((a \times b_1) \sqcup \dots \sqcup (a \times b_n) \rightarrow a \times (b_1 \sqcup \dots \sqcup b_n)\).
‣ LeftCartesianDistributivityFactoringWithGivenObjects ( s, a, L, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\)
The arguments are an object \(s = (a \times b_1) \sqcup \dots \sqcup (a \times b_n)\), an object \(a\), a list of objects \(L = (b_1, \dots, b_n)\), and an object \(r = a \times (b_1 \sqcup \dots \sqcup b_n)\). The output is the left distributivity morphism \(s \rightarrow r\).
‣ RightCartesianDistributivityExpanding ( L, a ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( (b_1 \sqcup \dots \sqcup b_n) \times a, (b_1 \times a) \sqcup \dots \sqcup (b_n \times a) )\)
The arguments are a list of objects \(L = (b_1, \dots, b_n)\) and an object \(a\). The output is the right distributivity morphism \((b_1 \sqcup \dots \sqcup b_n) \times a \rightarrow (b_1 \times a) \sqcup \dots \sqcup (b_n \times a)\).
‣ RightCartesianDistributivityExpandingWithGivenObjects ( s, L, a, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\)
The arguments are an object \(s = (b_1 \sqcup \dots \sqcup b_n) \times a\), a list of objects \(L = (b_1, \dots, b_n)\), an object \(a\), and an object \(r = (b_1 \times a) \sqcup \dots \sqcup (b_n \times a)\). The output is the right distributivity morphism \(s \rightarrow r\).
‣ RightCartesianDistributivityFactoring ( L, a ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( (b_1 \times a) \sqcup \dots \sqcup (b_n \times a), (b_1 \sqcup \dots \sqcup b_n) \times a)\)
The arguments are a list of objects \(L = (b_1, \dots, b_n)\) and an object \(a\). The output is the right distributivity morphism \((b_1 \times a) \sqcup \dots \sqcup (b_n \times a) \rightarrow (b_1 \sqcup \dots \sqcup b_n) \times a \).
‣ RightCartesianDistributivityFactoringWithGivenObjects ( s, L, a, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\)
The arguments are an object \(s = (b_1 \times a) \sqcup \dots \sqcup (b_n \times a)\), a list of objects \(L = (b_1, \dots, b_n)\), an object \(a\), and an object \(r = (b_1 \sqcup \dots \sqcup b_n) \times a\). The output is the right distributivity morphism \(s \rightarrow r\).
A cartesian category \(\mathbf{C}\) which has for each functor \(- \times b: \mathbf{C} \rightarrow \mathbf{C}\) a right adjoint (denoted by \(\mathrm{Exponential}(b,-)\)) is called a closed cartesian category.
The corresponding GAP property is called IsCartesianClosedCategory
.
‣ ExponentialOnObjects ( a, b ) | ( operation ) |
Returns: an object
The arguments are two objects \(a,b\). The output is the exponential object \(\mathrm{Exponential}(a,b)\).
‣ ExponentialOnMorphisms ( alpha, beta ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{Exponential}(a',b), \mathrm{Exponential}(a,b') )\)
The arguments are two morphisms \(\alpha: a \rightarrow a', \beta: b \rightarrow b'\). The output is the exponential morphism \(\mathrm{Exponential}(\alpha,\beta): \mathrm{Exponential}(a',b) \rightarrow \mathrm{Exponential}(a,b')\).
‣ ExponentialOnMorphismsWithGivenExponentials ( s, alpha, beta, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\)
The arguments are an object \(s = \mathrm{Exponential}(a',b)\), two morphisms \(\alpha: a \rightarrow a', \beta: b \rightarrow b'\), and an object \(r = \mathrm{Exponential}(a,b')\). The output is the exponential morphism \(\mathrm{Exponential}(\alpha,\beta): \mathrm{Exponential}(a',b) \rightarrow \mathrm{Exponential}(a,b')\).
‣ CartesianRightEvaluationMorphism ( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a \times \mathrm{Exponential}(a,b), b )\).
The arguments are two objects \(a, b\). The output is the right evaluation morphism \(\mathrm{ev}_{a,b}:a \times \mathrm{Exponential}(a,b) \rightarrow b\), i.e., the counit of the direct product-exponential adjunction.
‣ CartesianRightEvaluationMorphismWithGivenSource ( a, b, s ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, b )\).
The arguments are two objects \(a,b\) and an object \(s = a \times \mathrm{Exponential}(a,b)\). The output is the right evaluation morphism \(\mathrm{ev}_{a,b}: a \times \mathrm{Exponential}(a,b) \rightarrow b\), i.e., the counit of the direct product-exponential adjunction.
‣ CartesianRightCoevaluationMorphism ( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( b, \mathrm{Exponential}(a, a \times b) )\).
The arguments are two objects \(a,b\). The output is the right coevaluation morphism \(\mathrm{coev}_{a,b}: b \rightarrow \mathrm{Exponential}(a, a \times b)\), i.e., the unit of the direct product-exponential adjunction.
‣ CartesianRightCoevaluationMorphismWithGivenRange ( a, b, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( b, r )\).
The arguments are two objects \(a,b\) and an object \(r = \mathrm{Exponential}(a, a \times b)\). The output is the right coevaluation morphism \(\mathrm{coev}_{a,b}: b \rightarrow \mathrm{Exponential}(a, a \times b)\), i.e., the unit of the direct product-exponential adjunction.
‣ DirectProductToExponentialRightAdjunctMorphism ( a, b, f ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( b, \mathrm{Exponential}(a,c) )\).
The arguments are two objects \(a,b\) and a morphism \(f: a \times b \rightarrow c\). The output is a morphism \(g: b \rightarrow \mathrm{Exponential}(a,c)\) corresponding to \(f\) under the direct product-exponential adjunction.
‣ DirectProductToExponentialRightAdjunctMorphismWithGivenExponential ( a, b, f, i ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( b, i )\).
The arguments are two objects \(a,b\), a morphism \(f: a \times b \rightarrow c\) and an object \(i = \mathrm{Exponential}(a,c)\). The output is a morphism \(g: b \rightarrow i\) corresponding to \(f\) under the direct product-exponential adjunction.
‣ DirectProductToExponentialRightAdjunctionIsomorphism ( a, b, c ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( H(a \times b, c), H(b, \mathrm{Exponential}(a,c)) )\).
The arguments are three objects \(a,b,c\). The output is the tri-natural isomorphism \(H(a \times b, c) \to H(b, \mathrm{Exponential}(a,c))\) in the range category of the homomorphism structure \(H\).
‣ DirectProductToExponentialRightAdjunctionIsomorphismWithGivenObjects ( s, a, b, c, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\).
The arguments are fives objects \(s,a,b,c,r\) where \(s = H(a \times b, c)\) and \(r = H(b, \mathrm{Exponential}(a,c))\). The output is the tri-natural isomorphism \(s \to r\) in the range category of the homomorphism structure \(H\).
‣ ExponentialToDirectProductRightAdjunctMorphism ( a, c, g ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a \times b, c)\).
The arguments are two objects \(a,c\) and a morphism \(g: b \rightarrow \mathrm{Exponential}(a,c)\). The output is a morphism \(f: a \times b \rightarrow c\) corresponding to \(g\) under the direct product-exponential adjunction.
‣ ExponentialToDirectProductRightAdjunctMorphismWithGivenDirectProduct ( a, c, g, s ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(s, c)\).
The arguments are two objects \(a,c\), a morphism \(g: b \rightarrow \mathrm{Exponential}(a,c)\) and an object \(s = a \times b\). The output is a morphism \(f: s \rightarrow c\) corresponding to \(g\) under the direct product-exponential adjunction.
‣ ExponentialToDirectProductRightAdjunctionIsomorphism ( a, b, c ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( H(b, \mathrm{Exponential}(a,c)), H(a \times b, c) )\).
The arguments are three objects \(a,b,c\). The output is the tri-natural isomorphism \(H(b, \mathrm{Exponential}(a,c)) \to H(a \times b, c)\) in the range category of the homomorphism structure \(H\).
‣ ExponentialToDirectProductRightAdjunctionIsomorphismWithGivenObjects ( s, a, b, c, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\).
The arguments are fives objects \(s,a,b,c,r\) where \(s = H(b, \mathrm{Exponential}(a,c))\) and \(r = H(a \times b, c)\). The output is the tri-natural isomorphism \(s \to r\) in the range category of the homomorphism structure \(H\).
‣ CartesianLeftEvaluationMorphism ( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{Exponential}(a,b) \times a, b )\).
The arguments are two objects \(a, b\). The output is the left evaluation morphism \(\mathrm{ev}_{a,b}: \mathrm{Exponential}(a,b) \times a \rightarrow b\), i.e., the counit of the direct product-exponential adjunction.
‣ CartesianLeftEvaluationMorphismWithGivenSource ( a, b, s ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, b )\).
The arguments are two objects \(a,b\) and an object \(s = \mathrm{Exponential}(a,b) \times a\). The output is the left evaluation morphism \(\mathrm{ev}_{a,b}: \mathrm{Exponential}(a,b) \times a \rightarrow b\), i.e., the counit of the direct product-exponential adjunction.
‣ CartesianLeftCoevaluationMorphism ( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( b, \mathrm{Exponential}(a, b \times a) )\).
The arguments are two objects \(a,b\). The output is the left coevaluation morphism \(\mathrm{coev}_{a,b}: b \rightarrow \mathrm{Exponential}(a, b \times a)\), i.e., the unit of the direct product-exponential adjunction.
‣ CartesianLeftCoevaluationMorphismWithGivenRange ( a, b, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( b, r )\).
The arguments are two objects \(a,b\) and an object \(r = \mathrm{Exponential}(a, b \times a)\). The output is the left coevaluation morphism \(\mathrm{coev}_{a,b}: b \rightarrow \mathrm{Exponential}(a, b \times a)\), i.e., the unit of the direct product-exponential adjunction.
‣ DirectProductToExponentialLeftAdjunctMorphism ( a, b, f ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a, \mathrm{Exponential}(b,c) )\).
The arguments are two objects \(a,b\) and a morphism \(f: a \times b \rightarrow c\). The output is a morphism \(g: a \rightarrow \mathrm{Exponential}(b,c)\) corresponding to \(f\) under the direct product-exponential adjunction.
‣ DirectProductToExponentialLeftAdjunctMorphismWithGivenExponential ( a, b, f, i ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a, i )\).
The arguments are two objects \(a,b\), a morphism \(f: a \times b \rightarrow c\) and an object \(i = \mathrm{Exponential}(b,c)\). The output is a morphism \(g: a \rightarrow i\) corresponding to \(f\) under the direct product-exponential adjunction.
‣ DirectProductToExponentialLeftAdjunctionIsomorphism ( a, b, c ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( H(a \times b, c), H(a, \mathrm{Exponential}(b,c)) )\).
The arguments are three objects \(a,b,c\). The output is the tri-natural isomorphism \(H(a \times b, c) \to H(a, \mathrm{Exponential}(b,c))\) in the range category of the homomorphism structure \(H\).
‣ DirectProductToExponentialLeftAdjunctionIsomorphismWithGivenObjects ( s, a, b, c, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\).
The arguments are fives objects \(s,a,b,c,r\) where \(s = H(a \times b, c)\) and \(r = H(a, \mathrm{Exponential}(b,c))\). The output is the tri-natural isomorphism \(s \to r\) in the range category of the homomorphism structure \(H\).
‣ ExponentialToDirectProductLeftAdjunctMorphism ( b, c, g ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a \times b, c)\).
The arguments are two objects \(b,c\) and a morphism \(g: a \rightarrow \mathrm{Exponential}(b,c)\). The output is a morphism \(f: a \times b \rightarrow c\) corresponding to \(g\) under the direct product-exponential adjunction.
‣ ExponentialToDirectProductLeftAdjunctMorphismWithGivenDirectProduct ( b, c, g, s ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(s, c)\).
The arguments are two objects \(b,c\), a morphism \(g: a \rightarrow \mathrm{Exponential}(b,c)\) and an object \(s = a \times b\). The output is a morphism \(f: s \rightarrow c\) corresponding to \(g\) under the direct product-exponential adjunction.
‣ ExponentialToDirectProductLeftAdjunctionIsomorphism ( a, b, c ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( H(a, \mathrm{Exponential}(b,c)), H(a \times b, c) )\).
The arguments are three objects \(a,b,c\). The output is the tri-natural isomorphism \(H(a, \mathrm{Exponential}(b,c)) \to H(a \times b, c)\) in the range category of the homomorphism structure \(H\).
‣ ExponentialToDirectProductLeftAdjunctionIsomorphismWithGivenObjects ( s, a, b, c, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\).
The arguments are fives objects \(s,a,b,c,r\) where \(s = H(a, \mathrm{Exponential}(b,c))\) and \(r = H(a \times b, c)\). The output is the tri-natural isomorphism \(s \to r\) in the range category of the homomorphism structure \(H\).
‣ CartesianPreComposeMorphism ( a, b, c ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{Exponential}(a,b) \times \mathrm{Exponential}(b,c), \mathrm{Exponential}(a,c) )\).
The arguments are three objects \(a,b,c\). The output is the precomposition morphism \(\mathrm{CartesianPreComposeMorphism}_{a,b,c}: \mathrm{Exponential}(a,b) \times \mathrm{Exponential}(b,c) \rightarrow \mathrm{Exponential}(a,c)\).
‣ CartesianPreComposeMorphismWithGivenObjects ( s, a, b, c, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\).
The arguments are an object \(s = \mathrm{Exponential}(a,b) \times \mathrm{Exponential}(b,c)\), three objects \(a,b,c\), and an object \(r = \mathrm{Exponential}(a,c)\). The output is the precomposition morphism \(\mathrm{CartesianPreComposeMorphismWithGivenObjects}_{a,b,c}: \mathrm{Exponential}(a,b) \times \mathrm{Exponential}(b,c) \rightarrow \mathrm{Exponential}(a,c)\).
‣ CartesianPostComposeMorphism ( a, b, c ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{Exponential}(b,c) \times \mathrm{Exponential}(a,b), \mathrm{Exponential}(a,c) )\).
The arguments are three objects \(a,b,c\). The output is the postcomposition morphism \(\mathrm{CartesianPostComposeMorphism}_{a,b,c}: \mathrm{Exponential}(b,c) \times \mathrm{Exponential}(a,b) \rightarrow \mathrm{Exponential}(a,c)\).
‣ CartesianPostComposeMorphismWithGivenObjects ( s, a, b, c, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\).
The arguments are an object \(s = \mathrm{Exponential}(b,c) \times \mathrm{Exponential}(a,b)\), three objects \(a,b,c\), and an object \(r = \mathrm{Exponential}(a,c)\). The output is the postcomposition morphism \(\mathrm{CartesianPostComposeMorphismWithGivenObjects}_{a,b,c}: \mathrm{Exponential}(b,c) \times \mathrm{Exponential}(a,b) \rightarrow \mathrm{Exponential}(a,c)\).
‣ CartesianDualOnObjects ( a ) | ( attribute ) |
Returns: an object
The argument is an object \(a\). The output is its dual object \(a^{\vee}\).
‣ CartesianDualOnMorphisms ( alpha ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( b^{\vee}, a^{\vee} )\).
The argument is a morphism \(\alpha: a \rightarrow b\). The output is its dual morphism \(\alpha^{\vee}: b^{\vee} \rightarrow a^{\vee}\).
‣ CartesianDualOnMorphismsWithGivenCartesianDuals ( s, alpha, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\).
The argument is an object \(s = b^{\vee}\), a morphism \(\alpha: a \rightarrow b\), and an object \(r = a^{\vee}\). The output is the dual morphism \(\alpha^{\vee}: b^{\vee} \rightarrow a^{\vee}\).
‣ CartesianEvaluationForCartesianDual ( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( a^{\vee} \times a, 1 )\).
The argument is an object \(a\). The output is the evaluation morphism \(\mathrm{ev}_{a}: a^{\vee} \times a \rightarrow 1\).
‣ CartesianEvaluationForCartesianDualWithGivenDirectProduct ( s, a, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\).
The arguments are an object \(s = a^{\vee} \times a\), an object \(a\), and an object \(r = 1\). The output is the evaluation morphism \(\mathrm{ev}_{a}: a^{\vee} \times a \rightarrow 1\).
‣ MorphismToCartesianBidual ( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(a, (a^{\vee})^{\vee})\).
The argument is an object \(a\). The output is the morphism to the bidual \(a \rightarrow (a^{\vee})^{\vee}\).
‣ MorphismToCartesianBidualWithGivenCartesianBidual ( a, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a, r)\).
The arguments are an object \(a\), and an object \(r = (a^{\vee})^{\vee}\). The output is the morphism to the bidual \(a \rightarrow (a^{\vee})^{\vee}\).
‣ DirectProductExponentialCompatibilityMorphism ( list ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{Exponential}(a,a') \times \mathrm{Exponential}(b,b'), \mathrm{Exponential}(a \times b,a' \times b'))\).
The argument is a list of four objects \([ a, a', b, b' ]\). The output is the natural morphism \(\mathrm{DirectProductExponentialCompatibilityMorphism}_{a,a',b,b'}: \mathrm{Exponential}(a,a') \times \mathrm{Exponential}(b,b') \rightarrow \mathrm{Exponential}(a \times b,a' \times b')\).
‣ DirectProductExponentialCompatibilityMorphismWithGivenObjects ( s, list, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\).
The arguments are a list of four objects \([ a, a', b, b' ]\), and two objects \(s = \mathrm{Exponential}(a,a') \times \mathrm{Exponential}(b,b')\) and \(r = \mathrm{Exponential}(a \times b,a' \times b')\). The output is the natural morphism \(\mathrm{DirectProductExponentialCompatibilityMorphismWithGivenObjects}_{a,a',b,b'}: \mathrm{Exponential}(a,a') \times \mathrm{Exponential}(b,b') \rightarrow \mathrm{Exponential}(a \times b,a' \times b')\).
‣ DirectProductCartesianDualityCompatibilityMorphism ( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a^{\vee} \times b^{\vee}, (a \times b)^{\vee} )\).
The arguments are two objects \(a,b\). The output is the natural morphism \(\mathrm{DirectProductCartesianDualityCompatibilityMorphism}: a^{\vee} \times b^{\vee} \rightarrow (a \times b)^{\vee}\).
‣ DirectProductCartesianDualityCompatibilityMorphismWithGivenObjects ( s, a, b, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\).
The arguments are an object \(s = a^{\vee} \times b^{\vee}\), two objects \(a,b\), and an object \(r = (a \times b)^{\vee}\). The output is the natural morphism \(\mathrm{DirectProductCartesianDualityCompatibilityMorphismWithGivenObjects}_{a,b}: a^{\vee} \times b^{\vee} \rightarrow (a \times b)^{\vee}\).
‣ MorphismFromDirectProductToExponential ( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a^{\vee} \times b, \mathrm{Exponential}(a,b) )\).
The arguments are two objects \(a,b\). The output is the natural morphism \(\mathrm{MorphismFromDirectProductToExponential}_{a,b}: a^{\vee} \times b \rightarrow \mathrm{Exponential}(a,b)\).
‣ MorphismFromDirectProductToExponentialWithGivenObjects ( s, a, b, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\).
The arguments are an object \(s = a^{\vee} \times b\), two objects \(a,b\), and an object \(r = \mathrm{Exponential}(a,b)\). The output is the natural morphism \(\mathrm{MorphismFromDirectProductToExponentialWithGivenObjects}_{a,b}: a^{\vee} \times b \rightarrow \mathrm{Exponential}(a,b)\).
‣ IsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject ( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(a^{\vee}, \mathrm{Exponential}(a,1))\).
The argument is an object \(a\). The output is the isomorphism \(\mathrm{IsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject}_{a}: a^{\vee} \rightarrow \mathrm{Exponential}(a,1)\).
‣ IsomorphismFromExponentialIntoTerminalObjectToCartesianDualObject ( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(\mathrm{Exponential}(a,1), a^{\vee})\).
The argument is an object \(a\). The output is the isomorphism \(\mathrm{IsomorphismFromExponentialIntoTerminalObjectToCartesianDualObject}_{a}: \mathrm{Exponential}(a,1) \rightarrow a^{\vee}\).
‣ UniversalPropertyOfCartesianDual ( t, a, alpha ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(t, a^{\vee})\).
The arguments are two objects \(t,a\), and a morphism \(\alpha: t \times a \rightarrow 1\). The output is the morphism \(t \rightarrow a^{\vee}\) given by the universal property of \(a^{\vee}\).
‣ CartesianLambdaIntroduction ( alpha ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( 1, \mathrm{Exponential}(a,b) )\).
The argument is a morphism \(\alpha: a \rightarrow b\). The output is the corresponding morphism \(1 \rightarrow \mathrm{Exponential}(a,b)\) under the direct product-exponential adjunction.
‣ CartesianLambdaElimination ( a, b, alpha ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a,b)\).
The arguments are two objects \(a,b\), and a morphism \(\alpha: 1 \rightarrow \mathrm{Exponential}(a,b)\). The output is a morphism \(a \rightarrow b\) corresponding to \(\alpha\) under the direct product-exponential adjunction.
‣ IsomorphismFromObjectToExponential ( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(a, \mathrm{Exponential}(1,a))\).
The argument is an object \(a\). The output is the natural isomorphism \(a \rightarrow \mathrm{Exponential}(1,a)\).
‣ IsomorphismFromObjectToExponentialWithGivenExponential ( a, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a, r)\).
The argument is an object \(a\), and an object \(r = \mathrm{Exponential}(1,a)\). The output is the natural isomorphism \(a \rightarrow \mathrm{Exponential}(1,a)\).
‣ IsomorphismFromExponentialToObject ( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(\mathrm{Exponential}(1,a),a)\).
The argument is an object \(a\). The output is the natural isomorphism \(\mathrm{Exponential}(1,a) \rightarrow a\).
‣ IsomorphismFromExponentialToObjectWithGivenExponential ( a, s ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(s,a)\).
The argument is an object \(a\), and an object \(s = \mathrm{Exponential}(1,a)\). The output is the natural isomorphism \(\mathrm{Exponential}(1,a) \rightarrow a\).
‣ Exponential ( a, b ) | ( operation ) |
Returns: a cell
This is a convenience method. The arguments are two cells \(a,b\). The output is the exponential cell. If \(a,b\) are two CAP objects the output is the internal Hom object \(\mathrm{Exponential}(a,b)\). If at least one of the arguments is a CAP morphism the output is a CAP morphism, namely the exponential on morphisms, where any object is replaced by its identity morphism.
‣ AddCartesianBraiding ( C, F ) | ( operation ) |
‣ AddCartesianBraiding ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianBraiding
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b ) \mapsto \mathtt{CartesianBraiding}(a, b)\).
‣ AddCartesianBraidingInverse ( C, F ) | ( operation ) |
‣ AddCartesianBraidingInverse ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianBraidingInverse
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b ) \mapsto \mathtt{CartesianBraidingInverse}(a, b)\).
‣ AddCartesianBraidingInverseWithGivenDirectProducts ( C, F ) | ( operation ) |
‣ AddCartesianBraidingInverseWithGivenDirectProducts ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianBraidingInverseWithGivenDirectProducts
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( s, a, b, r ) \mapsto \mathtt{CartesianBraidingInverseWithGivenDirectProducts}(s, a, b, r)\).
‣ AddCartesianBraidingWithGivenDirectProducts ( C, F ) | ( operation ) |
‣ AddCartesianBraidingWithGivenDirectProducts ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianBraidingWithGivenDirectProducts
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( s, a, b, r ) \mapsto \mathtt{CartesianBraidingWithGivenDirectProducts}(s, a, b, r)\).
‣ AddCartesianAssociatorLeftToRight ( C, F ) | ( operation ) |
‣ AddCartesianAssociatorLeftToRight ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianAssociatorLeftToRight
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b, c ) \mapsto \mathtt{CartesianAssociatorLeftToRight}(a, b, c)\).
‣ AddCartesianAssociatorLeftToRightWithGivenDirectProducts ( C, F ) | ( operation ) |
‣ AddCartesianAssociatorLeftToRightWithGivenDirectProducts ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianAssociatorLeftToRightWithGivenDirectProducts
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( s, a, b, c, r ) \mapsto \mathtt{CartesianAssociatorLeftToRightWithGivenDirectProducts}(s, a, b, c, r)\).
‣ AddCartesianAssociatorRightToLeft ( C, F ) | ( operation ) |
‣ AddCartesianAssociatorRightToLeft ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianAssociatorRightToLeft
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b, c ) \mapsto \mathtt{CartesianAssociatorRightToLeft}(a, b, c)\).
‣ AddCartesianAssociatorRightToLeftWithGivenDirectProducts ( C, F ) | ( operation ) |
‣ AddCartesianAssociatorRightToLeftWithGivenDirectProducts ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianAssociatorRightToLeftWithGivenDirectProducts
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( s, a, b, c, r ) \mapsto \mathtt{CartesianAssociatorRightToLeftWithGivenDirectProducts}(s, a, b, c, r)\).
‣ AddCartesianDiagonal ( C, F ) | ( operation ) |
‣ AddCartesianDiagonal ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianDiagonal
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, n ) \mapsto \mathtt{CartesianDiagonal}(a, n)\).
‣ AddCartesianDiagonalWithGivenCartesianPower ( C, F ) | ( operation ) |
‣ AddCartesianDiagonalWithGivenCartesianPower ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianDiagonalWithGivenCartesianPower
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, n, cartesian_power ) \mapsto \mathtt{CartesianDiagonalWithGivenCartesianPower}(a, n, cartesian_power)\).
‣ AddCartesianLeftUnitor ( C, F ) | ( operation ) |
‣ AddCartesianLeftUnitor ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianLeftUnitor
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a ) \mapsto \mathtt{CartesianLeftUnitor}(a)\).
‣ AddCartesianLeftUnitorInverse ( C, F ) | ( operation ) |
‣ AddCartesianLeftUnitorInverse ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianLeftUnitorInverse
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a ) \mapsto \mathtt{CartesianLeftUnitorInverse}(a)\).
‣ AddCartesianLeftUnitorInverseWithGivenDirectProduct ( C, F ) | ( operation ) |
‣ AddCartesianLeftUnitorInverseWithGivenDirectProduct ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianLeftUnitorInverseWithGivenDirectProduct
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, r ) \mapsto \mathtt{CartesianLeftUnitorInverseWithGivenDirectProduct}(a, r)\).
‣ AddCartesianLeftUnitorWithGivenDirectProduct ( C, F ) | ( operation ) |
‣ AddCartesianLeftUnitorWithGivenDirectProduct ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianLeftUnitorWithGivenDirectProduct
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, s ) \mapsto \mathtt{CartesianLeftUnitorWithGivenDirectProduct}(a, s)\).
‣ AddCartesianRightUnitor ( C, F ) | ( operation ) |
‣ AddCartesianRightUnitor ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianRightUnitor
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a ) \mapsto \mathtt{CartesianRightUnitor}(a)\).
‣ AddCartesianRightUnitorInverse ( C, F ) | ( operation ) |
‣ AddCartesianRightUnitorInverse ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianRightUnitorInverse
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a ) \mapsto \mathtt{CartesianRightUnitorInverse}(a)\).
‣ AddCartesianRightUnitorInverseWithGivenDirectProduct ( C, F ) | ( operation ) |
‣ AddCartesianRightUnitorInverseWithGivenDirectProduct ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianRightUnitorInverseWithGivenDirectProduct
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, r ) \mapsto \mathtt{CartesianRightUnitorInverseWithGivenDirectProduct}(a, r)\).
‣ AddCartesianRightUnitorWithGivenDirectProduct ( C, F ) | ( operation ) |
‣ AddCartesianRightUnitorWithGivenDirectProduct ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianRightUnitorWithGivenDirectProduct
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, s ) \mapsto \mathtt{CartesianRightUnitorWithGivenDirectProduct}(a, s)\).
‣ AddDirectProductOnMorphisms ( C, F ) | ( operation ) |
‣ AddDirectProductOnMorphisms ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation DirectProductOnMorphisms
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( alpha, beta ) \mapsto \mathtt{DirectProductOnMorphisms}(alpha, beta)\).
‣ AddDirectProductOnMorphismsWithGivenDirectProducts ( C, F ) | ( operation ) |
‣ AddDirectProductOnMorphismsWithGivenDirectProducts ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation DirectProductOnMorphismsWithGivenDirectProducts
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( s, alpha, beta, r ) \mapsto \mathtt{DirectProductOnMorphismsWithGivenDirectProducts}(s, alpha, beta, r)\).
‣ AddCartesianDualOnMorphisms ( C, F ) | ( operation ) |
‣ AddCartesianDualOnMorphisms ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianDualOnMorphisms
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( alpha ) \mapsto \mathtt{CartesianDualOnMorphisms}(alpha)\).
‣ AddCartesianDualOnMorphismsWithGivenCartesianDuals ( C, F ) | ( operation ) |
‣ AddCartesianDualOnMorphismsWithGivenCartesianDuals ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianDualOnMorphismsWithGivenCartesianDuals
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( s, alpha, r ) \mapsto \mathtt{CartesianDualOnMorphismsWithGivenCartesianDuals}(s, alpha, r)\).
‣ AddCartesianDualOnObjects ( C, F ) | ( operation ) |
‣ AddCartesianDualOnObjects ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianDualOnObjects
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a ) \mapsto \mathtt{CartesianDualOnObjects}(a)\).
‣ AddCartesianEvaluationForCartesianDual ( C, F ) | ( operation ) |
‣ AddCartesianEvaluationForCartesianDual ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianEvaluationForCartesianDual
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a ) \mapsto \mathtt{CartesianEvaluationForCartesianDual}(a)\).
‣ AddCartesianEvaluationForCartesianDualWithGivenDirectProduct ( C, F ) | ( operation ) |
‣ AddCartesianEvaluationForCartesianDualWithGivenDirectProduct ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianEvaluationForCartesianDualWithGivenDirectProduct
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( s, a, r ) \mapsto \mathtt{CartesianEvaluationForCartesianDualWithGivenDirectProduct}(s, a, r)\).
‣ AddCartesianLambdaElimination ( C, F ) | ( operation ) |
‣ AddCartesianLambdaElimination ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianLambdaElimination
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b, alpha ) \mapsto \mathtt{CartesianLambdaElimination}(a, b, alpha)\).
‣ AddCartesianLambdaIntroduction ( C, F ) | ( operation ) |
‣ AddCartesianLambdaIntroduction ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianLambdaIntroduction
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( alpha ) \mapsto \mathtt{CartesianLambdaIntroduction}(alpha)\).
‣ AddCartesianLeftCoevaluationMorphism ( C, F ) | ( operation ) |
‣ AddCartesianLeftCoevaluationMorphism ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianLeftCoevaluationMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b ) \mapsto \mathtt{CartesianLeftCoevaluationMorphism}(a, b)\).
‣ AddCartesianLeftCoevaluationMorphismWithGivenRange ( C, F ) | ( operation ) |
‣ AddCartesianLeftCoevaluationMorphismWithGivenRange ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianLeftCoevaluationMorphismWithGivenRange
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b, r ) \mapsto \mathtt{CartesianLeftCoevaluationMorphismWithGivenRange}(a, b, r)\).
‣ AddCartesianLeftEvaluationMorphism ( C, F ) | ( operation ) |
‣ AddCartesianLeftEvaluationMorphism ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianLeftEvaluationMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b ) \mapsto \mathtt{CartesianLeftEvaluationMorphism}(a, b)\).
‣ AddCartesianLeftEvaluationMorphismWithGivenSource ( C, F ) | ( operation ) |
‣ AddCartesianLeftEvaluationMorphismWithGivenSource ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianLeftEvaluationMorphismWithGivenSource
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b, s ) \mapsto \mathtt{CartesianLeftEvaluationMorphismWithGivenSource}(a, b, s)\).
‣ AddCartesianPostComposeMorphism ( C, F ) | ( operation ) |
‣ AddCartesianPostComposeMorphism ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianPostComposeMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b, c ) \mapsto \mathtt{CartesianPostComposeMorphism}(a, b, c)\).
‣ AddCartesianPostComposeMorphismWithGivenObjects ( C, F ) | ( operation ) |
‣ AddCartesianPostComposeMorphismWithGivenObjects ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianPostComposeMorphismWithGivenObjects
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( s, a, b, c, r ) \mapsto \mathtt{CartesianPostComposeMorphismWithGivenObjects}(s, a, b, c, r)\).
‣ AddCartesianPreComposeMorphism ( C, F ) | ( operation ) |
‣ AddCartesianPreComposeMorphism ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianPreComposeMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b, c ) \mapsto \mathtt{CartesianPreComposeMorphism}(a, b, c)\).
‣ AddCartesianPreComposeMorphismWithGivenObjects ( C, F ) | ( operation ) |
‣ AddCartesianPreComposeMorphismWithGivenObjects ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianPreComposeMorphismWithGivenObjects
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( s, a, b, c, r ) \mapsto \mathtt{CartesianPreComposeMorphismWithGivenObjects}(s, a, b, c, r)\).
‣ AddCartesianRightCoevaluationMorphism ( C, F ) | ( operation ) |
‣ AddCartesianRightCoevaluationMorphism ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianRightCoevaluationMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b ) \mapsto \mathtt{CartesianRightCoevaluationMorphism}(a, b)\).
‣ AddCartesianRightCoevaluationMorphismWithGivenRange ( C, F ) | ( operation ) |
‣ AddCartesianRightCoevaluationMorphismWithGivenRange ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianRightCoevaluationMorphismWithGivenRange
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b, r ) \mapsto \mathtt{CartesianRightCoevaluationMorphismWithGivenRange}(a, b, r)\).
‣ AddCartesianRightEvaluationMorphism ( C, F ) | ( operation ) |
‣ AddCartesianRightEvaluationMorphism ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianRightEvaluationMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b ) \mapsto \mathtt{CartesianRightEvaluationMorphism}(a, b)\).
‣ AddCartesianRightEvaluationMorphismWithGivenSource ( C, F ) | ( operation ) |
‣ AddCartesianRightEvaluationMorphismWithGivenSource ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianRightEvaluationMorphismWithGivenSource
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b, s ) \mapsto \mathtt{CartesianRightEvaluationMorphismWithGivenSource}(a, b, s)\).
‣ AddDirectProductCartesianDualityCompatibilityMorphism ( C, F ) | ( operation ) |
‣ AddDirectProductCartesianDualityCompatibilityMorphism ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation DirectProductCartesianDualityCompatibilityMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b ) \mapsto \mathtt{DirectProductCartesianDualityCompatibilityMorphism}(a, b)\).
‣ AddDirectProductCartesianDualityCompatibilityMorphismWithGivenObjects ( C, F ) | ( operation ) |
‣ AddDirectProductCartesianDualityCompatibilityMorphismWithGivenObjects ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation DirectProductCartesianDualityCompatibilityMorphismWithGivenObjects
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( s, a, b, r ) \mapsto \mathtt{DirectProductCartesianDualityCompatibilityMorphismWithGivenObjects}(s, a, b, r)\).
‣ AddDirectProductExponentialCompatibilityMorphism ( C, F ) | ( operation ) |
‣ AddDirectProductExponentialCompatibilityMorphism ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation DirectProductExponentialCompatibilityMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( list ) \mapsto \mathtt{DirectProductExponentialCompatibilityMorphism}(list)\).
‣ AddDirectProductExponentialCompatibilityMorphismWithGivenObjects ( C, F ) | ( operation ) |
‣ AddDirectProductExponentialCompatibilityMorphismWithGivenObjects ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation DirectProductExponentialCompatibilityMorphismWithGivenObjects
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( source, list, range ) \mapsto \mathtt{DirectProductExponentialCompatibilityMorphismWithGivenObjects}(source, list, range)\).
‣ AddDirectProductToExponentialLeftAdjunctMorphism ( C, F ) | ( operation ) |
‣ AddDirectProductToExponentialLeftAdjunctMorphism ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation DirectProductToExponentialLeftAdjunctMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b, f ) \mapsto \mathtt{DirectProductToExponentialLeftAdjunctMorphism}(a, b, f)\).
‣ AddDirectProductToExponentialLeftAdjunctMorphismWithGivenExponential ( C, F ) | ( operation ) |
‣ AddDirectProductToExponentialLeftAdjunctMorphismWithGivenExponential ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation DirectProductToExponentialLeftAdjunctMorphismWithGivenExponential
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b, f, i ) \mapsto \mathtt{DirectProductToExponentialLeftAdjunctMorphismWithGivenExponential}(a, b, f, i)\).
‣ AddDirectProductToExponentialLeftAdjunctionIsomorphism ( C, F ) | ( operation ) |
‣ AddDirectProductToExponentialLeftAdjunctionIsomorphism ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation DirectProductToExponentialLeftAdjunctionIsomorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b, c ) \mapsto \mathtt{DirectProductToExponentialLeftAdjunctionIsomorphism}(a, b, c)\).
‣ AddDirectProductToExponentialLeftAdjunctionIsomorphismWithGivenObjects ( C, F ) | ( operation ) |
‣ AddDirectProductToExponentialLeftAdjunctionIsomorphismWithGivenObjects ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation DirectProductToExponentialLeftAdjunctionIsomorphismWithGivenObjects
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( s, a, b, c, r ) \mapsto \mathtt{DirectProductToExponentialLeftAdjunctionIsomorphismWithGivenObjects}(s, a, b, c, r)\).
‣ AddDirectProductToExponentialRightAdjunctMorphism ( C, F ) | ( operation ) |
‣ AddDirectProductToExponentialRightAdjunctMorphism ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation DirectProductToExponentialRightAdjunctMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b, f ) \mapsto \mathtt{DirectProductToExponentialRightAdjunctMorphism}(a, b, f)\).
‣ AddDirectProductToExponentialRightAdjunctMorphismWithGivenExponential ( C, F ) | ( operation ) |
‣ AddDirectProductToExponentialRightAdjunctMorphismWithGivenExponential ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation DirectProductToExponentialRightAdjunctMorphismWithGivenExponential
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b, f, i ) \mapsto \mathtt{DirectProductToExponentialRightAdjunctMorphismWithGivenExponential}(a, b, f, i)\).
‣ AddDirectProductToExponentialRightAdjunctionIsomorphism ( C, F ) | ( operation ) |
‣ AddDirectProductToExponentialRightAdjunctionIsomorphism ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation DirectProductToExponentialRightAdjunctionIsomorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b, c ) \mapsto \mathtt{DirectProductToExponentialRightAdjunctionIsomorphism}(a, b, c)\).
‣ AddDirectProductToExponentialRightAdjunctionIsomorphismWithGivenObjects ( C, F ) | ( operation ) |
‣ AddDirectProductToExponentialRightAdjunctionIsomorphismWithGivenObjects ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation DirectProductToExponentialRightAdjunctionIsomorphismWithGivenObjects
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( s, a, b, c, r ) \mapsto \mathtt{DirectProductToExponentialRightAdjunctionIsomorphismWithGivenObjects}(s, a, b, c, r)\).
‣ AddExponentialOnMorphisms ( C, F ) | ( operation ) |
‣ AddExponentialOnMorphisms ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation ExponentialOnMorphisms
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( alpha, beta ) \mapsto \mathtt{ExponentialOnMorphisms}(alpha, beta)\).
‣ AddExponentialOnMorphismsWithGivenExponentials ( C, F ) | ( operation ) |
‣ AddExponentialOnMorphismsWithGivenExponentials ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation ExponentialOnMorphismsWithGivenExponentials
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( s, alpha, beta, r ) \mapsto \mathtt{ExponentialOnMorphismsWithGivenExponentials}(s, alpha, beta, r)\).
‣ AddExponentialOnObjects ( C, F ) | ( operation ) |
‣ AddExponentialOnObjects ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation ExponentialOnObjects
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b ) \mapsto \mathtt{ExponentialOnObjects}(a, b)\).
‣ AddExponentialToDirectProductLeftAdjunctMorphism ( C, F ) | ( operation ) |
‣ AddExponentialToDirectProductLeftAdjunctMorphism ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation ExponentialToDirectProductLeftAdjunctMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( b, c, g ) \mapsto \mathtt{ExponentialToDirectProductLeftAdjunctMorphism}(b, c, g)\).
‣ AddExponentialToDirectProductLeftAdjunctMorphismWithGivenDirectProduct ( C, F ) | ( operation ) |
‣ AddExponentialToDirectProductLeftAdjunctMorphismWithGivenDirectProduct ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation ExponentialToDirectProductLeftAdjunctMorphismWithGivenDirectProduct
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( b, c, g, s ) \mapsto \mathtt{ExponentialToDirectProductLeftAdjunctMorphismWithGivenDirectProduct}(b, c, g, s)\).
‣ AddExponentialToDirectProductLeftAdjunctionIsomorphism ( C, F ) | ( operation ) |
‣ AddExponentialToDirectProductLeftAdjunctionIsomorphism ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation ExponentialToDirectProductLeftAdjunctionIsomorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b, c ) \mapsto \mathtt{ExponentialToDirectProductLeftAdjunctionIsomorphism}(a, b, c)\).
‣ AddExponentialToDirectProductLeftAdjunctionIsomorphismWithGivenObjects ( C, F ) | ( operation ) |
‣ AddExponentialToDirectProductLeftAdjunctionIsomorphismWithGivenObjects ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation ExponentialToDirectProductLeftAdjunctionIsomorphismWithGivenObjects
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( s, a, b, c, r ) \mapsto \mathtt{ExponentialToDirectProductLeftAdjunctionIsomorphismWithGivenObjects}(s, a, b, c, r)\).
‣ AddExponentialToDirectProductRightAdjunctMorphism ( C, F ) | ( operation ) |
‣ AddExponentialToDirectProductRightAdjunctMorphism ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation ExponentialToDirectProductRightAdjunctMorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, c, g ) \mapsto \mathtt{ExponentialToDirectProductRightAdjunctMorphism}(a, c, g)\).
‣ AddExponentialToDirectProductRightAdjunctMorphismWithGivenDirectProduct ( C, F ) | ( operation ) |
‣ AddExponentialToDirectProductRightAdjunctMorphismWithGivenDirectProduct ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation ExponentialToDirectProductRightAdjunctMorphismWithGivenDirectProduct
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, c, g, s ) \mapsto \mathtt{ExponentialToDirectProductRightAdjunctMorphismWithGivenDirectProduct}(a, c, g, s)\).
‣ AddExponentialToDirectProductRightAdjunctionIsomorphism ( C, F ) | ( operation ) |
‣ AddExponentialToDirectProductRightAdjunctionIsomorphism ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation ExponentialToDirectProductRightAdjunctionIsomorphism
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b, c ) \mapsto \mathtt{ExponentialToDirectProductRightAdjunctionIsomorphism}(a, b, c)\).
‣ AddExponentialToDirectProductRightAdjunctionIsomorphismWithGivenObjects ( C, F ) | ( operation ) |
‣ AddExponentialToDirectProductRightAdjunctionIsomorphismWithGivenObjects ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation ExponentialToDirectProductRightAdjunctionIsomorphismWithGivenObjects
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( s, a, b, c, r ) \mapsto \mathtt{ExponentialToDirectProductRightAdjunctionIsomorphismWithGivenObjects}(s, a, b, c, r)\).
‣ AddIsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject ( C, F ) | ( operation ) |
‣ AddIsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation IsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a ) \mapsto \mathtt{IsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject}(a)\).
‣ AddIsomorphismFromExponentialIntoTerminalObjectToCartesianDualObject ( C, F ) | ( operation ) |
‣ AddIsomorphismFromExponentialIntoTerminalObjectToCartesianDualObject ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation IsomorphismFromExponentialIntoTerminalObjectToCartesianDualObject
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a ) \mapsto \mathtt{IsomorphismFromExponentialIntoTerminalObjectToCartesianDualObject}(a)\).
‣ AddIsomorphismFromExponentialToObject ( C, F ) | ( operation ) |
‣ AddIsomorphismFromExponentialToObject ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation IsomorphismFromExponentialToObject
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a ) \mapsto \mathtt{IsomorphismFromExponentialToObject}(a)\).
‣ AddIsomorphismFromExponentialToObjectWithGivenExponential ( C, F ) | ( operation ) |
‣ AddIsomorphismFromExponentialToObjectWithGivenExponential ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation IsomorphismFromExponentialToObjectWithGivenExponential
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, s ) \mapsto \mathtt{IsomorphismFromExponentialToObjectWithGivenExponential}(a, s)\).
‣ AddIsomorphismFromObjectToExponential ( C, F ) | ( operation ) |
‣ AddIsomorphismFromObjectToExponential ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation IsomorphismFromObjectToExponential
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a ) \mapsto \mathtt{IsomorphismFromObjectToExponential}(a)\).
‣ AddIsomorphismFromObjectToExponentialWithGivenExponential ( C, F ) | ( operation ) |
‣ AddIsomorphismFromObjectToExponentialWithGivenExponential ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation IsomorphismFromObjectToExponentialWithGivenExponential
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, r ) \mapsto \mathtt{IsomorphismFromObjectToExponentialWithGivenExponential}(a, r)\).
‣ AddMorphismFromDirectProductToExponential ( C, F ) | ( operation ) |
‣ AddMorphismFromDirectProductToExponential ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation MorphismFromDirectProductToExponential
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b ) \mapsto \mathtt{MorphismFromDirectProductToExponential}(a, b)\).
‣ AddMorphismFromDirectProductToExponentialWithGivenObjects ( C, F ) | ( operation ) |
‣ AddMorphismFromDirectProductToExponentialWithGivenObjects ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation MorphismFromDirectProductToExponentialWithGivenObjects
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( s, a, b, r ) \mapsto \mathtt{MorphismFromDirectProductToExponentialWithGivenObjects}(s, a, b, r)\).
‣ AddMorphismToCartesianBidual ( C, F ) | ( operation ) |
‣ AddMorphismToCartesianBidual ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation MorphismToCartesianBidual
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a ) \mapsto \mathtt{MorphismToCartesianBidual}(a)\).
‣ AddMorphismToCartesianBidualWithGivenCartesianBidual ( C, F ) | ( operation ) |
‣ AddMorphismToCartesianBidualWithGivenCartesianBidual ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation MorphismToCartesianBidualWithGivenCartesianBidual
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, r ) \mapsto \mathtt{MorphismToCartesianBidualWithGivenCartesianBidual}(a, r)\).
‣ AddUniversalPropertyOfCartesianDual ( C, F ) | ( operation ) |
‣ AddUniversalPropertyOfCartesianDual ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation UniversalPropertyOfCartesianDual
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( t, a, alpha ) \mapsto \mathtt{UniversalPropertyOfCartesianDual}(t, a, alpha)\).
‣ AddLeftCartesianDistributivityExpanding ( C, F ) | ( operation ) |
‣ AddLeftCartesianDistributivityExpanding ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation LeftCartesianDistributivityExpanding
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, L ) \mapsto \mathtt{LeftCartesianDistributivityExpanding}(a, L)\).
‣ AddLeftCartesianDistributivityExpandingWithGivenObjects ( C, F ) | ( operation ) |
‣ AddLeftCartesianDistributivityExpandingWithGivenObjects ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation LeftCartesianDistributivityExpandingWithGivenObjects
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( s, a, L, r ) \mapsto \mathtt{LeftCartesianDistributivityExpandingWithGivenObjects}(s, a, L, r)\).
‣ AddLeftCartesianDistributivityFactoring ( C, F ) | ( operation ) |
‣ AddLeftCartesianDistributivityFactoring ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation LeftCartesianDistributivityFactoring
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, L ) \mapsto \mathtt{LeftCartesianDistributivityFactoring}(a, L)\).
‣ AddLeftCartesianDistributivityFactoringWithGivenObjects ( C, F ) | ( operation ) |
‣ AddLeftCartesianDistributivityFactoringWithGivenObjects ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation LeftCartesianDistributivityFactoringWithGivenObjects
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( s, a, L, r ) \mapsto \mathtt{LeftCartesianDistributivityFactoringWithGivenObjects}(s, a, L, r)\).
‣ AddRightCartesianDistributivityExpanding ( C, F ) | ( operation ) |
‣ AddRightCartesianDistributivityExpanding ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RightCartesianDistributivityExpanding
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( L, a ) \mapsto \mathtt{RightCartesianDistributivityExpanding}(L, a)\).
‣ AddRightCartesianDistributivityExpandingWithGivenObjects ( C, F ) | ( operation ) |
‣ AddRightCartesianDistributivityExpandingWithGivenObjects ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RightCartesianDistributivityExpandingWithGivenObjects
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( s, L, a, r ) \mapsto \mathtt{RightCartesianDistributivityExpandingWithGivenObjects}(s, L, a, r)\).
‣ AddRightCartesianDistributivityFactoring ( C, F ) | ( operation ) |
‣ AddRightCartesianDistributivityFactoring ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RightCartesianDistributivityFactoring
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( L, a ) \mapsto \mathtt{RightCartesianDistributivityFactoring}(L, a)\).
‣ AddRightCartesianDistributivityFactoringWithGivenObjects ( C, F ) | ( operation ) |
‣ AddRightCartesianDistributivityFactoringWithGivenObjects ( C, F, weight ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RightCartesianDistributivityFactoringWithGivenObjects
. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( s, L, a, r ) \mapsto \mathtt{RightCartesianDistributivityFactoringWithGivenObjects}(s, L, a, r)\).
generated by GAPDoc2HTML