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 ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianBraiding. F: ( a, b ) \mapsto \mathtt{CartesianBraiding}(a, b).
‣ AddCartesianBraidingInverse( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianBraidingInverse. F: ( a, b ) \mapsto \mathtt{CartesianBraidingInverse}(a, b).
‣ AddCartesianBraidingInverseWithGivenDirectProducts( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianBraidingInverseWithGivenDirectProducts. F: ( s, a, b, r ) \mapsto \mathtt{CartesianBraidingInverseWithGivenDirectProducts}(s, a, b, r).
‣ AddCartesianBraidingWithGivenDirectProducts( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianBraidingWithGivenDirectProducts. F: ( s, a, b, r ) \mapsto \mathtt{CartesianBraidingWithGivenDirectProducts}(s, a, b, r).
‣ AddCartesianAssociatorLeftToRight( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianAssociatorLeftToRight. F: ( a, b, c ) \mapsto \mathtt{CartesianAssociatorLeftToRight}(a, b, c).
‣ AddCartesianAssociatorLeftToRightWithGivenDirectProducts( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianAssociatorLeftToRightWithGivenDirectProducts. F: ( s, a, b, c, r ) \mapsto \mathtt{CartesianAssociatorLeftToRightWithGivenDirectProducts}(s, a, b, c, r).
‣ AddCartesianAssociatorRightToLeft( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianAssociatorRightToLeft. F: ( a, b, c ) \mapsto \mathtt{CartesianAssociatorRightToLeft}(a, b, c).
‣ AddCartesianAssociatorRightToLeftWithGivenDirectProducts( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianAssociatorRightToLeftWithGivenDirectProducts. F: ( s, a, b, c, r ) \mapsto \mathtt{CartesianAssociatorRightToLeftWithGivenDirectProducts}(s, a, b, c, r).
‣ AddCartesianDiagonal( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianDiagonal. F: ( a, n ) \mapsto \mathtt{CartesianDiagonal}(a, n).
‣ AddCartesianDiagonalWithGivenCartesianPower( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianDiagonalWithGivenCartesianPower. F: ( a, n, cartesian_power ) \mapsto \mathtt{CartesianDiagonalWithGivenCartesianPower}(a, n, cartesian_power).
‣ AddCartesianLeftUnitor( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianLeftUnitor. F: ( a ) \mapsto \mathtt{CartesianLeftUnitor}(a).
‣ AddCartesianLeftUnitorInverse( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianLeftUnitorInverse. F: ( a ) \mapsto \mathtt{CartesianLeftUnitorInverse}(a).
‣ AddCartesianLeftUnitorInverseWithGivenDirectProduct( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianLeftUnitorInverseWithGivenDirectProduct. F: ( a, r ) \mapsto \mathtt{CartesianLeftUnitorInverseWithGivenDirectProduct}(a, r).
‣ AddCartesianLeftUnitorWithGivenDirectProduct( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianLeftUnitorWithGivenDirectProduct. F: ( a, s ) \mapsto \mathtt{CartesianLeftUnitorWithGivenDirectProduct}(a, s).
‣ AddCartesianRightUnitor( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianRightUnitor. F: ( a ) \mapsto \mathtt{CartesianRightUnitor}(a).
‣ AddCartesianRightUnitorInverse( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianRightUnitorInverse. F: ( a ) \mapsto \mathtt{CartesianRightUnitorInverse}(a).
‣ AddCartesianRightUnitorInverseWithGivenDirectProduct( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianRightUnitorInverseWithGivenDirectProduct. F: ( a, r ) \mapsto \mathtt{CartesianRightUnitorInverseWithGivenDirectProduct}(a, r).
‣ AddCartesianRightUnitorWithGivenDirectProduct( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianRightUnitorWithGivenDirectProduct. F: ( a, s ) \mapsto \mathtt{CartesianRightUnitorWithGivenDirectProduct}(a, s).
‣ AddDirectProductOnMorphisms( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation DirectProductOnMorphisms. F: ( alpha, beta ) \mapsto \mathtt{DirectProductOnMorphisms}(alpha, beta).
‣ AddDirectProductOnMorphismsWithGivenDirectProducts( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation DirectProductOnMorphismsWithGivenDirectProducts. F: ( s, alpha, beta, r ) \mapsto \mathtt{DirectProductOnMorphismsWithGivenDirectProducts}(s, alpha, beta, r).
‣ AddCartesianDualOnMorphisms( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianDualOnMorphisms. F: ( alpha ) \mapsto \mathtt{CartesianDualOnMorphisms}(alpha).
‣ AddCartesianDualOnMorphismsWithGivenCartesianDuals( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianDualOnMorphismsWithGivenCartesianDuals. F: ( s, alpha, r ) \mapsto \mathtt{CartesianDualOnMorphismsWithGivenCartesianDuals}(s, alpha, r).
‣ AddCartesianDualOnObjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianDualOnObjects. F: ( a ) \mapsto \mathtt{CartesianDualOnObjects}(a).
‣ AddCartesianEvaluationForCartesianDual( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianEvaluationForCartesianDual. F: ( a ) \mapsto \mathtt{CartesianEvaluationForCartesianDual}(a).
‣ AddCartesianEvaluationForCartesianDualWithGivenDirectProduct( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianEvaluationForCartesianDualWithGivenDirectProduct. F: ( s, a, r ) \mapsto \mathtt{CartesianEvaluationForCartesianDualWithGivenDirectProduct}(s, a, r).
‣ AddCartesianLambdaElimination( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianLambdaElimination. F: ( a, b, alpha ) \mapsto \mathtt{CartesianLambdaElimination}(a, b, alpha).
‣ AddCartesianLambdaIntroduction( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianLambdaIntroduction. F: ( alpha ) \mapsto \mathtt{CartesianLambdaIntroduction}(alpha).
‣ AddCartesianLeftCoevaluationMorphism( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianLeftCoevaluationMorphism. F: ( a, b ) \mapsto \mathtt{CartesianLeftCoevaluationMorphism}(a, b).
‣ AddCartesianLeftCoevaluationMorphismWithGivenRange( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianLeftCoevaluationMorphismWithGivenRange. F: ( a, b, r ) \mapsto \mathtt{CartesianLeftCoevaluationMorphismWithGivenRange}(a, b, r).
‣ AddCartesianLeftEvaluationMorphism( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianLeftEvaluationMorphism. F: ( a, b ) \mapsto \mathtt{CartesianLeftEvaluationMorphism}(a, b).
‣ AddCartesianLeftEvaluationMorphismWithGivenSource( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianLeftEvaluationMorphismWithGivenSource. F: ( a, b, s ) \mapsto \mathtt{CartesianLeftEvaluationMorphismWithGivenSource}(a, b, s).
‣ AddCartesianPostComposeMorphism( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianPostComposeMorphism. F: ( a, b, c ) \mapsto \mathtt{CartesianPostComposeMorphism}(a, b, c).
‣ AddCartesianPostComposeMorphismWithGivenObjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianPostComposeMorphismWithGivenObjects. F: ( s, a, b, c, r ) \mapsto \mathtt{CartesianPostComposeMorphismWithGivenObjects}(s, a, b, c, r).
‣ AddCartesianPreComposeMorphism( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianPreComposeMorphism. F: ( a, b, c ) \mapsto \mathtt{CartesianPreComposeMorphism}(a, b, c).
‣ AddCartesianPreComposeMorphismWithGivenObjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianPreComposeMorphismWithGivenObjects. F: ( s, a, b, c, r ) \mapsto \mathtt{CartesianPreComposeMorphismWithGivenObjects}(s, a, b, c, r).
‣ AddCartesianRightCoevaluationMorphism( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianRightCoevaluationMorphism. F: ( a, b ) \mapsto \mathtt{CartesianRightCoevaluationMorphism}(a, b).
‣ AddCartesianRightCoevaluationMorphismWithGivenRange( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianRightCoevaluationMorphismWithGivenRange. F: ( a, b, r ) \mapsto \mathtt{CartesianRightCoevaluationMorphismWithGivenRange}(a, b, r).
‣ AddCartesianRightEvaluationMorphism( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianRightEvaluationMorphism. F: ( a, b ) \mapsto \mathtt{CartesianRightEvaluationMorphism}(a, b).
‣ AddCartesianRightEvaluationMorphismWithGivenSource( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation CartesianRightEvaluationMorphismWithGivenSource. F: ( a, b, s ) \mapsto \mathtt{CartesianRightEvaluationMorphismWithGivenSource}(a, b, s).
‣ AddDirectProductCartesianDualityCompatibilityMorphism( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation DirectProductCartesianDualityCompatibilityMorphism. F: ( a, b ) \mapsto \mathtt{DirectProductCartesianDualityCompatibilityMorphism}(a, b).
‣ AddDirectProductCartesianDualityCompatibilityMorphismWithGivenObjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation DirectProductCartesianDualityCompatibilityMorphismWithGivenObjects. F: ( s, a, b, r ) \mapsto \mathtt{DirectProductCartesianDualityCompatibilityMorphismWithGivenObjects}(s, a, b, r).
‣ AddDirectProductExponentialCompatibilityMorphism( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation DirectProductExponentialCompatibilityMorphism. F: ( list ) \mapsto \mathtt{DirectProductExponentialCompatibilityMorphism}(list).
‣ AddDirectProductExponentialCompatibilityMorphismWithGivenObjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation DirectProductExponentialCompatibilityMorphismWithGivenObjects. F: ( source, list, range ) \mapsto \mathtt{DirectProductExponentialCompatibilityMorphismWithGivenObjects}(source, list, range).
‣ AddDirectProductToExponentialLeftAdjunctMorphism( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation DirectProductToExponentialLeftAdjunctMorphism. F: ( a, b, f ) \mapsto \mathtt{DirectProductToExponentialLeftAdjunctMorphism}(a, b, f).
‣ AddDirectProductToExponentialLeftAdjunctMorphismWithGivenExponential( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation DirectProductToExponentialLeftAdjunctMorphismWithGivenExponential. F: ( a, b, f, i ) \mapsto \mathtt{DirectProductToExponentialLeftAdjunctMorphismWithGivenExponential}(a, b, f, i).
‣ AddDirectProductToExponentialLeftAdjunctionIsomorphism( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation DirectProductToExponentialLeftAdjunctionIsomorphism. F: ( a, b, c ) \mapsto \mathtt{DirectProductToExponentialLeftAdjunctionIsomorphism}(a, b, c).
‣ AddDirectProductToExponentialLeftAdjunctionIsomorphismWithGivenObjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation DirectProductToExponentialLeftAdjunctionIsomorphismWithGivenObjects. F: ( s, a, b, c, r ) \mapsto \mathtt{DirectProductToExponentialLeftAdjunctionIsomorphismWithGivenObjects}(s, a, b, c, r).
‣ AddDirectProductToExponentialRightAdjunctMorphism( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation DirectProductToExponentialRightAdjunctMorphism. F: ( a, b, f ) \mapsto \mathtt{DirectProductToExponentialRightAdjunctMorphism}(a, b, f).
‣ AddDirectProductToExponentialRightAdjunctMorphismWithGivenExponential( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation DirectProductToExponentialRightAdjunctMorphismWithGivenExponential. F: ( a, b, f, i ) \mapsto \mathtt{DirectProductToExponentialRightAdjunctMorphismWithGivenExponential}(a, b, f, i).
‣ AddDirectProductToExponentialRightAdjunctionIsomorphism( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation DirectProductToExponentialRightAdjunctionIsomorphism. F: ( a, b, c ) \mapsto \mathtt{DirectProductToExponentialRightAdjunctionIsomorphism}(a, b, c).
‣ AddDirectProductToExponentialRightAdjunctionIsomorphismWithGivenObjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation DirectProductToExponentialRightAdjunctionIsomorphismWithGivenObjects. F: ( s, a, b, c, r ) \mapsto \mathtt{DirectProductToExponentialRightAdjunctionIsomorphismWithGivenObjects}(s, a, b, c, r).
‣ AddExponentialOnMorphisms( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation ExponentialOnMorphisms. F: ( alpha, beta ) \mapsto \mathtt{ExponentialOnMorphisms}(alpha, beta).
‣ AddExponentialOnMorphismsWithGivenExponentials( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation ExponentialOnMorphismsWithGivenExponentials. F: ( s, alpha, beta, r ) \mapsto \mathtt{ExponentialOnMorphismsWithGivenExponentials}(s, alpha, beta, r).
‣ AddExponentialOnObjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation ExponentialOnObjects. F: ( a, b ) \mapsto \mathtt{ExponentialOnObjects}(a, b).
‣ AddExponentialToDirectProductLeftAdjunctMorphism( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation ExponentialToDirectProductLeftAdjunctMorphism. F: ( b, c, g ) \mapsto \mathtt{ExponentialToDirectProductLeftAdjunctMorphism}(b, c, g).
‣ AddExponentialToDirectProductLeftAdjunctMorphismWithGivenDirectProduct( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation ExponentialToDirectProductLeftAdjunctMorphismWithGivenDirectProduct. F: ( b, c, g, s ) \mapsto \mathtt{ExponentialToDirectProductLeftAdjunctMorphismWithGivenDirectProduct}(b, c, g, s).
‣ AddExponentialToDirectProductLeftAdjunctionIsomorphism( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation ExponentialToDirectProductLeftAdjunctionIsomorphism. F: ( a, b, c ) \mapsto \mathtt{ExponentialToDirectProductLeftAdjunctionIsomorphism}(a, b, c).
‣ AddExponentialToDirectProductLeftAdjunctionIsomorphismWithGivenObjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation ExponentialToDirectProductLeftAdjunctionIsomorphismWithGivenObjects. F: ( s, a, b, c, r ) \mapsto \mathtt{ExponentialToDirectProductLeftAdjunctionIsomorphismWithGivenObjects}(s, a, b, c, r).
‣ AddExponentialToDirectProductRightAdjunctMorphism( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation ExponentialToDirectProductRightAdjunctMorphism. F: ( a, c, g ) \mapsto \mathtt{ExponentialToDirectProductRightAdjunctMorphism}(a, c, g).
‣ AddExponentialToDirectProductRightAdjunctMorphismWithGivenDirectProduct( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation ExponentialToDirectProductRightAdjunctMorphismWithGivenDirectProduct. F: ( a, c, g, s ) \mapsto \mathtt{ExponentialToDirectProductRightAdjunctMorphismWithGivenDirectProduct}(a, c, g, s).
‣ AddExponentialToDirectProductRightAdjunctionIsomorphism( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation ExponentialToDirectProductRightAdjunctionIsomorphism. F: ( a, b, c ) \mapsto \mathtt{ExponentialToDirectProductRightAdjunctionIsomorphism}(a, b, c).
‣ AddExponentialToDirectProductRightAdjunctionIsomorphismWithGivenObjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation ExponentialToDirectProductRightAdjunctionIsomorphismWithGivenObjects. F: ( s, a, b, c, r ) \mapsto \mathtt{ExponentialToDirectProductRightAdjunctionIsomorphismWithGivenObjects}(s, a, b, c, r).
‣ AddIsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation IsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject. F: ( a ) \mapsto \mathtt{IsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject}(a).
‣ AddIsomorphismFromExponentialIntoTerminalObjectToCartesianDualObject( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation IsomorphismFromExponentialIntoTerminalObjectToCartesianDualObject. F: ( a ) \mapsto \mathtt{IsomorphismFromExponentialIntoTerminalObjectToCartesianDualObject}(a).
‣ AddIsomorphismFromExponentialToObject( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation IsomorphismFromExponentialToObject. F: ( a ) \mapsto \mathtt{IsomorphismFromExponentialToObject}(a).
‣ AddIsomorphismFromExponentialToObjectWithGivenExponential( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation IsomorphismFromExponentialToObjectWithGivenExponential. F: ( a, s ) \mapsto \mathtt{IsomorphismFromExponentialToObjectWithGivenExponential}(a, s).
‣ AddIsomorphismFromObjectToExponential( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation IsomorphismFromObjectToExponential. F: ( a ) \mapsto \mathtt{IsomorphismFromObjectToExponential}(a).
‣ AddIsomorphismFromObjectToExponentialWithGivenExponential( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation IsomorphismFromObjectToExponentialWithGivenExponential. F: ( a, r ) \mapsto \mathtt{IsomorphismFromObjectToExponentialWithGivenExponential}(a, r).
‣ AddMorphismFromDirectProductToExponential( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation MorphismFromDirectProductToExponential. F: ( a, b ) \mapsto \mathtt{MorphismFromDirectProductToExponential}(a, b).
‣ AddMorphismFromDirectProductToExponentialWithGivenObjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation MorphismFromDirectProductToExponentialWithGivenObjects. F: ( s, a, b, r ) \mapsto \mathtt{MorphismFromDirectProductToExponentialWithGivenObjects}(s, a, b, r).
‣ AddMorphismToCartesianBidual( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation MorphismToCartesianBidual. F: ( a ) \mapsto \mathtt{MorphismToCartesianBidual}(a).
‣ AddMorphismToCartesianBidualWithGivenCartesianBidual( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation MorphismToCartesianBidualWithGivenCartesianBidual. F: ( a, r ) \mapsto \mathtt{MorphismToCartesianBidualWithGivenCartesianBidual}(a, r).
‣ AddUniversalPropertyOfCartesianDual( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation UniversalPropertyOfCartesianDual. F: ( t, a, alpha ) \mapsto \mathtt{UniversalPropertyOfCartesianDual}(t, a, alpha).
‣ AddLeftCartesianDistributivityExpanding( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftCartesianDistributivityExpanding. F: ( a, L ) \mapsto \mathtt{LeftCartesianDistributivityExpanding}(a, L).
‣ AddLeftCartesianDistributivityExpandingWithGivenObjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftCartesianDistributivityExpandingWithGivenObjects. F: ( s, a, L, r ) \mapsto \mathtt{LeftCartesianDistributivityExpandingWithGivenObjects}(s, a, L, r).
‣ AddLeftCartesianDistributivityFactoring( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftCartesianDistributivityFactoring. F: ( a, L ) \mapsto \mathtt{LeftCartesianDistributivityFactoring}(a, L).
‣ AddLeftCartesianDistributivityFactoringWithGivenObjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation LeftCartesianDistributivityFactoringWithGivenObjects. F: ( s, a, L, r ) \mapsto \mathtt{LeftCartesianDistributivityFactoringWithGivenObjects}(s, a, L, r).
‣ AddRightCartesianDistributivityExpanding( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation RightCartesianDistributivityExpanding. F: ( L, a ) \mapsto \mathtt{RightCartesianDistributivityExpanding}(L, a).
‣ AddRightCartesianDistributivityExpandingWithGivenObjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation RightCartesianDistributivityExpandingWithGivenObjects. F: ( s, L, a, r ) \mapsto \mathtt{RightCartesianDistributivityExpandingWithGivenObjects}(s, L, a, r).
‣ AddRightCartesianDistributivityFactoring( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation RightCartesianDistributivityFactoring. F: ( L, a ) \mapsto \mathtt{RightCartesianDistributivityFactoring}(L, a).
‣ AddRightCartesianDistributivityFactoringWithGivenObjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation RightCartesianDistributivityFactoringWithGivenObjects. F: ( s, L, a, r ) \mapsto \mathtt{RightCartesianDistributivityFactoringWithGivenObjects}(s, L, a, r).
generated by GAPDoc2HTML