A \(6\)-tuple \(( \mathbf{C}, \otimes, 1, \alpha, \lambda, \rho )\) consisting of
a category \(\mathbf{C}\),
a functor \(\otimes: \mathbf{C} \times \mathbf{C} \rightarrow \mathbf{C}\) compatible with the congruence of morphisms,
an object \(1 \in \mathbf{C}\),
a natural isomorphism \(\alpha_{a,b,c}: a \otimes (b \otimes c) \cong (a \otimes b) \otimes c\),
a natural isomorphism \(\lambda_{a}: 1 \otimes a \cong a\),
a natural isomorphism \(\rho_{a}: a \otimes 1 \cong a\),
is called a monoidal category, if
for all objects \(a,b,c,d\), the pentagon identity holds:
\((\alpha_{a,b,c} \otimes \mathrm{id}_d) \circ \alpha_{a,b \otimes c, d} \circ ( \mathrm{id}_a \otimes \alpha_{b,c,d} ) \sim \alpha_{a \otimes b, c, d} \circ \alpha_{a,b,c \otimes d}\),
for all objects \(a,c\), the triangle identity holds:
\(( \rho_a \otimes \mathrm{id}_c ) \circ \alpha_{a,1,c} \sim \mathrm{id}_a \otimes \lambda_c\).
The corresponding GAP property is given by IsMonoidalCategory.
‣ TensorProductOnMorphisms( alpha, beta ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a \otimes b, a' \otimes b')\)
The arguments are two morphisms \(\alpha: a \rightarrow a', \beta: b \rightarrow b'\). The output is the tensor product \(\alpha \otimes \beta\).
‣ TensorProductOnMorphismsWithGivenTensorProducts( s, alpha, beta, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a \otimes b, a' \otimes b')\)
The arguments are an object \(s = a \otimes b\), two morphisms \(\alpha: a \rightarrow a', \beta: b \rightarrow b'\), and an object \(r = a' \otimes b'\). The output is the tensor product \(\alpha \otimes \beta\).
‣ AssociatorRightToLeft( a, b, c ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a \otimes (b \otimes c), (a \otimes b) \otimes c )\).
The arguments are three objects \(a,b,c\). The output is the associator \(\alpha_{a,(b,c)}: a \otimes (b \otimes c) \rightarrow (a \otimes b) \otimes c\).
‣ AssociatorRightToLeftWithGivenTensorProducts( s, a, b, c, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a \otimes (b \otimes c), (a \otimes b) \otimes c )\).
The arguments are an object \(s = a \otimes (b \otimes c)\), three objects \(a,b,c\), and an object \(r = (a \otimes b) \otimes c\). The output is the associator \(\alpha_{a,(b,c)}: a \otimes (b \otimes c) \rightarrow (a \otimes b) \otimes c\).
‣ AssociatorLeftToRight( a, b, c ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( (a \otimes b) \otimes c \rightarrow a \otimes (b \otimes c) )\).
The arguments are three objects \(a,b,c\). The output is the associator \(\alpha_{(a,b),c}: (a \otimes b) \otimes c \rightarrow a \otimes (b \otimes c)\).
‣ AssociatorLeftToRightWithGivenTensorProducts( s, a, b, c, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( (a \otimes b) \otimes c \rightarrow a \otimes (b \otimes c) )\).
The arguments are an object \(s = (a \otimes b) \otimes c\), three objects \(a,b,c\), and an object \(r = a \otimes (b \otimes c)\). The output is the associator \(\alpha_{(a,b),c}: (a \otimes b) \otimes c \rightarrow a \otimes (b \otimes c)\).
‣ LeftUnitor( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(1 \otimes a, a)\)
The argument is an object \(a\). The output is the left unitor \(\lambda_a: 1 \otimes a \rightarrow a\).
‣ LeftUnitorWithGivenTensorProduct( a, s ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(1 \otimes a, a)\)
The arguments are an object \(a\) and an object \(s = 1 \otimes a\). The output is the left unitor \(\lambda_a: 1 \otimes a \rightarrow a\).
‣ LeftUnitorInverse( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(a, 1 \otimes a)\)
The argument is an object \(a\). The output is the inverse of the left unitor \(\lambda_a^{-1}: a \rightarrow 1 \otimes a\).
‣ LeftUnitorInverseWithGivenTensorProduct( a, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a, 1 \otimes a)\)
The argument is an object \(a\) and an object \(r = 1 \otimes a\). The output is the inverse of the left unitor \(\lambda_a^{-1}: a \rightarrow 1 \otimes a\).
‣ RightUnitor( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(a \otimes 1, a)\)
The argument is an object \(a\). The output is the right unitor \(\rho_a: a \otimes 1 \rightarrow a\).
‣ RightUnitorWithGivenTensorProduct( a, s ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a \otimes 1, a)\)
The arguments are an object \(a\) and an object \(s = a \otimes 1\). The output is the right unitor \(\rho_a: a \otimes 1 \rightarrow a\).
‣ RightUnitorInverse( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(a, a \otimes 1)\)
The argument is an object \(a\). The output is the inverse of the right unitor \(\rho_a^{-1}: a \rightarrow a \otimes 1\).
‣ RightUnitorInverseWithGivenTensorProduct( a, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a, a \otimes 1)\)
The arguments are an object \(a\) and an object \(r = a \otimes 1\). The output is the inverse of the right unitor \(\rho_a^{-1}: a \rightarrow a \otimes 1\).
‣ TensorProductOnObjects( a, b ) | ( operation ) |
Returns: an object
The arguments are two objects \(a, b\). The output is the tensor product \(a \otimes b\).
‣ TensorUnit( C ) | ( attribute ) |
Returns: an object
The argument is a category \(\mathbf{C}\). The output is the tensor unit \(1\) of \(\mathbf{C}\).
‣ LeftDistributivityExpanding( a, L ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a \otimes (b_1 \oplus \dots \oplus b_n), (a \otimes b_1) \oplus \dots \oplus (a \otimes 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 \otimes (b_1 \oplus \dots \oplus b_n) \rightarrow (a \otimes b_1) \oplus \dots \oplus (a \otimes b_n)\).
‣ LeftDistributivityExpandingWithGivenObjects( s, a, L, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\)
The arguments are an object \(s = a \otimes (b_1 \oplus \dots \oplus b_n)\), an object \(a\), a list of objects \(L = (b_1, \dots, b_n)\), and an object \(r = (a \otimes b_1) \oplus \dots \oplus (a \otimes b_n)\). The output is the left distributivity morphism \(s \rightarrow r\).
‣ LeftDistributivityFactoring( a, L ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( (a \otimes b_1) \oplus \dots \oplus (a \otimes b_n), a \otimes (b_1 \oplus \dots \oplus 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 \otimes b_1) \oplus \dots \oplus (a \otimes b_n) \rightarrow a \otimes (b_1 \oplus \dots \oplus b_n)\).
‣ LeftDistributivityFactoringWithGivenObjects( s, a, L, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\)
The arguments are an object \(s = (a \otimes b_1) \oplus \dots \oplus (a \otimes b_n)\), an object \(a\), a list of objects \(L = (b_1, \dots, b_n)\), and an object \(r = a \otimes (b_1 \oplus \dots \oplus b_n)\). The output is the left distributivity morphism \(s \rightarrow r\).
‣ RightDistributivityExpanding( L, a ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( (b_1 \oplus \dots \oplus b_n) \otimes a, (b_1 \otimes a) \oplus \dots \oplus (b_n \otimes 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 \oplus \dots \oplus b_n) \otimes a \rightarrow (b_1 \otimes a) \oplus \dots \oplus (b_n \otimes a)\).
‣ RightDistributivityExpandingWithGivenObjects( s, L, a, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\)
The arguments are an object \(s = (b_1 \oplus \dots \oplus b_n) \otimes a\), a list of objects \(L = (b_1, \dots, b_n)\), an object \(a\), and an object \(r = (b_1 \otimes a) \oplus \dots \oplus (b_n \otimes a)\). The output is the right distributivity morphism \(s \rightarrow r\).
‣ RightDistributivityFactoring( L, a ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( (b_1 \otimes a) \oplus \dots \oplus (b_n \otimes a), (b_1 \oplus \dots \oplus b_n) \otimes 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 \otimes a) \oplus \dots \oplus (b_n \otimes a) \rightarrow (b_1 \oplus \dots \oplus b_n) \otimes a \).
‣ RightDistributivityFactoringWithGivenObjects( s, L, a, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\)
The arguments are an object \(s = (b_1 \otimes a) \oplus \dots \oplus (b_n \otimes a)\), a list of objects \(L = (b_1, \dots, b_n)\), an object \(a\), and an object \(r = (b_1 \oplus \dots \oplus b_n) \otimes a\). The output is the right distributivity morphism \(s \rightarrow r\).
A monoidal category \(\mathbf{C}\) equipped with a natural isomorphism \(B_{a,b}: a \otimes b \cong b \otimes a\) is called a braided monoidal category if
\(\lambda_a \circ B_{a,1} \sim \rho_a\),
\((B_{c,a} \otimes \mathrm{id}_b) \circ \alpha_{c,a,b} \circ B_{a \otimes b,c} \sim \alpha_{a,c,b} \circ ( \mathrm{id}_a \otimes B_{b,c}) \circ \alpha^{-1}_{a,b,c}\),
\(( \mathrm{id}_b \otimes B_{c,a} ) \circ \alpha^{-1}_{b,c,a} \circ B_{a,b \otimes c} \sim \alpha^{-1}_{b,a,c} \circ (B_{a,b} \otimes \mathrm{id}_c) \circ \alpha_{a,b,c}\).
The corresponding GAP property is given by IsBraidedMonoidalCategory.
‣ Braiding( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a \otimes b, b \otimes a )\).
The arguments are two objects \(a,b\). The output is the braiding \( B_{a,b}: a \otimes b \rightarrow b \otimes a\).
‣ BraidingWithGivenTensorProducts( s, a, b, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a \otimes b, b \otimes a )\).
The arguments are an object \(s = a \otimes b\), two objects \(a,b\), and an object \(r = b \otimes a\). The output is the braiding \( B_{a,b}: a \otimes b \rightarrow b \otimes a\).
‣ BraidingInverse( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( b \otimes a, a \otimes b )\).
The arguments are two objects \(a,b\). The output is the inverse braiding \( B_{a,b}^{-1}: b \otimes a \rightarrow a \otimes b\).
‣ BraidingInverseWithGivenTensorProducts( s, a, b, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( b \otimes a, a \otimes b )\).
The arguments are an object \(s = b \otimes a\), two objects \(a,b\), and an object \(r = a \otimes b\). The output is the inverse braiding \( B_{a,b}^{-1}: b \otimes a \rightarrow a \otimes b\).
A braided monoidal category \(\mathbf{C}\) is called symmetric monoidal category if \(B_{a,b}^{-1} \sim B_{b,a}\). The corresponding GAP property is given by IsSymmetricMonoidalCategory.
A monoidal category \(\mathbf{C}\) which has for each functor \(- \otimes b: \mathbf{C} \rightarrow \mathbf{C}\) a right adjoint (denoted by \(\mathrm{\underline{Hom}_\ell}(b,-)\)) is called a left closed monoidal category.
If no operations involving left duals are installed manually, the left dual objects will be derived as \(a^\vee \coloneqq \mathrm{\underline{Hom}_\ell}(a,1)\).
The corresponding GAP property is called IsLeftClosedMonoidalCategory.
‣ LeftInternalHomOnObjects( a, b ) | ( operation ) |
Returns: an object
The arguments are two objects \(a,b\). The output is the internal hom object \(\mathrm{\underline{Hom}_\ell}(a,b)\).
‣ LeftInternalHomOnMorphisms( alpha, beta ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{Hom}_\ell}(a',b), \mathrm{\underline{Hom}_\ell}(a,b') )\)
The arguments are two morphisms \(\alpha: a \rightarrow a', \beta: b \rightarrow b'\). The output is the internal hom morphism \(\mathrm{\underline{Hom}_\ell}(\alpha,\beta): \mathrm{\underline{Hom}_\ell}(a',b) \rightarrow \mathrm{\underline{Hom}_\ell}(a,b')\).
‣ LeftInternalHomOnMorphismsWithGivenLeftInternalHoms( s, alpha, beta, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\)
The arguments are an object \(s = \mathrm{\underline{Hom}_\ell}(a',b)\), two morphisms \(\alpha: a \rightarrow a', \beta: b \rightarrow b'\), and an object \(r = \mathrm{\underline{Hom}_\ell}(a,b')\). The output is the internal hom morphism \(\mathrm{\underline{Hom}_\ell}(\alpha,\beta): \mathrm{\underline{Hom}_\ell}(a',b) \rightarrow \mathrm{\underline{Hom}_\ell}(a,b')\).
‣ LeftClosedMonoidalEvaluationMorphism( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{Hom}_\ell}(a,b) \otimes a, b )\).
The arguments are two objects \(a, b\). The output is the evaluation morphism \(\mathrm{ev}_{a,b}: \mathrm{\underline{Hom}_\ell}(a,b) \otimes a \rightarrow b\), i.e., the counit of the tensor hom adjunction.
‣ LeftClosedMonoidalEvaluationMorphismWithGivenSource( a, b, s ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, b )\).
The arguments are two objects \(a,b\) and an object \(s = \mathrm{\underline{Hom}_\ell}(a,b) \otimes a\). The output is the evaluation morphism \(\mathrm{ev}_{a,b}: \mathrm{\underline{Hom}_\ell}(a,b) \otimes a \rightarrow b\), i.e., the counit of the tensor hom adjunction.
‣ LeftClosedMonoidalCoevaluationMorphism( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( b, \mathrm{\underline{Hom}_\ell}(a, b \otimes a) )\).
The arguments are two objects \(a,b\). The output is the coevaluation morphism \(\mathrm{coev}_{a,b}: b \rightarrow \mathrm{\underline{Hom}_\ell}(a, b \otimes a)\), i.e., the unit of the tensor hom adjunction.
‣ LeftClosedMonoidalCoevaluationMorphismWithGivenRange( a, b, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( b, r )\).
The arguments are two objects \(a,b\) and an object \(r = \mathrm{\underline{Hom}_\ell}(a, b \otimes a)\). The output is the coevaluation morphism \(\mathrm{coev}_{a,b}: b \rightarrow \mathrm{\underline{Hom}_\ell}(a, b \otimes a)\), i.e., the unit of the tensor hom adjunction.
‣ TensorProductToLeftInternalHomAdjunctMorphism( a, b, f ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a, \mathrm{\underline{Hom}_\ell}(b,c) )\).
The arguments are two objects \(a,b\) and a morphism \(f: a \otimes b \rightarrow c\). The output is a morphism \(g: a \rightarrow \mathrm{\underline{Hom}_\ell}(b,c)\) corresponding to \(f\) under the tensor hom adjunction.
‣ TensorProductToLeftInternalHomAdjunctMorphismWithGivenLeftInternalHom( a, b, f, i ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a, i )\).
The arguments are two objects \(a,b\), a morphism \(f: a \otimes b \rightarrow c\) and an object \(i = \mathrm{\underline{Hom}_\ell}(b,c)\). The output is a morphism \(g: a \rightarrow \mathrm{\underline{Hom}_\ell}(b,c)\) corresponding to \(f\) under the tensor hom adjunction.
‣ LeftInternalHomToTensorProductAdjunctMorphism( b, c, g ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a \otimes b, c)\).
The arguments are two objects \(b,c\) and a morphism \(g: a \rightarrow \mathrm{\underline{Hom}_\ell}(b,c)\). The output is a morphism \(f: a \otimes b \rightarrow c\) corresponding to \(g\) under the tensor hom adjunction.
‣ LeftInternalHomToTensorProductAdjunctMorphismWithGivenTensorProduct( b, c, g, t ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(t, c)\).
The arguments are two objects \(b,c\), a morphism \(g: a \rightarrow \mathrm{\underline{Hom}_\ell}(b,c)\) and an object \(t = a \otimes b\). The output is a morphism \(f: a \otimes b \rightarrow c\) corresponding to \(g\) under the tensor hom adjunction.
‣ LeftClosedMonoidalPreComposeMorphism( a, b, c ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{Hom}_\ell}(a,b) \otimes \mathrm{\underline{Hom}_\ell}(b,c), \mathrm{\underline{Hom}_\ell}(a,c) )\).
The arguments are three objects \(a,b,c\). The output is the precomposition morphism \(\mathrm{LeftClosedMonoidalPreComposeMorphism}_{a,b,c}: \mathrm{\underline{Hom}_\ell}(a,b) \otimes \mathrm{\underline{Hom}_\ell}(b,c) \rightarrow \mathrm{\underline{Hom}_\ell}(a,c)\).
‣ LeftClosedMonoidalPreComposeMorphismWithGivenObjects( s, a, b, c, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\).
The arguments are an object \(s = \mathrm{\underline{Hom}_\ell}(a,b) \otimes \mathrm{\underline{Hom}_\ell}(b,c)\), three objects \(a,b,c\), and an object \(r = \mathrm{\underline{Hom}_\ell}(a,c)\). The output is the precomposition morphism \(\mathrm{LeftClosedMonoidalPreComposeMorphismWithGivenObjects}_{a,b,c}: \mathrm{\underline{Hom}_\ell}(a,b) \otimes \mathrm{\underline{Hom}_\ell}(b,c) \rightarrow \mathrm{\underline{Hom}_\ell}(a,c)\).
‣ LeftClosedMonoidalPostComposeMorphism( a, b, c ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{Hom}_\ell}(b,c) \otimes \mathrm{\underline{Hom}_\ell}(a,b), \mathrm{\underline{Hom}_\ell}(a,c) )\).
The arguments are three objects \(a,b,c\). The output is the postcomposition morphism \(\mathrm{LeftClosedMonoidalPostComposeMorphism}_{a,b,c}: \mathrm{\underline{Hom}_\ell}(b,c) \otimes \mathrm{\underline{Hom}_\ell}(a,b) \rightarrow \mathrm{\underline{Hom}_\ell}(a,c)\).
‣ LeftClosedMonoidalPostComposeMorphismWithGivenObjects( s, a, b, c, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\).
The arguments are an object \(s = \mathrm{\underline{Hom}_\ell}(b,c) \otimes \mathrm{\underline{Hom}_\ell}(a,b)\), three objects \(a,b,c\), and an object \(r = \mathrm{\underline{Hom}_\ell}(a,c)\). The output is the postcomposition morphism \(\mathrm{LeftClosedMonoidalPostComposeMorphismWithGivenObjects}_{a,b,c}: \mathrm{\underline{Hom}_\ell}(b,c) \otimes \mathrm{\underline{Hom}_\ell}(a,b) \rightarrow \mathrm{\underline{Hom}_\ell}(a,c)\).
‣ LeftDualOnObjects( a ) | ( attribute ) |
Returns: an object
The argument is an object \(a\). The output is its dual object \(a^{\vee}\).
‣ LeftDualOnMorphisms( 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}\).
‣ LeftDualOnMorphismsWithGivenLeftDuals( 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}\).
‣ LeftClosedMonoidalEvaluationForLeftDual( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( a^{\vee} \otimes a, 1 )\).
The argument is an object \(a\). The output is the evaluation morphism \(\mathrm{ev}_{a}: a^{\vee} \otimes a \rightarrow 1\).
‣ LeftClosedMonoidalEvaluationForLeftDualWithGivenTensorProduct( s, a, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\).
The arguments are an object \(s = a^{\vee} \otimes a\), an object \(a\), and an object \(r = 1\). The output is the evaluation morphism \(\mathrm{ev}_{a}: a^{\vee} \otimes a \rightarrow 1\).
‣ MorphismToLeftBidual( 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}\).
‣ MorphismToLeftBidualWithGivenLeftBidual( 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}\).
‣ TensorProductLeftInternalHomCompatibilityMorphism( list ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{Hom}_\ell}(a,a') \otimes \mathrm{\underline{Hom}_\ell}(b,b'), \mathrm{\underline{Hom}_\ell}(a \otimes b,a' \otimes b'))\).
The argument is a list of four objects \([ a, a', b, b' ]\). The output is the natural morphism \(\mathrm{TensorProductLeftInternalHomCompatibilityMorphism}_{a,a',b,b'}: \mathrm{\underline{Hom}_\ell}(a,a') \otimes \mathrm{\underline{Hom}_\ell}(b,b') \rightarrow \mathrm{\underline{Hom}_\ell}(a \otimes b,a' \otimes b')\).
‣ TensorProductLeftInternalHomCompatibilityMorphismWithGivenObjects( 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{\underline{Hom}_\ell}(a,a') \otimes \mathrm{\underline{Hom}_\ell}(b,b')\) and \(r = \mathrm{\underline{Hom}_\ell}(a \otimes b,a' \otimes b')\). The output is the natural morphism \(\mathrm{TensorProductLeftInternalHomCompatibilityMorphismWithGivenObjects}_{a,a',b,b'}: \mathrm{\underline{Hom}_\ell}(a,a') \otimes \mathrm{\underline{Hom}_\ell}(b,b') \rightarrow \mathrm{\underline{Hom}_\ell}(a \otimes b,a' \otimes b')\).
‣ TensorProductLeftDualityCompatibilityMorphism( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a^{\vee} \otimes b^{\vee}, (a \otimes b)^{\vee} )\).
The arguments are two objects \(a,b\). The output is the natural morphism \(\mathrm{TensorProductLeftDualityCompatibilityMorphism}: a^{\vee} \otimes b^{\vee} \rightarrow (a \otimes b)^{\vee}\).
‣ TensorProductLeftDualityCompatibilityMorphismWithGivenObjects( s, a, b, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\).
The arguments are an object \(s = a^{\vee} \otimes b^{\vee}\), two objects \(a,b\), and an object \(r = (a \otimes b)^{\vee}\). The output is the natural morphism \(\mathrm{TensorProductLeftDualityCompatibilityMorphismWithGivenObjects}_{a,b}: a^{\vee} \otimes b^{\vee} \rightarrow (a \otimes b)^{\vee}\).
‣ MorphismFromTensorProductToLeftInternalHom( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a^{\vee} \otimes b, \mathrm{\underline{Hom}_\ell}(a,b) )\).
The arguments are two objects \(a,b\). The output is the natural morphism \(\mathrm{MorphismFromTensorProductToLeftInternalHom}_{a,b}: a^{\vee} \otimes b \rightarrow \mathrm{\underline{Hom}_\ell}(a,b)\).
‣ MorphismFromTensorProductToLeftInternalHomWithGivenObjects( s, a, b, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\).
The arguments are an object \(s = a^{\vee} \otimes b\), two objects \(a,b\), and an object \(r = \mathrm{\underline{Hom}_\ell}(a,b)\). The output is the natural morphism \(\mathrm{MorphismFromTensorProductToLeftInternalHomWithGivenObjects}_{a,b}: a^{\vee} \otimes b \rightarrow \mathrm{\underline{Hom}_\ell}(a,b)\).
‣ IsomorphismFromLeftDualObjectToLeftInternalHomIntoTensorUnit( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(a^{\vee}, \mathrm{\underline{Hom}_\ell}(a,1))\).
The argument is an object \(a\). The output is the isomorphism \(\mathrm{IsomorphismFromLeftDualObjectToLeftInternalHomIntoTensorUnit}_{a}: a^{\vee} \rightarrow \mathrm{\underline{Hom}_\ell}(a,1)\).
‣ IsomorphismFromLeftInternalHomIntoTensorUnitToLeftDualObject( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(\mathrm{\underline{Hom}_\ell}(a,1), a^{\vee})\).
The argument is an object \(a\). The output is the isomorphism \(\mathrm{IsomorphismFromLeftInternalHomIntoTensorUnitToLeftDualObject}_{a}: \mathrm{\underline{Hom}_\ell}(a,1) \rightarrow a^{\vee}\).
‣ UniversalPropertyOfLeftDual( 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 \otimes a \rightarrow 1\). The output is the morphism \(t \rightarrow a^{\vee}\) given by the universal property of \(a^{\vee}\).
‣ LeftClosedMonoidalLambdaIntroduction( alpha ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( 1, \mathrm{\underline{Hom}_\ell}(a,b) )\).
The argument is a morphism \(\alpha: a \rightarrow b\). The output is the corresponding morphism \(1 \rightarrow \mathrm{\underline{Hom}_\ell}(a,b)\) under the tensor hom adjunction.
‣ LeftClosedMonoidalLambdaElimination( 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{\underline{Hom}_\ell}(a,b)\). The output is a morphism \(a \rightarrow b\) corresponding to \(\alpha\) under the tensor hom adjunction.
‣ IsomorphismFromObjectToLeftInternalHom( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(a, \mathrm{\underline{Hom}_\ell}(1,a))\).
The argument is an object \(a\). The output is the natural isomorphism \(a \rightarrow \mathrm{\underline{Hom}_\ell}(1,a)\).
‣ IsomorphismFromObjectToLeftInternalHomWithGivenLeftInternalHom( a, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a, r)\).
The argument is an object \(a\), and an object \(r = \mathrm{\underline{Hom}_\ell}(1,a)\). The output is the natural isomorphism \(a \rightarrow \mathrm{\underline{Hom}_\ell}(1,a)\).
‣ IsomorphismFromLeftInternalHomToObject( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(\mathrm{\underline{Hom}_\ell}(1,a),a)\).
The argument is an object \(a\). The output is the natural isomorphism \(\mathrm{\underline{Hom}_\ell}(1,a) \rightarrow a\).
‣ IsomorphismFromLeftInternalHomToObjectWithGivenLeftInternalHom( a, s ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(s,a)\).
The argument is an object \(a\), and an object \(s = \mathrm{\underline{Hom}_\ell}(1,a)\). The output is the natural isomorphism \(\mathrm{\underline{Hom}_\ell}(1,a) \rightarrow a\).
A monoidal category \(\mathbf{C}\) which has for each functor \(- \otimes b: \mathbf{C} \rightarrow \mathbf{C}\) a right adjoint (denoted by \(\mathrm{\underline{Hom}_\ell}(b,-)\)) is called a closed monoidal category.
If no operations involving duals are installed manually, the dual objects will be derived as \(a^\vee \coloneqq \mathrm{\underline{Hom}_\ell}(a,1)\).
The corresponding GAP property is called IsClosedMonoidalCategory.
‣ InternalHomOnObjects( a, b ) | ( operation ) |
Returns: an object
The arguments are two objects \(a,b\). The output is the internal hom object \(\mathrm{\underline{Hom}}(a,b)\).
‣ InternalHomOnMorphisms( alpha, beta ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{Hom}}(a',b), \mathrm{\underline{Hom}}(a,b') )\)
The arguments are two morphisms \(\alpha: a \rightarrow a', \beta: b \rightarrow b'\). The output is the internal hom morphism \(\mathrm{\underline{Hom}}(\alpha,\beta): \mathrm{\underline{Hom}}(a',b) \rightarrow \mathrm{\underline{Hom}}(a,b')\).
‣ InternalHomOnMorphismsWithGivenInternalHoms( s, alpha, beta, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\)
The arguments are an object \(s = \mathrm{\underline{Hom}}(a',b)\), two morphisms \(\alpha: a \rightarrow a', \beta: b \rightarrow b'\), and an object \(r = \mathrm{\underline{Hom}}(a,b')\). The output is the internal hom morphism \(\mathrm{\underline{Hom}}(\alpha,\beta): \mathrm{\underline{Hom}}(a',b) \rightarrow \mathrm{\underline{Hom}}(a,b')\).
‣ ClosedMonoidalRightEvaluationMorphism( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a \otimes \mathrm{\underline{Hom}}(a,b), b )\).
The arguments are two objects \(a, b\). The output is the right evaluation morphism \(\mathrm{ev}_{a,b}:a \otimes \mathrm{\underline{Hom}}(a,b) \rightarrow b\), i.e., the counit of the tensor hom adjunction.
‣ ClosedMonoidalRightEvaluationMorphismWithGivenSource( a, b, s ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, b )\).
The arguments are two objects \(a,b\) and an object \(s = a \otimes \mathrm{\underline{Hom}}(a,b)\). The output is the right evaluation morphism \(\mathrm{ev}_{a,b}: a \otimes \mathrm{\underline{Hom}}(a,b) \rightarrow b\), i.e., the counit of the tensor hom adjunction.
‣ ClosedMonoidalRightCoevaluationMorphism( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( b, \mathrm{\underline{Hom}}(a, a \otimes b) )\).
The arguments are two objects \(a,b\). The output is the right coevaluation morphism \(\mathrm{coev}_{a,b}: b \rightarrow \mathrm{\underline{Hom}}(a, a \otimes b)\), i.e., the unit of the tensor hom adjunction.
‣ ClosedMonoidalRightCoevaluationMorphismWithGivenRange( a, b, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( b, r )\).
The arguments are two objects \(a,b\) and an object \(r = \mathrm{\underline{Hom}}(a, a \otimes b)\). The output is the right coevaluation morphism \(\mathrm{coev}_{a,b}: b \rightarrow \mathrm{\underline{Hom}}(a, a \otimes b)\), i.e., the unit of the tensor hom adjunction.
‣ TensorProductToInternalHomRightAdjunctMorphism( a, b, f ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( b, \mathrm{\underline{Hom}}(a,c) )\).
The arguments are two objects \(a,b\) and a morphism \(f: a \otimes b \rightarrow c\). The output is a morphism \(g: b \rightarrow \mathrm{\underline{Hom}}(a,c)\) corresponding to \(f\) under the tensor hom adjunction.
‣ TensorProductToInternalHomRightAdjunctMorphismWithGivenInternalHom( a, b, f, i ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( b, i )\).
The arguments are two objects \(a,b\), a morphism \(f: a \otimes b \rightarrow c\) and an object \(i = \mathrm{\underline{Hom}}(a,c)\). The output is a morphism \(g: b \rightarrow i\) corresponding to \(f\) under the tensor hom adjunction.
‣ TensorProductToInternalHomRightAdjunctionIsomorphism( a, b, c ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( H(a \otimes b, c), H(b, \mathrm{\underline{Hom}}(a,c)) )\).
The arguments are three objects \(a,b,c\). The output is the tri-natural isomorphism \(H(a \otimes b, c) \to H(b, \mathrm{\underline{Hom}}(a,c))\) in the range category of the homomorphism structure \(H\).
‣ TensorProductToInternalHomRightAdjunctionIsomorphismWithGivenObjects( 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 \otimes b, c)\) and \(r = H(b, \mathrm{\underline{Hom}}(a,c))\). The output is the tri-natural isomorphism \(s \to r\) in the range category of the homomorphism structure \(H\).
‣ InternalHomToTensorProductRightAdjunctMorphism( a, c, g ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a \otimes b, c)\).
The arguments are two objects \(a,c\) and a morphism \(g: b \rightarrow \mathrm{\underline{Hom}}(a,c)\). The output is a morphism \(f: a \otimes b \rightarrow c\) corresponding to \(g\) under the tensor hom adjunction.
‣ InternalHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct( 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{\underline{Hom}}(a,c)\) and an object \(s = a \otimes b\). The output is a morphism \(f: s \rightarrow c\) corresponding to \(g\) under the tensor hom adjunction.
‣ InternalHomToTensorProductRightAdjunctionIsomorphism( a, b, c ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( H(b, \mathrm{\underline{Hom}}(a,c)), H(a \otimes b, c) )\).
The arguments are three objects \(a,b,c\). The output is the tri-natural isomorphism \(H(b, \mathrm{\underline{Hom}}(a,c)) \to H(a \otimes b, c)\) in the range category of the homomorphism structure \(H\).
‣ InternalHomToTensorProductRightAdjunctionIsomorphismWithGivenObjects( 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{\underline{Hom}}(a,c))\) and \(r = H(a \otimes b, c)\). The output is the tri-natural isomorphism \(s \to r\) in the range category of the homomorphism structure \(H\).
‣ ClosedMonoidalLeftEvaluationMorphism( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{Hom}}(a,b) \otimes a, b )\).
The arguments are two objects \(a, b\). The output is the left evaluation morphism \(\mathrm{ev}_{a,b}: \mathrm{\underline{Hom}}(a,b) \otimes a \rightarrow b\), i.e., the counit of the tensor hom adjunction.
‣ ClosedMonoidalLeftEvaluationMorphismWithGivenSource( a, b, s ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, b )\).
The arguments are two objects \(a,b\) and an object \(s = \mathrm{\underline{Hom}}(a,b) \otimes a\). The output is the left evaluation morphism \(\mathrm{ev}_{a,b}: \mathrm{\underline{Hom}}(a,b) \otimes a \rightarrow b\), i.e., the counit of the tensor hom adjunction.
‣ ClosedMonoidalLeftCoevaluationMorphism( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( b, \mathrm{\underline{Hom}}(a, b \otimes a) )\).
The arguments are two objects \(a,b\). The output is the left coevaluation morphism \(\mathrm{coev}_{a,b}: b \rightarrow \mathrm{\underline{Hom}}(a, b \otimes a)\), i.e., the unit of the tensor hom adjunction.
‣ ClosedMonoidalLeftCoevaluationMorphismWithGivenRange( a, b, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( b, r )\).
The arguments are two objects \(a,b\) and an object \(r = \mathrm{\underline{Hom}}(a, b \otimes a)\). The output is the left coevaluation morphism \(\mathrm{coev}_{a,b}: b \rightarrow \mathrm{\underline{Hom}}(a, b \otimes a)\), i.e., the unit of the tensor hom adjunction.
‣ TensorProductToInternalHomLeftAdjunctMorphism( a, b, f ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a, \mathrm{\underline{Hom}}(b,c) )\).
The arguments are two objects \(a,b\) and a morphism \(f: a \otimes b \rightarrow c\). The output is a morphism \(g: a \rightarrow \mathrm{\underline{Hom}}(b,c)\) corresponding to \(f\) under the tensor hom adjunction.
‣ TensorProductToInternalHomLeftAdjunctMorphismWithGivenInternalHom( a, b, f, i ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a, i )\).
The arguments are two objects \(a,b\), a morphism \(f: a \otimes b \rightarrow c\) and an object \(i = \mathrm{\underline{Hom}}(b,c)\). The output is a morphism \(g: a \rightarrow i\) corresponding to \(f\) under the tensor hom adjunction.
‣ TensorProductToInternalHomLeftAdjunctionIsomorphism( a, b, c ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( H(a \otimes b, c), H(a, \mathrm{\underline{Hom}}(b,c)) )\).
The arguments are three objects \(a,b,c\). The output is the tri-natural isomorphism \(H(a \otimes b, c) \to H(a, \mathrm{\underline{Hom}}(b,c))\) in the range category of the homomorphism structure \(H\).
‣ TensorProductToInternalHomLeftAdjunctionIsomorphismWithGivenObjects( 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 \otimes b, c)\) and \(r = H(a, \mathrm{\underline{Hom}}(b,c))\). The output is the tri-natural isomorphism \(s \to r\) in the range category of the homomorphism structure \(H\).
‣ InternalHomToTensorProductLeftAdjunctMorphism( b, c, g ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a \otimes b, c)\).
The arguments are two objects \(b,c\) and a morphism \(g: a \rightarrow \mathrm{\underline{Hom}}(b,c)\). The output is a morphism \(f: a \otimes b \rightarrow c\) corresponding to \(g\) under the tensor hom adjunction.
‣ InternalHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct( 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{\underline{Hom}}(b,c)\) and an object \(s = a \otimes b\). The output is a morphism \(f: s \rightarrow c\) corresponding to \(g\) under the tensor hom adjunction.
‣ InternalHomToTensorProductLeftAdjunctionIsomorphism( a, b, c ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( H(a, \mathrm{\underline{Hom}}(b,c)), H(a \otimes b, c) )\).
The arguments are three objects \(a,b,c\). The output is the tri-natural isomorphism \(H(a, \mathrm{\underline{Hom}}(b,c)) \to H(a \otimes b, c)\) in the range category of the homomorphism structure \(H\).
‣ InternalHomToTensorProductLeftAdjunctionIsomorphismWithGivenObjects( 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{\underline{Hom}}(b,c))\) and \(r = H(a \otimes b, c)\). The output is the tri-natural isomorphism \(s \to r\) in the range category of the homomorphism structure \(H\).
‣ MonoidalPreComposeMorphism( a, b, c ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{Hom}}(a,b) \otimes \mathrm{\underline{Hom}}(b,c), \mathrm{\underline{Hom}}(a,c) )\).
The arguments are three objects \(a,b,c\). The output is the precomposition morphism \(\mathrm{MonoidalPreComposeMorphism}_{a,b,c}: \mathrm{\underline{Hom}}(a,b) \otimes \mathrm{\underline{Hom}}(b,c) \rightarrow \mathrm{\underline{Hom}}(a,c)\).
‣ MonoidalPreComposeMorphismWithGivenObjects( s, a, b, c, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\).
The arguments are an object \(s = \mathrm{\underline{Hom}}(a,b) \otimes \mathrm{\underline{Hom}}(b,c)\), three objects \(a,b,c\), and an object \(r = \mathrm{\underline{Hom}}(a,c)\). The output is the precomposition morphism \(\mathrm{MonoidalPreComposeMorphismWithGivenObjects}_{a,b,c}: \mathrm{\underline{Hom}}(a,b) \otimes \mathrm{\underline{Hom}}(b,c) \rightarrow \mathrm{\underline{Hom}}(a,c)\).
‣ MonoidalPostComposeMorphism( a, b, c ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{Hom}}(b,c) \otimes \mathrm{\underline{Hom}}(a,b), \mathrm{\underline{Hom}}(a,c) )\).
The arguments are three objects \(a,b,c\). The output is the postcomposition morphism \(\mathrm{MonoidalPostComposeMorphism}_{a,b,c}: \mathrm{\underline{Hom}}(b,c) \otimes \mathrm{\underline{Hom}}(a,b) \rightarrow \mathrm{\underline{Hom}}(a,c)\).
‣ MonoidalPostComposeMorphismWithGivenObjects( s, a, b, c, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\).
The arguments are an object \(s = \mathrm{\underline{Hom}}(b,c) \otimes \mathrm{\underline{Hom}}(a,b)\), three objects \(a,b,c\), and an object \(r = \mathrm{\underline{Hom}}(a,c)\). The output is the postcomposition morphism \(\mathrm{MonoidalPostComposeMorphismWithGivenObjects}_{a,b,c}: \mathrm{\underline{Hom}}(b,c) \otimes \mathrm{\underline{Hom}}(a,b) \rightarrow \mathrm{\underline{Hom}}(a,c)\).
‣ DualOnObjects( a ) | ( attribute ) |
Returns: an object
The argument is an object \(a\). The output is its dual object \(a^{\vee}\).
‣ DualOnMorphisms( 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}\).
‣ DualOnMorphismsWithGivenDuals( 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}\).
‣ EvaluationForDual( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( a^{\vee} \otimes a, 1 )\).
The argument is an object \(a\). The output is the evaluation morphism \(\mathrm{ev}_{a}: a^{\vee} \otimes a \rightarrow 1\).
‣ EvaluationForDualWithGivenTensorProduct( s, a, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\).
The arguments are an object \(s = a^{\vee} \otimes a\), an object \(a\), and an object \(r = 1\). The output is the evaluation morphism \(\mathrm{ev}_{a}: a^{\vee} \otimes a \rightarrow 1\).
‣ MorphismToBidual( 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}\).
‣ MorphismToBidualWithGivenBidual( 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}\).
‣ TensorProductInternalHomCompatibilityMorphism( list ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b'), \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b'))\).
The argument is a list of four objects \([ a, a', b, b' ]\). The output is the natural morphism \(\mathrm{TensorProductInternalHomCompatibilityMorphism}_{a,a',b,b'}: \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b') \rightarrow \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b')\).
‣ TensorProductInternalHomCompatibilityMorphismWithGivenObjects( 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{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b')\) and \(r = \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b')\). The output is the natural morphism \(\mathrm{TensorProductInternalHomCompatibilityMorphismWithGivenObjects}_{a,a',b,b'}: \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b') \rightarrow \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b')\).
‣ TensorProductDualityCompatibilityMorphism( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a^{\vee} \otimes b^{\vee}, (a \otimes b)^{\vee} )\).
The arguments are two objects \(a,b\). The output is the natural morphism \(\mathrm{TensorProductDualityCompatibilityMorphism}: a^{\vee} \otimes b^{\vee} \rightarrow (a \otimes b)^{\vee}\).
‣ TensorProductDualityCompatibilityMorphismWithGivenObjects( s, a, b, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\).
The arguments are an object \(s = a^{\vee} \otimes b^{\vee}\), two objects \(a,b\), and an object \(r = (a \otimes b)^{\vee}\). The output is the natural morphism \(\mathrm{TensorProductDualityCompatibilityMorphismWithGivenObjects}_{a,b}: a^{\vee} \otimes b^{\vee} \rightarrow (a \otimes b)^{\vee}\).
‣ MorphismFromTensorProductToInternalHom( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a^{\vee} \otimes b, \mathrm{\underline{Hom}}(a,b) )\).
The arguments are two objects \(a,b\). The output is the natural morphism \(\mathrm{MorphismFromTensorProductToInternalHom}_{a,b}: a^{\vee} \otimes b \rightarrow \mathrm{\underline{Hom}}(a,b)\).
‣ MorphismFromTensorProductToInternalHomWithGivenObjects( s, a, b, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\).
The arguments are an object \(s = a^{\vee} \otimes b\), two objects \(a,b\), and an object \(r = \mathrm{\underline{Hom}}(a,b)\). The output is the natural morphism \(\mathrm{MorphismFromTensorProductToInternalHomWithGivenObjects}_{a,b}: a^{\vee} \otimes b \rightarrow \mathrm{\underline{Hom}}(a,b)\).
‣ IsomorphismFromDualObjectToInternalHomIntoTensorUnit( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(a^{\vee}, \mathrm{\underline{Hom}}(a,1))\).
The argument is an object \(a\). The output is the isomorphism \(\mathrm{IsomorphismFromDualObjectToInternalHomIntoTensorUnit}_{a}: a^{\vee} \rightarrow \mathrm{\underline{Hom}}(a,1)\).
‣ IsomorphismFromInternalHomIntoTensorUnitToDualObject( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(\mathrm{\underline{Hom}}(a,1), a^{\vee})\).
The argument is an object \(a\). The output is the isomorphism \(\mathrm{IsomorphismFromInternalHomIntoTensorUnitToDualObject}_{a}: \mathrm{\underline{Hom}}(a,1) \rightarrow a^{\vee}\).
‣ UniversalPropertyOfDual( 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 \otimes a \rightarrow 1\). The output is the morphism \(t \rightarrow a^{\vee}\) given by the universal property of \(a^{\vee}\).
‣ LambdaIntroduction( alpha ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( 1, \mathrm{\underline{Hom}}(a,b) )\).
The argument is a morphism \(\alpha: a \rightarrow b\). The output is the corresponding morphism \(1 \rightarrow \mathrm{\underline{Hom}}(a,b)\) under the tensor hom adjunction.
‣ LambdaElimination( 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{\underline{Hom}}(a,b)\). The output is a morphism \(a \rightarrow b\) corresponding to \(\alpha\) under the tensor hom adjunction.
‣ IsomorphismFromObjectToInternalHom( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(a, \mathrm{\underline{Hom}}(1,a))\).
The argument is an object \(a\). The output is the natural isomorphism \(a \rightarrow \mathrm{\underline{Hom}}(1,a)\).
‣ IsomorphismFromObjectToInternalHomWithGivenInternalHom( a, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a, r)\).
The argument is an object \(a\), and an object \(r = \mathrm{\underline{Hom}}(1,a)\). The output is the natural isomorphism \(a \rightarrow \mathrm{\underline{Hom}}(1,a)\).
‣ IsomorphismFromInternalHomToObject( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(\mathrm{\underline{Hom}}(1,a),a)\).
The argument is an object \(a\). The output is the natural isomorphism \(\mathrm{\underline{Hom}}(1,a) \rightarrow a\).
‣ IsomorphismFromInternalHomToObjectWithGivenInternalHom( a, s ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(s,a)\).
The argument is an object \(a\), and an object \(s = \mathrm{\underline{Hom}}(1,a)\). The output is the natural isomorphism \(\mathrm{\underline{Hom}}(1,a) \rightarrow a\).
A monoidal category \(\mathbf{C}\) which has for each functor \(- \otimes b: \mathbf{C} \rightarrow \mathbf{C}\) a left adjoint (denoted by \(\mathrm{\underline{coHom}}(-,b)\)) is called a left coclosed monoidal category.
If no operations involving left coduals are installed manually, the left codual objects will be derived as \(a_\vee \coloneqq \mathrm{\underline{coHom}}(1,a)\).
The corresponding GAP property is called IsLeftCoclosedMonoidalCategory.
‣ LeftInternalCoHomOnObjects( a, b ) | ( operation ) |
Returns: an object
The arguments are two objects \(a,b\). The output is the internal cohom object \(\mathrm{\underline{coHom}_\ell}(a,b)\).
‣ LeftInternalCoHomOnMorphisms( alpha, beta ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}_\ell}(a,b'), \mathrm{\underline{coHom}_\ell}(a',b) )\)
The arguments are two morphisms \(\alpha: a \rightarrow a', \beta: b \rightarrow b'\). The output is the internal cohom morphism \(\mathrm{\underline{coHom}_\ell}(\alpha,\beta): \mathrm{\underline{coHom}_\ell}(a,b') \rightarrow \mathrm{\underline{coHom}_\ell}(a',b)\).
‣ LeftInternalCoHomOnMorphismsWithGivenLeftInternalCoHoms( s, alpha, beta, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\)
The arguments are an object \(s = \mathrm{\underline{coHom}_\ell}(a,b')\), two morphisms \(\alpha: a \rightarrow a', \beta: b \rightarrow b'\), and an object \(r = \mathrm{\underline{coHom}_\ell}(a',b)\). The output is the internal cohom morphism \(\mathrm{\underline{coHom}_\ell}(\alpha,\beta): \mathrm{\underline{coHom}_\ell}(a,b') \rightarrow \mathrm{\underline{coHom}_\ell}(a',b)\).
‣ LeftCoclosedMonoidalEvaluationMorphism( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( b, \mathrm{\underline{coHom}_\ell}(b,a) \otimes a )\).
The arguments are two objects \(a, b\). The output is the coclosed evaluation morphism \(\mathrm{coclev}_{a,b}: b \rightarrow \mathrm{\underline{coHom}_\ell}(b,a) \otimes a\), i.e., the unit of the cohom tensor adjunction.
‣ LeftCoclosedMonoidalEvaluationMorphismWithGivenRange( a, b, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( b, r )\).
The arguments are two objects \(a,b\) and an object \(r = \mathrm{\underline{coHom}_\ell}(b,a) \otimes a\). The output is the coclosed evaluation morphism \(\mathrm{coclev}_{a,b}: b \rightarrow \mathrm{\underline{coHom}_\ell}(b,a) \otimes a\), i.e., the unit of the cohom tensor adjunction.
‣ LeftCoclosedMonoidalCoevaluationMorphism( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}_\ell}(b \otimes a, a), b )\).
The arguments are two objects \(a,b\). The output is the coclosed coevaluation morphism \(\mathrm{coclcoev}_{a,b}: \mathrm{\underline{coHom}_\ell}(b \otimes a, a) \rightarrow b\), i.e., the counit of the cohom tensor adjunction.
‣ LeftCoclosedMonoidalCoevaluationMorphismWithGivenSource( a, b, s ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, b )\).
The arguments are two objects \(a,b\) and an object \(s = \mathrm{\underline{coHom}_\ell}(b \otimes a, a)\). The output is the coclosed coevaluation morphism \(\mathrm{coclcoev}_{a,b}: \mathrm{\underline{coHom}_\ell}(b \otimes a, a) \rightarrow b\), i.e., the unit of the cohom tensor adjunction.
‣ TensorProductToLeftInternalCoHomAdjunctMorphism( b, c, g ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}_\ell}(a,c), b )\).
The arguments are two objects \(b,c\) and a morphism \(g: a \rightarrow b \otimes c\). The output is a morphism \(f: \mathrm{\underline{coHom}_\ell}(a,c) \rightarrow b\) corresponding to \(g\) under the cohom tensor adjunction.
‣ TensorProductToLeftInternalCoHomAdjunctMorphismWithGivenLeftInternalCoHom( b, c, g, i ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( i, b )\).
The arguments are two objects \(b,c\), a morphism \(g: a \rightarrow b \otimes c\) and an object \(i = \mathrm{\underline{coHom}_\ell}(a,c)\). The output is a morphism \(f: \mathrm{\underline{coHom}_\ell}(a,c) \rightarrow b\) corresponding to \(g\) under the cohom tensor adjunction.
‣ LeftInternalCoHomToTensorProductAdjunctMorphism( a, c, f ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a, b \otimes c)\).
The arguments are two objects \(a,c\) and a morphism \(f: \mathrm{\underline{coHom}_\ell}(a,c) \rightarrow b\). The output is a morphism \(g: a \rightarrow b \otimes c\) corresponding to \(f\) under the cohom tensor adjunction.
‣ LeftInternalCoHomToTensorProductAdjunctMorphismWithGivenTensorProduct( a, c, f, t ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a, t )\).
The arguments are two objects \(a,c\), a morphism \(f: \mathrm{\underline{coHom}_\ell}(a,c) \rightarrow b\) and an object \(t = b \otimes c\). The output is a morphism \(g: a \rightarrow b \otimes c\) corresponding to \(f\) under the cohom tensor adjunction.
‣ LeftCoclosedMonoidalPreCoComposeMorphism( a, b, c ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}_\ell}(a,c), \mathrm{\underline{coHom}_\ell}(b,c) \otimes \mathrm{\underline{coHom}_\ell}(a,b) )\).
The arguments are three objects \(a,b,c\). The output is the precocomposition morphism \(\mathrm{LeftCoclosedMonoidalPreCoComposeMorphism}_{a,b,c}: \mathrm{\underline{coHom}_\ell}(a,c) \rightarrow \mathrm{\underline{coHom}_\ell}(b,c) \otimes \mathrm{\underline{coHom}_\ell}(a,b)\).
‣ LeftCoclosedMonoidalPreCoComposeMorphismWithGivenObjects( s, a, b, c, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\).
The arguments are an object \(s = \mathrm{\underline{coHom}_\ell}(a,c)\), three objects \(a,b,c\), and an object \(r = \mathrm{\underline{coHom}_\ell}(a,b) \otimes \mathrm{\underline{coHom}_\ell}(b,c)\). The output is the precocomposition morphism \(\mathrm{LeftCoclosedMonoidalPreCoComposeMorphismWithGivenObjects}_{a,b,c}: \mathrm{\underline{coHom}_\ell}(a,c) \rightarrow \mathrm{\underline{coHom}_\ell}(b,c) \otimes \mathrm{\underline{coHom}_\ell}(a,b)\).
‣ LeftCoclosedMonoidalPostCoComposeMorphism( a, b, c ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}_\ell}(a,c), \mathrm{\underline{coHom}_\ell}(a,b) \otimes \mathrm{\underline{coHom}_\ell}(b,c) )\).
The arguments are three objects \(a,b,c\). The output is the postcocomposition morphism \(\mathrm{LeftCoclosedMonoidalPostCoComposeMorphism}_{a,b,c}: \mathrm{\underline{coHom}_\ell}(a,c) \rightarrow \mathrm{\underline{coHom}_\ell}(a,b) \otimes \mathrm{\underline{coHom}_\ell}(b,c)\).
‣ LeftCoclosedMonoidalPostCoComposeMorphismWithGivenObjects( s, a, b, c, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\).
The arguments are an object \(s = \mathrm{\underline{coHom}_\ell}(a,c)\), three objects \(a,b,c\), and an object \(r = \mathrm{\underline{coHom}_\ell}(b,c) \otimes \mathrm{\underline{coHom}_\ell}(a,b)\). The output is the postcocomposition morphism \(\mathrm{LeftCoclosedMonoidalPostCoComposeMorphismWithGivenObjects}_{a,b,c}: \mathrm{\underline{coHom}_\ell}(a,c) \rightarrow \mathrm{\underline{coHom}_\ell}(a,b) \otimes \mathrm{\underline{coHom}_\ell}(b,c)\).
‣ LeftCoDualOnObjects( a ) | ( attribute ) |
Returns: an object
The argument is an object \(a\). The output is its codual object \(a_{\vee}\).
‣ LeftCoDualOnMorphisms( alpha ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( b_{\vee}, a_{\vee} )\).
The argument is a morphism \(\alpha: a \rightarrow b\). The output is its codual morphism \(\alpha_{\vee}: b_{\vee} \rightarrow a_{\vee}\).
‣ LeftCoDualOnMorphismsWithGivenLeftCoDuals( 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}\).
‣ LeftCoclosedMonoidalEvaluationForLeftCoDual( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( 1, a_{\vee} \otimes a )\).
The argument is an object \(a\). The output is the coclosed evaluation morphism \(\mathrm{coclev}_{a}: 1 \rightarrow a_{\vee} \otimes a\).
‣ LeftCoclosedMonoidalEvaluationForLeftCoDualWithGivenTensorProduct( s, a, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\).
The arguments are an object \(s = 1\), an object \(a\), and an object \(r = a_{\vee} \otimes a\). The output is the coclosed evaluation morphism \(\mathrm{coclev}_{a}: 1 \rightarrow a_{\vee} \otimes a\).
‣ MorphismFromLeftCoBidual( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}((a_{\vee})_{\vee}, a)\).
The argument is an object \(a\). The output is the morphism from the cobidual \((a_{\vee})_{\vee} \rightarrow a\).
‣ MorphismFromLeftCoBidualWithGivenLeftCoBidual( a, s ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(s, a)\).
The arguments are an object \(a\), and an object \(s = (a_{\vee})_{\vee}\). The output is the morphism from the cobidual \((a_{\vee})_{\vee} \rightarrow a\).
‣ LeftInternalCoHomTensorProductCompatibilityMorphism( list ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}_\ell}(a \otimes a', b \otimes b'), \mathrm{\underline{coHom}_\ell}(a,b) \otimes \mathrm{\underline{coHom}_\ell}(a',b'))\).
The argument is a list of four objects \([ a, a', b, b' ]\). The output is the natural morphism \(\mathrm{LeftInternalCoHomTensorProductCompatibilityMorphism}_{a,a',b,b'}: \mathrm{\underline{coHom}_\ell}(a \otimes a', b \otimes b') \rightarrow \mathrm{\underline{coHom}_\ell}(a,b) \otimes \mathrm{\underline{coHom}_\ell}(a',b')\).
‣ LeftInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects( 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{\underline{coHom}_\ell}(a \otimes a', b \otimes b')\) and \(r = \mathrm{\underline{coHom}_\ell}(a,b) \otimes \mathrm{\underline{coHom}_\ell}(a',b')\). The output is the natural morphism \(\mathrm{LeftInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects}_{a,a',b,b'}: \mathrm{\underline{coHom}_\ell}(a \otimes a', b \otimes b') \rightarrow \mathrm{\underline{coHom}_\ell}(a,b) \otimes \mathrm{\underline{coHom}_\ell}(a',b')\).
‣ LeftCoDualityTensorProductCompatibilityMorphism( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( (a \otimes b)_{\vee}, a_{\vee} \otimes b_{\vee} )\).
The arguments are two objects \(a,b\). The output is the natural morphism \(\mathrm{LeftCoDualityTensorProductCompatibilityMorphism}: (a \otimes b)_{\vee} \rightarrow a_{\vee} \otimes b_{\vee}\).
‣ LeftCoDualityTensorProductCompatibilityMorphismWithGivenObjects( s, a, b, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\).
The arguments are an object \(s = (a \otimes b)_{\vee}\), two objects \(a,b\), and an object \(r = a_{\vee} \otimes b_{\vee}\). The output is the natural morphism \(\mathrm{LeftCoDualityTensorProductCompatibilityMorphismWithGivenObjects}_{a,b}: (a \otimes b)_{\vee} \rightarrow a_{\vee} \otimes b_{\vee}\).
‣ MorphismFromLeftInternalCoHomToTensorProduct( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}_\ell}(a,b), b_{\vee} \otimes a )\).
The arguments are two objects \(a,b\). The output is the natural morphism \(\mathrm{MorphismFromLeftInternalCoHomToTensorProduct}_{a,b}: \mathrm{\underline{coHom}_\ell}(a,b) \rightarrow b_{\vee} \otimes a\).
‣ MorphismFromLeftInternalCoHomToTensorProductWithGivenObjects( s, a, b, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\).
The arguments are an object \(s = \mathrm{\underline{coHom}_\ell}(a,b)\), two objects \(a,b\), and an object \(r = b_{\vee} \otimes a\). The output is the natural morphism \(\mathrm{MorphismFromLeftInternalCoHomToTensorProductWithGivenObjects}_{a,b}: \mathrm{\underline{coHom}_\ell}(a,b) \rightarrow a \otimes b_{\vee}\).
‣ IsomorphismFromLeftCoDualObjectToLeftInternalCoHomFromTensorUnit( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(a_{\vee}, \mathrm{\underline{coHom}_\ell}(1,a))\).
The argument is an object \(a\). The output is the isomorphism \(\mathrm{IsomorphismFromLeftCoDualObjectToLeftInternalCoHomFromTensorUnit}_{a}: a_{\vee} \rightarrow \mathrm{\underline{coHom}_\ell}(1,a)\).
‣ IsomorphismFromLeftInternalCoHomFromTensorUnitToLeftCoDualObject( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(\mathrm{\underline{coHom}_\ell}(1,a), a_{\vee})\).
The argument is an object \(a\). The output is the isomorphism \(\mathrm{IsomorphismFromLeftInternalCoHomFromTensorUnitToLeftCoDualObject}_{a}: \mathrm{\underline{coHom}_\ell}(1,a) \rightarrow a_{\vee}\).
‣ UniversalPropertyOfLeftCoDual( t, a, alpha ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a_{\vee}, t)\).
The arguments are two objects \(t,a\), and a morphism \(\alpha: 1 \rightarrow t \otimes a\). The output is the morphism \(a_{\vee} \rightarrow t\) given by the universal property of \(a_{\vee}\).
‣ LeftCoclosedMonoidalLambdaIntroduction( alpha ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}_\ell}(a,b), 1 )\).
The argument is a morphism \(\alpha: a \rightarrow b\). The output is the corresponding morphism \( \mathrm{\underline{coHom}_\ell}(a,b) \rightarrow 1\) under the cohom tensor adjunction.
‣ LeftCoclosedMonoidalLambdaElimination( a, b, alpha ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a,b)\).
The arguments are two objects \(a,b\), and a morphism \(\alpha: \mathrm{\underline{coHom}_\ell}(a,b) \rightarrow 1\). The output is a morphism \(a \rightarrow b\) corresponding to \(\alpha\) under the cohom tensor adjunction.
‣ IsomorphismFromObjectToLeftInternalCoHom( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(a, \mathrm{\underline{coHom}_\ell}(a,1))\).
The argument is an object \(a\). The output is the natural isomorphism \(a \rightarrow \mathrm{\underline{coHom}_\ell}(a,1)\).
‣ IsomorphismFromObjectToLeftInternalCoHomWithGivenLeftInternalCoHom( a, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a, r)\).
The argument is an object \(a\), and an object \(r = \mathrm{\underline{coHom}_\ell}(a,1)\). The output is the natural isomorphism \(a \rightarrow \mathrm{\underline{coHom}_\ell}(a,1)\).
‣ IsomorphismFromLeftInternalCoHomToObject( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(\mathrm{\underline{coHom}_\ell}(a,1), a)\).
The argument is an object \(a\). The output is the natural isomorphism \(\mathrm{\underline{coHom}_\ell}(a,1) \rightarrow a\).
‣ IsomorphismFromLeftInternalCoHomToObjectWithGivenLeftInternalCoHom( a, s ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(s, a)\).
The argument is an object \(a\), and an object \(s = \mathrm{\underline{coHom}_\ell}(a,1)\). The output is the natural isomorphism \(\mathrm{\underline{coHom}_\ell}(a,1) \rightarrow a\).
A monoidal category \(\mathbf{C}\) which has for each functor \(- \otimes b: \mathbf{C} \rightarrow \mathbf{C}\) a left adjoint (denoted by \(\mathrm{\underline{coHom}}(-,b)\)) is called a coclosed monoidal category.
If no operations involving coduals are installed manually, the codual objects will be derived as \(a_\vee \coloneqq \mathrm{\underline{coHom}}(1,a)\).
The corresponding GAP property is called IsCoclosedMonoidalCategory.
‣ InternalCoHomOnObjects( a, b ) | ( operation ) |
Returns: an object
The arguments are two objects \(a,b\). The output is the internal cohom object \(\mathrm{\underline{coHom}}(a,b)\).
‣ InternalCoHomOnMorphisms( alpha, beta ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}}(a,b'), \mathrm{\underline{coHom}}(a',b) )\)
The arguments are two morphisms \(\alpha: a \rightarrow a', \beta: b \rightarrow b'\). The output is the internal cohom morphism \(\mathrm{\underline{coHom}}(\alpha,\beta): \mathrm{\underline{coHom}}(a,b') \rightarrow \mathrm{\underline{coHom}}(a',b)\).
‣ InternalCoHomOnMorphismsWithGivenInternalCoHoms( s, alpha, beta, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\)
The arguments are an object \(s = \mathrm{\underline{coHom}}(a,b')\), two morphisms \(\alpha: a \rightarrow a', \beta: b \rightarrow b'\), and an object \(r = \mathrm{\underline{coHom}}(a',b)\). The output is the internal cohom morphism \(\mathrm{\underline{coHom}}(\alpha,\beta): \mathrm{\underline{coHom}}(a,b') \rightarrow \mathrm{\underline{coHom}}(a',b)\).
‣ CoclosedMonoidalRightEvaluationMorphism( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( b, a \otimes \mathrm{\underline{coHom}}(b,a) )\).
The arguments are two objects \(a, b\). The output is the coclosed right evaluation morphism \(\mathrm{coclev}_{a,b}: b \rightarrow a \otimes \mathrm{\underline{coHom}}(b,a)\), i.e., the unit of the cohom tensor adjunction.
‣ CoclosedMonoidalRightEvaluationMorphismWithGivenRange( a, b, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( b, r )\).
The arguments are two objects \(a,b\) and an object \(r = a \otimes \mathrm{\underline{coHom}}(b,a)\). The output is the coclosed right evaluation morphism \(\mathrm{coclev}_{a,b}: b \rightarrow a \otimes \mathrm{\underline{coHom}}(b,a)\), i.e., the unit of the cohom tensor adjunction.
‣ CoclosedMonoidalRightCoevaluationMorphism( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}}(a \otimes b, a), b )\).
The arguments are two objects \(a,b\). The output is the coclosed right coevaluation morphism \(\mathrm{coclcoev}_{a,b}: \mathrm{\underline{coHom}}(a \otimes b, a) \rightarrow b\), i.e., the counit of the cohom tensor adjunction.
‣ CoclosedMonoidalRightCoevaluationMorphismWithGivenSource( a, b, s ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, b )\).
The arguments are two objects \(a,b\) and an object \(s = \mathrm{\underline{coHom}}(a \otimes b, a)\). The output is the coclosed right coevaluation morphism \(\mathrm{coclcoev}_{a,b}: \mathrm{\underline{coHom}}(a \otimes b, a) \rightarrow b\), i.e., the unit of the cohom tensor adjunction.
‣ TensorProductToInternalCoHomRightAdjunctMorphism( b, c, g ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}}(a,b), c )\).
The arguments are two objects \(b,c\) and a morphism \(g: a \rightarrow b \otimes c\). The output is a morphism \(f: \mathrm{\underline{coHom}}(a,b) \rightarrow c\) corresponding to \(g\) under the cohom tensor adjunction.
‣ TensorProductToInternalCoHomRightAdjunctMorphismWithGivenInternalCoHom( b, c, g, i ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( i, c )\).
The arguments are two objects \(b,c\), a morphism \(g: a \rightarrow b \otimes c\) and an object \(i = \mathrm{\underline{coHom}}(a,b)\). The output is a morphism \(f: \mathrm{\underline{coHom}}(a,b) \rightarrow c\) corresponding to \(g\) under the cohom tensor adjunction.
‣ InternalCoHomToTensorProductRightAdjunctMorphism( a, b, f ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a, b \otimes c)\).
The arguments are two objects \(a,b\) and a morphism \(f: \mathrm{\underline{coHom}}(a,b) \rightarrow c\). The output is a morphism \(g: a \rightarrow b \otimes c\) corresponding to \(f\) under the cohom tensor adjunction.
‣ InternalCoHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct( a, b, f, t ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a, t )\).
The arguments are two objects \(a,b\), a morphism \(f: \mathrm{\underline{coHom}}(a,b) \rightarrow c\) and an object \(t = b \otimes c\). The output is a morphism \(g: a \rightarrow t\) corresponding to \(f\) under the cohom tensor adjunction.
‣ CoclosedMonoidalLeftEvaluationMorphism( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( b, \mathrm{\underline{coHom}}(b,a) \otimes a )\).
The arguments are two objects \(a, b\). The output is the coclosed left evaluation morphism \(\mathrm{coclev}_{a,b}: b \rightarrow \mathrm{\underline{coHom}}(b,a) \otimes a\), i.e., the unit of the cohom tensor adjunction.
‣ CoclosedMonoidalLeftEvaluationMorphismWithGivenRange( a, b, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( b, r )\).
The arguments are two objects \(a,b\) and an object \(r = \mathrm{\underline{coHom}}(b,a) \otimes a\). The output is the coclosed left evaluation morphism \(\mathrm{coclev}_{a,b}: b \rightarrow \mathrm{\underline{coHom}}(b,a) \otimes a\), i.e., the unit of the cohom tensor adjunction.
‣ CoclosedMonoidalLeftCoevaluationMorphism( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}}(b \otimes a, a), b )\).
The arguments are two objects \(a,b\). The output is the coclosed left coevaluation morphism \(\mathrm{coclcoev}_{a,b}: \mathrm{\underline{coHom}}(b \otimes a, a) \rightarrow b\), i.e., the counit of the cohom tensor adjunction.
‣ CoclosedMonoidalLeftCoevaluationMorphismWithGivenSource( a, b, s ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, b )\).
The arguments are two objects \(a,b\) and an object \(s = \mathrm{\underline{coHom}}(b \otimes a, a)\). The output is the coclosed left coevaluation morphism \(\mathrm{coclcoev}_{a,b}: \mathrm{\underline{coHom}}(b \otimes a, a) \rightarrow b\), i.e., the unit of the cohom tensor adjunction.
‣ TensorProductToInternalCoHomLeftAdjunctMorphism( b, c, g ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}}(a,c), b )\).
The arguments are two objects \(b,c\) and a morphism \(g: a \rightarrow b \otimes c\). The output is a morphism \(f: \mathrm{\underline{coHom}}(a,c) \rightarrow b\) corresponding to \(g\) under the cohom tensor adjunction.
‣ TensorProductToInternalCoHomLeftAdjunctMorphismWithGivenInternalCoHom( b, c, g, i ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( i, b )\).
The arguments are two objects \(b,c\), a morphism \(g: a \rightarrow b \otimes c\) and an object \(i = \mathrm{\underline{coHom}}(a,c)\). The output is a morphism \(f: \mathrm{\underline{coHom}}(a,c) \rightarrow b\) corresponding to \(g\) under the cohom tensor adjunction.
‣ InternalCoHomToTensorProductLeftAdjunctMorphism( a, c, f ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a, b \otimes c)\).
The arguments are two objects \(a,c\) and a morphism \(f: \mathrm{\underline{coHom}}(a,c) \rightarrow b\). The output is a morphism \(g: a \rightarrow b \otimes c\) corresponding to \(f\) under the cohom tensor adjunction.
‣ InternalCoHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct( a, c, f, t ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a, t )\).
The arguments are two objects \(a,c\), a morphism \(f: \mathrm{\underline{coHom}}(a,c) \rightarrow b\) and an object \(t = b \otimes c\). The output is a morphism \(g: a \rightarrow t\) corresponding to \(f\) under the cohom tensor adjunction.
‣ MonoidalPreCoComposeMorphism( a, b, c ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}}(a,c), \mathrm{\underline{coHom}}(b,c) \otimes \mathrm{\underline{coHom}}(a,b) )\).
The arguments are three objects \(a,b,c\). The output is the precocomposition morphism \(\mathrm{MonoidalPreCoComposeMorphism}_{a,b,c}: \mathrm{\underline{coHom}}(a,c) \rightarrow \mathrm{\underline{coHom}}(b,c) \otimes \mathrm{\underline{coHom}}(a,b)\).
‣ MonoidalPreCoComposeMorphismWithGivenObjects( s, a, b, c, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\).
The arguments are an object \(s = \mathrm{\underline{coHom}}(a,c)\), three objects \(a,b,c\), and an object \(r = \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(b,c)\). The output is the precocomposition morphism \(\mathrm{MonoidalPreCoComposeMorphismWithGivenObjects}_{a,b,c}: \mathrm{\underline{coHom}}(a,c) \rightarrow \mathrm{\underline{coHom}}(b,c) \otimes \mathrm{\underline{coHom}}(a,b)\).
‣ MonoidalPostCoComposeMorphism( a, b, c ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}}(a,c), \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(b,c) )\).
The arguments are three objects \(a,b,c\). The output is the postcocomposition morphism \(\mathrm{MonoidalPostCoComposeMorphism}_{a,b,c}: \mathrm{\underline{coHom}}(a,c) \rightarrow \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(b,c)\).
‣ MonoidalPostCoComposeMorphismWithGivenObjects( s, a, b, c, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\).
The arguments are an object \(s = \mathrm{\underline{coHom}}(a,c)\), three objects \(a,b,c\), and an object \(r = \mathrm{\underline{coHom}}(b,c) \otimes \mathrm{\underline{coHom}}(a,b)\). The output is the postcocomposition morphism \(\mathrm{MonoidalPostCoComposeMorphismWithGivenObjects}_{a,b,c}: \mathrm{\underline{coHom}}(a,c) \rightarrow \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(b,c)\).
‣ CoDualOnObjects( a ) | ( attribute ) |
Returns: an object
The argument is an object \(a\). The output is its codual object \(a_{\vee}\).
‣ CoDualOnMorphisms( alpha ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( b_{\vee}, a_{\vee} )\).
The argument is a morphism \(\alpha: a \rightarrow b\). The output is its codual morphism \(\alpha_{\vee}: b_{\vee} \rightarrow a_{\vee}\).
‣ CoDualOnMorphismsWithGivenCoDuals( 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}\).
‣ CoclosedEvaluationForCoDual( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( 1, a_{\vee} \otimes a )\).
The argument is an object \(a\). The output is the coclosed evaluation morphism \(\mathrm{coclev}_{a}: 1 \rightarrow a_{\vee} \otimes a\).
‣ CoclosedEvaluationForCoDualWithGivenTensorProduct( s, a, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\).
The arguments are an object \(s = 1\), an object \(a\), and an object \(r = a_{\vee} \otimes a\). The output is the coclosed evaluation morphism \(\mathrm{coclev}_{a}: 1 \rightarrow a_{\vee} \otimes a\).
‣ MorphismFromCoBidual( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}((a_{\vee})_{\vee}, a)\).
The argument is an object \(a\). The output is the morphism from the cobidual \((a_{\vee})_{\vee} \rightarrow a\).
‣ MorphismFromCoBidualWithGivenCoBidual( a, s ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(s, a)\).
The arguments are an object \(a\), and an object \(s = (a_{\vee})_{\vee}\). The output is the morphism from the cobidual \((a_{\vee})_{\vee} \rightarrow a\).
‣ InternalCoHomTensorProductCompatibilityMorphism( list ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}}(a \otimes a', b \otimes b'), \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(a',b'))\).
The argument is a list of four objects \([ a, a', b, b' ]\). The output is the natural morphism \(\mathrm{InternalCoHomTensorProductCompatibilityMorphism}_{a,a',b,b'}: \mathrm{\underline{coHom}}(a \otimes a', b \otimes b') \rightarrow \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(a',b')\).
‣ InternalCoHomTensorProductCompatibilityMorphismWithGivenObjects( 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{\underline{coHom}}(a \otimes a', b \otimes b')\) and \(r = \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(a',b')\). The output is the natural morphism \(\mathrm{InternalCoHomTensorProductCompatibilityMorphismWithGivenObjects}_{a,a',b,b'}: \mathrm{\underline{coHom}}(a \otimes a', b \otimes b') \rightarrow \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(a',b')\).
‣ CoDualityTensorProductCompatibilityMorphism( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( (a \otimes b)_{\vee}, a_{\vee} \otimes b_{\vee} )\).
The arguments are two objects \(a,b\). The output is the natural morphism \(\mathrm{CoDualityTensorProductCompatibilityMorphism}: (a \otimes b)_{\vee} \rightarrow a_{\vee} \otimes b_{\vee}\).
‣ CoDualityTensorProductCompatibilityMorphismWithGivenObjects( s, a, b, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\).
The arguments are an object \(s = (a \otimes b)_{\vee}\), two objects \(a,b\), and an object \(r = a_{\vee} \otimes b_{\vee}\). The output is the natural morphism \(\mathrm{CoDualityTensorProductCompatibilityMorphismWithGivenObjects}_{a,b}: (a \otimes b)_{\vee} \rightarrow a_{\vee} \otimes b_{\vee}\).
‣ MorphismFromInternalCoHomToTensorProduct( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}}(a,b), b_{\vee} \otimes a )\).
The arguments are two objects \(a,b\). The output is the natural morphism \(\mathrm{MorphismFromInternalCoHomToTensorProduct}_{a,b}: \mathrm{\underline{coHom}}(a,b) \rightarrow b_{\vee} \otimes a\).
‣ MorphismFromInternalCoHomToTensorProductWithGivenObjects( s, a, b, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( s, r )\).
The arguments are an object \(s = \mathrm{\underline{coHom}}(a,b)\), two objects \(a,b\), and an object \(r = b_{\vee} \otimes a\). The output is the natural morphism \(\mathrm{MorphismFromInternalCoHomToTensorProductWithGivenObjects}_{a,b}: \mathrm{\underline{coHom}}(a,b) \rightarrow a \otimes b_{\vee}\).
‣ IsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(a_{\vee}, \mathrm{\underline{coHom}}(1,a))\).
The argument is an object \(a\). The output is the isomorphism \(\mathrm{IsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit}_{a}: a_{\vee} \rightarrow \mathrm{\underline{coHom}}(1,a)\).
‣ IsomorphismFromInternalCoHomFromTensorUnitToCoDualObject( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(\mathrm{\underline{coHom}}(1,a), a_{\vee})\).
The argument is an object \(a\). The output is the isomorphism \(\mathrm{IsomorphismFromInternalCoHomFromTensorUnitToCoDualObject}_{a}: \mathrm{\underline{coHom}}(1,a) \rightarrow a_{\vee}\).
‣ UniversalPropertyOfCoDual( t, a, alpha ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a_{\vee}, t)\).
The arguments are two objects \(t,a\), and a morphism \(\alpha: 1 \rightarrow t \otimes a\). The output is the morphism \(a_{\vee} \rightarrow t\) given by the universal property of \(a_{\vee}\).
‣ CoLambdaIntroduction( alpha ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}}(a,b), 1 )\).
The argument is a morphism \(\alpha: a \rightarrow b\). The output is the corresponding morphism \( \mathrm{\underline{coHom}}(a,b) \rightarrow 1\) under the cohom tensor adjunction.
‣ CoLambdaElimination( a, b, alpha ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a,b)\).
The arguments are two objects \(a,b\), and a morphism \(\alpha: \mathrm{\underline{coHom}}(a,b) \rightarrow 1\). The output is a morphism \(a \rightarrow b\) corresponding to \(\alpha\) under the cohom tensor adjunction.
‣ IsomorphismFromObjectToInternalCoHom( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(a, \mathrm{\underline{coHom}}(a,1))\).
The argument is an object \(a\). The output is the natural isomorphism \(a \rightarrow \mathrm{\underline{coHom}}(a,1)\).
‣ IsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom( a, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a, r)\).
The argument is an object \(a\), and an object \(r = \mathrm{\underline{coHom}}(a,1)\). The output is the natural isomorphism \(a \rightarrow \mathrm{\underline{coHom}}(a,1)\).
‣ IsomorphismFromInternalCoHomToObject( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(\mathrm{\underline{coHom}}(a,1), a)\).
The argument is an object \(a\). The output is the natural isomorphism \(\mathrm{\underline{coHom}}(a,1) \rightarrow a\).
‣ IsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom( a, s ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(s, a)\).
The argument is an object \(a\), and an object \(s = \mathrm{\underline{coHom}}(a,1)\). The output is the natural isomorphism \(\mathrm{\underline{coHom}}(a,1) \rightarrow a\).
A monoidal category \(\mathbf{C}\) which is symmetric and closed is called a symmetric closed monoidal category.
The corresponding GAP property is given by IsSymmetricClosedMonoidalCategory.
A monoidal category \(\mathbf{C}\) which is symmetric and coclosed is called a symmetric coclosed monoidal category.
The corresponding GAP property is given by IsSymmetricCoclosedMonoidalCategory.
A symmetric closed monoidal category \(\mathbf{C}\) satisfying
the natural morphism
\(\mathrm{\underline{Hom}_\ell}(a, a') \otimes \mathrm{\underline{Hom}_\ell}(b, b') \rightarrow \mathrm{\underline{Hom}_\ell}(a \otimes b, a' \otimes b')\) is an isomorphism,
the natural morphism
\(a \rightarrow \mathrm{\underline{Hom}_\ell}(\mathrm{\underline{Hom}_\ell}(a, 1), 1)\) is an isomorphism is called a rigid symmetric closed monoidal category.
If no operations involving the closed structure are installed manually, the internal hom objects will be derived as \(\mathrm{\underline{Hom}_\ell}(a,b) \coloneqq a^\vee \otimes b\) and, in particular, \(\mathrm{\underline{Hom}_\ell}(a,1) \coloneqq a^\vee \otimes 1\).
The corresponding GAP property is given by IsRigidSymmetricClosedMonoidalCategory.
‣ IsomorphismFromTensorProductWithDualObjectToInternalHom( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a^{\vee} \otimes b, \mathrm{\underline{Hom}}(a,b) )\).
The arguments are two objects \(a,b\). The output is the natural morphism \(\mathrm{IsomorphismFromTensorProductWithDualObjectToInternalHom}_{a,b}: a^{\vee} \otimes b \rightarrow \mathrm{\underline{Hom}}(a,b)\).
‣ IsomorphismFromInternalHomToTensorProductWithDualObject( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{Hom}}(a,b), a^{\vee} \otimes b )\).
The arguments are two objects \(a,b\). The output is the inverse of \(\mathrm{IsomorphismFromTensorProductWithDualObjectToInternalHom}\), namely \(\mathrm{IsomorphismFromInternalHomToTensorProductWithDualObject}_{a,b}: \mathrm{\underline{Hom}}(a,b) \rightarrow a^{\vee} \otimes b\).
‣ MorphismFromInternalHomToTensorProduct( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{Hom}}(a,b), a^{\vee} \otimes b )\).
The arguments are two objects \(a,b\). The output is the inverse of \(\mathrm{MorphismFromTensorProductToInternalHomWithGivenObjects}\), namely \(\mathrm{MorphismFromInternalHomToTensorProductWithGivenObjects}_{a,b}: \mathrm{\underline{Hom}}(a,b) \rightarrow a^{\vee} \otimes b\).
‣ MorphismFromInternalHomToTensorProductWithGivenObjects( s, a, b, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{Hom}}(a,b), a^{\vee} \otimes b )\).
The arguments are an object \(s = \mathrm{\underline{Hom}}(a,b)\), two objects \(a,b\), and an object \(r = a^{\vee} \otimes b\). The output is the inverse of \(\mathrm{MorphismFromTensorProductToInternalHomWithGivenObjects}\), namely \(\mathrm{MorphismFromInternalHomToTensorProductWithGivenObjects}_{a,b}: \mathrm{\underline{Hom}}(a,b) \rightarrow a^{\vee} \otimes b\).
‣ TensorProductInternalHomCompatibilityMorphismInverse( list ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b'), \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b') )\).
The argument is a list of four objects \([ a, a', b, b' ]\). The output is the natural morphism \(\mathrm{TensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects}_{a,a',b,b'}: \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b') \rightarrow \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b')\).
‣ TensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects( s, list, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b'), \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b') )\).
The arguments are a list of four objects \([ a, a', b, b' ]\), and two objects \(s = \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b')\) and \(r = \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b')\). The output is the natural morphism \(\mathrm{TensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects}_{a,a',b,b'}: \mathrm{\underline{Hom}}(a \otimes b,a' \otimes b') \rightarrow \mathrm{\underline{Hom}}(a,a') \otimes \mathrm{\underline{Hom}}(b,b')\).
‣ CoevaluationForDual( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(1,a \otimes a^{\vee})\).
The argument is an object \(a\). The output is the coevaluation morphism \(\mathrm{coev}_{a}:1 \rightarrow a \otimes a^{\vee}\).
‣ CoevaluationForDualWithGivenTensorProduct( s, a, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(1,a \otimes a^{\vee})\).
The arguments are an object \(s = 1\), an object \(a\), and an object \(r = a \otimes a^{\vee}\). The output is the coevaluation morphism \(\mathrm{coev}_{a}:1 \rightarrow a \otimes a^{\vee}\).
‣ TraceMap( alpha ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(1,1)\).
The argument is an endomorphism \(\alpha: a \rightarrow a\). The output is the trace morphism \(\mathrm{trace}_{\alpha}: 1 \rightarrow 1\).
‣ RankMorphism( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(1,1)\).
The argument is an object \(a\). The output is the rank morphism \(\mathrm{rank}_a: 1 \rightarrow 1\).
‣ MorphismFromBidual( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}((a^{\vee})^{\vee},a)\).
The argument is an object \(a\). The output is the inverse of the morphism to the bidual \((a^{\vee})^{\vee} \rightarrow a\).
‣ MorphismFromBidualWithGivenBidual( a, s ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}((a^{\vee})^{\vee},a)\).
The argument is an object \(a\), and an object \(s = (a^{\vee})^{\vee}\). The output is the inverse of the morphism to the bidual \((a^{\vee})^{\vee} \rightarrow a\).
A symmetric coclosed monoidal category \(\mathbf{C}\) satisfying
the natural morphism
\(\mathrm{\underline{coHom}}(a \otimes a', b \otimes b') \rightarrow \mathrm{\underline{coHom}}(a, b) \otimes \mathrm{\underline{coHom}}(a', b')\) is an isomorphism,
the natural morphism
\(\mathrm{\underline{coHom}}(1, \mathrm{\underline{coHom}}(1, a)) \rightarrow a\) is an isomorphism is called a rigid symmetric coclosed monoidal category.
If no operations involving the coclosed structure are installed manually, the internal cohom objects will be derived as \(\mathrm{\underline{coHom}}(a,b) \coloneqq a \otimes b_\vee\) and, in particular, \(\mathrm{\underline{coHom}}(1,a) \coloneqq 1 \otimes a_\vee\).
The corresponding GAP property is given by IsRigidSymmetricCoclosedMonoidalCategory.
‣ IsomorphismFromInternalCoHomToTensorProductWithCoDualObject( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}}(a,b), b_{\vee} \otimes a )\).
The arguments are two objects \(a,b\). The output is the natural morphism \(\mathrm{IsomorphismFromInternalCoHomToTensorProductWithCoDualObjectWithGivenObjects}_{a,b}: \mathrm{\underline{coHom}}(a,b) \rightarrow b_{\vee} \otimes a\).
‣ IsomorphismFromTensorProductWithCoDualObjectToInternalCoHom( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a_{\vee} \otimes b, \mathrm{\underline{coHom}}(b,a)\).
The arguments are two objects \(a,b\). The output is the inverse of \(\mathrm{IsomorphismFromInternalCoHomToTensorProductWithCoDualObject}\), namely \(\mathrm{IsomorphismFromTensorProductWithCoDualObjectToInternalCoHom}_{a,b}: a_{\vee} \otimes b \rightarrow \mathrm{\underline{coHom}}(b,a)\).
‣ MorphismFromTensorProductToInternalCoHom( a, b ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a_{\vee} \otimes b, \mathrm{\underline{coHom}}(b,a) )\).
The arguments are two objects \(a,b\). The output is the inverse of \(\mathrm{MorphismFromInternalCoHomToTensorProductWithGivenObjects}\), namely \(\mathrm{MorphismFromTensorProductToInternalCoHomWithGivenObjects}_{a,b}: a_{\vee} \otimes b \rightarrow \mathrm{\underline{coHom}}(b,a)\).
‣ MorphismFromTensorProductToInternalCoHomWithGivenObjects( s, a, b, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a_{\vee} \otimes b, \mathrm{\underline{coHom}}(b,a)\).
The arguments are an object \(s_{\vee} = a \otimes b\), two objects \(a,b\), and an object \(r = \mathrm{\underline{coHom}}(b,a)\). The output is the inverse of \(\mathrm{MorphismFromInternalCoHomToTensorProductWithGivenObjects}\), namely \(\mathrm{MorphismFromTensorProductToInternalCoHomWithGivenObjects}_{a,b}: a_{\vee} \otimes b \rightarrow \mathrm{\underline{coHom}}(b,a)\).
‣ InternalCoHomTensorProductCompatibilityMorphismInverse( list ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(a',b'), \mathrm{\underline{coHom}}(a \otimes a', b \otimes b' )\).
The argument is a list of four objects \([ a, a', b, b' ]\). The output is the natural morphism \(\mathrm{InternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects}_{a,a',b,b'}: \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(a',b') \rightarrow \mathrm{\underline{coHom}}(a \otimes a', b \otimes b')\).
‣ InternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects( s, list, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(a',b'), \mathrm{\underline{coHom}}(a \otimes a', b \otimes b' )\).
The arguments are a list of four objects \([ a, a', b, b' ]\), and two objects \(s = \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(a',b')\) and \(r = \mathrm{\underline{coHom}}(a \otimes a', b \otimes b')\). The output is the natural morphism \(\mathrm{InternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects}_{a,a',b,b'}: \mathrm{\underline{coHom}}(a,b) \otimes \mathrm{\underline{coHom}}(a',b') \rightarrow \mathrm{\underline{coHom}}(a \otimes a', b \otimes b')\).
‣ CoclosedCoevaluationForCoDual( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(a \otimes a_{\vee}, 1)\).
The argument is an object \(a\). The output is the coclosed coevaluation morphism \(\mathrm{coclcoev}_{a}: a \otimes a_{\vee} \rightarrow 1\).
‣ CoclosedCoevaluationForCoDualWithGivenTensorProduct( s, a, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a \otimes a_{\vee}, 1)\).
The arguments are an object \(s = a \otimes a_{\vee}\), an object \(a\), and an object \(r = 1\). The output is the coclosed coevaluation morphism \(\mathrm{coclcoev}_{a}: a \otimes a_{\vee} \rightarrow 1\).
‣ CoTraceMap( alpha ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(1,1)\).
The argument is an endomorphism \(\alpha: a \rightarrow a\). The output is the cotrace morphism \(\mathrm{cotrace}_{\alpha}: 1 \rightarrow 1\).
‣ CoRankMorphism( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(1,1)\).
The argument is an object \(a\). The output is the corank morphism \(\mathrm{corank}_a: 1 \rightarrow 1\).
‣ MorphismToCoBidual( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(a, (a_{\vee})_{\vee})\).
The argument is an object \(a\). The output is the inverse of the morphism from the cobidual \(a \rightarrow (a_{\vee})_{\vee}\).
‣ MorphismToCoBidualWithGivenCoBidual( a, r ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a,(a_{\vee})_{\vee})\).
The argument is an object \(a\), and an object \(r = (a_{\vee})_{\vee}\). The output is the inverse of the morphism from the cobidual \(a \rightarrow (a_{\vee})_{\vee}\).
‣ InternalHom( a, b ) | ( operation ) |
Returns: a cell
This is a convenience method. The arguments are two cells \(a,b\). The output is the internal hom cell. If \(a,b\) are two CAP objects the output is the internal Hom object \(\mathrm{\underline{Hom}}(a,b)\). If at least one of the arguments is a CAP morphism the output is a CAP morphism, namely the internal hom on morphisms, where any object is replaced by its identity morphism.
‣ InternalCoHom( a, b ) | ( operation ) |
Returns: a cell
This is a convenience method. The arguments are two cells \(a,b\). The output is the internal cohom cell. If \(a,b\) are two CAP objects the output is the internal cohom object \(\mathrm{\underline{coHom}}(a,b)\). If at least one of the arguments is a CAP morphism the output is a CAP morphism, namely the internal cohom on morphisms, where any object is replaced by its identity morphism.
‣ LeftInternalHom( a, b ) | ( operation ) |
Returns: a cell
This is a convenience method. The arguments are two cells \(a,b\). The output is the internal hom cell. If \(a,b\) are two CAP objects the output is the internal Hom object \(\mathrm{\underline{Hom}_\ell}(a,b)\). If at least one of the arguments is a CAP morphism the output is a CAP morphism, namely the internal hom on morphisms, where any object is replaced by its identity morphism.
‣ LeftInternalCoHom( a, b ) | ( operation ) |
Returns: a cell
This is a convenience method. The arguments are two cells \(a,b\). The output is the internal cohom cell. If \(a,b\) are two CAP objects the output is the internal cohom object \(\mathrm{\underline{coHom}_\ell}(a,b)\). If at least one of the arguments is a CAP morphism the output is a CAP morphism, namely the internal cohom on morphisms, where any object is replaced by its identity morphism.
‣ AddLeftDistributivityExpanding( C, F ) | ( operation ) |
‣ AddLeftDistributivityExpanding( 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 LeftDistributivityExpanding. 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{LeftDistributivityExpanding}(a, L)\).
‣ AddLeftDistributivityExpandingWithGivenObjects( C, F ) | ( operation ) |
‣ AddLeftDistributivityExpandingWithGivenObjects( 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 LeftDistributivityExpandingWithGivenObjects. 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{LeftDistributivityExpandingWithGivenObjects}(s, a, L, r)\).
‣ AddLeftDistributivityFactoring( C, F ) | ( operation ) |
‣ AddLeftDistributivityFactoring( 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 LeftDistributivityFactoring. 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{LeftDistributivityFactoring}(a, L)\).
‣ AddLeftDistributivityFactoringWithGivenObjects( C, F ) | ( operation ) |
‣ AddLeftDistributivityFactoringWithGivenObjects( 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 LeftDistributivityFactoringWithGivenObjects. 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{LeftDistributivityFactoringWithGivenObjects}(s, a, L, r)\).
‣ AddRightDistributivityExpanding( C, F ) | ( operation ) |
‣ AddRightDistributivityExpanding( 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 RightDistributivityExpanding. 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{RightDistributivityExpanding}(L, a)\).
‣ AddRightDistributivityExpandingWithGivenObjects( C, F ) | ( operation ) |
‣ AddRightDistributivityExpandingWithGivenObjects( 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 RightDistributivityExpandingWithGivenObjects. 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{RightDistributivityExpandingWithGivenObjects}(s, L, a, r)\).
‣ AddRightDistributivityFactoring( C, F ) | ( operation ) |
‣ AddRightDistributivityFactoring( 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 RightDistributivityFactoring. 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{RightDistributivityFactoring}(L, a)\).
‣ AddRightDistributivityFactoringWithGivenObjects( C, F ) | ( operation ) |
‣ AddRightDistributivityFactoringWithGivenObjects( 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 RightDistributivityFactoringWithGivenObjects. 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{RightDistributivityFactoringWithGivenObjects}(s, L, a, r)\).
‣ AddBraiding( C, F ) | ( operation ) |
‣ AddBraiding( 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 Braiding. 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{Braiding}(a, b)\).
‣ AddBraidingInverse( C, F ) | ( operation ) |
‣ AddBraidingInverse( 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 BraidingInverse. 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{BraidingInverse}(a, b)\).
‣ AddBraidingInverseWithGivenTensorProducts( C, F ) | ( operation ) |
‣ AddBraidingInverseWithGivenTensorProducts( 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 BraidingInverseWithGivenTensorProducts. 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{BraidingInverseWithGivenTensorProducts}(s, a, b, r)\).
‣ AddBraidingWithGivenTensorProducts( C, F ) | ( operation ) |
‣ AddBraidingWithGivenTensorProducts( 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 BraidingWithGivenTensorProducts. 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{BraidingWithGivenTensorProducts}(s, a, b, r)\).
‣ AddClosedMonoidalLeftCoevaluationMorphism( C, F ) | ( operation ) |
‣ AddClosedMonoidalLeftCoevaluationMorphism( 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 ClosedMonoidalLeftCoevaluationMorphism. 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{ClosedMonoidalLeftCoevaluationMorphism}(a, b)\).
‣ AddClosedMonoidalLeftCoevaluationMorphismWithGivenRange( C, F ) | ( operation ) |
‣ AddClosedMonoidalLeftCoevaluationMorphismWithGivenRange( 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 ClosedMonoidalLeftCoevaluationMorphismWithGivenRange. 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{ClosedMonoidalLeftCoevaluationMorphismWithGivenRange}(a, b, r)\).
‣ AddClosedMonoidalLeftEvaluationMorphism( C, F ) | ( operation ) |
‣ AddClosedMonoidalLeftEvaluationMorphism( 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 ClosedMonoidalLeftEvaluationMorphism. 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{ClosedMonoidalLeftEvaluationMorphism}(a, b)\).
‣ AddClosedMonoidalLeftEvaluationMorphismWithGivenSource( C, F ) | ( operation ) |
‣ AddClosedMonoidalLeftEvaluationMorphismWithGivenSource( 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 ClosedMonoidalLeftEvaluationMorphismWithGivenSource. 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{ClosedMonoidalLeftEvaluationMorphismWithGivenSource}(a, b, s)\).
‣ AddClosedMonoidalRightCoevaluationMorphism( C, F ) | ( operation ) |
‣ AddClosedMonoidalRightCoevaluationMorphism( 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 ClosedMonoidalRightCoevaluationMorphism. 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{ClosedMonoidalRightCoevaluationMorphism}(a, b)\).
‣ AddClosedMonoidalRightCoevaluationMorphismWithGivenRange( C, F ) | ( operation ) |
‣ AddClosedMonoidalRightCoevaluationMorphismWithGivenRange( 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 ClosedMonoidalRightCoevaluationMorphismWithGivenRange. 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{ClosedMonoidalRightCoevaluationMorphismWithGivenRange}(a, b, r)\).
‣ AddClosedMonoidalRightEvaluationMorphism( C, F ) | ( operation ) |
‣ AddClosedMonoidalRightEvaluationMorphism( 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 ClosedMonoidalRightEvaluationMorphism. 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{ClosedMonoidalRightEvaluationMorphism}(a, b)\).
‣ AddClosedMonoidalRightEvaluationMorphismWithGivenSource( C, F ) | ( operation ) |
‣ AddClosedMonoidalRightEvaluationMorphismWithGivenSource( 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 ClosedMonoidalRightEvaluationMorphismWithGivenSource. 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{ClosedMonoidalRightEvaluationMorphismWithGivenSource}(a, b, s)\).
‣ AddDualOnMorphisms( C, F ) | ( operation ) |
‣ AddDualOnMorphisms( 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 DualOnMorphisms. 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{DualOnMorphisms}(alpha)\).
‣ AddDualOnMorphismsWithGivenDuals( C, F ) | ( operation ) |
‣ AddDualOnMorphismsWithGivenDuals( 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 DualOnMorphismsWithGivenDuals. 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{DualOnMorphismsWithGivenDuals}(s, alpha, r)\).
‣ AddDualOnObjects( C, F ) | ( operation ) |
‣ AddDualOnObjects( 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 DualOnObjects. 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{DualOnObjects}(a)\).
‣ AddEvaluationForDual( C, F ) | ( operation ) |
‣ AddEvaluationForDual( 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 EvaluationForDual. 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{EvaluationForDual}(a)\).
‣ AddEvaluationForDualWithGivenTensorProduct( C, F ) | ( operation ) |
‣ AddEvaluationForDualWithGivenTensorProduct( 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 EvaluationForDualWithGivenTensorProduct. 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{EvaluationForDualWithGivenTensorProduct}(s, a, r)\).
‣ AddInternalHomOnMorphisms( C, F ) | ( operation ) |
‣ AddInternalHomOnMorphisms( 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 InternalHomOnMorphisms. 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{InternalHomOnMorphisms}(alpha, beta)\).
‣ AddInternalHomOnMorphismsWithGivenInternalHoms( C, F ) | ( operation ) |
‣ AddInternalHomOnMorphismsWithGivenInternalHoms( 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 InternalHomOnMorphismsWithGivenInternalHoms. 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{InternalHomOnMorphismsWithGivenInternalHoms}(s, alpha, beta, r)\).
‣ AddInternalHomOnObjects( C, F ) | ( operation ) |
‣ AddInternalHomOnObjects( 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 InternalHomOnObjects. 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{InternalHomOnObjects}(a, b)\).
‣ AddInternalHomToTensorProductLeftAdjunctMorphism( C, F ) | ( operation ) |
‣ AddInternalHomToTensorProductLeftAdjunctMorphism( 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 InternalHomToTensorProductLeftAdjunctMorphism. 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{InternalHomToTensorProductLeftAdjunctMorphism}(b, c, g)\).
‣ AddInternalHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct( C, F ) | ( operation ) |
‣ AddInternalHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct( 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 InternalHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct. 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{InternalHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct}(b, c, g, s)\).
‣ AddInternalHomToTensorProductLeftAdjunctionIsomorphism( C, F ) | ( operation ) |
‣ AddInternalHomToTensorProductLeftAdjunctionIsomorphism( 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 InternalHomToTensorProductLeftAdjunctionIsomorphism. 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{InternalHomToTensorProductLeftAdjunctionIsomorphism}(a, b, c)\).
‣ AddInternalHomToTensorProductLeftAdjunctionIsomorphismWithGivenObjects( C, F ) | ( operation ) |
‣ AddInternalHomToTensorProductLeftAdjunctionIsomorphismWithGivenObjects( 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 InternalHomToTensorProductLeftAdjunctionIsomorphismWithGivenObjects. 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{InternalHomToTensorProductLeftAdjunctionIsomorphismWithGivenObjects}(s, a, b, c, r)\).
‣ AddInternalHomToTensorProductRightAdjunctMorphism( C, F ) | ( operation ) |
‣ AddInternalHomToTensorProductRightAdjunctMorphism( 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 InternalHomToTensorProductRightAdjunctMorphism. 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{InternalHomToTensorProductRightAdjunctMorphism}(a, c, g)\).
‣ AddInternalHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct( C, F ) | ( operation ) |
‣ AddInternalHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct( 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 InternalHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct. 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{InternalHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct}(a, c, g, s)\).
‣ AddInternalHomToTensorProductRightAdjunctionIsomorphism( C, F ) | ( operation ) |
‣ AddInternalHomToTensorProductRightAdjunctionIsomorphism( 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 InternalHomToTensorProductRightAdjunctionIsomorphism. 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{InternalHomToTensorProductRightAdjunctionIsomorphism}(a, b, c)\).
‣ AddInternalHomToTensorProductRightAdjunctionIsomorphismWithGivenObjects( C, F ) | ( operation ) |
‣ AddInternalHomToTensorProductRightAdjunctionIsomorphismWithGivenObjects( 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 InternalHomToTensorProductRightAdjunctionIsomorphismWithGivenObjects. 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{InternalHomToTensorProductRightAdjunctionIsomorphismWithGivenObjects}(s, a, b, c, r)\).
‣ AddIsomorphismFromDualObjectToInternalHomIntoTensorUnit( C, F ) | ( operation ) |
‣ AddIsomorphismFromDualObjectToInternalHomIntoTensorUnit( 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 IsomorphismFromDualObjectToInternalHomIntoTensorUnit. 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{IsomorphismFromDualObjectToInternalHomIntoTensorUnit}(a)\).
‣ AddIsomorphismFromInternalHomIntoTensorUnitToDualObject( C, F ) | ( operation ) |
‣ AddIsomorphismFromInternalHomIntoTensorUnitToDualObject( 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 IsomorphismFromInternalHomIntoTensorUnitToDualObject. 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{IsomorphismFromInternalHomIntoTensorUnitToDualObject}(a)\).
‣ AddIsomorphismFromInternalHomToObject( C, F ) | ( operation ) |
‣ AddIsomorphismFromInternalHomToObject( 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 IsomorphismFromInternalHomToObject. 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{IsomorphismFromInternalHomToObject}(a)\).
‣ AddIsomorphismFromInternalHomToObjectWithGivenInternalHom( C, F ) | ( operation ) |
‣ AddIsomorphismFromInternalHomToObjectWithGivenInternalHom( 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 IsomorphismFromInternalHomToObjectWithGivenInternalHom. 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{IsomorphismFromInternalHomToObjectWithGivenInternalHom}(a, s)\).
‣ AddIsomorphismFromObjectToInternalHom( C, F ) | ( operation ) |
‣ AddIsomorphismFromObjectToInternalHom( 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 IsomorphismFromObjectToInternalHom. 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{IsomorphismFromObjectToInternalHom}(a)\).
‣ AddIsomorphismFromObjectToInternalHomWithGivenInternalHom( C, F ) | ( operation ) |
‣ AddIsomorphismFromObjectToInternalHomWithGivenInternalHom( 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 IsomorphismFromObjectToInternalHomWithGivenInternalHom. 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{IsomorphismFromObjectToInternalHomWithGivenInternalHom}(a, r)\).
‣ AddLambdaElimination( C, F ) | ( operation ) |
‣ AddLambdaElimination( 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 LambdaElimination. 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{LambdaElimination}(a, b, alpha)\).
‣ AddLambdaIntroduction( C, F ) | ( operation ) |
‣ AddLambdaIntroduction( 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 LambdaIntroduction. 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{LambdaIntroduction}(alpha)\).
‣ AddMonoidalPostComposeMorphism( C, F ) | ( operation ) |
‣ AddMonoidalPostComposeMorphism( 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 MonoidalPostComposeMorphism. 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{MonoidalPostComposeMorphism}(a, b, c)\).
‣ AddMonoidalPostComposeMorphismWithGivenObjects( C, F ) | ( operation ) |
‣ AddMonoidalPostComposeMorphismWithGivenObjects( 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 MonoidalPostComposeMorphismWithGivenObjects. 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{MonoidalPostComposeMorphismWithGivenObjects}(s, a, b, c, r)\).
‣ AddMonoidalPreComposeMorphism( C, F ) | ( operation ) |
‣ AddMonoidalPreComposeMorphism( 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 MonoidalPreComposeMorphism. 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{MonoidalPreComposeMorphism}(a, b, c)\).
‣ AddMonoidalPreComposeMorphismWithGivenObjects( C, F ) | ( operation ) |
‣ AddMonoidalPreComposeMorphismWithGivenObjects( 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 MonoidalPreComposeMorphismWithGivenObjects. 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{MonoidalPreComposeMorphismWithGivenObjects}(s, a, b, c, r)\).
‣ AddMorphismFromTensorProductToInternalHom( C, F ) | ( operation ) |
‣ AddMorphismFromTensorProductToInternalHom( 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 MorphismFromTensorProductToInternalHom. 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{MorphismFromTensorProductToInternalHom}(a, b)\).
‣ AddMorphismFromTensorProductToInternalHomWithGivenObjects( C, F ) | ( operation ) |
‣ AddMorphismFromTensorProductToInternalHomWithGivenObjects( 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 MorphismFromTensorProductToInternalHomWithGivenObjects. 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{MorphismFromTensorProductToInternalHomWithGivenObjects}(s, a, b, r)\).
‣ AddMorphismToBidual( C, F ) | ( operation ) |
‣ AddMorphismToBidual( 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 MorphismToBidual. 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{MorphismToBidual}(a)\).
‣ AddMorphismToBidualWithGivenBidual( C, F ) | ( operation ) |
‣ AddMorphismToBidualWithGivenBidual( 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 MorphismToBidualWithGivenBidual. 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{MorphismToBidualWithGivenBidual}(a, r)\).
‣ AddTensorProductDualityCompatibilityMorphism( C, F ) | ( operation ) |
‣ AddTensorProductDualityCompatibilityMorphism( 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 TensorProductDualityCompatibilityMorphism. 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{TensorProductDualityCompatibilityMorphism}(a, b)\).
‣ AddTensorProductDualityCompatibilityMorphismWithGivenObjects( C, F ) | ( operation ) |
‣ AddTensorProductDualityCompatibilityMorphismWithGivenObjects( 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 TensorProductDualityCompatibilityMorphismWithGivenObjects. 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{TensorProductDualityCompatibilityMorphismWithGivenObjects}(s, a, b, r)\).
‣ AddTensorProductInternalHomCompatibilityMorphism( C, F ) | ( operation ) |
‣ AddTensorProductInternalHomCompatibilityMorphism( 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 TensorProductInternalHomCompatibilityMorphism. 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{TensorProductInternalHomCompatibilityMorphism}(list)\).
‣ AddTensorProductInternalHomCompatibilityMorphismWithGivenObjects( C, F ) | ( operation ) |
‣ AddTensorProductInternalHomCompatibilityMorphismWithGivenObjects( 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 TensorProductInternalHomCompatibilityMorphismWithGivenObjects. 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{TensorProductInternalHomCompatibilityMorphismWithGivenObjects}(source, list, range)\).
‣ AddTensorProductToInternalHomLeftAdjunctMorphism( C, F ) | ( operation ) |
‣ AddTensorProductToInternalHomLeftAdjunctMorphism( 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 TensorProductToInternalHomLeftAdjunctMorphism. 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{TensorProductToInternalHomLeftAdjunctMorphism}(a, b, f)\).
‣ AddTensorProductToInternalHomLeftAdjunctMorphismWithGivenInternalHom( C, F ) | ( operation ) |
‣ AddTensorProductToInternalHomLeftAdjunctMorphismWithGivenInternalHom( 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 TensorProductToInternalHomLeftAdjunctMorphismWithGivenInternalHom. 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{TensorProductToInternalHomLeftAdjunctMorphismWithGivenInternalHom}(a, b, f, i)\).
‣ AddTensorProductToInternalHomLeftAdjunctionIsomorphism( C, F ) | ( operation ) |
‣ AddTensorProductToInternalHomLeftAdjunctionIsomorphism( 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 TensorProductToInternalHomLeftAdjunctionIsomorphism. 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{TensorProductToInternalHomLeftAdjunctionIsomorphism}(a, b, c)\).
‣ AddTensorProductToInternalHomLeftAdjunctionIsomorphismWithGivenObjects( C, F ) | ( operation ) |
‣ AddTensorProductToInternalHomLeftAdjunctionIsomorphismWithGivenObjects( 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 TensorProductToInternalHomLeftAdjunctionIsomorphismWithGivenObjects. 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{TensorProductToInternalHomLeftAdjunctionIsomorphismWithGivenObjects}(s, a, b, c, r)\).
‣ AddTensorProductToInternalHomRightAdjunctMorphism( C, F ) | ( operation ) |
‣ AddTensorProductToInternalHomRightAdjunctMorphism( 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 TensorProductToInternalHomRightAdjunctMorphism. 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{TensorProductToInternalHomRightAdjunctMorphism}(a, b, f)\).
‣ AddTensorProductToInternalHomRightAdjunctMorphismWithGivenInternalHom( C, F ) | ( operation ) |
‣ AddTensorProductToInternalHomRightAdjunctMorphismWithGivenInternalHom( 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 TensorProductToInternalHomRightAdjunctMorphismWithGivenInternalHom. 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{TensorProductToInternalHomRightAdjunctMorphismWithGivenInternalHom}(a, b, f, i)\).
‣ AddTensorProductToInternalHomRightAdjunctionIsomorphism( C, F ) | ( operation ) |
‣ AddTensorProductToInternalHomRightAdjunctionIsomorphism( 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 TensorProductToInternalHomRightAdjunctionIsomorphism. 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{TensorProductToInternalHomRightAdjunctionIsomorphism}(a, b, c)\).
‣ AddTensorProductToInternalHomRightAdjunctionIsomorphismWithGivenObjects( C, F ) | ( operation ) |
‣ AddTensorProductToInternalHomRightAdjunctionIsomorphismWithGivenObjects( 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 TensorProductToInternalHomRightAdjunctionIsomorphismWithGivenObjects. 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{TensorProductToInternalHomRightAdjunctionIsomorphismWithGivenObjects}(s, a, b, c, r)\).
‣ AddUniversalPropertyOfDual( C, F ) | ( operation ) |
‣ AddUniversalPropertyOfDual( 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 UniversalPropertyOfDual. 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{UniversalPropertyOfDual}(t, a, alpha)\).
‣ AddCoDualOnMorphisms( C, F ) | ( operation ) |
‣ AddCoDualOnMorphisms( 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 CoDualOnMorphisms. 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{CoDualOnMorphisms}(alpha)\).
‣ AddCoDualOnMorphismsWithGivenCoDuals( C, F ) | ( operation ) |
‣ AddCoDualOnMorphismsWithGivenCoDuals( 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 CoDualOnMorphismsWithGivenCoDuals. 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{CoDualOnMorphismsWithGivenCoDuals}(s, alpha, r)\).
‣ AddCoDualOnObjects( C, F ) | ( operation ) |
‣ AddCoDualOnObjects( 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 CoDualOnObjects. 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{CoDualOnObjects}(a)\).
‣ AddCoDualityTensorProductCompatibilityMorphism( C, F ) | ( operation ) |
‣ AddCoDualityTensorProductCompatibilityMorphism( 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 CoDualityTensorProductCompatibilityMorphism. 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{CoDualityTensorProductCompatibilityMorphism}(a, b)\).
‣ AddCoDualityTensorProductCompatibilityMorphismWithGivenObjects( C, F ) | ( operation ) |
‣ AddCoDualityTensorProductCompatibilityMorphismWithGivenObjects( 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 CoDualityTensorProductCompatibilityMorphismWithGivenObjects. 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{CoDualityTensorProductCompatibilityMorphismWithGivenObjects}(s, a, b, r)\).
‣ AddCoLambdaElimination( C, F ) | ( operation ) |
‣ AddCoLambdaElimination( 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 CoLambdaElimination. 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{CoLambdaElimination}(a, b, alpha)\).
‣ AddCoLambdaIntroduction( C, F ) | ( operation ) |
‣ AddCoLambdaIntroduction( 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 CoLambdaIntroduction. 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{CoLambdaIntroduction}(alpha)\).
‣ AddCoclosedEvaluationForCoDual( C, F ) | ( operation ) |
‣ AddCoclosedEvaluationForCoDual( 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 CoclosedEvaluationForCoDual. 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{CoclosedEvaluationForCoDual}(a)\).
‣ AddCoclosedEvaluationForCoDualWithGivenTensorProduct( C, F ) | ( operation ) |
‣ AddCoclosedEvaluationForCoDualWithGivenTensorProduct( 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 CoclosedEvaluationForCoDualWithGivenTensorProduct. 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{CoclosedEvaluationForCoDualWithGivenTensorProduct}(s, a, r)\).
‣ AddCoclosedMonoidalLeftCoevaluationMorphism( C, F ) | ( operation ) |
‣ AddCoclosedMonoidalLeftCoevaluationMorphism( 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 CoclosedMonoidalLeftCoevaluationMorphism. 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{CoclosedMonoidalLeftCoevaluationMorphism}(a, b)\).
‣ AddCoclosedMonoidalLeftCoevaluationMorphismWithGivenSource( C, F ) | ( operation ) |
‣ AddCoclosedMonoidalLeftCoevaluationMorphismWithGivenSource( 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 CoclosedMonoidalLeftCoevaluationMorphismWithGivenSource. 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{CoclosedMonoidalLeftCoevaluationMorphismWithGivenSource}(a, b, s)\).
‣ AddCoclosedMonoidalLeftEvaluationMorphism( C, F ) | ( operation ) |
‣ AddCoclosedMonoidalLeftEvaluationMorphism( 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 CoclosedMonoidalLeftEvaluationMorphism. 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{CoclosedMonoidalLeftEvaluationMorphism}(a, b)\).
‣ AddCoclosedMonoidalLeftEvaluationMorphismWithGivenRange( C, F ) | ( operation ) |
‣ AddCoclosedMonoidalLeftEvaluationMorphismWithGivenRange( 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 CoclosedMonoidalLeftEvaluationMorphismWithGivenRange. 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{CoclosedMonoidalLeftEvaluationMorphismWithGivenRange}(a, b, r)\).
‣ AddCoclosedMonoidalRightCoevaluationMorphism( C, F ) | ( operation ) |
‣ AddCoclosedMonoidalRightCoevaluationMorphism( 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 CoclosedMonoidalRightCoevaluationMorphism. 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{CoclosedMonoidalRightCoevaluationMorphism}(a, b)\).
‣ AddCoclosedMonoidalRightCoevaluationMorphismWithGivenSource( C, F ) | ( operation ) |
‣ AddCoclosedMonoidalRightCoevaluationMorphismWithGivenSource( 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 CoclosedMonoidalRightCoevaluationMorphismWithGivenSource. 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{CoclosedMonoidalRightCoevaluationMorphismWithGivenSource}(a, b, s)\).
‣ AddCoclosedMonoidalRightEvaluationMorphism( C, F ) | ( operation ) |
‣ AddCoclosedMonoidalRightEvaluationMorphism( 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 CoclosedMonoidalRightEvaluationMorphism. 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{CoclosedMonoidalRightEvaluationMorphism}(a, b)\).
‣ AddCoclosedMonoidalRightEvaluationMorphismWithGivenRange( C, F ) | ( operation ) |
‣ AddCoclosedMonoidalRightEvaluationMorphismWithGivenRange( 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 CoclosedMonoidalRightEvaluationMorphismWithGivenRange. 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{CoclosedMonoidalRightEvaluationMorphismWithGivenRange}(a, b, r)\).
‣ AddInternalCoHomOnMorphisms( C, F ) | ( operation ) |
‣ AddInternalCoHomOnMorphisms( 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 InternalCoHomOnMorphisms. 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{InternalCoHomOnMorphisms}(alpha, beta)\).
‣ AddInternalCoHomOnMorphismsWithGivenInternalCoHoms( C, F ) | ( operation ) |
‣ AddInternalCoHomOnMorphismsWithGivenInternalCoHoms( 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 InternalCoHomOnMorphismsWithGivenInternalCoHoms. 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{InternalCoHomOnMorphismsWithGivenInternalCoHoms}(s, alpha, beta, r)\).
‣ AddInternalCoHomOnObjects( C, F ) | ( operation ) |
‣ AddInternalCoHomOnObjects( 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 InternalCoHomOnObjects. 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{InternalCoHomOnObjects}(a, b)\).
‣ AddInternalCoHomTensorProductCompatibilityMorphism( C, F ) | ( operation ) |
‣ AddInternalCoHomTensorProductCompatibilityMorphism( 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 InternalCoHomTensorProductCompatibilityMorphism. 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{InternalCoHomTensorProductCompatibilityMorphism}(list)\).
‣ AddInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects( C, F ) | ( operation ) |
‣ AddInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects( 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 InternalCoHomTensorProductCompatibilityMorphismWithGivenObjects. 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{InternalCoHomTensorProductCompatibilityMorphismWithGivenObjects}(source, list, range)\).
‣ AddInternalCoHomToTensorProductLeftAdjunctMorphism( C, F ) | ( operation ) |
‣ AddInternalCoHomToTensorProductLeftAdjunctMorphism( 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 InternalCoHomToTensorProductLeftAdjunctMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, c, f ) \mapsto \mathtt{InternalCoHomToTensorProductLeftAdjunctMorphism}(a, c, f)\).
‣ AddInternalCoHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct( C, F ) | ( operation ) |
‣ AddInternalCoHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct( 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 InternalCoHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, c, f, t ) \mapsto \mathtt{InternalCoHomToTensorProductLeftAdjunctMorphismWithGivenTensorProduct}(a, c, f, t)\).
‣ AddInternalCoHomToTensorProductRightAdjunctMorphism( C, F ) | ( operation ) |
‣ AddInternalCoHomToTensorProductRightAdjunctMorphism( 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 InternalCoHomToTensorProductRightAdjunctMorphism. 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{InternalCoHomToTensorProductRightAdjunctMorphism}(a, b, f)\).
‣ AddInternalCoHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct( C, F ) | ( operation ) |
‣ AddInternalCoHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct( 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 InternalCoHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b, f, t ) \mapsto \mathtt{InternalCoHomToTensorProductRightAdjunctMorphismWithGivenTensorProduct}(a, b, f, t)\).
‣ AddIsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit( C, F ) | ( operation ) |
‣ AddIsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit( 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 IsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit. 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{IsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit}(a)\).
‣ AddIsomorphismFromInternalCoHomFromTensorUnitToCoDualObject( C, F ) | ( operation ) |
‣ AddIsomorphismFromInternalCoHomFromTensorUnitToCoDualObject( 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 IsomorphismFromInternalCoHomFromTensorUnitToCoDualObject. 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{IsomorphismFromInternalCoHomFromTensorUnitToCoDualObject}(a)\).
‣ AddIsomorphismFromInternalCoHomToObject( C, F ) | ( operation ) |
‣ AddIsomorphismFromInternalCoHomToObject( 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 IsomorphismFromInternalCoHomToObject. 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{IsomorphismFromInternalCoHomToObject}(a)\).
‣ AddIsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom( C, F ) | ( operation ) |
‣ AddIsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom( 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 IsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom. 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{IsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom}(a, s)\).
‣ AddIsomorphismFromObjectToInternalCoHom( C, F ) | ( operation ) |
‣ AddIsomorphismFromObjectToInternalCoHom( 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 IsomorphismFromObjectToInternalCoHom. 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{IsomorphismFromObjectToInternalCoHom}(a)\).
‣ AddIsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom( C, F ) | ( operation ) |
‣ AddIsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom( 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 IsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom. 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{IsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom}(a, r)\).
‣ AddMonoidalPostCoComposeMorphism( C, F ) | ( operation ) |
‣ AddMonoidalPostCoComposeMorphism( 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 MonoidalPostCoComposeMorphism. 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{MonoidalPostCoComposeMorphism}(a, b, c)\).
‣ AddMonoidalPostCoComposeMorphismWithGivenObjects( C, F ) | ( operation ) |
‣ AddMonoidalPostCoComposeMorphismWithGivenObjects( 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 MonoidalPostCoComposeMorphismWithGivenObjects. 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{MonoidalPostCoComposeMorphismWithGivenObjects}(s, a, b, c, r)\).
‣ AddMonoidalPreCoComposeMorphism( C, F ) | ( operation ) |
‣ AddMonoidalPreCoComposeMorphism( 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 MonoidalPreCoComposeMorphism. 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{MonoidalPreCoComposeMorphism}(a, b, c)\).
‣ AddMonoidalPreCoComposeMorphismWithGivenObjects( C, F ) | ( operation ) |
‣ AddMonoidalPreCoComposeMorphismWithGivenObjects( 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 MonoidalPreCoComposeMorphismWithGivenObjects. 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{MonoidalPreCoComposeMorphismWithGivenObjects}(s, a, b, c, r)\).
‣ AddMorphismFromCoBidual( C, F ) | ( operation ) |
‣ AddMorphismFromCoBidual( 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 MorphismFromCoBidual. 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{MorphismFromCoBidual}(a)\).
‣ AddMorphismFromCoBidualWithGivenCoBidual( C, F ) | ( operation ) |
‣ AddMorphismFromCoBidualWithGivenCoBidual( 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 MorphismFromCoBidualWithGivenCoBidual. 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{MorphismFromCoBidualWithGivenCoBidual}(a, s)\).
‣ AddMorphismFromInternalCoHomToTensorProduct( C, F ) | ( operation ) |
‣ AddMorphismFromInternalCoHomToTensorProduct( 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 MorphismFromInternalCoHomToTensorProduct. 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{MorphismFromInternalCoHomToTensorProduct}(a, b)\).
‣ AddMorphismFromInternalCoHomToTensorProductWithGivenObjects( C, F ) | ( operation ) |
‣ AddMorphismFromInternalCoHomToTensorProductWithGivenObjects( 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 MorphismFromInternalCoHomToTensorProductWithGivenObjects. 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{MorphismFromInternalCoHomToTensorProductWithGivenObjects}(s, a, b, r)\).
‣ AddTensorProductToInternalCoHomLeftAdjunctMorphism( C, F ) | ( operation ) |
‣ AddTensorProductToInternalCoHomLeftAdjunctMorphism( 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 TensorProductToInternalCoHomLeftAdjunctMorphism. 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{TensorProductToInternalCoHomLeftAdjunctMorphism}(b, c, g)\).
‣ AddTensorProductToInternalCoHomLeftAdjunctMorphismWithGivenInternalCoHom( C, F ) | ( operation ) |
‣ AddTensorProductToInternalCoHomLeftAdjunctMorphismWithGivenInternalCoHom( 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 TensorProductToInternalCoHomLeftAdjunctMorphismWithGivenInternalCoHom. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( b, c, g, i ) \mapsto \mathtt{TensorProductToInternalCoHomLeftAdjunctMorphismWithGivenInternalCoHom}(b, c, g, i)\).
‣ AddTensorProductToInternalCoHomRightAdjunctMorphism( C, F ) | ( operation ) |
‣ AddTensorProductToInternalCoHomRightAdjunctMorphism( 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 TensorProductToInternalCoHomRightAdjunctMorphism. 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{TensorProductToInternalCoHomRightAdjunctMorphism}(b, c, g)\).
‣ AddTensorProductToInternalCoHomRightAdjunctMorphismWithGivenInternalCoHom( C, F ) | ( operation ) |
‣ AddTensorProductToInternalCoHomRightAdjunctMorphismWithGivenInternalCoHom( 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 TensorProductToInternalCoHomRightAdjunctMorphismWithGivenInternalCoHom. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( b, c, g, i ) \mapsto \mathtt{TensorProductToInternalCoHomRightAdjunctMorphismWithGivenInternalCoHom}(b, c, g, i)\).
‣ AddUniversalPropertyOfCoDual( C, F ) | ( operation ) |
‣ AddUniversalPropertyOfCoDual( 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 UniversalPropertyOfCoDual. 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{UniversalPropertyOfCoDual}(t, a, alpha)\).
‣ AddIsomorphismFromLeftDualObjectToLeftInternalHomIntoTensorUnit( C, F ) | ( operation ) |
‣ AddIsomorphismFromLeftDualObjectToLeftInternalHomIntoTensorUnit( 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 IsomorphismFromLeftDualObjectToLeftInternalHomIntoTensorUnit. 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{IsomorphismFromLeftDualObjectToLeftInternalHomIntoTensorUnit}(a)\).
‣ AddIsomorphismFromLeftInternalHomIntoTensorUnitToLeftDualObject( C, F ) | ( operation ) |
‣ AddIsomorphismFromLeftInternalHomIntoTensorUnitToLeftDualObject( 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 IsomorphismFromLeftInternalHomIntoTensorUnitToLeftDualObject. 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{IsomorphismFromLeftInternalHomIntoTensorUnitToLeftDualObject}(a)\).
‣ AddIsomorphismFromLeftInternalHomToObject( C, F ) | ( operation ) |
‣ AddIsomorphismFromLeftInternalHomToObject( 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 IsomorphismFromLeftInternalHomToObject. 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{IsomorphismFromLeftInternalHomToObject}(a)\).
‣ AddIsomorphismFromLeftInternalHomToObjectWithGivenLeftInternalHom( C, F ) | ( operation ) |
‣ AddIsomorphismFromLeftInternalHomToObjectWithGivenLeftInternalHom( 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 IsomorphismFromLeftInternalHomToObjectWithGivenLeftInternalHom. 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{IsomorphismFromLeftInternalHomToObjectWithGivenLeftInternalHom}(a, s)\).
‣ AddIsomorphismFromObjectToLeftInternalHom( C, F ) | ( operation ) |
‣ AddIsomorphismFromObjectToLeftInternalHom( 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 IsomorphismFromObjectToLeftInternalHom. 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{IsomorphismFromObjectToLeftInternalHom}(a)\).
‣ AddIsomorphismFromObjectToLeftInternalHomWithGivenLeftInternalHom( C, F ) | ( operation ) |
‣ AddIsomorphismFromObjectToLeftInternalHomWithGivenLeftInternalHom( 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 IsomorphismFromObjectToLeftInternalHomWithGivenLeftInternalHom. 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{IsomorphismFromObjectToLeftInternalHomWithGivenLeftInternalHom}(a, r)\).
‣ AddLeftClosedMonoidalCoevaluationMorphism( C, F ) | ( operation ) |
‣ AddLeftClosedMonoidalCoevaluationMorphism( 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 LeftClosedMonoidalCoevaluationMorphism. 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{LeftClosedMonoidalCoevaluationMorphism}(a, b)\).
‣ AddLeftClosedMonoidalCoevaluationMorphismWithGivenRange( C, F ) | ( operation ) |
‣ AddLeftClosedMonoidalCoevaluationMorphismWithGivenRange( 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 LeftClosedMonoidalCoevaluationMorphismWithGivenRange. 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{LeftClosedMonoidalCoevaluationMorphismWithGivenRange}(a, b, r)\).
‣ AddLeftClosedMonoidalEvaluationForLeftDual( C, F ) | ( operation ) |
‣ AddLeftClosedMonoidalEvaluationForLeftDual( 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 LeftClosedMonoidalEvaluationForLeftDual. 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{LeftClosedMonoidalEvaluationForLeftDual}(a)\).
‣ AddLeftClosedMonoidalEvaluationForLeftDualWithGivenTensorProduct( C, F ) | ( operation ) |
‣ AddLeftClosedMonoidalEvaluationForLeftDualWithGivenTensorProduct( 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 LeftClosedMonoidalEvaluationForLeftDualWithGivenTensorProduct. 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{LeftClosedMonoidalEvaluationForLeftDualWithGivenTensorProduct}(s, a, r)\).
‣ AddLeftClosedMonoidalEvaluationMorphism( C, F ) | ( operation ) |
‣ AddLeftClosedMonoidalEvaluationMorphism( 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 LeftClosedMonoidalEvaluationMorphism. 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{LeftClosedMonoidalEvaluationMorphism}(a, b)\).
‣ AddLeftClosedMonoidalEvaluationMorphismWithGivenSource( C, F ) | ( operation ) |
‣ AddLeftClosedMonoidalEvaluationMorphismWithGivenSource( 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 LeftClosedMonoidalEvaluationMorphismWithGivenSource. 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{LeftClosedMonoidalEvaluationMorphismWithGivenSource}(a, b, s)\).
‣ AddLeftClosedMonoidalLambdaElimination( C, F ) | ( operation ) |
‣ AddLeftClosedMonoidalLambdaElimination( 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 LeftClosedMonoidalLambdaElimination. 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{LeftClosedMonoidalLambdaElimination}(a, b, alpha)\).
‣ AddLeftClosedMonoidalLambdaIntroduction( C, F ) | ( operation ) |
‣ AddLeftClosedMonoidalLambdaIntroduction( 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 LeftClosedMonoidalLambdaIntroduction. 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{LeftClosedMonoidalLambdaIntroduction}(alpha)\).
‣ AddLeftClosedMonoidalPostComposeMorphism( C, F ) | ( operation ) |
‣ AddLeftClosedMonoidalPostComposeMorphism( 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 LeftClosedMonoidalPostComposeMorphism. 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{LeftClosedMonoidalPostComposeMorphism}(a, b, c)\).
‣ AddLeftClosedMonoidalPostComposeMorphismWithGivenObjects( C, F ) | ( operation ) |
‣ AddLeftClosedMonoidalPostComposeMorphismWithGivenObjects( 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 LeftClosedMonoidalPostComposeMorphismWithGivenObjects. 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{LeftClosedMonoidalPostComposeMorphismWithGivenObjects}(s, a, b, c, r)\).
‣ AddLeftClosedMonoidalPreComposeMorphism( C, F ) | ( operation ) |
‣ AddLeftClosedMonoidalPreComposeMorphism( 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 LeftClosedMonoidalPreComposeMorphism. 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{LeftClosedMonoidalPreComposeMorphism}(a, b, c)\).
‣ AddLeftClosedMonoidalPreComposeMorphismWithGivenObjects( C, F ) | ( operation ) |
‣ AddLeftClosedMonoidalPreComposeMorphismWithGivenObjects( 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 LeftClosedMonoidalPreComposeMorphismWithGivenObjects. 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{LeftClosedMonoidalPreComposeMorphismWithGivenObjects}(s, a, b, c, r)\).
‣ AddLeftDualOnMorphisms( C, F ) | ( operation ) |
‣ AddLeftDualOnMorphisms( 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 LeftDualOnMorphisms. 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{LeftDualOnMorphisms}(alpha)\).
‣ AddLeftDualOnMorphismsWithGivenLeftDuals( C, F ) | ( operation ) |
‣ AddLeftDualOnMorphismsWithGivenLeftDuals( 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 LeftDualOnMorphismsWithGivenLeftDuals. 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{LeftDualOnMorphismsWithGivenLeftDuals}(s, alpha, r)\).
‣ AddLeftDualOnObjects( C, F ) | ( operation ) |
‣ AddLeftDualOnObjects( 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 LeftDualOnObjects. 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{LeftDualOnObjects}(a)\).
‣ AddLeftInternalHomOnMorphisms( C, F ) | ( operation ) |
‣ AddLeftInternalHomOnMorphisms( 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 LeftInternalHomOnMorphisms. 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{LeftInternalHomOnMorphisms}(alpha, beta)\).
‣ AddLeftInternalHomOnMorphismsWithGivenLeftInternalHoms( C, F ) | ( operation ) |
‣ AddLeftInternalHomOnMorphismsWithGivenLeftInternalHoms( 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 LeftInternalHomOnMorphismsWithGivenLeftInternalHoms. 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{LeftInternalHomOnMorphismsWithGivenLeftInternalHoms}(s, alpha, beta, r)\).
‣ AddLeftInternalHomOnObjects( C, F ) | ( operation ) |
‣ AddLeftInternalHomOnObjects( 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 LeftInternalHomOnObjects. 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{LeftInternalHomOnObjects}(a, b)\).
‣ AddLeftInternalHomToTensorProductAdjunctMorphism( C, F ) | ( operation ) |
‣ AddLeftInternalHomToTensorProductAdjunctMorphism( 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 LeftInternalHomToTensorProductAdjunctMorphism. 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{LeftInternalHomToTensorProductAdjunctMorphism}(b, c, g)\).
‣ AddLeftInternalHomToTensorProductAdjunctMorphismWithGivenTensorProduct( C, F ) | ( operation ) |
‣ AddLeftInternalHomToTensorProductAdjunctMorphismWithGivenTensorProduct( 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 LeftInternalHomToTensorProductAdjunctMorphismWithGivenTensorProduct. 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, t ) \mapsto \mathtt{LeftInternalHomToTensorProductAdjunctMorphismWithGivenTensorProduct}(b, c, g, t)\).
‣ AddMorphismFromTensorProductToLeftInternalHom( C, F ) | ( operation ) |
‣ AddMorphismFromTensorProductToLeftInternalHom( 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 MorphismFromTensorProductToLeftInternalHom. 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{MorphismFromTensorProductToLeftInternalHom}(a, b)\).
‣ AddMorphismFromTensorProductToLeftInternalHomWithGivenObjects( C, F ) | ( operation ) |
‣ AddMorphismFromTensorProductToLeftInternalHomWithGivenObjects( 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 MorphismFromTensorProductToLeftInternalHomWithGivenObjects. 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{MorphismFromTensorProductToLeftInternalHomWithGivenObjects}(s, a, b, r)\).
‣ AddMorphismToLeftBidual( C, F ) | ( operation ) |
‣ AddMorphismToLeftBidual( 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 MorphismToLeftBidual. 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{MorphismToLeftBidual}(a)\).
‣ AddMorphismToLeftBidualWithGivenLeftBidual( C, F ) | ( operation ) |
‣ AddMorphismToLeftBidualWithGivenLeftBidual( 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 MorphismToLeftBidualWithGivenLeftBidual. 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{MorphismToLeftBidualWithGivenLeftBidual}(a, r)\).
‣ AddTensorProductLeftDualityCompatibilityMorphism( C, F ) | ( operation ) |
‣ AddTensorProductLeftDualityCompatibilityMorphism( 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 TensorProductLeftDualityCompatibilityMorphism. 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{TensorProductLeftDualityCompatibilityMorphism}(a, b)\).
‣ AddTensorProductLeftDualityCompatibilityMorphismWithGivenObjects( C, F ) | ( operation ) |
‣ AddTensorProductLeftDualityCompatibilityMorphismWithGivenObjects( 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 TensorProductLeftDualityCompatibilityMorphismWithGivenObjects. 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{TensorProductLeftDualityCompatibilityMorphismWithGivenObjects}(s, a, b, r)\).
‣ AddTensorProductLeftInternalHomCompatibilityMorphism( C, F ) | ( operation ) |
‣ AddTensorProductLeftInternalHomCompatibilityMorphism( 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 TensorProductLeftInternalHomCompatibilityMorphism. 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{TensorProductLeftInternalHomCompatibilityMorphism}(list)\).
‣ AddTensorProductLeftInternalHomCompatibilityMorphismWithGivenObjects( C, F ) | ( operation ) |
‣ AddTensorProductLeftInternalHomCompatibilityMorphismWithGivenObjects( 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 TensorProductLeftInternalHomCompatibilityMorphismWithGivenObjects. 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{TensorProductLeftInternalHomCompatibilityMorphismWithGivenObjects}(source, list, range)\).
‣ AddTensorProductToLeftInternalHomAdjunctMorphism( C, F ) | ( operation ) |
‣ AddTensorProductToLeftInternalHomAdjunctMorphism( 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 TensorProductToLeftInternalHomAdjunctMorphism. 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{TensorProductToLeftInternalHomAdjunctMorphism}(a, b, f)\).
‣ AddTensorProductToLeftInternalHomAdjunctMorphismWithGivenLeftInternalHom( C, F ) | ( operation ) |
‣ AddTensorProductToLeftInternalHomAdjunctMorphismWithGivenLeftInternalHom( 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 TensorProductToLeftInternalHomAdjunctMorphismWithGivenLeftInternalHom. 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{TensorProductToLeftInternalHomAdjunctMorphismWithGivenLeftInternalHom}(a, b, f, i)\).
‣ AddUniversalPropertyOfLeftDual( C, F ) | ( operation ) |
‣ AddUniversalPropertyOfLeftDual( 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 UniversalPropertyOfLeftDual. 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{UniversalPropertyOfLeftDual}(t, a, alpha)\).
‣ AddIsomorphismFromLeftCoDualObjectToLeftInternalCoHomFromTensorUnit( C, F ) | ( operation ) |
‣ AddIsomorphismFromLeftCoDualObjectToLeftInternalCoHomFromTensorUnit( 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 IsomorphismFromLeftCoDualObjectToLeftInternalCoHomFromTensorUnit. 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{IsomorphismFromLeftCoDualObjectToLeftInternalCoHomFromTensorUnit}(a)\).
‣ AddIsomorphismFromLeftInternalCoHomFromTensorUnitToLeftCoDualObject( C, F ) | ( operation ) |
‣ AddIsomorphismFromLeftInternalCoHomFromTensorUnitToLeftCoDualObject( 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 IsomorphismFromLeftInternalCoHomFromTensorUnitToLeftCoDualObject. 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{IsomorphismFromLeftInternalCoHomFromTensorUnitToLeftCoDualObject}(a)\).
‣ AddIsomorphismFromLeftInternalCoHomToObject( C, F ) | ( operation ) |
‣ AddIsomorphismFromLeftInternalCoHomToObject( 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 IsomorphismFromLeftInternalCoHomToObject. 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{IsomorphismFromLeftInternalCoHomToObject}(a)\).
‣ AddIsomorphismFromLeftInternalCoHomToObjectWithGivenLeftInternalCoHom( C, F ) | ( operation ) |
‣ AddIsomorphismFromLeftInternalCoHomToObjectWithGivenLeftInternalCoHom( 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 IsomorphismFromLeftInternalCoHomToObjectWithGivenLeftInternalCoHom. 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{IsomorphismFromLeftInternalCoHomToObjectWithGivenLeftInternalCoHom}(a, s)\).
‣ AddIsomorphismFromObjectToLeftInternalCoHom( C, F ) | ( operation ) |
‣ AddIsomorphismFromObjectToLeftInternalCoHom( 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 IsomorphismFromObjectToLeftInternalCoHom. 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{IsomorphismFromObjectToLeftInternalCoHom}(a)\).
‣ AddIsomorphismFromObjectToLeftInternalCoHomWithGivenLeftInternalCoHom( C, F ) | ( operation ) |
‣ AddIsomorphismFromObjectToLeftInternalCoHomWithGivenLeftInternalCoHom( 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 IsomorphismFromObjectToLeftInternalCoHomWithGivenLeftInternalCoHom. 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{IsomorphismFromObjectToLeftInternalCoHomWithGivenLeftInternalCoHom}(a, r)\).
‣ AddLeftCoDualOnMorphisms( C, F ) | ( operation ) |
‣ AddLeftCoDualOnMorphisms( 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 LeftCoDualOnMorphisms. 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{LeftCoDualOnMorphisms}(alpha)\).
‣ AddLeftCoDualOnMorphismsWithGivenLeftCoDuals( C, F ) | ( operation ) |
‣ AddLeftCoDualOnMorphismsWithGivenLeftCoDuals( 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 LeftCoDualOnMorphismsWithGivenLeftCoDuals. 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{LeftCoDualOnMorphismsWithGivenLeftCoDuals}(s, alpha, r)\).
‣ AddLeftCoDualOnObjects( C, F ) | ( operation ) |
‣ AddLeftCoDualOnObjects( 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 LeftCoDualOnObjects. 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{LeftCoDualOnObjects}(a)\).
‣ AddLeftCoDualityTensorProductCompatibilityMorphism( C, F ) | ( operation ) |
‣ AddLeftCoDualityTensorProductCompatibilityMorphism( 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 LeftCoDualityTensorProductCompatibilityMorphism. 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{LeftCoDualityTensorProductCompatibilityMorphism}(a, b)\).
‣ AddLeftCoDualityTensorProductCompatibilityMorphismWithGivenObjects( C, F ) | ( operation ) |
‣ AddLeftCoDualityTensorProductCompatibilityMorphismWithGivenObjects( 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 LeftCoDualityTensorProductCompatibilityMorphismWithGivenObjects. 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{LeftCoDualityTensorProductCompatibilityMorphismWithGivenObjects}(s, a, b, r)\).
‣ AddLeftCoclosedMonoidalCoevaluationMorphism( C, F ) | ( operation ) |
‣ AddLeftCoclosedMonoidalCoevaluationMorphism( 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 LeftCoclosedMonoidalCoevaluationMorphism. 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{LeftCoclosedMonoidalCoevaluationMorphism}(a, b)\).
‣ AddLeftCoclosedMonoidalCoevaluationMorphismWithGivenSource( C, F ) | ( operation ) |
‣ AddLeftCoclosedMonoidalCoevaluationMorphismWithGivenSource( 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 LeftCoclosedMonoidalCoevaluationMorphismWithGivenSource. 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{LeftCoclosedMonoidalCoevaluationMorphismWithGivenSource}(a, b, s)\).
‣ AddLeftCoclosedMonoidalEvaluationForLeftCoDual( C, F ) | ( operation ) |
‣ AddLeftCoclosedMonoidalEvaluationForLeftCoDual( 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 LeftCoclosedMonoidalEvaluationForLeftCoDual. 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{LeftCoclosedMonoidalEvaluationForLeftCoDual}(a)\).
‣ AddLeftCoclosedMonoidalEvaluationForLeftCoDualWithGivenTensorProduct( C, F ) | ( operation ) |
‣ AddLeftCoclosedMonoidalEvaluationForLeftCoDualWithGivenTensorProduct( 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 LeftCoclosedMonoidalEvaluationForLeftCoDualWithGivenTensorProduct. 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{LeftCoclosedMonoidalEvaluationForLeftCoDualWithGivenTensorProduct}(s, a, r)\).
‣ AddLeftCoclosedMonoidalEvaluationMorphism( C, F ) | ( operation ) |
‣ AddLeftCoclosedMonoidalEvaluationMorphism( 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 LeftCoclosedMonoidalEvaluationMorphism. 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{LeftCoclosedMonoidalEvaluationMorphism}(a, b)\).
‣ AddLeftCoclosedMonoidalEvaluationMorphismWithGivenRange( C, F ) | ( operation ) |
‣ AddLeftCoclosedMonoidalEvaluationMorphismWithGivenRange( 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 LeftCoclosedMonoidalEvaluationMorphismWithGivenRange. 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{LeftCoclosedMonoidalEvaluationMorphismWithGivenRange}(a, b, r)\).
‣ AddLeftCoclosedMonoidalLambdaElimination( C, F ) | ( operation ) |
‣ AddLeftCoclosedMonoidalLambdaElimination( 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 LeftCoclosedMonoidalLambdaElimination. 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{LeftCoclosedMonoidalLambdaElimination}(a, b, alpha)\).
‣ AddLeftCoclosedMonoidalLambdaIntroduction( C, F ) | ( operation ) |
‣ AddLeftCoclosedMonoidalLambdaIntroduction( 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 LeftCoclosedMonoidalLambdaIntroduction. 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{LeftCoclosedMonoidalLambdaIntroduction}(alpha)\).
‣ AddLeftCoclosedMonoidalPostCoComposeMorphism( C, F ) | ( operation ) |
‣ AddLeftCoclosedMonoidalPostCoComposeMorphism( 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 LeftCoclosedMonoidalPostCoComposeMorphism. 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{LeftCoclosedMonoidalPostCoComposeMorphism}(a, b, c)\).
‣ AddLeftCoclosedMonoidalPostCoComposeMorphismWithGivenObjects( C, F ) | ( operation ) |
‣ AddLeftCoclosedMonoidalPostCoComposeMorphismWithGivenObjects( 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 LeftCoclosedMonoidalPostCoComposeMorphismWithGivenObjects. 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{LeftCoclosedMonoidalPostCoComposeMorphismWithGivenObjects}(s, a, b, c, r)\).
‣ AddLeftCoclosedMonoidalPreCoComposeMorphism( C, F ) | ( operation ) |
‣ AddLeftCoclosedMonoidalPreCoComposeMorphism( 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 LeftCoclosedMonoidalPreCoComposeMorphism. 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{LeftCoclosedMonoidalPreCoComposeMorphism}(a, b, c)\).
‣ AddLeftCoclosedMonoidalPreCoComposeMorphismWithGivenObjects( C, F ) | ( operation ) |
‣ AddLeftCoclosedMonoidalPreCoComposeMorphismWithGivenObjects( 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 LeftCoclosedMonoidalPreCoComposeMorphismWithGivenObjects. 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{LeftCoclosedMonoidalPreCoComposeMorphismWithGivenObjects}(s, a, b, c, r)\).
‣ AddLeftInternalCoHomOnMorphisms( C, F ) | ( operation ) |
‣ AddLeftInternalCoHomOnMorphisms( 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 LeftInternalCoHomOnMorphisms. 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{LeftInternalCoHomOnMorphisms}(alpha, beta)\).
‣ AddLeftInternalCoHomOnMorphismsWithGivenLeftInternalCoHoms( C, F ) | ( operation ) |
‣ AddLeftInternalCoHomOnMorphismsWithGivenLeftInternalCoHoms( 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 LeftInternalCoHomOnMorphismsWithGivenLeftInternalCoHoms. 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{LeftInternalCoHomOnMorphismsWithGivenLeftInternalCoHoms}(s, alpha, beta, r)\).
‣ AddLeftInternalCoHomOnObjects( C, F ) | ( operation ) |
‣ AddLeftInternalCoHomOnObjects( 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 LeftInternalCoHomOnObjects. 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{LeftInternalCoHomOnObjects}(a, b)\).
‣ AddLeftInternalCoHomTensorProductCompatibilityMorphism( C, F ) | ( operation ) |
‣ AddLeftInternalCoHomTensorProductCompatibilityMorphism( 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 LeftInternalCoHomTensorProductCompatibilityMorphism. 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{LeftInternalCoHomTensorProductCompatibilityMorphism}(list)\).
‣ AddLeftInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects( C, F ) | ( operation ) |
‣ AddLeftInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects( 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 LeftInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects. 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{LeftInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects}(source, list, range)\).
‣ AddLeftInternalCoHomToTensorProductAdjunctMorphism( C, F ) | ( operation ) |
‣ AddLeftInternalCoHomToTensorProductAdjunctMorphism( 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 LeftInternalCoHomToTensorProductAdjunctMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, c, f ) \mapsto \mathtt{LeftInternalCoHomToTensorProductAdjunctMorphism}(a, c, f)\).
‣ AddLeftInternalCoHomToTensorProductAdjunctMorphismWithGivenTensorProduct( C, F ) | ( operation ) |
‣ AddLeftInternalCoHomToTensorProductAdjunctMorphismWithGivenTensorProduct( 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 LeftInternalCoHomToTensorProductAdjunctMorphismWithGivenTensorProduct. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, c, f, t ) \mapsto \mathtt{LeftInternalCoHomToTensorProductAdjunctMorphismWithGivenTensorProduct}(a, c, f, t)\).
‣ AddMorphismFromLeftCoBidual( C, F ) | ( operation ) |
‣ AddMorphismFromLeftCoBidual( 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 MorphismFromLeftCoBidual. 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{MorphismFromLeftCoBidual}(a)\).
‣ AddMorphismFromLeftCoBidualWithGivenLeftCoBidual( C, F ) | ( operation ) |
‣ AddMorphismFromLeftCoBidualWithGivenLeftCoBidual( 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 MorphismFromLeftCoBidualWithGivenLeftCoBidual. 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{MorphismFromLeftCoBidualWithGivenLeftCoBidual}(a, s)\).
‣ AddMorphismFromLeftInternalCoHomToTensorProduct( C, F ) | ( operation ) |
‣ AddMorphismFromLeftInternalCoHomToTensorProduct( 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 MorphismFromLeftInternalCoHomToTensorProduct. 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{MorphismFromLeftInternalCoHomToTensorProduct}(a, b)\).
‣ AddMorphismFromLeftInternalCoHomToTensorProductWithGivenObjects( C, F ) | ( operation ) |
‣ AddMorphismFromLeftInternalCoHomToTensorProductWithGivenObjects( 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 MorphismFromLeftInternalCoHomToTensorProductWithGivenObjects. 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{MorphismFromLeftInternalCoHomToTensorProductWithGivenObjects}(s, a, b, r)\).
‣ AddTensorProductToLeftInternalCoHomAdjunctMorphism( C, F ) | ( operation ) |
‣ AddTensorProductToLeftInternalCoHomAdjunctMorphism( 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 TensorProductToLeftInternalCoHomAdjunctMorphism. 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{TensorProductToLeftInternalCoHomAdjunctMorphism}(b, c, g)\).
‣ AddTensorProductToLeftInternalCoHomAdjunctMorphismWithGivenLeftInternalCoHom( C, F ) | ( operation ) |
‣ AddTensorProductToLeftInternalCoHomAdjunctMorphismWithGivenLeftInternalCoHom( 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 TensorProductToLeftInternalCoHomAdjunctMorphismWithGivenLeftInternalCoHom. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( b, c, g, i ) \mapsto \mathtt{TensorProductToLeftInternalCoHomAdjunctMorphismWithGivenLeftInternalCoHom}(b, c, g, i)\).
‣ AddUniversalPropertyOfLeftCoDual( C, F ) | ( operation ) |
‣ AddUniversalPropertyOfLeftCoDual( 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 UniversalPropertyOfLeftCoDual. 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{UniversalPropertyOfLeftCoDual}(t, a, alpha)\).
‣ AddAssociatorLeftToRight( C, F ) | ( operation ) |
‣ AddAssociatorLeftToRight( 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 AssociatorLeftToRight. 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{AssociatorLeftToRight}(a, b, c)\).
‣ AddAssociatorLeftToRightWithGivenTensorProducts( C, F ) | ( operation ) |
‣ AddAssociatorLeftToRightWithGivenTensorProducts( 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 AssociatorLeftToRightWithGivenTensorProducts. 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{AssociatorLeftToRightWithGivenTensorProducts}(s, a, b, c, r)\).
‣ AddAssociatorRightToLeft( C, F ) | ( operation ) |
‣ AddAssociatorRightToLeft( 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 AssociatorRightToLeft. 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{AssociatorRightToLeft}(a, b, c)\).
‣ AddAssociatorRightToLeftWithGivenTensorProducts( C, F ) | ( operation ) |
‣ AddAssociatorRightToLeftWithGivenTensorProducts( 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 AssociatorRightToLeftWithGivenTensorProducts. 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{AssociatorRightToLeftWithGivenTensorProducts}(s, a, b, c, r)\).
‣ AddLeftUnitor( C, F ) | ( operation ) |
‣ AddLeftUnitor( 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 LeftUnitor. 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{LeftUnitor}(a)\).
‣ AddLeftUnitorInverse( C, F ) | ( operation ) |
‣ AddLeftUnitorInverse( 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 LeftUnitorInverse. 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{LeftUnitorInverse}(a)\).
‣ AddLeftUnitorInverseWithGivenTensorProduct( C, F ) | ( operation ) |
‣ AddLeftUnitorInverseWithGivenTensorProduct( 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 LeftUnitorInverseWithGivenTensorProduct. 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{LeftUnitorInverseWithGivenTensorProduct}(a, r)\).
‣ AddLeftUnitorWithGivenTensorProduct( C, F ) | ( operation ) |
‣ AddLeftUnitorWithGivenTensorProduct( 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 LeftUnitorWithGivenTensorProduct. 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{LeftUnitorWithGivenTensorProduct}(a, s)\).
‣ AddRightUnitor( C, F ) | ( operation ) |
‣ AddRightUnitor( 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 RightUnitor. 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{RightUnitor}(a)\).
‣ AddRightUnitorInverse( C, F ) | ( operation ) |
‣ AddRightUnitorInverse( 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 RightUnitorInverse. 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{RightUnitorInverse}(a)\).
‣ AddRightUnitorInverseWithGivenTensorProduct( C, F ) | ( operation ) |
‣ AddRightUnitorInverseWithGivenTensorProduct( 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 RightUnitorInverseWithGivenTensorProduct. 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{RightUnitorInverseWithGivenTensorProduct}(a, r)\).
‣ AddRightUnitorWithGivenTensorProduct( C, F ) | ( operation ) |
‣ AddRightUnitorWithGivenTensorProduct( 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 RightUnitorWithGivenTensorProduct. 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{RightUnitorWithGivenTensorProduct}(a, s)\).
‣ AddTensorProductOnMorphisms( C, F ) | ( operation ) |
‣ AddTensorProductOnMorphisms( 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 TensorProductOnMorphisms. 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{TensorProductOnMorphisms}(alpha, beta)\).
‣ AddTensorProductOnMorphismsWithGivenTensorProducts( C, F ) | ( operation ) |
‣ AddTensorProductOnMorphismsWithGivenTensorProducts( 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 TensorProductOnMorphismsWithGivenTensorProducts. 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{TensorProductOnMorphismsWithGivenTensorProducts}(s, alpha, beta, r)\).
‣ AddTensorProductOnObjects( C, F ) | ( operation ) |
‣ AddTensorProductOnObjects( 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 TensorProductOnObjects. 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: ( arg2, arg3 ) \mapsto \mathtt{TensorProductOnObjects}(arg2, arg3)\).
‣ AddTensorUnit( C, F ) | ( operation ) |
‣ AddTensorUnit( 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 TensorUnit. 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: ( ) \mapsto \mathtt{TensorUnit}()\).
‣ AddCoevaluationForDual( C, F ) | ( operation ) |
‣ AddCoevaluationForDual( 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 CoevaluationForDual. 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{CoevaluationForDual}(a)\).
‣ AddCoevaluationForDualWithGivenTensorProduct( C, F ) | ( operation ) |
‣ AddCoevaluationForDualWithGivenTensorProduct( 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 CoevaluationForDualWithGivenTensorProduct. 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{CoevaluationForDualWithGivenTensorProduct}(s, a, r)\).
‣ AddIsomorphismFromInternalHomToTensorProductWithDualObject( C, F ) | ( operation ) |
‣ AddIsomorphismFromInternalHomToTensorProductWithDualObject( 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 IsomorphismFromInternalHomToTensorProductWithDualObject. 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{IsomorphismFromInternalHomToTensorProductWithDualObject}(a, b)\).
‣ AddIsomorphismFromTensorProductWithDualObjectToInternalHom( C, F ) | ( operation ) |
‣ AddIsomorphismFromTensorProductWithDualObjectToInternalHom( 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 IsomorphismFromTensorProductWithDualObjectToInternalHom. 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{IsomorphismFromTensorProductWithDualObjectToInternalHom}(a, b)\).
‣ AddMorphismFromBidual( C, F ) | ( operation ) |
‣ AddMorphismFromBidual( 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 MorphismFromBidual. 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{MorphismFromBidual}(a)\).
‣ AddMorphismFromBidualWithGivenBidual( C, F ) | ( operation ) |
‣ AddMorphismFromBidualWithGivenBidual( 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 MorphismFromBidualWithGivenBidual. 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{MorphismFromBidualWithGivenBidual}(a, s)\).
‣ AddMorphismFromInternalHomToTensorProduct( C, F ) | ( operation ) |
‣ AddMorphismFromInternalHomToTensorProduct( 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 MorphismFromInternalHomToTensorProduct. 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{MorphismFromInternalHomToTensorProduct}(a, b)\).
‣ AddMorphismFromInternalHomToTensorProductWithGivenObjects( C, F ) | ( operation ) |
‣ AddMorphismFromInternalHomToTensorProductWithGivenObjects( 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 MorphismFromInternalHomToTensorProductWithGivenObjects. 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{MorphismFromInternalHomToTensorProductWithGivenObjects}(s, a, b, r)\).
‣ AddRankMorphism( C, F ) | ( operation ) |
‣ AddRankMorphism( 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 RankMorphism. 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{RankMorphism}(a)\).
‣ AddTensorProductInternalHomCompatibilityMorphismInverse( C, F ) | ( operation ) |
‣ AddTensorProductInternalHomCompatibilityMorphismInverse( 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 TensorProductInternalHomCompatibilityMorphismInverse. 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{TensorProductInternalHomCompatibilityMorphismInverse}(list)\).
‣ AddTensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects( C, F ) | ( operation ) |
‣ AddTensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects( 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 TensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects. 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{TensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects}(source, list, range)\).
‣ AddTraceMap( C, F ) | ( operation ) |
‣ AddTraceMap( 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 TraceMap. 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{TraceMap}(alpha)\).
‣ AddCoRankMorphism( C, F ) | ( operation ) |
‣ AddCoRankMorphism( 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 CoRankMorphism. 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{CoRankMorphism}(a)\).
‣ AddCoTraceMap( C, F ) | ( operation ) |
‣ AddCoTraceMap( 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 CoTraceMap. 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{CoTraceMap}(alpha)\).
‣ AddCoclosedCoevaluationForCoDual( C, F ) | ( operation ) |
‣ AddCoclosedCoevaluationForCoDual( 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 CoclosedCoevaluationForCoDual. 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{CoclosedCoevaluationForCoDual}(a)\).
‣ AddCoclosedCoevaluationForCoDualWithGivenTensorProduct( C, F ) | ( operation ) |
‣ AddCoclosedCoevaluationForCoDualWithGivenTensorProduct( 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 CoclosedCoevaluationForCoDualWithGivenTensorProduct. 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{CoclosedCoevaluationForCoDualWithGivenTensorProduct}(s, a, r)\).
‣ AddInternalCoHomTensorProductCompatibilityMorphismInverse( C, F ) | ( operation ) |
‣ AddInternalCoHomTensorProductCompatibilityMorphismInverse( 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 InternalCoHomTensorProductCompatibilityMorphismInverse. 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{InternalCoHomTensorProductCompatibilityMorphismInverse}(list)\).
‣ AddInternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects( C, F ) | ( operation ) |
‣ AddInternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects( 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 InternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects. 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{InternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects}(source, list, range)\).
‣ AddIsomorphismFromInternalCoHomToTensorProductWithCoDualObject( C, F ) | ( operation ) |
‣ AddIsomorphismFromInternalCoHomToTensorProductWithCoDualObject( 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 IsomorphismFromInternalCoHomToTensorProductWithCoDualObject. 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{IsomorphismFromInternalCoHomToTensorProductWithCoDualObject}(a, b)\).
‣ AddIsomorphismFromTensorProductWithCoDualObjectToInternalCoHom( C, F ) | ( operation ) |
‣ AddIsomorphismFromTensorProductWithCoDualObjectToInternalCoHom( 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 IsomorphismFromTensorProductWithCoDualObjectToInternalCoHom. 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{IsomorphismFromTensorProductWithCoDualObjectToInternalCoHom}(a, b)\).
‣ AddMorphismFromTensorProductToInternalCoHom( C, F ) | ( operation ) |
‣ AddMorphismFromTensorProductToInternalCoHom( 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 MorphismFromTensorProductToInternalCoHom. 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{MorphismFromTensorProductToInternalCoHom}(a, b)\).
‣ AddMorphismFromTensorProductToInternalCoHomWithGivenObjects( C, F ) | ( operation ) |
‣ AddMorphismFromTensorProductToInternalCoHomWithGivenObjects( 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 MorphismFromTensorProductToInternalCoHomWithGivenObjects. 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{MorphismFromTensorProductToInternalCoHomWithGivenObjects}(s, a, b, r)\).
‣ AddMorphismToCoBidual( C, F ) | ( operation ) |
‣ AddMorphismToCoBidual( 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 MorphismToCoBidual. 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{MorphismToCoBidual}(a)\).
‣ AddMorphismToCoBidualWithGivenCoBidual( C, F ) | ( operation ) |
‣ AddMorphismToCoBidualWithGivenCoBidual( 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 MorphismToCoBidualWithGivenCoBidual. 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{MorphismToCoBidualWithGivenCoBidual}(a, r)\).
generated by GAPDoc2HTML