chap7.txt

  
  7 Tensor Product and Internal Hom
  
  
  7.1 Monoidal Categories
  
  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},
  
      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}  ) = \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}   =  \mathrm{id}_a  \otimes
        \lambda_c.
  
  The corresponding GAP property is given by IsMonoidalCategory.
  
  7.1-1 TensorProductOnObjects
  
  TensorProductOnObjects( a, b )  operation
  Returns:  an object
  
  The  arguments  are  two  objects  a,  b. The output is the tensor product a
  \otimes b.
  
  7.1-2 AddTensorProductOnObjects
  
  AddTensorProductOnObjects( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  TensorProductOnObjects. F: (a,b) \mapsto a \otimes b.
  
  7.1-3 TensorProductOnMorphisms
  
  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.
  
  7.1-4 TensorProductOnMorphismsWithGivenTensorProducts
  
  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.
  
  7.1-5 AddTensorProductOnMorphismsWithGivenTensorProducts
  
  AddTensorProductOnMorphismsWithGivenTensorProducts( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  TensorProductOnMorphismsWithGivenTensorProducts. F: ( a \otimes b, \alpha: a
  \rightarrow  a',  \beta:  b  \rightarrow  b', a' \otimes b' ) \mapsto \alpha
  \otimes \beta.
  
  7.1-6 AssociatorRightToLeft
  
  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.
  
  7.1-7 AssociatorRightToLeftWithGivenTensorProducts
  
  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.
  
  7.1-8 AddAssociatorRightToLeftWithGivenTensorProducts
  
  AddAssociatorRightToLeftWithGivenTensorProducts( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  AssociatorRightToLeftWithGivenTensorProducts.  F: ( a \otimes (b \otimes c),
  a, b, c, (a \otimes b) \otimes c ) \mapsto \alpha_{a,(b,c)}.
  
  7.1-9 AssociatorLeftToRight
  
  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).
  
  7.1-10 AssociatorLeftToRightWithGivenTensorProducts
  
  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).
  
  7.1-11 AddAssociatorLeftToRightWithGivenTensorProducts
  
  AddAssociatorLeftToRightWithGivenTensorProducts( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  AssociatorLeftToRightWithGivenTensorProducts. F: (( a \otimes b ) \otimes c,
  a, b, c, a \otimes (b \otimes c )) \mapsto \alpha_{(a,b),c}.
  
  7.1-12 TensorUnit
  
  TensorUnit( C )  attribute
  Returns:  an object
  
  The  argument  is  a category \mathbf{C}. The output is the tensor unit 1 of
  \mathbf{C}.
  
  7.1-13 AddTensorUnit
  
  AddTensorUnit( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given  function F to the category for the basic operation TensorUnit. F: ( )
  \mapsto 1.
  
  7.1-14 LeftUnitor
  
  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.
  
  7.1-15 LeftUnitorWithGivenTensorProduct
  
  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.
  
  7.1-16 AddLeftUnitorWithGivenTensorProduct
  
  AddLeftUnitorWithGivenTensorProduct( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  LeftUnitorWithGivenTensorProduct. F: (a, 1 \otimes a) \mapsto \lambda_a.
  
  7.1-17 LeftUnitorInverse
  
  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.
  
  7.1-18 LeftUnitorInverseWithGivenTensorProduct
  
  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.
  
  7.1-19 AddLeftUnitorInverseWithGivenTensorProduct
  
  AddLeftUnitorInverseWithGivenTensorProduct( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  LeftUnitorInverseWithGivenTensorProduct.   F:   (a,  1  \otimes  a)  \mapsto
  \lambda_a^{-1}.
  
  7.1-20 RightUnitor
  
  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.
  
  7.1-21 RightUnitorWithGivenTensorProduct
  
  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.
  
  7.1-22 AddRightUnitorWithGivenTensorProduct
  
  AddRightUnitorWithGivenTensorProduct( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  RightUnitorWithGivenTensorProduct. F: (a, a \otimes 1) \mapsto \rho_a.
  
  7.1-23 RightUnitorInverse
  
  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.
  
  7.1-24 RightUnitorInverseWithGivenTensorProduct
  
  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.
  
  7.1-25 AddRightUnitorInverseWithGivenTensorProduct
  
  AddRightUnitorInverseWithGivenTensorProduct( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  RightUnitorInverseWithGivenTensorProduct.   F:  (a,  a  \otimes  1)  \mapsto
  \rho_a^{-1}.
  
  7.1-26 LeftDistributivityExpanding
  
  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).
  
  7.1-27 LeftDistributivityExpandingWithGivenObjects
  
  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.
  
  7.1-28 AddLeftDistributivityExpandingWithGivenObjects
  
  AddLeftDistributivityExpandingWithGivenObjects( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  LeftDistributivityExpandingWithGivenObjects. F: (a \otimes (b_1 \oplus \dots
  \oplus  b_n),  a,  L,  (a  \otimes b_1) \oplus \dots \oplus (a \otimes b_n))
  \mapsto \mathrm{LeftDistributivityExpandingWithGivenObjects}(a,L).
  
  7.1-29 LeftDistributivityFactoring
  
  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).
  
  7.1-30 LeftDistributivityFactoringWithGivenObjects
  
  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.
  
  7.1-31 AddLeftDistributivityFactoringWithGivenObjects
  
  AddLeftDistributivityFactoringWithGivenObjects( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  LeftDistributivityFactoringWithGivenObjects.  F:  ((a  \otimes  b_1)  \oplus
  \dots \oplus (a \otimes b_n), a, L, a \otimes (b_1 \oplus \dots \oplus b_n))
  \mapsto \mathrm{LeftDistributivityFactoringWithGivenObjects}(a,L).
  
  7.1-32 RightDistributivityExpanding
  
  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).
  
  7.1-33 RightDistributivityExpandingWithGivenObjects
  
  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.
  
  7.1-34 AddRightDistributivityExpandingWithGivenObjects
  
  AddRightDistributivityExpandingWithGivenObjects( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  RightDistributivityExpandingWithGivenObjects.  F:  ((b_1 \oplus \dots \oplus
  b_n)  \otimes  a, L, a, (b_1 \otimes a) \oplus \dots \oplus (b_n \otimes a))
  \mapsto \mathrm{RightDistributivityExpandingWithGivenObjects}(L,a).
  
  7.1-35 RightDistributivityFactoring
  
  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 .
  
  7.1-36 RightDistributivityFactoringWithGivenObjects
  
  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.
  
  7.1-37 AddRightDistributivityFactoringWithGivenObjects
  
  AddRightDistributivityFactoringWithGivenObjects( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  RightDistributivityFactoringWithGivenObjects.  F:  ((b_1  \otimes  a) \oplus
  \dots \oplus (b_n \otimes a), L, a, (b_1 \oplus \dots \oplus b_n) \otimes a)
  \mapsto \mathrm{RightDistributivityFactoringWithGivenObjects}(L,a).
  
  
  7.2 Braided Monoidal Categories
  
  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} = \rho_a,
  
      (B_{c,a}   \otimes  \mathrm{id}_b)  \circ  \alpha_{c,a,b}  \circ  B_{a
        \otimes  b,c}  = \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}  =  \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.
  
  7.2-1 Braiding
  
  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.
  
  7.2-2 BraidingWithGivenTensorProducts
  
  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.
  
  7.2-3 AddBraidingWithGivenTensorProducts
  
  AddBraidingWithGivenTensorProducts( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  BraidingWithGivenTensorProducts.  F:  (a  \otimes  b,  a,  b,  b  \otimes a)
  \rightarrow B_{a,b}.
  
  7.2-4 BraidingInverse
  
  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 of the braiding
   B_{a,b}^{-1}: b \otimes a \rightarrow a \otimes b.
  
  7.2-5 BraidingInverseWithGivenTensorProducts
  
  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 braiding  B_{a,b}^{-1}: b \otimes a
  \rightarrow a \otimes b.
  
  7.2-6 AddBraidingInverseWithGivenTensorProducts
  
  AddBraidingInverseWithGivenTensorProducts( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  BraidingInverseWithGivenTensorProducts.  F: (b \otimes a, a, b, a \otimes b)
  \rightarrow B_{a,b}^{-1}.
  
  
  7.3 Symmetric Monoidal Categories
  
  A braided monoidal category \mathbf{C} is called symmetric monoidal category
  if  B_{a,b}^{-1}  =  B_{b,a}.  The  corresponding  GAP  property is given by
  IsSymmetricMonoidalCategory.
  
  
  7.4 Symmetric Closed Monoidal Categories
  
  A  symmetric  monoidal  category  \mathbf{C}  which  has  for each functor -
  \otimes  b:  \mathbf{C}  \rightarrow  \mathbf{C} a right adjoint (denoted by
  \underline{\mathrm{Hom}}(b,-))   is   called  a  symmetric  closed  monoidal
  category.     The     corresponding     GAP    property    is    given    by
  IsSymmetricClosedMonoidalCategory.
  
  7.4-1 InternalHomOnObjects
  
  InternalHomOnObjects( a, b )  operation
  Returns:  an object
  
  The  arguments  are  two  objects a,b. The output is the internal hom object
  \underline{\mathrm{Hom}}(a,b).
  
  7.4-2 AddInternalHomOnObjects
  
  AddInternalHomOnObjects( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  InternalHomOnObjects. F: (a,b) \mapsto \underline{\mathrm{Hom}}(a,b).
  
  7.4-3 InternalHomOnMorphisms
  
  InternalHomOnMorphisms( alpha, beta )  operation
  Returns:  a   morphism   in   \mathrm{Hom}(  \underline{\mathrm{Hom}}(a',b),
            \underline{\mathrm{Hom}}(a,b') )
  
  The  arguments  are  two  morphisms  \alpha:  a  \rightarrow  a',  \beta:  b
  \rightarrow    b'.    The    output    is    the   internal   hom   morphism
  \underline{\mathrm{Hom}}(\alpha,\beta):       \underline{\mathrm{Hom}}(a',b)
  \rightarrow \underline{\mathrm{Hom}}(a,b').
  
  7.4-4 InternalHomOnMorphismsWithGivenInternalHoms
  
  InternalHomOnMorphismsWithGivenInternalHoms( s, alpha, beta, r )  operation
  Returns:  a   morphism   in   \mathrm{Hom}(  \underline{\mathrm{Hom}}(a',b),
            \underline{\mathrm{Hom}}(a,b') )
  
  The   arguments  are  an  object  s  =  \underline{\mathrm{Hom}}(a',b),  two
  morphisms \alpha: a \rightarrow a', \beta: b \rightarrow b', and an object r
  =  \underline{\mathrm{Hom}}(a,b').  The  output is the internal hom morphism
  \underline{\mathrm{Hom}}(\alpha,\beta):       \underline{\mathrm{Hom}}(a',b)
  \rightarrow \underline{\mathrm{Hom}}(a,b').
  
  7.4-5 AddInternalHomOnMorphismsWithGivenInternalHoms
  
  AddInternalHomOnMorphismsWithGivenInternalHoms( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  InternalHomOnMorphismsWithGivenInternalHoms.                              F:
  (\underline{\mathrm{Hom}}(a',b),   \alpha:   a   \rightarrow  a',  \beta:  b
  \rightarrow      b',      \underline{\mathrm{Hom}}(a,b')      )      \mapsto
  \underline{\mathrm{Hom}}(\alpha,\beta).
  
  7.4-6 EvaluationMorphism
  
  EvaluationMorphism( 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 evaluation morphism
  \mathrm{ev}_{a,b}:  \mathrm{\underline{Hom}}(a,b)  \otimes  a \rightarrow b,
  i.e., the counit of the tensor hom adjunction.
  
  7.4-7 EvaluationMorphismWithGivenSource
  
  EvaluationMorphismWithGivenSource( a, b, s )  operation
  Returns:  a  morphism in \mathrm{Hom}( \mathrm{\underline{Hom}}(a,b) \otimes
            a, b ).
  
  The    arguments    are    two    objects    a,b   and   an   object   s   =
  \mathrm{\underline{Hom}}(a,b)  \otimes  a.  The  output  is  the  evaluation
  morphism    \mathrm{ev}_{a,b}:   \mathrm{\underline{Hom}}(a,b)   \otimes   a
  \rightarrow b, i.e., the counit of the tensor hom adjunction.
  
  7.4-8 AddEvaluationMorphismWithGivenSource
  
  AddEvaluationMorphismWithGivenSource( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  EvaluationMorphismWithGivenSource.  F:  (a, b, \mathrm{\underline{Hom}}(a,b)
  \otimes a) \mapsto \mathrm{ev}_{a,b}.
  
  7.4-9 CoevaluationMorphism
  
  CoevaluationMorphism( a, b )  operation
  Returns:  a  morphism  in  \mathrm{Hom}(  a,  \mathrm{\underline{Hom}}(b,  a
            \otimes b) ).
  
  The  arguments  are two objects a,b. The output is the coevaluation morphism
  \mathrm{coev}_{a,b}: a \rightarrow \mathrm{\underline{Hom}(b, a \otimes b)},
  i.e., the unit of the tensor hom adjunction.
  
  7.4-10 CoevaluationMorphismWithGivenRange
  
  CoevaluationMorphismWithGivenRange( a, b, r )  operation
  Returns:  a  morphism  in  \mathrm{Hom}(  a,  \mathrm{\underline{Hom}}(b,  a
            \otimes b) ).
  
  The    arguments    are    two    objects    a,b   and   an   object   r   =
  \mathrm{\underline{Hom}(b,  a  \otimes  b)}.  The output is the coevaluation
  morphism  \mathrm{coev}_{a,b}:  a  \rightarrow  \mathrm{\underline{Hom}(b, a
  \otimes b)}, i.e., the unit of the tensor hom adjunction.
  
  7.4-11 AddCoevaluationMorphismWithGivenRange
  
  AddCoevaluationMorphismWithGivenRange( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  CoevaluationMorphismWithGivenRange.  F: (a, b, \mathrm{\underline{Hom}}(b, a
  \otimes b)) \mapsto \mathrm{coev}_{a,b}.
  
  7.4-12 TensorProductToInternalHomAdjunctionMap
  
  TensorProductToInternalHomAdjunctionMap( a, b, f )  operation
  Returns:  a morphism in \mathrm{Hom}( a, \mathrm{\underline{Hom}}(b,c) ).
  
  The  arguments  are 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.
  
  7.4-13 AddTensorProductToInternalHomAdjunctionMap
  
  AddTensorProductToInternalHomAdjunctionMap( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  TensorProductToInternalHomAdjunctionMap.   F:   (a,   b,   f:  a  \otimes  b
  \rightarrow c) \mapsto ( g: a \rightarrow \mathrm{\underline{Hom}}(b,c) ).
  
  7.4-14 InternalHomToTensorProductAdjunctionMap
  
  InternalHomToTensorProductAdjunctionMap( b, c, g )  operation
  Returns:  a morphism in \mathrm{Hom}(a \otimes b, c).
  
  The   arguments   are   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.
  
  7.4-15 AddInternalHomToTensorProductAdjunctionMap
  
  AddInternalHomToTensorProductAdjunctionMap( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  InternalHomToTensorProductAdjunctionMap.   F:   (b,   c,  g:  a  \rightarrow
  \mathrm{\underline{Hom}}(b,c)) \mapsto ( g: a \otimes b \rightarrow c ).
  
  7.4-16 MonoidalPreComposeMorphism
  
  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{MonoidalPreComposeMorphismWithGivenObjects}_{a,b,c}:
  \mathrm{\underline{Hom}}(a,b)      \otimes     \mathrm{\underline{Hom}}(b,c)
  \rightarrow \mathrm{\underline{Hom}}(a,c).
  
  7.4-17 MonoidalPreComposeMorphismWithGivenObjects
  
  MonoidalPreComposeMorphismWithGivenObjects( s, a, b, c, r )  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  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).
  
  7.4-18 AddMonoidalPreComposeMorphismWithGivenObjects
  
  AddMonoidalPreComposeMorphismWithGivenObjects( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  MonoidalPreComposeMorphismWithGivenObjects.                               F:
  (\mathrm{\underline{Hom}}(a,b)                                       \otimes
  \mathrm{\underline{Hom}}(b,c),a,b,c,\mathrm{\underline{Hom}}(a,c))   \mapsto
  \mathrm{MonoidalPreComposeMorphismWithGivenObjects}_{a,b,c}.
  
  7.4-19 MonoidalPostComposeMorphism
  
  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{MonoidalPostComposeMorphismWithGivenObjects}_{a,b,c}:
  \mathrm{\underline{Hom}}(b,c)      \otimes     \mathrm{\underline{Hom}}(a,b)
  \rightarrow \mathrm{\underline{Hom}}(a,c).
  
  7.4-20 MonoidalPostComposeMorphismWithGivenObjects
  
  MonoidalPostComposeMorphismWithGivenObjects( s, a, b, c, r )  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  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).
  
  7.4-21 AddMonoidalPostComposeMorphismWithGivenObjects
  
  AddMonoidalPostComposeMorphismWithGivenObjects( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  MonoidalPostComposeMorphismWithGivenObjects.                              F:
  (\mathrm{\underline{Hom}}(b,c)                                       \otimes
  \mathrm{\underline{Hom}}(a,b),a,b,c,\mathrm{\underline{Hom}}(a,c))   \mapsto
  \mathrm{MonoidalPostComposeMorphismWithGivenObjects}_{a,b,c}.
  
  7.4-22 DualOnObjects
  
  DualOnObjects( a )  attribute
  Returns:  an object
  
  The argument is an object a. The output is its dual object a^{\vee}.
  
  7.4-23 AddDualOnObjects
  
  AddDualOnObjects( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given function F to the category for the basic operation DualOnObjects. F: a
  \mapsto a^{\vee}.
  
  7.4-24 DualOnMorphisms
  
  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}.
  
  7.4-25 DualOnMorphismsWithGivenDuals
  
  DualOnMorphismsWithGivenDuals( s, alpha, r )  operation
  Returns:  a morphism in \mathrm{Hom}( b^{\vee}, a^{\vee} ).
  
  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}.
  
  7.4-26 AddDualOnMorphismsWithGivenDuals
  
  AddDualOnMorphismsWithGivenDuals( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  DualOnMorphismsWithGivenDuals.    F:    (b^{\vee},\alpha,a^{\vee})   \mapsto
  \alpha^{\vee}.
  
  7.4-27 EvaluationForDual
  
  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.
  
  7.4-28 EvaluationForDualWithGivenTensorProduct
  
  EvaluationForDualWithGivenTensorProduct( s, a, r )  operation
  Returns:  a morphism in \mathrm{Hom}( a^{\vee} \otimes a, 1 ).
  
  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.
  
  7.4-29 AddEvaluationForDualWithGivenTensorProduct
  
  AddEvaluationForDualWithGivenTensorProduct( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  EvaluationForDualWithGivenTensorProduct.  F:  (a^{\vee}  \otimes  a,  a,  1)
  \mapsto \mathrm{ev}_{a}.
  
  7.4-30 CoevaluationForDual
  
  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}.
  
  7.4-31 CoevaluationForDualWithGivenTensorProduct
  
  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}.
  
  7.4-32 AddCoevaluationForDualWithGivenTensorProduct
  
  AddCoevaluationForDualWithGivenTensorProduct( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  CoevaluationForDualWithGivenTensorProduct.  F:  (1,  a,  a \otimes a^{\vee})
  \mapsto \mathrm{coev}_{a}.
  
  7.4-33 MorphismToBidual
  
  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}.
  
  7.4-34 MorphismToBidualWithGivenBidual
  
  MorphismToBidualWithGivenBidual( a, r )  operation
  Returns:  a morphism in \mathrm{Hom}(a, (a^{\vee})^{\vee}).
  
  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}.
  
  7.4-35 AddMorphismToBidualWithGivenBidual
  
  AddMorphismToBidualWithGivenBidual( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  MorphismToBidualWithGivenBidual.   F:   (a,  (a^{\vee})^{\vee})  \mapsto  (a
  \rightarrow (a^{\vee})^{\vee}).
  
  7.4-36 TensorProductInternalHomCompatibilityMorphism
  
  TensorProductInternalHomCompatibilityMorphism( a, a', b, b' )  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  arguments  are  four  objects  a,  a', b, 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').
  
  7.4-37 TensorProductInternalHomCompatibilityMorphismWithGivenObjects
  
  TensorProductInternalHomCompatibilityMorphismWithGivenObjects( a, a', b, b', L )  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   arguments  are  four  objects  a,  a',  b,  b',  and  a  list  L  =  [
  \mathrm{\underline{Hom}}(a,a')    \otimes    \mathrm{\underline{Hom}}(b,b'),
  \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').
  
  7.4-38 AddTensorProductInternalHomCompatibilityMorphismWithGivenObjects
  
  AddTensorProductInternalHomCompatibilityMorphismWithGivenObjects( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  TensorProductInternalHomCompatibilityMorphismWithGivenObjects.      F:     (
  a,a',b,b',          [         \mathrm{\underline{Hom}}(a,a')         \otimes
  \mathrm{\underline{Hom}}(b,b'),   \mathrm{\underline{Hom}}(a   \otimes  b,a'
  \otimes                   b')                   ])                   \mapsto
  \mathrm{TensorProductInternalHomCompatibilityMorphismWithGivenObjects}_{a,a',b,b'}
  .
  
  7.4-39 TensorProductDualityCompatibilityMorphism
  
  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{TensorProductDualityCompatibilityMorphismWithGivenObjects}: a^{\vee}
  \otimes b^{\vee} \rightarrow (a \otimes b)^{\vee}.
  
  7.4-40 TensorProductDualityCompatibilityMorphismWithGivenObjects
  
  TensorProductDualityCompatibilityMorphismWithGivenObjects( s, a, b, r )  operation
  Returns:  a  morphism in \mathrm{Hom}( a^{\vee} \otimes b^{\vee}, (a \otimes
            b)^{\vee} ).
  
  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}.
  
  7.4-41 AddTensorProductDualityCompatibilityMorphismWithGivenObjects
  
  AddTensorProductDualityCompatibilityMorphismWithGivenObjects( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  TensorProductDualityCompatibilityMorphismWithGivenObjects.   F:  (  a^{\vee}
  \otimes    b^{\vee},    a,    b,    (a    \otimes    b)^{\vee}   )   \mapsto
  \mathrm{TensorProductDualityCompatibilityMorphismWithGivenObjects}_{a,b}.
  
  7.4-42 MorphismFromTensorProductToInternalHom
  
  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{MorphismFromTensorProductToInternalHomWithGivenObjects}_{a,b}:
  a^{\vee} \otimes b \rightarrow \mathrm{\underline{Hom}}(a,b).
  
  7.4-43 MorphismFromTensorProductToInternalHomWithGivenObjects
  
  MorphismFromTensorProductToInternalHomWithGivenObjects( s, a, b, r )  operation
  Returns:  a     morphism    in    \mathrm{Hom}(    a^{\vee}    \otimes    b,
            \mathrm{\underline{Hom}}(a,b) ).
  
  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).
  
  7.4-44 AddMorphismFromTensorProductToInternalHomWithGivenObjects
  
  AddMorphismFromTensorProductToInternalHomWithGivenObjects( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  MorphismFromTensorProductToInternalHomWithGivenObjects.    F:   (   a^{\vee}
  \otimes     b,     a,    b,    \mathrm{\underline{Hom}}(a,b)    )    \mapsto
  \mathrm{MorphismFromTensorProductToInternalHomWithGivenObjects}_{a,b}.
  
  7.4-45 IsomorphismFromTensorProductToInternalHom
  
  IsomorphismFromTensorProductToInternalHom( 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{IsomorphismFromTensorProductToInternalHom}_{a,b}: a^{\vee} \otimes b
  \rightarrow \mathrm{\underline{Hom}}(a,b).
  
  7.4-46 AddIsomorphismFromTensorProductToInternalHom
  
  AddIsomorphismFromTensorProductToInternalHom( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  IsomorphismFromTensorProductToInternalHom.    F:    (   a,   b   )   \mapsto
  \mathrm{IsomorphismFromTensorProductToInternalHom}_{a,b}.
  
  7.4-47 MorphismFromInternalHomToTensorProduct
  
  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.
  
  7.4-48 MorphismFromInternalHomToTensorProductWithGivenObjects
  
  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.
  
  7.4-49 AddMorphismFromInternalHomToTensorProductWithGivenObjects
  
  AddMorphismFromInternalHomToTensorProductWithGivenObjects( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  MorphismFromInternalHomToTensorProductWithGivenObjects.         F:         (
  \mathrm{\underline{Hom}}(a,b),a,b,a^{\vee}     \otimes     b    )    \mapsto
  \mathrm{MorphismFromInternalHomToTensorProductWithGivenObjects}_{a,b}.
  
  7.4-50 IsomorphismFromInternalHomToTensorProduct
  
  IsomorphismFromInternalHomToTensorProduct( 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{IsomorphismFromTensorProductToInternalHom},                   namely
  \mathrm{IsomorphismFromInternalHomToTensorProduct}_{a,b}:
  \mathrm{\underline{Hom}}(a,b) \rightarrow a^{\vee} \otimes b.
  
  7.4-51 AddIsomorphismFromInternalHomToTensorProduct
  
  AddIsomorphismFromInternalHomToTensorProduct( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  IsomorphismFromInternalHomToTensorProduct.    F:    (    a,b    )    \mapsto
  \mathrm{IsomorphismFromInternalHomToTensorProduct}_{a,b}.
  
  7.4-52 TraceMap
  
  TraceMap( alpha )  attribute
  Returns:  a morphism in \mathrm{Hom}(1,1).
  
  The  argument  is  a  morphism  \alpha.  The  output  is  the trace morphism
  \mathrm{trace}_{\alpha}: 1 \rightarrow 1.
  
  7.4-53 AddTraceMap
  
  AddTraceMap( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given function F to the category for the basic operation TraceMap. F: \alpha
  \mapsto \mathrm{trace}_{\alpha}
  
  7.4-54 RankMorphism
  
  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.
  
  7.4-55 AddRankMorphism
  
  AddRankMorphism( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given  function F to the category for the basic operation RankMorphism. F: a
  \mapsto \mathrm{rank}_{a}
  
  7.4-56 IsomorphismFromDualToInternalHom
  
  IsomorphismFromDualToInternalHom( a )  attribute
  Returns:  a morphism in \mathrm{Hom}(a^{\vee}, \mathrm{Hom}(a,1)).
  
  The   argument   is   an   object   a.   The   output   is  the  isomorphism
  \mathrm{IsomorphismFromDualToInternalHom}_{a}:      a^{\vee}     \rightarrow
  \mathrm{Hom}(a,1).
  
  7.4-57 AddIsomorphismFromDualToInternalHom
  
  AddIsomorphismFromDualToInternalHom( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  IsomorphismFromDualToInternalHom.           F:           a           \mapsto
  \mathrm{IsomorphismFromDualToInternalHom}_{a}
  
  7.4-58 IsomorphismFromInternalHomToDual
  
  IsomorphismFromInternalHomToDual( a )  attribute
  Returns:  a morphism in \mathrm{Hom}(\mathrm{Hom}(a,1), a^{\vee}).
  
  The   argument   is   an   object   a.   The   output   is  the  isomorphism
  \mathrm{IsomorphismFromInternalHomToDual}_{a}: \mathrm{Hom}(a,1) \rightarrow
  a^{\vee}.
  
  7.4-59 AddIsomorphismFromInternalHomToDual
  
  AddIsomorphismFromInternalHomToDual( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  IsomorphismFromInternalHomToDual.           F:           a           \mapsto
  \mathrm{IsomorphismFromInternalHomToDual}_{a}
  
  7.4-60 UniversalPropertyOfDual
  
  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}.
  
  7.4-61 AddUniversalPropertyOfDual
  
  AddUniversalPropertyOfDual( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  UniversalPropertyOfDual.  F:  (  t,a,\alpha:  t  \otimes  a  \rightarrow 1 )
  \mapsto ( t \rightarrow a^{\vee} ).
  
  7.4-62 LambdaIntroduction
  
  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.
  
  7.4-63 AddLambdaIntroduction
  
  AddLambdaIntroduction( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given function F to the category for the basic operation LambdaIntroduction.
  F:    (    \alpha:   a   \rightarrow   b   )   \mapsto   (   1   \rightarrow
  \mathrm{\underline{Hom}}(a,b) ).
  
  7.4-64 LambdaElimination
  
  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.
  
  7.4-65 AddLambdaElimination
  
  AddLambdaElimination( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given  function F to the category for the basic operation LambdaElimination.
  F:  (  a,b,\alpha: 1 \rightarrow \mathrm{\underline{Hom}}(a,b) ) \mapsto ( a
  \rightarrow b ).
  
  7.4-66 IsomorphismFromObjectToInternalHom
  
  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).
  
  7.4-67 IsomorphismFromObjectToInternalHomWithGivenInternalHom
  
  IsomorphismFromObjectToInternalHomWithGivenInternalHom( a, r )  operation
  Returns:  a morphism in \mathrm{Hom}(a, \mathrm{\underline{Hom}}(1,a)).
  
  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).
  
  7.4-68 AddIsomorphismFromObjectToInternalHomWithGivenInternalHom
  
  AddIsomorphismFromObjectToInternalHomWithGivenInternalHom( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  IsomorphismFromObjectToInternalHomWithGivenInternalHom.      F:     (     a,
  \mathrm{\underline{Hom}}(1,a)      )     \mapsto     (     a     \rightarrow
  \mathrm{\underline{Hom}}(1,a) ).
  
  7.4-69 IsomorphismFromInternalHomToObject
  
  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.
  
  7.4-70 IsomorphismFromInternalHomToObjectWithGivenInternalHom
  
  IsomorphismFromInternalHomToObjectWithGivenInternalHom( a, s )  operation
  Returns:  a morphism in \mathrm{Hom}(\mathrm{\underline{Hom}}(1,a),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.
  
  7.4-71 AddIsomorphismFromInternalHomToObjectWithGivenInternalHom
  
  AddIsomorphismFromInternalHomToObjectWithGivenInternalHom( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  IsomorphismFromInternalHomToObjectWithGivenInternalHom.      F:     (     a,
  \mathrm{\underline{Hom}}(1,a)   )  \mapsto  (  \mathrm{\underline{Hom}}(1,a)
  \rightarrow a ).
  
  
  7.5 Rigid Symmetric Closed Monoidal Categories
  
  A symmetric closed monoidal category \mathbf{C} satisfying
  
      the   natural   morphism   \underline{\mathrm{Hom}}(a_1,b_1)   \otimes
        \underline{\mathrm{Hom}}(a_2,b_2)                          \rightarrow
        \underline{\mathrm{Hom}}(a_1   \otimes  a_2,b_1  \otimes  b_2)  is  an
        isomorphism,
  
      the          natural          morphism          a          \rightarrow
        \underline{\mathrm{Hom}}(\underline{\mathrm{Hom}}(a,   1),  1)  is  an
        isomorphism
  
  is called a rigid symmetric closed monoidal category.
  
  7.5-1 TensorProductInternalHomCompatibilityMorphismInverse
  
  TensorProductInternalHomCompatibilityMorphismInverse( a, a', b, b' )  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  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').
  
  7.5-2 TensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects
  
  TensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects( a, a', b, b', L )  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  four  objects  a,  a',  b,  b',  and  a  list  L  =  [
  \mathrm{\underline{Hom}}(a,a')    \otimes    \mathrm{\underline{Hom}}(b,b'),
  \mathrm{\underline{Hom}}(a  \otimes  b,a'  \otimes  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').
  
  7.5-3 AddTensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects
  
  AddTensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  TensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects.  F:  (
  a,a',b,b',          [         \mathrm{\underline{Hom}}(a,a')         \otimes
  \mathrm{\underline{Hom}}(b,b'),   \mathrm{\underline{Hom}}(a   \otimes  b,a'
  \otimes                   b')                   ])                   \mapsto
  \mathrm{TensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects}_{a,a',b,b'}
  .
  
  7.5-4 MorphismFromBidual
  
  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.
  
  7.5-5 MorphismFromBidualWithGivenBidual
  
  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.
  
  7.5-6 AddMorphismFromBidualWithGivenBidual
  
  AddMorphismFromBidualWithGivenBidual( C, F )  operation
  Returns:  nothing
  
  The  arguments  are  a category C and a function F. This operations adds the
  given    function    F   to   the   category   for   the   basic   operation
  MorphismFromBidualWithGivenBidual.   F:   (a,   (a^{\vee})^{\vee})   \mapsto
  ((a^{\vee})^{\vee} \rightarrow a).