chap6.txt

  
  6 Universal Objects
  
  
  6.1 Kernel
  
  For a given morphism \alpha: A \rightarrow B, a kernel of \alpha consists of
  three parts:
  
      an object K,
  
      a  morphism  \iota:  K  \rightarrow  A  such  that  \alpha \circ \iota
        \sim_{K,B} 0,
  
      a  dependent  function  u  mapping each morphism \tau: T \rightarrow A
        satisfying  \alpha  \circ  \tau  \sim_{T,B} 0 to a morphism u(\tau): T
        \rightarrow K such that \iota \circ u( \tau ) \sim_{T,A} \tau.
  
  The  triple ( K, \iota, u ) is called a kernel of \alpha if the morphisms u(
  \tau  ) are uniquely determined up to congruence of morphisms. We denote the
  object  K of such a triple by \mathrm{KernelObject}(\alpha). We say that the
  morphism  u(\tau)  is  induced  by the universal property of the kernel. \\ 
  \mathrm{KernelObject}  is  a  functorial  operation.  This means: for \mu: A
  \rightarrow  A', \nu: B \rightarrow B', \alpha: A \rightarrow B, \alpha': A'
  \rightarrow  B' such that \nu \circ \alpha \sim_{A,B'} \alpha' \circ \mu, we
  obtain    a    morphism    \mathrm{KernelObject}(   \alpha   )   \rightarrow
  \mathrm{KernelObject}( \alpha' ).
  
  6.1-1 KernelObject
  
  KernelObject( alpha )  attribute
  Returns:  an object
  
  The argument is a morphism \alpha. The output is the kernel K of \alpha.
  
  6.1-2 KernelEmbedding
  
  KernelEmbedding( alpha )  attribute
  Returns:  a morphism in \mathrm{Hom}(\mathrm{KernelObject}(\alpha),A)
  
  The argument is a morphism \alpha: A \rightarrow B. The output is the kernel
  embedding \iota: \mathrm{KernelObject}(\alpha) \rightarrow A.
  
  6.1-3 KernelEmbeddingWithGivenKernelObject
  
  KernelEmbeddingWithGivenKernelObject( alpha, K )  operation
  Returns:  a morphism in \mathrm{Hom}(K,A)
  
  The  arguments  are  a  morphism  \alpha:  A \rightarrow B and an object K =
  \mathrm{KernelObject}(\alpha).  The  output is the kernel embedding \iota: K
  \rightarrow A.
  
  6.1-4 KernelLift
  
  KernelLift( alpha, tau )  operation
  Returns:  a morphism in \mathrm{Hom}(T,\mathrm{KernelObject}(\alpha))
  
  The  arguments  are  a  morphism \alpha: A \rightarrow B and a test morphism
  \tau:  T \rightarrow A satisfying \alpha \circ \tau \sim_{T,B} 0. The output
  is  the  morphism u(\tau): T \rightarrow \mathrm{KernelObject}(\alpha) given
  by the universal property of the kernel.
  
  6.1-5 KernelLiftWithGivenKernelObject
  
  KernelLiftWithGivenKernelObject( alpha, tau, K )  operation
  Returns:  a morphism in \mathrm{Hom}(T,K)
  
  The  arguments are a morphism \alpha: A \rightarrow B, a test morphism \tau:
  T \rightarrow A satisfying \alpha \circ \tau \sim_{T,B} 0, and an object K =
  \mathrm{KernelObject}(\alpha).   The  output  is  the  morphism  u(\tau):  T
  \rightarrow K given by the universal property of the kernel.
  
  6.1-6 AddKernelObject
  
  AddKernelObject( 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 KernelObject. F:
  \alpha \mapsto \mathrm{KernelObject}(\alpha).
  
  6.1-7 AddKernelEmbedding
  
  AddKernelEmbedding( 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 KernelEmbedding. F:
  \alpha \mapsto \iota.
  
  6.1-8 AddKernelEmbeddingWithGivenKernelObject
  
  AddKernelEmbeddingWithGivenKernelObject( 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
  KernelEmbeddingWithGivenKernelObject. F: (\alpha, K) \mapsto \iota.
  
  6.1-9 AddKernelLift
  
  AddKernelLift( 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 KernelLift. F:
  (\alpha, \tau) \mapsto u(\tau).
  
  6.1-10 AddKernelLiftWithGivenKernelObject
  
  AddKernelLiftWithGivenKernelObject( 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
  KernelLiftWithGivenKernelObject. F: (\alpha, \tau, K) \mapsto u.
  
  6.1-11 KernelObjectFunctorial
  
  KernelObjectFunctorial( L )  operation
  Returns:  a  morphism  in  \mathrm{Hom}(  \mathrm{KernelObject}(  \alpha  ),
            \mathrm{KernelObject}( \alpha' ) )
  
  The  argument  is a list L = [ \alpha: A \rightarrow B, [ \mu: A \rightarrow
  A',  \nu: B \rightarrow B' ], \alpha': A' \rightarrow B' ] of morphisms. The
  output   is   the   morphism  \mathrm{KernelObject}(  \alpha  )  \rightarrow
  \mathrm{KernelObject}( \alpha' ) given by the functorality of the kernel.
  
  6.1-12 KernelObjectFunctorial
  
  KernelObjectFunctorial( alpha, mu, alpha_prime )  operation
  Returns:  a  morphism  in  \mathrm{Hom}(  \mathrm{KernelObject}(  \alpha  ),
            \mathrm{KernelObject}( \alpha' ) )
  
  The   arguments  are  three  morphisms  \alpha:  A  \rightarrow  B,  \mu:  A
  \rightarrow  A',  \alpha':  A'  \rightarrow  B'.  The output is the morphism
  \mathrm{KernelObject}( \alpha ) \rightarrow \mathrm{KernelObject}( \alpha' )
  given by the functorality of the kernel.
  
  6.1-13 KernelObjectFunctorialWithGivenKernelObjects
  
  KernelObjectFunctorialWithGivenKernelObjects( s, alpha, mu, alpha_prime, r )  operation
  Returns:  a morphism in \mathrm{Hom}( s, r )
  
  The  arguments  are  an  object  s  = \mathrm{KernelObject}( \alpha ), three
  morphisms  \alpha:  A  \rightarrow  B,  \mu:  A  \rightarrow A', \alpha': A'
  \rightarrow  B',  and  an  object  r = \mathrm{KernelObject}( \alpha' ). The
  output   is   the   morphism  \mathrm{KernelObject}(  \alpha  )  \rightarrow
  \mathrm{KernelObject}( \alpha' ) given by the functorality of the kernel.
  
  6.1-14 AddKernelObjectFunctorialWithGivenKernelObjects
  
  AddKernelObjectFunctorialWithGivenKernelObjects( 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
  KernelObjectFunctorialWithGivenKernelObjects.   F:   (\mathrm{KernelObject}(
  \alpha  ),  \alpha,  \mu, \alpha', \mathrm{KernelObject}( \alpha' )) \mapsto
  (\mathrm{KernelObject}(  \alpha ) \rightarrow \mathrm{KernelObject}( \alpha'
  )).
  
  
  6.2 Cokernel
  
  For  a given morphism \alpha: A \rightarrow B, a cokernel of \alpha consists
  of three parts:
  
      an object K,
  
      a  morphism  \epsilon: B \rightarrow K such that \epsilon \circ \alpha
        \sim_{A,K} 0,
  
      a  dependent  function u mapping each \tau: B \rightarrow T satisfying
        \tau  \circ \alpha \sim_{A, T} 0 to a morphism u(\tau):K \rightarrow T
        such that u(\tau) \circ \epsilon \sim_{B,T} \tau.
  
  The  triple  (  K,  \epsilon,  u  )  is  called  a cokernel of \alpha if the
  morphisms  u(  \tau ) are uniquely determined up to congruence of morphisms.
  We  denote the object K of such a triple by \mathrm{CokernelObject}(\alpha).
  We say that the morphism u(\tau) is induced by the universal property of the
  cokernel. \\  \mathrm{CokernelObject} is a functorial operation. This means:
  for  \mu:  A \rightarrow A', \nu: B \rightarrow B', \alpha: A \rightarrow B,
  \alpha':  A'  \rightarrow  B' such that \nu \circ \alpha \sim_{A,B'} \alpha'
  \circ   \mu,   we   obtain  a  morphism  \mathrm{CokernelObject}(  \alpha  )
  \rightarrow \mathrm{CokernelObject}( \alpha' ).
  
  6.2-1 CokernelObject
  
  CokernelObject( alpha )  attribute
  Returns:  an object
  
  The  argument  is  a  morphism  \alpha:  A  \rightarrow B. The output is the
  cokernel K of \alpha.
  
  6.2-2 CokernelProjection
  
  CokernelProjection( alpha )  attribute
  Returns:  a morphism in \mathrm{Hom}(B, \mathrm{CokernelObject}( \alpha ))
  
  The  argument  is  a  morphism  \alpha:  A  \rightarrow B. The output is the
  cokernel  projection \epsilon: B \rightarrow \mathrm{CokernelObject}( \alpha
  ).
  
  6.2-3 CokernelProjectionWithGivenCokernelObject
  
  CokernelProjectionWithGivenCokernelObject( alpha, K )  operation
  Returns:  a morphism in \mathrm{Hom}(B, K)
  
  The  arguments  are  a  morphism  \alpha:  A \rightarrow B and an object K =
  \mathrm{CokernelObject}(\alpha).  The  output  is  the  cokernel  projection
  \epsilon: B \rightarrow \mathrm{CokernelObject}( \alpha ).
  
  6.2-4 CokernelColift
  
  CokernelColift( alpha, tau )  operation
  Returns:  a morphism in \mathrm{Hom}(\mathrm{CokernelObject}(\alpha),T)
  
  The  arguments  are  a  morphism \alpha: A \rightarrow B and a test morphism
  \tau: B \rightarrow T satisfying \tau \circ \alpha \sim_{A, T} 0. The output
  is the morphism u(\tau): \mathrm{CokernelObject}(\alpha) \rightarrow T given
  by the universal property of the cokernel.
  
  6.2-5 CokernelColiftWithGivenCokernelObject
  
  CokernelColiftWithGivenCokernelObject( alpha, tau, K )  operation
  Returns:  a morphism in \mathrm{Hom}(K,T)
  
  The  arguments are a morphism \alpha: A \rightarrow B, a test morphism \tau:
  B  \rightarrow T satisfying \tau \circ \alpha \sim_{A, T} 0, and an object K
  =  \mathrm{CokernelObject}(\alpha).  The  output  is the morphism u(\tau): K
  \rightarrow T given by the universal property of the cokernel.
  
  6.2-6 AddCokernelObject
  
  AddCokernelObject( 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 CokernelObject. F:
  \alpha \mapsto K.
  
  6.2-7 AddCokernelProjection
  
  AddCokernelProjection( 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 CokernelProjection.
  F: \alpha \mapsto \epsilon.
  
  6.2-8 AddCokernelProjectionWithGivenCokernelObject
  
  AddCokernelProjectionWithGivenCokernelObject( 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 CokernelProjection.
  F: (\alpha, K) \mapsto \epsilon.
  
  6.2-9 AddCokernelColift
  
  AddCokernelColift( 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 CokernelProjection.
  F: (\alpha, \tau) \mapsto u(\tau).
  
  6.2-10 AddCokernelColiftWithGivenCokernelObject
  
  AddCokernelColiftWithGivenCokernelObject( 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 CokernelProjection.
  F: (\alpha, \tau, K) \mapsto u(\tau).
  
  6.2-11 CokernelObjectFunctorial
  
  CokernelObjectFunctorial( L )  operation
  Returns:  a  morphism  in  \mathrm{Hom}(\mathrm{CokernelObject}(  \alpha  ),
            \mathrm{CokernelObject}( \alpha' ))
  
  The  argument  is  a list L = [ \alpha: A \rightarrow B, [ \mu:A \rightarrow
  A', \nu: B \rightarrow B' ], \alpha': A' \rightarrow B' ]. The output is the
  morphism       \mathrm{CokernelObject}(       \alpha      )      \rightarrow
  \mathrm{CokernelObject}(   \alpha'  )  given  by  the  functorality  of  the
  cokernel.
  
  6.2-12 CokernelObjectFunctorial
  
  CokernelObjectFunctorial( alpha, nu, alpha_prime )  operation
  Returns:  a  morphism  in  \mathrm{Hom}(\mathrm{CokernelObject}(  \alpha  ),
            \mathrm{CokernelObject}( \alpha' ))
  
  The   arguments  are  three  morphisms  \alpha:  A  \rightarrow  B,  \nu:  B
  \rightarrow  B',  \alpha':  A'  \rightarrow  B'.  The output is the morphism
  \mathrm{CokernelObject}(   \alpha   )  \rightarrow  \mathrm{CokernelObject}(
  \alpha' ) given by the functorality of the cokernel.
  
  6.2-13 CokernelObjectFunctorialWithGivenCokernelObjects
  
  CokernelObjectFunctorialWithGivenCokernelObjects( s, alpha, nu, alpha_prime, r )  operation
  Returns:  a morphism in \mathrm{Hom}(s, r)
  
  The  arguments  are  an  object s = \mathrm{CokernelObject}( \alpha ), three
  morphisms  \alpha:  A  \rightarrow  B,  \nu:  B  \rightarrow B', \alpha': A'
  \rightarrow  B',  and  an object r = \mathrm{CokernelObject}( \alpha' ). The
  output   is  the  morphism  \mathrm{CokernelObject}(  \alpha  )  \rightarrow
  \mathrm{CokernelObject}(   \alpha'  )  given  by  the  functorality  of  the
  cokernel.
  
  6.2-14 AddCokernelObjectFunctorialWithGivenCokernelObjects
  
  AddCokernelObjectFunctorialWithGivenCokernelObjects( 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
  CokernelObjectFunctorialWithGivenCokernelObjects.                         F:
  (\mathrm{CokernelObject}(     \alpha     ),     \alpha,     \nu,    \alpha',
  \mathrm{CokernelObject}( \alpha' )) \mapsto (\mathrm{CokernelObject}( \alpha
  ) \rightarrow \mathrm{CokernelObject}( \alpha' )).
  
  
  6.3 Zero Object
  
  A zero object consists of three parts:
  
      an object Z,
  
      a  function  u_{\mathrm{in}}  mapping  each  object  A  to  a morphism
        u_{\mathrm{in}}(A): A \rightarrow Z,
  
      a  function  u_{\mathrm{out}}  mapping  each  object  A  to a morphism
        u_{\mathrm{out}}(A): Z \rightarrow A.
  
  The triple (Z, u_{\mathrm{in}}, u_{\mathrm{out}}) is called a zero object if
  the   morphisms   u_{\mathrm{in}}(A),   u_{\mathrm{out}}(A)   are   uniquely
  determined  up  to congruence of morphisms. We denote the object Z of such a
  triple  by \mathrm{ZeroObject}. We say that the morphisms u_{\mathrm{in}}(A)
  and  u_{\mathrm{out}}(A)  are  induced by the universal property of the zero
  object.
  
  6.3-1 ZeroObject
  
  ZeroObject( C )  attribute
  Returns:  an object
  
  The argument is a category C. The output is a zero object Z of C.
  
  6.3-2 ZeroObject
  
  ZeroObject( c )  attribute
  Returns:  an object
  
  This is a convenience method. The argument is a cell c. The output is a zero
  object Z of the category C for which c \in C.
  
  6.3-3 MorphismFromZeroObject
  
  MorphismFromZeroObject( A )  attribute
  Returns:  a morphism in \mathrm{Hom}(\mathrm{ZeroObject}, A)
  
  This  is  a  convenience  method.  The  argument  is  an  object A. It calls
  \mathrm{UniversalMorphismFromZeroObject} on A.
  
  6.3-4 MorphismIntoZeroObject
  
  MorphismIntoZeroObject( A )  attribute
  Returns:  a morphism in \mathrm{Hom}(A, \mathrm{ZeroObject})
  
  This  is  a  convenience  method.  The  argument  is  an  object A. It calls
  \mathrm{UniversalMorphismIntoZeroObject} on A.
  
  6.3-5 UniversalMorphismFromZeroObject
  
  UniversalMorphismFromZeroObject( A )  attribute
  Returns:  a morphism in \mathrm{Hom}(\mathrm{ZeroObject}, A)
  
  The  argument  is  an  object  A.  The  output  is  the  universal  morphism
  u_{\mathrm{out}}: \mathrm{ZeroObject} \rightarrow A.
  
  6.3-6 UniversalMorphismFromZeroObjectWithGivenZeroObject
  
  UniversalMorphismFromZeroObjectWithGivenZeroObject( A, Z )  operation
  Returns:  a morphism in \mathrm{Hom}(Z, A)
  
  The  arguments  are  an object A, and a zero object Z = \mathrm{ZeroObject}.
  The output is the universal morphism u_{\mathrm{out}}: Z \rightarrow A.
  
  6.3-7 UniversalMorphismIntoZeroObject
  
  UniversalMorphismIntoZeroObject( A )  attribute
  Returns:  a morphism in \mathrm{Hom}(A, \mathrm{ZeroObject})
  
  The  argument  is  an  object  A.  The  output  is  the  universal  morphism
  u_{\mathrm{in}}: A \rightarrow \mathrm{ZeroObject}.
  
  6.3-8 UniversalMorphismIntoZeroObjectWithGivenZeroObject
  
  UniversalMorphismIntoZeroObjectWithGivenZeroObject( A, Z )  operation
  Returns:  a morphism in \mathrm{Hom}(A, Z)
  
  The  arguments  are  an object A, and a zero object Z = \mathrm{ZeroObject}.
  The output is the universal morphism u_{\mathrm{in}}: A \rightarrow Z.
  
  6.3-9 IsomorphismFromZeroObjectToInitialObject
  
  IsomorphismFromZeroObjectToInitialObject( C )  attribute
  Returns:  a        morphism       in       \mathrm{Hom}(\mathrm{ZeroObject},
            \mathrm{InitialObject})
  
  The  argument  is  a  category  C.  The  output  is  the  unique isomorphism
  \mathrm{ZeroObject} \rightarrow \mathrm{InitialObject}.
  
  6.3-10 IsomorphismFromInitialObjectToZeroObject
  
  IsomorphismFromInitialObjectToZeroObject( C )  attribute
  Returns:  a       morphism      in      \mathrm{Hom}(\mathrm{InitialObject},
            \mathrm{ZeroObject})
  
  The  argument  is  a  category  C.  The  output  is  the  unique isomorphism
  \mathrm{InitialObject} \rightarrow \mathrm{ZeroObject}.
  
  6.3-11 IsomorphismFromZeroObjectToTerminalObject
  
  IsomorphismFromZeroObjectToTerminalObject( C )  attribute
  Returns:  a        morphism       in       \mathrm{Hom}(\mathrm{ZeroObject},
            \mathrm{TerminalObject})
  
  The  argument  is  a  category  C.  The  output  is  the  unique isomorphism
  \mathrm{ZeroObject} \rightarrow \mathrm{TerminalObject}.
  
  6.3-12 IsomorphismFromTerminalObjectToZeroObject
  
  IsomorphismFromTerminalObjectToZeroObject( C )  attribute
  Returns:  a      morphism      in      \mathrm{Hom}(\mathrm{TerminalObject},
            \mathrm{ZeroObject})
  
  The  argument  is  a  category  C.  The  output  is  the  unique isomorphism
  \mathrm{TerminalObject} \rightarrow \mathrm{ZeroObject}.
  
  6.3-13 AddZeroObject
  
  AddZeroObject( 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 ZeroObject. F: ()
  \mapsto \mathrm{ZeroObject}.
  
  6.3-14 AddUniversalMorphismIntoZeroObject
  
  AddUniversalMorphismIntoZeroObject( 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
  UniversalMorphismIntoZeroObject. F: A \mapsto u_{\mathrm{in}}(A).
  
  6.3-15 AddUniversalMorphismIntoZeroObjectWithGivenZeroObject
  
  AddUniversalMorphismIntoZeroObjectWithGivenZeroObject( 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
  UniversalMorphismIntoZeroObjectWithGivenZeroObject.   F:   (A,   Z)  \mapsto
  u_{\mathrm{in}}(A).
  
  6.3-16 AddUniversalMorphismFromZeroObject
  
  AddUniversalMorphismFromZeroObject( 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
  UniversalMorphismFromZeroObject. F: A \mapsto u_{\mathrm{out}}(A).
  
  6.3-17 AddUniversalMorphismFromZeroObjectWithGivenZeroObject
  
  AddUniversalMorphismFromZeroObjectWithGivenZeroObject( 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
  UniversalMorphismFromZeroObjectWithGivenZeroObject.    F:    (A,Z)   \mapsto
  u_{\mathrm{out}}(A).
  
  6.3-18 AddIsomorphismFromZeroObjectToInitialObject
  
  AddIsomorphismFromZeroObjectToInitialObject( 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
  IsomorphismFromZeroObjectToInitialObject. F: () \mapsto (\mathrm{ZeroObject}
  \rightarrow \mathrm{InitialObject}).
  
  6.3-19 AddIsomorphismFromInitialObjectToZeroObject
  
  AddIsomorphismFromInitialObjectToZeroObject( 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
  IsomorphismFromInitialObjectToZeroObject.      F:      ()      \mapsto     (
  \mathrm{InitialObject} \rightarrow \mathrm{ZeroObject}).
  
  6.3-20 AddIsomorphismFromZeroObjectToTerminalObject
  
  AddIsomorphismFromZeroObjectToTerminalObject( 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
  IsomorphismFromZeroObjectToTerminalObject.        F:        ()       \mapsto
  (\mathrm{ZeroObject} \rightarrow \mathrm{TerminalObject}).
  
  6.3-21 AddIsomorphismFromTerminalObjectToZeroObject
  
  AddIsomorphismFromTerminalObjectToZeroObject( 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
  IsomorphismFromTerminalObjectToZeroObject.      F:      ()     \mapsto     (
  \mathrm{TerminalObject} \rightarrow \mathrm{ZeroObject}).
  
  6.3-22 ZeroObjectFunctorial
  
  ZeroObjectFunctorial( C )  attribute
  Returns:  a        morphism       in       \mathrm{Hom}(\mathrm{ZeroObject},
            \mathrm{ZeroObject} )
  
  The   argument   is  a  category  C.  The  output  is  the  unique  morphism
  \mathrm{ZeroObject} \rightarrow \mathrm{ZeroObject}.
  
  6.3-23 AddZeroObjectFunctorial
  
  AddZeroObjectFunctorial( 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
  ZeroObjectFunctorial. F: () \mapsto (T \rightarrow T).
  
  
  6.4 Terminal Object
  
  A terminal object consists of two parts:
  
      an object T,
  
      a function u mapping each object A to a morphism u( A ): A \rightarrow
        T.
  
  The  pair  (  T, u ) is called a terminal object if the morphisms u( A ) are
  uniquely determined up to congruence of morphisms. We denote the object T of
  such  a  pair by \mathrm{TerminalObject}. We say that the morphism u( A ) is
  induced   by   the   universal   property   of  the  terminal  object.  \\  
  \mathrm{TerminalObject}  is  a  functorial operation. This just means: There
  exists a unique morphism T \rightarrow T.
  
  6.4-1 TerminalObject
  
  TerminalObject( C )  attribute
  Returns:  an object
  
  The argument is a category C. The output is a terminal object T of C.
  
  6.4-2 TerminalObject
  
  TerminalObject( c )  attribute
  Returns:  an object
  
  This  is  a  convenience  method.  The argument is a cell c. The output is a
  terminal object T of the category C for which c \in C.
  
  6.4-3 UniversalMorphismIntoTerminalObject
  
  UniversalMorphismIntoTerminalObject( A )  attribute
  Returns:  a morphism in \mathrm{Hom}( A, \mathrm{TerminalObject} )
  
  The  argument  is  an object A. The output is the universal morphism u(A): A
  \rightarrow \mathrm{TerminalObject}.
  
  6.4-4 UniversalMorphismIntoTerminalObjectWithGivenTerminalObject
  
  UniversalMorphismIntoTerminalObjectWithGivenTerminalObject( A, T )  operation
  Returns:  a morphism in \mathrm{Hom}( A, T )
  
  The argument are an object A, and an object T = \mathrm{TerminalObject}. The
  output is the universal morphism u(A): A \rightarrow T.
  
  6.4-5 AddTerminalObject
  
  AddTerminalObject( 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 TerminalObject. F:
  () \mapsto T.
  
  6.4-6 AddUniversalMorphismIntoTerminalObject
  
  AddUniversalMorphismIntoTerminalObject( 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
  UniversalMorphismIntoTerminalObject. F: A \mapsto u(A).
  
  6.4-7 AddUniversalMorphismIntoTerminalObjectWithGivenTerminalObject
  
  AddUniversalMorphismIntoTerminalObjectWithGivenTerminalObject( 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
  UniversalMorphismIntoTerminalObjectWithGivenTerminalObject. F: (A,T) \mapsto
  u(A).
  
  6.4-8 TerminalObjectFunctorial
  
  TerminalObjectFunctorial( C )  attribute
  Returns:  a      morphism      in      \mathrm{Hom}(\mathrm{TerminalObject},
            \mathrm{TerminalObject} )
  
  The   argument   is  a  category  C.  The  output  is  the  unique  morphism
  \mathrm{TerminalObject} \rightarrow \mathrm{TerminalObject}.
  
  6.4-9 AddTerminalObjectFunctorial
  
  AddTerminalObjectFunctorial( 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
  TerminalObjectFunctorial. F: () \mapsto (T \rightarrow T).
  
  
  6.5 Initial Object
  
  An initial object consists of two parts:
  
      an object I,
  
      a function u mapping each object A to a morphism u( A ): I \rightarrow
        A.
  
  The pair (I,u) is called a initial object if the morphisms u(A) are uniquely
  determined  up  to congruence of morphisms. We denote the object I of such a
  triple by \mathrm{InitialObject}. We say that the morphism u( A ) is induced
  by  the universal property of the initial object. \\  \mathrm{InitialObject}
  is  a functorial operation. This just means: There exists a unique morphisms
  I \rightarrow I.
  
  6.5-1 InitialObject
  
  InitialObject( C )  attribute
  Returns:  an object
  
  The argument is a category C. The output is an initial object I of C.
  
  6.5-2 InitialObject
  
  InitialObject( c )  attribute
  Returns:  an object
  
  This  is  a  convenience  method. The argument is a cell c. The output is an
  initial object I of the category C for which c \in C.
  
  6.5-3 UniversalMorphismFromInitialObject
  
  UniversalMorphismFromInitialObject( A )  attribute
  Returns:  a morphism in \mathrm{Hom}(\mathrm{InitialObject} \rightarrow A).
  
  The  argument  is  an  object  A. The output is the universal morphism u(A):
  \mathrm{InitialObject} \rightarrow A.
  
  6.5-4 UniversalMorphismFromInitialObjectWithGivenInitialObject
  
  UniversalMorphismFromInitialObjectWithGivenInitialObject( A, I )  operation
  Returns:  a morphism in \mathrm{Hom}(\mathrm{InitialObject} \rightarrow A).
  
  The arguments are an object A, and an object I = \mathrm{InitialObject}. The
  output is the universal morphism u(A): \mathrm{InitialObject} \rightarrow A.
  
  6.5-5 AddInitialObject
  
  AddInitialObject( 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 InitialObject. F:
  () \mapsto I.
  
  6.5-6 AddUniversalMorphismFromInitialObject
  
  AddUniversalMorphismFromInitialObject( 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
  UniversalMorphismFromInitialObject. F: A \mapsto u(A).
  
  6.5-7 AddUniversalMorphismFromInitialObjectWithGivenInitialObject
  
  AddUniversalMorphismFromInitialObjectWithGivenInitialObject( 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
  UniversalMorphismFromInitialObjectWithGivenInitialObject.  F:  (A,I) \mapsto
  u(A).
  
  6.5-8 InitialObjectFunctorial
  
  InitialObjectFunctorial( C )  attribute
  Returns:  a     morphism     in     \mathrm{Hom}(    \mathrm{InitialObject},
            \mathrm{InitialObject} )
  
  The   argument   is  a  category  C.  The  output  is  the  unique  morphism
  \mathrm{InitialObject} \rightarrow \mathrm{InitialObject}.
  
  6.5-9 AddInitialObjectFunctorial
  
  AddInitialObjectFunctorial( 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
  InitialObjectFunctorial. F: () \rightarrow ( I \rightarrow I ).
  
  
  6.6 Direct Sum
  
  For  a  given  list  D  =  (S_1, \dots, S_n) in an Ab-category, a direct sum
  consists of five parts:
  
      an object S,
  
      a list of morphisms \pi = (\pi_i: S \rightarrow S_i)_{i = 1 \dots n},
  
      a  list of morphisms \iota = (\iota_i: S_i \rightarrow S)_{i = 1 \dots
        n},
  
      a  dependent  function  u_{\mathrm{in}}  mapping  every  list \tau = (
        \tau_i:   T   \rightarrow  S_i  )_{i  =  1  \dots  n}  to  a  morphism
        u_{\mathrm{in}}(\tau):   T   \rightarrow   S  such  that  \pi_i  \circ
        u_{\mathrm{in}}(\tau) \sim_{T,S_i} \tau_i for all i = 1, \dots, n.
  
      a  dependent  function  u_{\mathrm{out}}  mapping  every list \tau = (
        \tau_i:   S_i   \rightarrow  T  )_{i  =  1  \dots  n}  to  a  morphism
        u_{\mathrm{out}}(\tau):      S     \rightarrow     T     such     that
        u_{\mathrm{out}}(\tau)  \circ \iota_i \sim_{S_i, T} \tau_i for all i =
        1, \dots, n,
  
  such that
  
      \sum_{i=1}^{n} \iota_i \circ \pi_i = \mathrm{id}_S,
  
      \pi_j \circ \iota_i = \delta_{i,j},
  
  where  \delta_{i,j} \in \mathrm{Hom}( S_i, S_j ) is the identity if i=j, and
  0  otherwise. The 5-tuple (S, \pi, \iota, u_{\mathrm{in}}, u_{\mathrm{out}})
  is  called  a  direct  sum of D. We denote the object S of such a 5-tuple by
  \bigoplus_{i=1}^n  S_i.  We  say  that  the morphisms u_{\mathrm{in}}(\tau),
  u_{\mathrm{out}}(\tau)  are  induced by the universal property of the direct
  sum.  \\    \mathrm{DirectSum}  is  a  functorial operation. This means: For
  (\mu_i:   S_i   \rightarrow   S'_i)_{i=1\dots   n},  we  obtain  a  morphism
  \bigoplus_{i=1}^n S_i \rightarrow \bigoplus_{i=1}^n S_i'.
  
  6.6-1 DirectSumOp
  
  DirectSumOp( D, method_selection_object )  operation
  Returns:  an object
  
  The  argument  is  a list of objects D = (S_1, \dots, S_n) and an object for
  method selection. The output is the direct sum \bigoplus_{i=1}^n S_i.
  
  6.6-2 ProjectionInFactorOfDirectSum
  
  ProjectionInFactorOfDirectSum( D, k )  operation
  Returns:  a morphism in \mathrm{Hom}( \bigoplus_{i=1}^n S_i, S_k )
  
  The  arguments are a list of objects D = (S_1, \dots, S_n) and an integer k.
  The  output  is the k-th projection \pi_k: \bigoplus_{i=1}^n S_i \rightarrow
  S_k.
  
  6.6-3 ProjectionInFactorOfDirectSumOp
  
  ProjectionInFactorOfDirectSumOp( D, k, method_selection_object )  operation
  Returns:  a morphism in \mathrm{Hom}( \bigoplus_{i=1}^n S_i, S_k )
  
  The arguments are a list of objects D = (S_1, \dots, S_n), an integer k, and
  an  object  for  method  selection. The output is the k-th projection \pi_k:
  \bigoplus_{i=1}^n S_i \rightarrow S_k.
  
  6.6-4 ProjectionInFactorOfDirectSumWithGivenDirectSum
  
  ProjectionInFactorOfDirectSumWithGivenDirectSum( D, k, S )  operation
  Returns:  a morphism in \mathrm{Hom}( S, S_k )
  
  The arguments are a list of objects D = (S_1, \dots, S_n), an integer k, and
  an  object  S  =  \bigoplus_{i=1}^n  S_i.  The output is the k-th projection
  \pi_k: S \rightarrow S_k.
  
  6.6-5 InjectionOfCofactorOfDirectSum
  
  InjectionOfCofactorOfDirectSum( D, k )  operation
  Returns:  a morphism in \mathrm{Hom}( S_k, \bigoplus_{i=1}^n S_i )
  
  The  arguments are a list of objects D = (S_1, \dots, S_n) and an integer k.
  The  output is the k-th injection \iota_k: S_k \rightarrow \bigoplus_{i=1}^n
  S_i.
  
  6.6-6 InjectionOfCofactorOfDirectSumOp
  
  InjectionOfCofactorOfDirectSumOp( D, k, method_selection_object )  operation
  Returns:  a morphism in \mathrm{Hom}( S_k, \bigoplus_{i=1}^n S_i )
  
  The arguments are a list of objects D = (S_1, \dots, S_n), an integer k, and
  an  object  for  method selection. The output is the k-th injection \iota_k:
  S_k \rightarrow \bigoplus_{i=1}^n S_i.
  
  6.6-7 InjectionOfCofactorOfDirectSumWithGivenDirectSum
  
  InjectionOfCofactorOfDirectSumWithGivenDirectSum( D, k, S )  operation
  Returns:  a morphism in \mathrm{Hom}( S_k, S )
  
  The arguments are a list of objects D = (S_1, \dots, S_n), an integer k, and
  an  object  S  =  \bigoplus_{i=1}^n  S_i.  The  output is the k-th injection
  \iota_k: S_k \rightarrow S.
  
  6.6-8 UniversalMorphismIntoDirectSum
  
  UniversalMorphismIntoDirectSum( arg )  function
  Returns:  a morphism in \mathrm{Hom}(T, \bigoplus_{i=1}^n S_i)
  
  This  is  a  convenience  method. There are three different ways to use this
  method:
  
      The  arguments  are a list of objects D = (S_1, \dots, S_n) and a list
        of morphisms \tau = ( \tau_i: T \rightarrow S_i )_{i = 1 \dots n}.
  
      The argument is a list of morphisms \tau = ( \tau_i: T \rightarrow S_i
        )_{i = 1 \dots n}.
  
      The  arguments are morphisms \tau_1: T \rightarrow S_1, \dots, \tau_n:
        T \rightarrow S_n.
  
  The   output   is   the   morphism   u_{\mathrm{in}}(\tau):   T  \rightarrow
  \bigoplus_{i=1}^n S_i given by the universal property of the direct sum.
  
  6.6-9 UniversalMorphismIntoDirectSumOp
  
  UniversalMorphismIntoDirectSumOp( D, tau, method_selection_object )  operation
  Returns:  a morphism in \mathrm{Hom}(T, \bigoplus_{i=1}^n S_i)
  
  The  arguments  are  a  list  of  objects  D  = (S_1, \dots, S_n), a list of
  morphisms  \tau  =  (  \tau_i:  T  \rightarrow S_i )_{i = 1 \dots n}, and an
  object    for    method    selection.    The    output   is   the   morphism
  u_{\mathrm{in}}(\tau):  T  \rightarrow  \bigoplus_{i=1}^n  S_i  given by the
  universal property of the direct sum.
  
  6.6-10 UniversalMorphismIntoDirectSumWithGivenDirectSum
  
  UniversalMorphismIntoDirectSumWithGivenDirectSum( D, tau, S )  operation
  Returns:  a morphism in \mathrm{Hom}(T, S)
  
  The  arguments  are  a  list  of  objects  D  = (S_1, \dots, S_n), a list of
  morphisms  \tau  =  (  \tau_i:  T  \rightarrow S_i )_{i = 1 \dots n}, and an
  object   S   =   \bigoplus_{i=1}^n   S_i.   The   output   is  the  morphism
  u_{\mathrm{in}}(\tau):  T  \rightarrow  S given by the universal property of
  the direct sum.
  
  6.6-11 UniversalMorphismFromDirectSum
  
  UniversalMorphismFromDirectSum( arg )  function
  Returns:  a morphism in \mathrm{Hom}(\bigoplus_{i=1}^n S_i, T)
  
  This  is  a  convenience  method. There are three different ways to use this
  method:
  
      The  arguments  are a list of objects D = (S_1, \dots, S_n) and a list
        of morphisms \tau = ( \tau_i: S_i \rightarrow T )_{i = 1 \dots n}.
  
      The argument is a list of morphisms \tau = ( \tau_i: S_i \rightarrow T
        )_{i = 1 \dots n}.
  
      The  arguments are morphisms S_1 \rightarrow T, \dots, S_n \rightarrow
        T.
  
  The  output  is  the  morphism u_{\mathrm{out}}(\tau): \bigoplus_{i=1}^n S_i
  \rightarrow T given by the universal property of the direct sum.
  
  6.6-12 UniversalMorphismFromDirectSumOp
  
  UniversalMorphismFromDirectSumOp( D, tau, method_selection_object )  operation
  Returns:  a morphism in \mathrm{Hom}(\bigoplus_{i=1}^n S_i, T)
  
  The  arguments  are  a  list  of  objects  D  = (S_1, \dots, S_n), a list of
  morphisms  \tau  =  (  \tau_i:  S_i  \rightarrow T )_{i = 1 \dots n}, and an
  object    for    method    selection.    The    output   is   the   morphism
  u_{\mathrm{out}}(\tau):  \bigoplus_{i=1}^n  S_i  \rightarrow  T given by the
  universal property of the direct sum.
  
  6.6-13 UniversalMorphismFromDirectSumWithGivenDirectSum
  
  UniversalMorphismFromDirectSumWithGivenDirectSum( D, tau, S )  operation
  Returns:  a morphism in \mathrm{Hom}(S, T)
  
  The  arguments  are  a  list  of  objects  D  = (S_1, \dots, S_n), a list of
  morphisms  \tau  =  (  \tau_i:  S_i  \rightarrow T )_{i = 1 \dots n}, and an
  object   S   =   \bigoplus_{i=1}^n   S_i.   The   output   is  the  morphism
  u_{\mathrm{out}}(\tau):  S  \rightarrow T given by the universal property of
  the direct sum.
  
  6.6-14 IsomorphismFromDirectSumToDirectProduct
  
  IsomorphismFromDirectSumToDirectProduct( D )  operation
  Returns:  a     morphism    in    \mathrm{Hom}(    \bigoplus_{i=1}^n    S_i,
            \prod_{i=1}^{n}S_i )
  
  The  argument  is a list of objects D = (S_1, \dots, S_n). The output is the
  canonical isomorphism \bigoplus_{i=1}^n S_i \rightarrow \prod_{i=1}^{n}S_i.
  
  6.6-15 IsomorphismFromDirectSumToDirectProductOp
  
  IsomorphismFromDirectSumToDirectProductOp( D, method_selection_object )  operation
  Returns:  a     morphism    in    \mathrm{Hom}(    \bigoplus_{i=1}^n    S_i,
            \prod_{i=1}^{n}S_i )
  
  The  arguments are a list of objects D = (S_1, \dots, S_n) and an object for
  method  selection. The output is the canonical isomorphism \bigoplus_{i=1}^n
  S_i \rightarrow \prod_{i=1}^{n}S_i.
  
  6.6-16 IsomorphismFromDirectProductToDirectSum
  
  IsomorphismFromDirectProductToDirectSum( D )  operation
  Returns:  a  morphism in \mathrm{Hom}( \prod_{i=1}^{n}S_i, \bigoplus_{i=1}^n
            S_i )
  
  The  argument  is a list of objects D = (S_1, \dots, S_n). The output is the
  canonical isomorphism \prod_{i=1}^{n}S_i \rightarrow \bigoplus_{i=1}^n S_i.
  
  6.6-17 IsomorphismFromDirectProductToDirectSumOp
  
  IsomorphismFromDirectProductToDirectSumOp( D, method_selection_object )  operation
  Returns:  a  morphism in \mathrm{Hom}( \prod_{i=1}^{n}S_i, \bigoplus_{i=1}^n
            S_i )
  
  The  argument  is  a list of objects D = (S_1, \dots, S_n) and an object for
  method selection. The output is the canonical isomorphism \prod_{i=1}^{n}S_i
  \rightarrow \bigoplus_{i=1}^n S_i.
  
  6.6-18 IsomorphismFromDirectSumToCoproduct
  
  IsomorphismFromDirectSumToCoproduct( D )  operation
  Returns:  a     morphism    in    \mathrm{Hom}(    \bigoplus_{i=1}^n    S_i,
            \bigsqcup_{i=1}^{n}S_i )
  
  The  argument  is a list of objects D = (S_1, \dots, S_n). The output is the
  canonical       isomorphism      \bigoplus_{i=1}^n      S_i      \rightarrow
  \bigsqcup_{i=1}^{n}S_i.
  
  6.6-19 IsomorphismFromDirectSumToCoproductOp
  
  IsomorphismFromDirectSumToCoproductOp( D, method_selection_object )  operation
  Returns:  a     morphism    in    \mathrm{Hom}(    \bigoplus_{i=1}^n    S_i,
            \bigsqcup_{i=1}^{n}S_i )
  
  The  argument  is  a list of objects D = (S_1, \dots, S_n) and an object for
  method  selection. The output is the canonical isomorphism \bigoplus_{i=1}^n
  S_i \rightarrow \bigsqcup_{i=1}^{n}S_i.
  
  6.6-20 IsomorphismFromCoproductToDirectSum
  
  IsomorphismFromCoproductToDirectSum( D )  operation
  Returns:  a     morphism     in     \mathrm{Hom}(    \bigsqcup_{i=1}^{n}S_i,
            \bigoplus_{i=1}^n S_i )
  
  The  argument  is a list of objects D = (S_1, \dots, S_n). The output is the
  canonical  isomorphism  \bigsqcup_{i=1}^{n}S_i \rightarrow \bigoplus_{i=1}^n
  S_i.
  
  6.6-21 IsomorphismFromCoproductToDirectSumOp
  
  IsomorphismFromCoproductToDirectSumOp( D, method_selection_object )  operation
  Returns:  a     morphism     in     \mathrm{Hom}(    \bigsqcup_{i=1}^{n}S_i,
            \bigoplus_{i=1}^n S_i )
  
  The  argument  is  a list of objects D = (S_1, \dots, S_n) and an object for
  method    selection.    The    output    is    the   canonical   isomorphism
  \bigsqcup_{i=1}^{n}S_i \rightarrow \bigoplus_{i=1}^n S_i.
  
  6.6-22 MorphismBetweenDirectSums
  
  MorphismBetweenDirectSums( M )  operation
  MorphismBetweenDirectSums( S, M, T )  operation
  Returns:  a       morphism      in      \mathrm{Hom}(\bigoplus_{i=1}^{m}A_i,
            \bigoplus_{j=1}^n B_j)
  
  The  argument M = ( ( \phi_{i,j}: A_i \rightarrow B_j )_{j = 1 \dots n} )_{i
  =  1  \dots  m}  is a list of lists of morphisms. The output is the morphism
  \bigoplus_{i=1}^{m}A_i  \rightarrow  \bigoplus_{j=1}^n  B_j  defined  by the
  matrix   M.   The  extra  arguments  S  =  \bigoplus_{i=1}^{m}A_i  and  T  =
  \bigoplus_{j=1}^n  B_j  are  source  and target of the output, respectively.
  They must be provided in case M is an empty list or a list of empty lists.
  
  6.6-23 MorphismBetweenDirectSumsOp
  
  MorphismBetweenDirectSumsOp( M, m, n, method_selection_morphism )  operation
  Returns:  a       morphism      in      \mathrm{Hom}(\bigoplus_{i=1}^{m}A_i,
            \bigoplus_{j=1}^n B_j)
  
  The  arguments  are  a list M = ( \phi_{1,1}, \phi_{1,2}, \dots, \phi_{1,n},
  \phi_{2,1},  \dots,  \phi_{m,n}  )  of morphisms \phi_{i,j}: A_i \rightarrow
  B_j, an integer m, an integer n, and a method selection morphism. The output
  is  the  morphism  \bigoplus_{i=1}^{m}A_i  \rightarrow \bigoplus_{j=1}^n B_j
  defined by the list M regarded as a matrix of dimension m \times n.
  
  6.6-24 AddProjectionInFactorOfDirectSum
  
  AddProjectionInFactorOfDirectSum( 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
  ProjectionInFactorOfDirectSum. F: (D,k) \mapsto \pi_{k}.
  
  6.6-25 AddProjectionInFactorOfDirectSumWithGivenDirectSum
  
  AddProjectionInFactorOfDirectSumWithGivenDirectSum( 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
  ProjectionInFactorOfDirectSumWithGivenDirectSum. F: (D,k,S) \mapsto \pi_{k}.
  
  6.6-26 AddInjectionOfCofactorOfDirectSum
  
  AddInjectionOfCofactorOfDirectSum( 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
  InjectionOfCofactorOfDirectSum. F: (D,k) \mapsto \iota_{k}.
  
  6.6-27 AddInjectionOfCofactorOfDirectSumWithGivenDirectSum
  
  AddInjectionOfCofactorOfDirectSumWithGivenDirectSum( 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
  InjectionOfCofactorOfDirectSumWithGivenDirectSum.    F:    (D,k,S)   \mapsto
  \iota_{k}.
  
  6.6-28 AddUniversalMorphismIntoDirectSum
  
  AddUniversalMorphismIntoDirectSum( 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
  UniversalMorphismIntoDirectSum. F: (D,\tau) \mapsto u_{\mathrm{in}}(\tau).
  
  6.6-29 AddUniversalMorphismIntoDirectSumWithGivenDirectSum
  
  AddUniversalMorphismIntoDirectSumWithGivenDirectSum( 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
  UniversalMorphismIntoDirectSumWithGivenDirectSum.   F:   (D,\tau,S)  \mapsto
  u_{\mathrm{in}}(\tau).
  
  6.6-30 AddUniversalMorphismFromDirectSum
  
  AddUniversalMorphismFromDirectSum( 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
  UniversalMorphismFromDirectSum. F: (D,\tau) \mapsto u_{\mathrm{out}}(\tau).
  
  6.6-31 AddUniversalMorphismFromDirectSumWithGivenDirectSum
  
  AddUniversalMorphismFromDirectSumWithGivenDirectSum( 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
  UniversalMorphismFromDirectSumWithGivenDirectSum.   F:   (D,\tau,S)  \mapsto
  u_{\mathrm{out}}(\tau).
  
  6.6-32 AddIsomorphismFromDirectSumToDirectProduct
  
  AddIsomorphismFromDirectSumToDirectProduct( 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
  IsomorphismFromDirectSumToDirectProduct. F: D \mapsto (\bigoplus_{i=1}^n S_i
  \rightarrow \prod_{i=1}^{n}S_i).
  
  6.6-33 AddIsomorphismFromDirectProductToDirectSum
  
  AddIsomorphismFromDirectProductToDirectSum( 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
  IsomorphismFromDirectProductToDirectSum.  F:  D \mapsto ( \prod_{i=1}^{n}S_i
  \rightarrow \bigoplus_{i=1}^n S_i ).
  
  6.6-34 AddIsomorphismFromDirectSumToCoproduct
  
  AddIsomorphismFromDirectSumToCoproduct( 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
  IsomorphismFromDirectSumToCoproduct.  F:  D  \mapsto ( \bigoplus_{i=1}^n S_i
  \rightarrow \bigsqcup_{i=1}^{n}S_i ).
  
  6.6-35 AddIsomorphismFromCoproductToDirectSum
  
  AddIsomorphismFromCoproductToDirectSum( 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
  IsomorphismFromCoproductToDirectSum.  F:  D \mapsto ( \bigsqcup_{i=1}^{n}S_i
  \rightarrow \bigoplus_{i=1}^n S_i ).
  
  6.6-36 AddDirectSum
  
  AddDirectSum( 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 DirectSum. F: D
  \mapsto \bigoplus_{i=1}^n S_i.
  
  6.6-37 DirectSumFunctorial
  
  DirectSumFunctorial( L )  operation
  Returns:  a     morphism    in    \mathrm{Hom}(    \bigoplus_{i=1}^n    S_i,
            \bigoplus_{i=1}^n S_i' )
  
  The  argument  is  a  list  of  morphisms L = ( \mu_1: S_1 \rightarrow S_1',
  \dots,   \mu_n:   S_n   \rightarrow   S_n'  ).  The  output  is  a  morphism
  \bigoplus_{i=1}^n  S_i  \rightarrow  \bigoplus_{i=1}^n  S_i'  given  by  the
  functorality of the direct sum.
  
  6.6-38 DirectSumFunctorialWithGivenDirectSums
  
  DirectSumFunctorialWithGivenDirectSums( d_1, L, d_2 )  operation
  Returns:  a morphism in \mathrm{Hom}( d_1, d_2 )
  
  The arguments are an object d_1 = \bigoplus_{i=1}^n S_i, a list of morphisms
  L = ( \mu_1: S_1 \rightarrow S_1', \dots, \mu_n: S_n \rightarrow S_n' ), and
  an  object  d_2  =  \bigoplus_{i=1}^n  S_i'.  The  output  is a morphism d_1
  \rightarrow d_2 given by the functorality of the direct sum.
  
  6.6-39 AddDirectSumFunctorialWithGivenDirectSums
  
  AddDirectSumFunctorialWithGivenDirectSums( 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
  DirectSumFunctorialWithGivenDirectSums.  F: (\bigoplus_{i=1}^n S_i, ( \mu_1,
  \dots,  \mu_n  ),  \bigoplus_{i=1}^n  S_i')  \mapsto  (\bigoplus_{i=1}^n S_i
  \rightarrow \bigoplus_{i=1}^n S_i').
  
  
  6.7 Coproduct
  
  For  a  given  list  of  objects  D  = ( I_1, \dots, I_n ), a coproduct of D
  consists of three parts:
  
      an object I,
  
      a  list  of  morphisms  \iota  = ( \iota_i: I_i \rightarrow I )_{i = 1
        \dots n}
  
      a dependent function u mapping each list of morphisms \tau = ( \tau_i:
        I_i \rightarrow T ) to a morphism u( \tau ): I \rightarrow T such that
        u( \tau ) \circ \iota_i \sim_{I_i, T} \tau_i for all i = 1, \dots, n.
  
  The  triple  (  I, \iota, u ) is called a coproduct of D if the morphisms u(
  \tau  ) are uniquely determined up to congruence of morphisms. We denote the
  object I of such a triple by \bigsqcup_{i=1}^n I_i. We say that the morphism
  u(  \tau  )  is  induced  by  the  universal  property of the coproduct. \\ 
  \mathrm{Coproduct}  is  a  functorial operation. This means: For (\mu_i: I_i
  \rightarrow  I'_i)_{i=1\dots  n}, we obtain a morphism \bigsqcup_{i=1}^n I_i
  \rightarrow \bigsqcup_{i=1}^n I_i'.
  
  6.7-1 Coproduct
  
  Coproduct( D )  attribute
  Returns:  an object
  
  The argument is a list of objects D = ( I_1, \dots, I_n ). The output is the
  coproduct \bigsqcup_{i=1}^n I_i.
  
  6.7-2 Coproduct
  
  Coproduct( I1, I2 )  operation
  Returns:  an object
  
  This  is  a  convenience method. The arguments are two objects I_1, I_2. The
  output is the coproduct I_1 \bigsqcup I_2.
  
  6.7-3 Coproduct
  
  Coproduct( I1, I2 )  operation
  Returns:  an object
  
  This is a convenience method. The arguments are three objects I_1, I_2, I_3.
  The output is the coproduct I_1 \bigsqcup I_2 \bigsqcup I_3.
  
  6.7-4 CoproductOp
  
  CoproductOp( D, method_selection_object )  operation
  Returns:  an object
  
  The  arguments  are  a  list of objects D = ( I_1, \dots, I_n ) and a method
  selection object. The output is the coproduct \bigsqcup_{i=1}^n I_i.
  
  6.7-5 InjectionOfCofactorOfCoproduct
  
  InjectionOfCofactorOfCoproduct( D, k )  operation
  Returns:  a morphism in \mathrm{Hom}(I_k, \bigsqcup_{i=1}^n I_i)
  
  The  arguments  are a list of objects D = ( I_1, \dots, I_n ) and an integer
  k.   The   output   is   the   k-th   injection   \iota_k:  I_k  \rightarrow
  \bigsqcup_{i=1}^n I_i.
  
  6.7-6 InjectionOfCofactorOfCoproductOp
  
  InjectionOfCofactorOfCoproductOp( D, k, method_selection_object )  operation
  Returns:  a morphism in \mathrm{Hom}(I_k, \bigsqcup_{i=1}^n I_i)
  
  The  arguments  are a list of objects D = ( I_1, \dots, I_n ), an integer k,
  and a method selection object. The output is the k-th injection \iota_k: I_k
  \rightarrow \bigsqcup_{i=1}^n I_i.
  
  6.7-7 InjectionOfCofactorOfCoproductWithGivenCoproduct
  
  InjectionOfCofactorOfCoproductWithGivenCoproduct( D, k, I )  operation
  Returns:  a morphism in \mathrm{Hom}(I_k, I)
  
  The  arguments  are a list of objects D = ( I_1, \dots, I_n ), an integer k,
  and  an  object  I = \bigsqcup_{i=1}^n I_i. The output is the k-th injection
  \iota_k: I_k \rightarrow I.
  
  6.7-8 UniversalMorphismFromCoproduct
  
  UniversalMorphismFromCoproduct( arg )  function
  Returns:  a morphism in \mathrm{Hom}(\bigsqcup_{i=1}^n I_i, T)
  
  This  is  a  convenience  method. There are three different ways to use this
  method.
  
      The arguments are a list of objects D = ( I_1, \dots, I_n ), a list of
        morphisms \tau = ( \tau_i: I_i \rightarrow T ).
  
      The argument is a list of morphisms \tau = ( \tau_i: I_i \rightarrow T
        ).
  
      The  arguments are morphisms \tau_1: I_1 \rightarrow T, \dots, \tau_n:
        I_n \rightarrow T
  
  The  output  is  the morphism u( \tau ): \bigsqcup_{i=1}^n I_i \rightarrow T
  given by the universal property of the coproduct.
  
  6.7-9 UniversalMorphismFromCoproductOp
  
  UniversalMorphismFromCoproductOp( D, tau, method_selection_object )  operation
  Returns:  a morphism in \mathrm{Hom}(\bigsqcup_{i=1}^n I_i, T)
  
  The  arguments  are  a  list  of  objects D = ( I_1, \dots, I_n ), a list of
  morphisms  \tau  =  (  \tau_i:  I_i  \rightarrow T ), and a method selection
  object.  The  output  is  the  morphism  u(  \tau  ):  \bigsqcup_{i=1}^n I_i
  \rightarrow T given by the universal property of the coproduct.
  
  6.7-10 UniversalMorphismFromCoproductWithGivenCoproduct
  
  UniversalMorphismFromCoproductWithGivenCoproduct( D, tau, I )  operation
  Returns:  a morphism in \mathrm{Hom}(I, T)
  
  The  arguments  are  a  list  of  objects D = ( I_1, \dots, I_n ), a list of
  morphisms  \tau  =  (  \tau_i:  I_i  \rightarrow  T  ),  and  an  object I =
  \bigsqcup_{i=1}^n I_i. The output is the morphism u( \tau ): I \rightarrow T
  given by the universal property of the coproduct.
  
  6.7-11 AddCoproduct
  
  AddCoproduct( 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 Coproduct. F: (
  (I_1, \dots, I_n) ) \mapsto I.
  
  6.7-12 AddInjectionOfCofactorOfCoproduct
  
  AddInjectionOfCofactorOfCoproduct( 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
  InjectionOfCofactorOfCoproduct. F: ( (I_1, \dots, I_n), i ) \mapsto \iota_i.
  
  6.7-13 AddInjectionOfCofactorOfCoproductWithGivenCoproduct
  
  AddInjectionOfCofactorOfCoproductWithGivenCoproduct( 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
  InjectionOfCofactorOfCoproductWithGivenCoproduct. F: ( (I_1, \dots, I_n), i,
  I ) \mapsto \iota_i.
  
  6.7-14 AddUniversalMorphismFromCoproduct
  
  AddUniversalMorphismFromCoproduct( 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
  UniversalMorphismFromCoproduct.  F:  (  (I_1, \dots, I_n), \tau ) \mapsto u(
  \tau ).
  
  6.7-15 AddUniversalMorphismFromCoproductWithGivenCoproduct
  
  AddUniversalMorphismFromCoproductWithGivenCoproduct( 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
  UniversalMorphismFromCoproductWithGivenCoproduct.  F:  (  (I_1, \dots, I_n),
  \tau, I ) \mapsto u( \tau ).
  
  6.7-16 CoproductFunctorial
  
  CoproductFunctorial( L )  operation
  Returns:  a      morphism     in     \mathrm{Hom}(\bigsqcup_{i=1}^n     I_i,
            \bigsqcup_{i=1}^n I_i')
  
  The  argument is a list L = ( \mu_1: I_1 \rightarrow I_1', \dots, \mu_n: I_n
  \rightarrow   I_n'  ).  The  output  is  a  morphism  \bigsqcup_{i=1}^n  I_i
  \rightarrow   \bigsqcup_{i=1}^n  I_i'  given  by  the  functorality  of  the
  coproduct.
  
  6.7-17 CoproductFunctorialWithGivenCoproducts
  
  CoproductFunctorialWithGivenCoproducts( s, L, r )  operation
  Returns:  a morphism in \mathrm{Hom}(s, r)
  
  The  arguments  are an object s = \bigsqcup_{i=1}^n I_i, a list L = ( \mu_1:
  I_1  \rightarrow I_1', \dots, \mu_n: I_n \rightarrow I_n' ), and an object r
  =  \bigsqcup_{i=1}^n  I_i'.  The  output is a morphism \bigsqcup_{i=1}^n I_i
  \rightarrow   \bigsqcup_{i=1}^n  I_i'  given  by  the  functorality  of  the
  coproduct.
  
  6.7-18 AddCoproductFunctorialWithGivenCoproducts
  
  AddCoproductFunctorialWithGivenCoproducts( 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
  CoproductFunctorialWithGivenCoproducts.  F:  (\bigsqcup_{i=1}^n I_i, (\mu_1,
  \dots,  \mu_n),  \bigsqcup_{i=1}^n  I_i') \rightarrow (\bigsqcup_{i=1}^n I_i
  \rightarrow \bigsqcup_{i=1}^n I_i').
  
  
  6.8 Direct Product
  
  For  a  given list of objects D = ( P_1, \dots, P_n ), a direct product of D
  consists of three parts:
  
      an object P,
  
      a list of morphisms \pi = ( \pi_i: P \rightarrow P_i )_{i = 1 \dots n}
  
      a dependent function u mapping each list of morphisms \tau = ( \tau_i:
        T  \rightarrow  P_i  )_{i  =  1,  \dots,  n}  to a morphism u(\tau): T
        \rightarrow  P such that \pi_i \circ u( \tau ) \sim_{T,P_i} \tau_i for
        all i = 1, \dots, n.
  
  The triple ( P, \pi, u ) is called a direct product of D if the morphisms u(
  \tau  ) are uniquely determined up to congruence of morphisms. We denote the
  object  P of such a triple by \prod_{i=1}^n P_i. We say that the morphism u(
  \tau  )  is  induced  by  the  universal property of the direct product. \\ 
  \mathrm{DirectProduct}  is  a  functorial operation. This means: For (\mu_i:
  P_i  \rightarrow  P'_i)_{i=1\dots n}, we obtain a morphism \prod_{i=1}^n P_i
  \rightarrow \prod_{i=1}^n P_i'.
  
  6.8-1 DirectProductOp
  
  DirectProductOp( D )  operation
  Returns:  an object
  
  The  arguments  are  a list of objects D = ( P_1, \dots, P_n ) and an object
  for method selection. The output is the direct product \prod_{i=1}^n P_i.
  
  6.8-2 ProjectionInFactorOfDirectProduct
  
  ProjectionInFactorOfDirectProduct( D, k )  operation
  Returns:  a morphism in \mathrm{Hom}(\prod_{i=1}^n P_i, P_k)
  
  The  arguments  are a list of objects D = ( P_1, \dots, P_n ) and an integer
  k.  The  output  is the k-th projection \pi_k: \prod_{i=1}^n P_i \rightarrow
  P_k.
  
  6.8-3 ProjectionInFactorOfDirectProductOp
  
  ProjectionInFactorOfDirectProductOp( D, k, method_selection_object )  operation
  Returns:  a morphism in \mathrm{Hom}(\prod_{i=1}^n P_i, P_k)
  
  The  arguments  are a list of objects D = ( P_1, \dots, P_n ), an integer k,
  and an object for method selection. The output is the k-th projection \pi_k:
  \prod_{i=1}^n P_i \rightarrow P_k.
  
  6.8-4 ProjectionInFactorOfDirectProductWithGivenDirectProduct
  
  ProjectionInFactorOfDirectProductWithGivenDirectProduct( D, k, P )  operation
  Returns:  a morphism in \mathrm{Hom}(P, P_k)
  
  The  arguments  are a list of objects D = ( P_1, \dots, P_n ), an integer k,
  and  an  object  P  =  \prod_{i=1}^n  P_i. The output is the k-th projection
  \pi_k: P \rightarrow P_k.
  
  6.8-5 UniversalMorphismIntoDirectProduct
  
  UniversalMorphismIntoDirectProduct( arg )  function
  Returns:  a morphism in \mathrm{Hom}(T, \prod_{i=1}^n P_i)
  
  This  is  a  convenience  method. There are three different ways to use this
  method.
  
      The arguments are a list of objects D = ( P_1, \dots, P_n ) and a list
        of morphisms \tau = ( \tau_i: T \rightarrow P_i )_{i = 1, \dots, n}.
  
      The argument is a list of morphisms \tau = ( \tau_i: T \rightarrow P_i
        )_{i = 1, \dots, n}.
  
      The  arguments are morphisms \tau_1: T \rightarrow P_1, \dots, \tau_n:
        T \rightarrow P_n.
  
  The output is the morphism u(\tau): T \rightarrow \prod_{i=1}^n P_i given by
  the universal property of the direct product.
  
  6.8-6 UniversalMorphismIntoDirectProductOp
  
  UniversalMorphismIntoDirectProductOp( D, tau, method_selection_object )  operation
  Returns:  a morphism in \mathrm{Hom}(T, \prod_{i=1}^n P_i)
  
  The  arguments  are  a  list  of  objects D = ( P_1, \dots, P_n ), a list of
  morphisms  \tau  =  (  \tau_i: T \rightarrow P_i )_{i = 1, \dots, n}, and an
  object  for  method  selection.  The  output  is  the  morphism  u(\tau):  T
  \rightarrow  \prod_{i=1}^n P_i given by the universal property of the direct
  product.
  
  6.8-7 UniversalMorphismIntoDirectProductWithGivenDirectProduct
  
  UniversalMorphismIntoDirectProductWithGivenDirectProduct( D, tau, P )  operation
  Returns:  a morphism in \mathrm{Hom}(T, \prod_{i=1}^n P_i)
  
  The  arguments  are  a  list  of  objects D = ( P_1, \dots, P_n ), a list of
  morphisms  \tau  =  (  \tau_i: T \rightarrow P_i )_{i = 1, \dots, n}, and an
  object  P  =  \prod_{i=1}^n  P_i.  The  output  is  the  morphism u(\tau): T
  \rightarrow  \prod_{i=1}^n P_i given by the universal property of the direct
  product.
  
  6.8-8 AddDirectProduct
  
  AddDirectProduct( 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 DirectProduct. F: (
  (P_1, \dots, P_n) ) \mapsto P
  
  6.8-9 AddProjectionInFactorOfDirectProduct
  
  AddProjectionInFactorOfDirectProduct( 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
  ProjectionInFactorOfDirectProduct. F: ( (P_1, \dots, P_n),k ) \mapsto \pi_k
  
  6.8-10 AddProjectionInFactorOfDirectProductWithGivenDirectProduct
  
  AddProjectionInFactorOfDirectProductWithGivenDirectProduct( 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
  ProjectionInFactorOfDirectProductWithGivenDirectProduct.  F:  ( (P_1, \dots,
  P_n),k,P ) \mapsto \pi_k
  
  6.8-11 AddUniversalMorphismIntoDirectProduct
  
  AddUniversalMorphismIntoDirectProduct( 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
  UniversalMorphismIntoDirectProduct.  F:  ( (P_1, \dots, P_n), \tau ) \mapsto
  u( \tau )
  
  6.8-12 AddUniversalMorphismIntoDirectProductWithGivenDirectProduct
  
  AddUniversalMorphismIntoDirectProductWithGivenDirectProduct( 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
  UniversalMorphismIntoDirectProductWithGivenDirectProduct.  F: ( (P_1, \dots,
  P_n), \tau, P ) \mapsto u( \tau )
  
  6.8-13 DirectProductFunctorial
  
  DirectProductFunctorial( L )  operation
  Returns:  a  morphism in \mathrm{Hom}( \prod_{i=1}^n P_i, \prod_{i=1}^n P_i'
            )
  
  The   argument   is  a  list  of  morphisms  L  =  (\mu_i:  P_i  \rightarrow
  P'_i)_{i=1\dots  n}.  The output is a morphism \prod_{i=1}^n P_i \rightarrow
  \prod_{i=1}^n P_i' given by the functorality of the direct product.
  
  6.8-14 DirectProductFunctorialWithGivenDirectProducts
  
  DirectProductFunctorialWithGivenDirectProducts( s, L, r )  operation
  Returns:  a morphism in \mathrm{Hom}( s, r )
  
  The  arguments  are an object s = \prod_{i=1}^n P_i, a list of morphisms L =
  (\mu_i:  P_i \rightarrow P'_i)_{i=1\dots n}, and an object r = \prod_{i=1}^n
  P_i'.  The  output is a morphism \prod_{i=1}^n P_i \rightarrow \prod_{i=1}^n
  P_i' given by the functorality of the direct product.
  
  6.8-15 AddDirectProductFunctorialWithGivenDirectProducts
  
  AddDirectProductFunctorialWithGivenDirectProducts( 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
  DirectProductFunctorialWithGivenDirectProducts.   F:  (  \prod_{i=1}^n  P_i,
  (\mu_i:  P_i  \rightarrow  P'_i)_{i=1\dots  n}, \prod_{i=1}^n P_i' ) \mapsto
  (\prod_{i=1}^n P_i \rightarrow \prod_{i=1}^n P_i')
  
  
  6.9 Fiber Product
  
  For  a  given  list  of  morphisms D = ( \beta_i: P_i \rightarrow B )_{i = 1
  \dots n}, a fiber product of D consists of three parts:
  
      an object P,
  
      a list of morphisms \pi = ( \pi_i: P \rightarrow P_i )_{i = 1 \dots n}
        such  that \beta_i \circ \pi_i \sim_{P, B} \beta_j \circ \pi_j for all
        pairs i,j.
  
      a dependent function u mapping each list of morphisms \tau = ( \tau_i:
        T \rightarrow P_i ) such that \beta_i \circ \tau_i \sim_{T, B} \beta_j
        \circ  \tau_j for all pairs i,j to a morphism u( \tau ): T \rightarrow
        P  such that \pi_i \circ u( \tau ) \sim_{T, P_i} \tau_i for all i = 1,
        \dots, n.
  
  The  triple ( P, \pi, u ) is called a fiber product of D if the morphisms u(
  \tau  ) are uniquely determined up to congruence of morphisms. We denote the
  object  P  of  such  a  triple  by \mathrm{FiberProduct}(D). We say that the
  morphism  u(  \tau  )  is  induced  by  the  universal property of the fiber
  product.  \\    \mathrm{FiberProduct} is a functorial operation. This means:
  For  a  second  diagram D' = (\beta_i': P_i' \rightarrow B')_{i = 1 \dots n}
  and  a  natural  morphism  between  pullback diagrams (i.e., a collection of
  morphisms   (\mu_i:   P_i   \rightarrow  P'_i)_{i=1\dots  n}  and  \beta:  B
  \rightarrow  B'  such  that  \beta_i'  \circ \mu_i \sim_{P_i,B'} \beta \circ
  \beta_i for i = 1, \dots, n) we obtain a morphism \mathrm{FiberProduct}( D )
  \rightarrow \mathrm{FiberProduct}( D' ).
  
  6.9-1 IsomorphismFromFiberProductToKernelOfDiagonalDifference
  
  IsomorphismFromFiberProductToKernelOfDiagonalDifference( D )  operation
  Returns:  a morphism in \mathrm{Hom}(\mathrm{FiberProduct}(D), \Delta)
  
  The  argument is a list of morphisms D = ( \beta_i: P_i \rightarrow B )_{i =
  1  \dots  n}.  The output is a morphism \mathrm{FiberProduct}(D) \rightarrow
  \Delta,  where  \Delta  denotes  the  kernel object equalizing the morphisms
  \beta_i.
  
  6.9-2 IsomorphismFromFiberProductToKernelOfDiagonalDifferenceOp
  
  IsomorphismFromFiberProductToKernelOfDiagonalDifferenceOp( D, method_selection_morphism )  operation
  Returns:  a morphism in \mathrm{Hom}(\mathrm{FiberProduct}(D), \Delta)
  
  The  arguments are a list of morphisms D = ( \beta_i: P_i \rightarrow B )_{i
  =  1  \dots n} and a morphism for method selection. The output is a morphism
  \mathrm{FiberProduct}(D) \rightarrow \Delta, where \Delta denotes the kernel
  object equalizing the morphisms \beta_i.
  
  6.9-3 AddIsomorphismFromFiberProductToKernelOfDiagonalDifference
  
  AddIsomorphismFromFiberProductToKernelOfDiagonalDifference( 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
  IsomorphismFromFiberProductToKernelOfDiagonalDifference. F: ( ( \beta_i: P_i
  \rightarrow   B  )_{i  =  1  \dots  n}  )  \mapsto  \mathrm{FiberProduct}(D)
  \rightarrow \Delta
  
  6.9-4 IsomorphismFromKernelOfDiagonalDifferenceToFiberProduct
  
  IsomorphismFromKernelOfDiagonalDifferenceToFiberProduct( D )  operation
  Returns:  a morphism in \mathrm{Hom}(\Delta, \mathrm{FiberProduct}(D))
  
  The  argument is a list of morphisms D = ( \beta_i: P_i \rightarrow B )_{i =
  1    \dots    n}.    The   output   is   a   morphism   \Delta   \rightarrow
  \mathrm{FiberProduct}(D),  where \Delta denotes the kernel object equalizing
  the morphisms \beta_i.
  
  6.9-5 IsomorphismFromKernelOfDiagonalDifferenceToFiberProductOp
  
  IsomorphismFromKernelOfDiagonalDifferenceToFiberProductOp( D )  operation
  Returns:  a morphism in \mathrm{Hom}(\Delta, \mathrm{FiberProduct}(D))
  
  The  argument is a list of morphisms D = ( \beta_i: P_i \rightarrow B )_{i =
  1  \dots  n}  and  a morphism for method selection. The output is a morphism
  \Delta \rightarrow \mathrm{FiberProduct}(D), where \Delta denotes the kernel
  object equalizing the morphisms \beta_i.
  
  6.9-6 AddIsomorphismFromKernelOfDiagonalDifferenceToFiberProduct
  
  AddIsomorphismFromKernelOfDiagonalDifferenceToFiberProduct( 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
  IsomorphismFromKernelOfDiagonalDifferenceToFiberProduct. F: ( ( \beta_i: P_i
  \rightarrow   B   )_{i   =   1   \dots   n}  )  \mapsto  \Delta  \rightarrow
  \mathrm{FiberProduct}(D)
  
  6.9-7 DirectSumDiagonalDifference
  
  DirectSumDiagonalDifference( D )  operation
  Returns:  a morphism in \mathrm{Hom}( \bigoplus_{i=1}^n P_i, B )
  
  The  argument is a list of morphisms D = ( \beta_i: P_i \rightarrow B )_{i =
  1  \dots  n}.  The  output is a morphism \bigoplus_{i=1}^n P_i \rightarrow B
  such that its kernel equalizes the \beta_i.
  
  6.9-8 DirectSumDiagonalDifferenceOp
  
  DirectSumDiagonalDifferenceOp( D, method_selection_morphism )  operation
  Returns:  a morphism in \mathrm{Hom}( \bigoplus_{i=1}^n P_i, B )
  
  The  argument is a list of morphisms D = ( \beta_i: P_i \rightarrow B )_{i =
  1  \dots  n}  and  a morphism for method selection. The output is a morphism
  \bigoplus_{i=1}^n  P_i  \rightarrow  B  such  that  its kernel equalizes the
  \beta_i.
  
  6.9-9 AddDirectSumDiagonalDifference
  
  AddDirectSumDiagonalDifference( 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
  DirectSumDiagonalDifference.        F:       (       D       )       \mapsto
  \mathrm{DirectSumDiagonalDifference}(D)
  
  6.9-10 FiberProductEmbeddingInDirectSum
  
  FiberProductEmbeddingInDirectSum( D )  operation
  Returns:  a     morphism    in    \mathrm{Hom}(    \mathrm{FiberProduct}(D),
            \bigoplus_{i=1}^n P_i )
  
  The  argument is a list of morphisms D = ( \beta_i: P_i \rightarrow B )_{i =
  1  \dots  n}.  The  output is the natural embedding \mathrm{FiberProduct}(D)
  \rightarrow \bigoplus_{i=1}^n P_i.
  
  6.9-11 FiberProductEmbeddingInDirectSumOp
  
  FiberProductEmbeddingInDirectSumOp( D, method_selection_morphism )  operation
  Returns:  a     morphism    in    \mathrm{Hom}(    \mathrm{FiberProduct}(D),
            \bigoplus_{i=1}^n P_i )
  
  The  argument is a list of morphisms D = ( \beta_i: P_i \rightarrow B )_{i =
  1  \dots  n}  and a morphism for method selection. The output is the natural
  embedding \mathrm{FiberProduct}(D) \rightarrow \bigoplus_{i=1}^n P_i.
  
  6.9-12 AddFiberProductEmbeddingInDirectSum
  
  AddFiberProductEmbeddingInDirectSum( 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
  FiberProductEmbeddingInDirectSum. F: ( ( \beta_i: P_i \rightarrow B )_{i = 1
  \dots  n}  )  \mapsto \mathrm{FiberProduct}(D) \rightarrow \bigoplus_{i=1}^n
  P_i
  
  6.9-13 FiberProduct
  
  FiberProduct( arg )  function
  Returns:  an object
  
  This  is  a  convenience  method.  There  are two different ways to use this
  method:
  
      The  argument  is a list of morphisms D = ( \beta_i: P_i \rightarrow B
        )_{i = 1 \dots n}.
  
      The  arguments  are  morphisms  \beta_1:  P_1  \rightarrow  B,  \dots,
        \beta_n: P_n \rightarrow B.
  
  The output is the fiber product \mathrm{FiberProduct}(D).
  
  6.9-14 FiberProductOp
  
  FiberProductOp( D, method_selection_morphism )  operation
  Returns:  an object
  
  The  arguments are a list of morphisms D = ( \beta_i: P_i \rightarrow B )_{i
  =  1  \dots  n} and a morphism for method selection. The output is the fiber
  product \mathrm{FiberProduct}(D).
  
  6.9-15 ProjectionInFactorOfFiberProduct
  
  ProjectionInFactorOfFiberProduct( D, k )  operation
  Returns:  a morphism in \mathrm{Hom}( \mathrm{FiberProduct}(D), P_k )
  
  The  arguments are a list of morphisms D = ( \beta_i: P_i \rightarrow B )_{i
  =  1  \dots  n} and an integer k. The output is the k-th projection \pi_{k}:
  \mathrm{FiberProduct}(D) \rightarrow P_k.
  
  6.9-16 ProjectionInFactorOfFiberProductOp
  
  ProjectionInFactorOfFiberProductOp( D, k, method_selection_morphism )  operation
  Returns:  a morphism in \mathrm{Hom}( \mathrm{FiberProduct}(D), P_k )
  
  The  arguments are a list of morphisms D = ( \beta_i: P_i \rightarrow B )_{i
  =  1 \dots n}, an integer k, and a morphism for method selection. The output
  is the k-th projection \pi_{k}: \mathrm{FiberProduct}(D) \rightarrow P_k.
  
  6.9-17 ProjectionInFactorOfFiberProductWithGivenFiberProduct
  
  ProjectionInFactorOfFiberProductWithGivenFiberProduct( D, k, P )  operation
  Returns:  a morphism in \mathrm{Hom}( P, P_k )
  
  The  arguments are a list of morphisms D = ( \beta_i: P_i \rightarrow B )_{i
  =  1 \dots n}, an integer k, and an object P = \mathrm{FiberProduct}(D). The
  output is the k-th projection \pi_{k}: P \rightarrow P_k.
  
  6.9-18 UniversalMorphismIntoFiberProduct
  
  UniversalMorphismIntoFiberProduct( arg )  function
  
  This  is  a  convenience  method. There are three different ways to use this
  method:
  
      The arguments are a list of morphisms D = ( \beta_i: P_i \rightarrow B
        )_{i  =  1  \dots  n}  and  a  list  of  morphisms  \tau = ( \tau_i: T
        \rightarrow  P_i  ) such that \beta_i \circ \tau_i \sim_{T, B} \beta_j
        \circ  \tau_j for all pairs i,j. The output is the morphism u( \tau ):
        T \rightarrow \mathrm{FiberProduct}(D) given by the universal property
        of the fiber product.
  
      The arguments are a list of morphisms D = ( \beta_i: P_i \rightarrow B
        )_{i  =  1  \dots  n}  and morphisms \tau_1: T \rightarrow P_1, \dots,
        \tau_n:  T  \rightarrow P_n such that \beta_i \circ \tau_i \sim_{T, B}
        \beta_j  \circ \tau_j for all pairs i,j. The output is the morphism u(
        \tau  ): T \rightarrow \mathrm{FiberProduct}(D) given by the universal
        property of the fiber product.
  
  6.9-19 UniversalMorphismIntoFiberProductOp
  
  UniversalMorphismIntoFiberProductOp( D, tau, method_selection_morphism )  operation
  Returns:  a morphism in \mathrm{Hom}( T, \mathrm{FiberProduct}(D) )
  
  The  arguments are a list of morphisms D = ( \beta_i: P_i \rightarrow B )_{i
  =  1 \dots n}, a list of morphisms \tau = ( \tau_i: T \rightarrow P_i ) such
  that  \beta_i  \circ  \tau_i  \sim_{T, B} \beta_j \circ \tau_j for all pairs
  i,j, and a morphism for method selection. The output is the morphism u( \tau
  ): T \rightarrow \mathrm{FiberProduct}(D) given by the universal property of
  the fiber product.
  
  6.9-20 UniversalMorphismIntoFiberProductWithGivenFiberProduct
  
  UniversalMorphismIntoFiberProductWithGivenFiberProduct( D, tau, P )  operation
  Returns:  a morphism in \mathrm{Hom}( T, P )
  
  The  arguments are a list of morphisms D = ( \beta_i: P_i \rightarrow B )_{i
  =  1 \dots n}, a list of morphisms \tau = ( \tau_i: T \rightarrow P_i ) such
  that  \beta_i  \circ  \tau_i  \sim_{T, B} \beta_j \circ \tau_j for all pairs
  i,j,  and an object P = \mathrm{FiberProduct}(D). The output is the morphism
  u(  \tau  ):  T  \rightarrow  P given by the universal property of the fiber
  product.
  
  6.9-21 AddFiberProduct
  
  AddFiberProduct( 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 FiberProduct. F: (
  (\beta_i: P_i \rightarrow B)_{i = 1 \dots n} ) \mapsto P
  
  6.9-22 AddProjectionInFactorOfFiberProduct
  
  AddProjectionInFactorOfFiberProduct( 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
  ProjectionInFactorOfFiberProduct.  F:  ( (\beta_i: P_i \rightarrow B)_{i = 1
  \dots n}, k ) \mapsto \pi_k
  
  6.9-23 AddProjectionInFactorOfFiberProductWithGivenFiberProduct
  
  AddProjectionInFactorOfFiberProductWithGivenFiberProduct( 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
  ProjectionInFactorOfFiberProductWithGivenFiberProduct.  F:  (  (\beta_i: P_i
  \rightarrow B)_{i = 1 \dots n}, k,P ) \mapsto \pi_k
  
  6.9-24 AddUniversalMorphismIntoFiberProduct
  
  AddUniversalMorphismIntoFiberProduct( 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
  UniversalMorphismIntoFiberProduct.  F: ( (\beta_i: P_i \rightarrow B)_{i = 1
  \dots n}, \tau ) \mapsto u(\tau)
  
  6.9-25 AddUniversalMorphismIntoFiberProductWithGivenFiberProduct
  
  AddUniversalMorphismIntoFiberProductWithGivenFiberProduct( 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
  UniversalMorphismIntoFiberProductWithGivenFiberProduct.  F:  ( (\beta_i: P_i
  \rightarrow B)_{i = 1 \dots n}, \tau, P ) \mapsto u(\tau)
  
  6.9-26 FiberProductFunctorial
  
  FiberProductFunctorial( L )  operation
  Returns:  a morphism in \mathrm{Hom}(\mathrm{FiberProduct}( ( \beta_i )_{i=1
            \dots n} ), \mathrm{FiberProduct}( ( \beta_i' )_{i=1 \dots n} ))
  
  The  argument  is  a  list  of  triples  of  morphisms  L  = ( (\beta_i: P_i
  \rightarrow  B,  \mu_i:  P_i  \rightarrow  P_i',  \beta_i': P_i' \rightarrow
  B')_{i = 1 \dots n} ) such that there exists a morphism \beta: B \rightarrow
  B'  such that \beta_i' \circ \mu_i \sim_{P_i,B'} \beta \circ \beta_i for i =
  1,  \dots,  n.  The  output is the morphism \mathrm{FiberProduct}( ( \beta_i
  )_{i=1 \dots n} ) \rightarrow \mathrm{FiberProduct}( ( \beta_i' )_{i=1 \dots
  n} ) given by the functorality of the fiber product.
  
  6.9-27 FiberProductFunctorialWithGivenFiberProducts
  
  FiberProductFunctorialWithGivenFiberProducts( s, L, r )  operation
  Returns:  a morphism in \mathrm{Hom}(s, r)
  
  The  arguments  are  an  object  s = \mathrm{FiberProduct}( ( \beta_i )_{i=1
  \dots  n}  ), a list of triples of morphisms L = ( (\beta_i: P_i \rightarrow
  B,  \mu_i: P_i \rightarrow P_i', \beta_i': P_i' \rightarrow B')_{i = 1 \dots
  n}  )  such  that  there exists a morphism \beta: B \rightarrow B' such that
  \beta_i'  \circ \mu_i \sim_{P_i,B'} \beta \circ \beta_i for i = 1, \dots, n,
  and  an  object r = \mathrm{FiberProduct}( ( \beta_i' )_{i=1 \dots n} ). The
  output  is  the  morphism  s  \rightarrow r given by the functorality of the
  fiber product.
  
  6.9-28 AddFiberProductFunctorialWithGivenFiberProducts
  
  AddFiberProductFunctorialWithGivenFiberProducts( 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
  FiberProductFunctorialWithGivenFiberProducts.  F: ( \mathrm{FiberProduct}( (
  \beta_i  )_{i=1  \dots  n}  ),  (\beta_i:  P_i  \rightarrow  B,  \mu_i:  P_i
  \rightarrow   P_i',   \beta_i':  P_i'  \rightarrow  B')_{i  =  1  \dots  n},
  \mathrm{FiberProduct}(   (   \beta_i'   )_{i=1   \dots   n}   )   )  \mapsto
  (\mathrm{FiberProduct}(   (   \beta_i   )_{i=1   \dots   n}   )  \rightarrow
  \mathrm{FiberProduct}( ( \beta_i' )_{i=1 \dots n} ) )
  
  
  6.10 Pushout
  
  For  a  given  list  of  morphisms D = ( \beta_i: B \rightarrow I_i )_{i = 1
  \dots n}, a pushout of D consists of three parts:
  
      an object I,
  
      a  list  of  morphisms  \iota  = ( \iota_i: I_i \rightarrow I )_{i = 1
        \dots  n}  such  that  \iota_i  \circ \beta_i \sim_{B,I} \iota_j \circ
        \beta_j for all pairs i,j,
  
      a dependent function u mapping each list of morphisms \tau = ( \tau_i:
        I_i  \rightarrow  T  )_{i  = 1 \dots n} such that \tau_i \circ \beta_i
        \sim_{B,T} \tau_j \circ \beta_j to a morphism u( \tau ): I \rightarrow
        T  such  that u( \tau ) \circ \iota_i \sim_{I_i, T} \tau_i for all i =
        1, \dots, n.
  
  The triple ( I, \iota, u ) is called a pushout of D if the morphisms u( \tau
  )  are  uniquely  determined  up  to  congruence of morphisms. We denote the
  object  I  of such a triple by \mathrm{Pushout}(D). We say that the morphism
  u(  \tau  )  is  induced  by  the  universal  property  of  the pushout. \\ 
  \mathrm{Pushout} is a functorial operation. This means: For a second diagram
  D'  = (\beta_i': B' \rightarrow I_i')_{i = 1 \dots n} and a natural morphism
  between  pushout  diagrams  (i.e.,  a  collection  of  morphisms (\mu_i: I_i
  \rightarrow  I'_i)_{i=1\dots  n}  and  \beta:  B  \rightarrow  B'  such that
  \beta_i'  \circ \beta \sim_{B, I_i'} \mu_i \circ \beta_i for i = 1, \dots n)
  we  obtain a morphism \mathrm{Pushout}( D ) \rightarrow \mathrm{Pushout}( D'
  ).
  
  6.10-1 IsomorphismFromPushoutToCokernelOfDiagonalDifference
  
  IsomorphismFromPushoutToCokernelOfDiagonalDifference( D )  operation
  Returns:  a morphism in \mathrm{Hom}( \mathrm{Pushout}(D), \Delta)
  
  The  argument is a list of morphisms D = ( \beta_i: B \rightarrow I_i )_{i =
  1 \dots n}. The output is a morphism \mathrm{Pushout}(D) \rightarrow \Delta,
  where \Delta denotes the cokernel object coequalizing the morphisms \beta_i.
  
  6.10-2 IsomorphismFromPushoutToCokernelOfDiagonalDifferenceOp
  
  IsomorphismFromPushoutToCokernelOfDiagonalDifferenceOp( D, method_selection_morphism )  operation
  Returns:  a morphism in \mathrm{Hom}( \mathrm{Pushout}(D), \Delta)
  
  The  argument is a list of morphisms D = ( \beta_i: B \rightarrow I_i )_{i =
  1  \dots  n}  and  a morphism for method selection. The output is a morphism
  \mathrm{Pushout}(D)  \rightarrow  \Delta,  where \Delta denotes the cokernel
  object coequalizing the morphisms \beta_i.
  
  6.10-3 AddIsomorphismFromPushoutToCokernelOfDiagonalDifference
  
  AddIsomorphismFromPushoutToCokernelOfDiagonalDifference( 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
  IsomorphismFromPushoutToCokernelOfDiagonalDifference.  F:  (  (  \beta_i:  B
  \rightarrow I_i )_{i = 1 \dots n} ) \mapsto (\mathrm{Pushout}(D) \rightarrow
  \Delta)
  
  6.10-4 IsomorphismFromCokernelOfDiagonalDifferenceToPushout
  
  IsomorphismFromCokernelOfDiagonalDifferenceToPushout( D )  operation
  Returns:  a morphism in \mathrm{Hom}( \Delta, \mathrm{Pushout}(D))
  
  The  argument is a list of morphisms D = ( \beta_i: B \rightarrow I_i )_{i =
  1 \dots n}. The output is a morphism \Delta \rightarrow \mathrm{Pushout}(D),
  where \Delta denotes the cokernel object coequalizing the morphisms \beta_i.
  
  6.10-5 IsomorphismFromCokernelOfDiagonalDifferenceToPushoutOp
  
  IsomorphismFromCokernelOfDiagonalDifferenceToPushoutOp( D, method_selection_morphism )  operation
  Returns:  a morphism in \mathrm{Hom}( \Delta, \mathrm{Pushout}(D))
  
  The  argument is a list of morphisms D = ( \beta_i: B \rightarrow I_i )_{i =
  1  \dots  n}  and  a morphism for method selection. The output is a morphism
  \Delta  \rightarrow  \mathrm{Pushout}(D),  where \Delta denotes the cokernel
  object coequalizing the morphisms \beta_i.
  
  6.10-6 AddIsomorphismFromCokernelOfDiagonalDifferenceToPushout
  
  AddIsomorphismFromCokernelOfDiagonalDifferenceToPushout( 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
  IsomorphismFromCokernelOfDiagonalDifferenceToPushout.  F:  (  (  \beta_i:  B
  \rightarrow   I_i   )_{i   =  1  \dots  n}  )  \mapsto  (\Delta  \rightarrow
  \mathrm{Pushout}(D))
  
  6.10-7 DirectSumCodiagonalDifference
  
  DirectSumCodiagonalDifference( D )  operation
  Returns:  a morphism in \mathrm{Hom}(B, \bigoplus_{i=1}^n I_i)
  
  The  argument is a list of morphisms D = ( \beta_i: B \rightarrow I_i )_{i =
  1  \dots  n}.  The  output is a morphism B \rightarrow \bigoplus_{i=1}^n I_i
  such that its cokernel coequalizes the \beta_i.
  
  6.10-8 DirectSumCodiagonalDifferenceOp
  
  DirectSumCodiagonalDifferenceOp( D, method_selection_morphism )  operation
  Returns:  a morphism in \mathrm{Hom}(B, \bigoplus_{i=1}^n I_i)
  
  The  argument is a list of morphisms D = ( \beta_i: B \rightarrow I_i )_{i =
  1  \dots  n} and a morphism for method selection. The output is a morphism B
  \rightarrow  \bigoplus_{i=1}^n  I_i  such  that its cokernel coequalizes the
  \beta_i.
  
  6.10-9 AddDirectSumCodiagonalDifference
  
  AddDirectSumCodiagonalDifference( 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
  DirectSumCodiagonalDifference.       F:       (       D       )      \mapsto
  \mathrm{DirectSumCodiagonalDifference}(D)
  
  6.10-10 DirectSumProjectionInPushout
  
  DirectSumProjectionInPushout( D )  operation
  Returns:  a     morphism    in    \mathrm{Hom}(    \bigoplus_{i=1}^n    I_i,
            \mathrm{Pushout}(D) )
  
  The  argument is a list of morphisms D = ( \beta_i: B \rightarrow I_i )_{i =
  1  \dots  n}.  The  output  is  the natural projection \bigoplus_{i=1}^n I_i
  \rightarrow \mathrm{Pushout}(D).
  
  6.10-11 DirectSumProjectionInPushoutOp
  
  DirectSumProjectionInPushoutOp( D, method_selection_morphism )  operation
  Returns:  a     morphism    in    \mathrm{Hom}(    \bigoplus_{i=1}^n    I_i,
            \mathrm{Pushout}(D) )
  
  The  argument is a list of morphisms D = ( \beta_i: B \rightarrow I_i )_{i =
  1  \dots  n}  and a morphism for method selection. The output is the natural
  projection \bigoplus_{i=1}^n I_i \rightarrow \mathrm{Pushout}(D).
  
  6.10-12 AddDirectSumProjectionInPushout
  
  AddDirectSumProjectionInPushout( 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
  DirectSumProjectionInPushout.  F:  (  (  \beta_i: B \rightarrow I_i )_{i = 1
  \dots n} ) \mapsto (\bigoplus_{i=1}^n I_i \rightarrow \mathrm{Pushout}(D))
  
  6.10-13 Pushout
  
  Pushout( D )  operation
  Returns:  an object
  
  The  argument is a list of morphisms D = ( \beta_i: B \rightarrow I_i )_{i =
  1 \dots n} The output is the pushout \mathrm{Pushout}(D).
  
  6.10-14 Pushout
  
  Pushout( D )  operation
  Returns:  an object
  
  This  is  a  convenience  method.  The arguments are a morphism \alpha and a
  morphism \beta. The output is the pushout \mathrm{Pushout}(\alpha, \beta).
  
  6.10-15 PushoutOp
  
  PushoutOp( D )  operation
  Returns:  an object
  
  The  arguments are a list of morphisms D = ( \beta_i: B \rightarrow I_i )_{i
  =  1 \dots n} and a morphism for method selection. The output is the pushout
  \mathrm{Pushout}(D).
  
  6.10-16 InjectionOfCofactorOfPushout
  
  InjectionOfCofactorOfPushout( D, k )  operation
  Returns:  a morphism in \mathrm{Hom}( I_k, \mathrm{Pushout}( D ) ).
  
  The  arguments are a list of morphisms D = ( \beta_i: B \rightarrow I_i )_{i
  = 1 \dots n} and an integer k. The output is the k-th injection \iota_k: I_k
  \rightarrow \mathrm{Pushout}( D ).
  
  6.10-17 InjectionOfCofactorOfPushoutOp
  
  InjectionOfCofactorOfPushoutOp( D, k, method_selection_morphism )  operation
  Returns:  a morphism in \mathrm{Hom}( I_k, \mathrm{Pushout}( D ) ).
  
  The  arguments are a list of morphisms D = ( \beta_i: B \rightarrow I_i )_{i
  =  1 \dots n}, an integer k, and a morphism for method selection. The output
  is the k-th injection \iota_k: I_k \rightarrow \mathrm{Pushout}( D ).
  
  6.10-18 InjectionOfCofactorOfPushoutWithGivenPushout
  
  InjectionOfCofactorOfPushoutWithGivenPushout( D, k, I )  operation
  Returns:  a morphism in \mathrm{Hom}( I_k, \mathrm{Pushout}( D ) ).
  
  The  arguments are a list of morphisms D = ( \beta_i: B \rightarrow I_i )_{i
  =  1  \dots  n},  an  integer  k, and an object I = \mathrm{Pushout}(D). The
  output is the k-th injection \iota_k: I_k \rightarrow \mathrm{Pushout}( D ).
  
  6.10-19 UniversalMorphismFromPushout
  
  UniversalMorphismFromPushout( arg )  function
  
  This  is  a  convenience  method. There are three different ways to use this
  method:
  
      The arguments are a list of morphisms D = ( \beta_i: B \rightarrow I_i
        )_{i  =  1  \dots  n}  and  a  list  of morphisms \tau = ( \tau_i: I_i
        \rightarrow  T  )_{i  =  1  \dots  n}  such  that \tau_i \circ \beta_i
        \sim_{B,T} \tau_j \circ \beta_j. The output is the morphism u( \tau ):
        \mathrm{Pushout}(D)  \rightarrow  T given by the universal property of
        the pushout.
  
      The arguments are a list of morphisms D = ( \beta_i: B \rightarrow I_i
        )_{i  =  1  \dots  n}  and morphisms \tau_1: I_1 \rightarrow T, \dots,
        \tau_n:  I_n  \rightarrow  T such that \tau_i \circ \beta_i \sim_{B,T}
        \tau_j   \circ  \beta_j.  The  output  is  the  morphism  u(  \tau  ):
        \mathrm{Pushout}(D)  \rightarrow  T given by the universal property of
        the pushout.
  
  6.10-20 UniversalMorphismFromPushoutOp
  
  UniversalMorphismFromPushoutOp( D, tau, method_selection_morphism )  operation
  Returns:  a morphism in \mathrm{Hom}( \mathrm{Pushout}(D), T )
  
  The  arguments are a list of morphisms D = ( \beta_i: B \rightarrow I_i )_{i
  =  1 \dots n}, a list of morphisms \tau = ( \tau_i: I_i \rightarrow T )_{i =
  1  \dots  n} such that \tau_i \circ \beta_i \sim_{B,T} \tau_j \circ \beta_j,
  and  a  morphism for method selection. The output is the morphism u( \tau ):
  \mathrm{Pushout}(D)  \rightarrow  T  given  by the universal property of the
  pushout.
  
  6.10-21 UniversalMorphismFromPushoutWithGivenPushout
  
  UniversalMorphismFromPushoutWithGivenPushout( D, tau, I )  operation
  Returns:  a morphism in \mathrm{Hom}( I, T )
  
  The  arguments are a list of morphisms D = ( \beta_i: B \rightarrow I_i )_{i
  =  1 \dots n}, a list of morphisms \tau = ( \tau_i: I_i \rightarrow T )_{i =
  1  \dots  n} such that \tau_i \circ \beta_i \sim_{B,T} \tau_j \circ \beta_j,
  and an object I = \mathrm{Pushout}(D). The output is the morphism u( \tau ):
  I \rightarrow T given by the universal property of the pushout.
  
  6.10-22 AddPushout
  
  AddPushout( 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 Pushout. F: (
  (\beta_i: B \rightarrow I_i)_{i = 1 \dots n} ) \mapsto I
  
  6.10-23 AddInjectionOfCofactorOfPushout
  
  AddInjectionOfCofactorOfPushout( 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
  InjectionOfCofactorOfPushout. F: ( (\beta_i: B \rightarrow I_i)_{i = 1 \dots
  n}, k ) \mapsto \iota_k
  
  6.10-24 AddInjectionOfCofactorOfPushoutWithGivenPushout
  
  AddInjectionOfCofactorOfPushoutWithGivenPushout( 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
  InjectionOfCofactorOfPushoutWithGivenPushout.  F:  ( (\beta_i: B \rightarrow
  I_i)_{i = 1 \dots n}, k, I ) \mapsto \iota_k
  
  6.10-25 AddUniversalMorphismFromPushout
  
  AddUniversalMorphismFromPushout( 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
  UniversalMorphismFromPushout. F: ( (\beta_i: B \rightarrow I_i)_{i = 1 \dots
  n}, \tau ) \mapsto u(\tau)
  
  6.10-26 AddUniversalMorphismFromPushoutWithGivenPushout
  
  AddUniversalMorphismFromPushoutWithGivenPushout( 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
  UniversalMorphismFromPushout. F: ( (\beta_i: B \rightarrow I_i)_{i = 1 \dots
  n}, \tau, I ) \mapsto u(\tau)
  
  6.10-27 PushoutFunctorial
  
  PushoutFunctorial( L )  operation
  Returns:  a  morphism  in \mathrm{Hom}(\mathrm{Pushout}( ( \beta_i )_{i=1}^n
            ), \mathrm{Pushout}( ( \beta_i' )_{i=1}^n ))
  
  The  argument  is  a  list  L  =  ( ( \beta_i: B \rightarrow I_i, \mu_i: I_i
  \rightarrow  I_i',  \beta_i':  B'  \rightarrow I_i' )_{i = 1 \dots n} ) such
  that  there  exists  a  morphism  \beta: B \rightarrow B' such that \beta_i'
  \circ  \beta  \sim_{B,  I_i'}  \mu_i  \circ  \beta_i for i = 1, \dots n. The
  output  is  the morphism \mathrm{Pushout}( ( \beta_i )_{i=1}^n ) \rightarrow
  \mathrm{Pushout}(  (  \beta_i'  )_{i=1}^n ) given by the functorality of the
  pushout.
  
  6.10-28 PushoutFunctorialWithGivenPushouts
  
  PushoutFunctorialWithGivenPushouts( s, L, r )  operation
  Returns:  a morphism in \mathrm{Hom}(s, r)
  
  The  arguments  are an object s = \mathrm{Pushout}( ( \beta_i )_{i=1}^n ), a
  list  L  =  (  (  \beta_i:  B  \rightarrow I_i, \mu_i: I_i \rightarrow I_i',
  \beta_i':  B'  \rightarrow I_i' )_{i = 1 \dots n} ) such that there exists a
  morphism  \beta:  B  \rightarrow  B' such that \beta_i' \circ \beta \sim_{B,
  I_i'}  \mu_i  \circ  \beta_i  for  i  =  1,  \dots  n,  and  an  object  r =
  \mathrm{Pushout}(  (  \beta_i'  )_{i=1}^n  ).  The  output is the morphism s
  \rightarrow r given by the functorality of the pushout.
  
  6.10-29 AddPushoutFunctorialWithGivenPushouts
  
  AddPushoutFunctorialWithGivenPushouts( 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 PushoutFunctorial.
  F:  ( \mathrm{Pushout}( ( \beta_i )_{i=1}^n ), ( \beta_i: B \rightarrow I_i,
  \mu_i:  I_i  \rightarrow  I_i', \beta_i': B' \rightarrow I_i' )_{i = 1 \dots
  n},  \mathrm{Pushout}( ( \beta_i' )_{i=1}^n ) ) \mapsto (\mathrm{Pushout}( (
  \beta_i )_{i=1}^n ) \rightarrow \mathrm{Pushout}( ( \beta_i' )_{i=1}^n ) )
  
  
  6.11 Image
  
  For a given morphism \alpha: A \rightarrow B, an image of \alpha consists of
  four parts:
  
      an object I,
  
      a morphism c: A \rightarrow I,
  
      a  monomorphism  \iota:  I  \hookrightarrow  B such that \iota \circ c
        \sim_{A,B} \alpha,
  
      a dependent function u mapping each pair of morphisms \tau = ( \tau_1:
        A  \rightarrow  T,  \tau_2:  T  \hookrightarrow  B ) where \tau_2 is a
        monomorphism  such  that  \tau_2  \circ  \tau_1 \sim_{A,B} \alpha to a
        morphism  u(\tau):  I  \rightarrow  T  such  that \tau_2 \circ u(\tau)
        \sim_{I,B} \iota and u(\tau) \circ c \sim_{A,T} \tau_1.
  
  The 4-tuple ( I, c, \iota, u ) is called an image of \alpha if the morphisms
  u(  \tau  ) are uniquely determined up to congruence of morphisms. We denote
  the  object  I  of  such  a  4-tuple by \mathrm{im}(\alpha). We say that the
  morphism u( \tau ) is induced by the universal property of the image.
  
  6.11-1 IsomorphismFromImageObjectToKernelOfCokernel
  
  IsomorphismFromImageObjectToKernelOfCokernel( alpha )  attribute
  Returns:  a      morphism      in     \mathrm{Hom}(     \mathrm{im}(\alpha),
            \mathrm{KernelObject}( \mathrm{CokernelProjection}( \alpha ) ) )
  
  The  argument  is  a  morphism  \alpha. The output is the canonical morphism
  \mathrm{im}(\alpha)            \rightarrow            \mathrm{KernelObject}(
  \mathrm{CokernelProjection}( \alpha ) ).
  
  6.11-2 AddIsomorphismFromImageObjectToKernelOfCokernel
  
  AddIsomorphismFromImageObjectToKernelOfCokernel( 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
  IsomorphismFromImageObjectToKernelOfCokernel.    F:    \alpha    \mapsto   (
  \mathrm{im}(\alpha)            \rightarrow            \mathrm{KernelObject}(
  \mathrm{CokernelProjection}( \alpha ) ) )
  
  6.11-3 IsomorphismFromKernelOfCokernelToImageObject
  
  IsomorphismFromKernelOfCokernelToImageObject( alpha )  attribute
  Returns:  a     morphism     in     \mathrm{Hom}(     \mathrm{KernelObject}(
            \mathrm{CokernelProjection}( \alpha ) ), \mathrm{im}(\alpha) )
  
  The  argument  is  a  morphism  \alpha. The output is the canonical morphism
  \mathrm{KernelObject}(  \mathrm{CokernelProjection}(  \alpha ) ) \rightarrow
  \mathrm{im}(\alpha).
  
  6.11-4 AddIsomorphismFromKernelOfCokernelToImageObject
  
  AddIsomorphismFromKernelOfCokernelToImageObject( 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
  IsomorphismFromKernelOfCokernelToImageObject.    F:    \alpha    \mapsto   (
  \mathrm{KernelObject}(  \mathrm{CokernelProjection}(  \alpha ) ) \rightarrow
  \mathrm{im}(\alpha) )
  
  6.11-5 ImageObject
  
  ImageObject( alpha )  attribute
  Returns:  an object
  
  The  argument  is  a  morphism  \alpha. The output is the image \mathrm{im}(
  \alpha ).
  
  6.11-6 ImageEmbedding
  
  ImageEmbedding( alpha )  attribute
  Returns:  a morphism in \mathrm{Hom}(\mathrm{im}(\alpha), B)
  
  The  argument is a morphism \alpha: A \rightarrow B. The output is the image
  embedding \iota: \mathrm{im}(\alpha) \hookrightarrow B.
  
  6.11-7 ImageEmbeddingWithGivenImageObject
  
  ImageEmbeddingWithGivenImageObject( alpha, I )  operation
  Returns:  a morphism in \mathrm{Hom}(I, B)
  
  The  argument  is  a  morphism  \alpha:  A  \rightarrow  B and an object I =
  \mathrm{im}(   \alpha  ).  The  output  is  the  image  embedding  \iota:  I
  \hookrightarrow B.
  
  6.11-8 CoastrictionToImage
  
  CoastrictionToImage( alpha )  attribute
  Returns:  a morphism in \mathrm{Hom}(A, \mathrm{im}( \alpha ))
  
  The  argument  is  a  morphism  \alpha:  A  \rightarrow B. The output is the
  coastriction to image c: A \rightarrow \mathrm{im}( \alpha ).
  
  6.11-9 CoastrictionToImageWithGivenImageObject
  
  CoastrictionToImageWithGivenImageObject( alpha, I )  operation
  Returns:  a morphism in \mathrm{Hom}(A, I)
  
  The  argument  is  a  morphism  \alpha:  A  \rightarrow  B and an object I =
  \mathrm{im}(  \alpha  ).  The  output  is  the  coastriction  to  image c: A
  \rightarrow I.
  
  6.11-10 UniversalMorphismFromImage
  
  UniversalMorphismFromImage( alpha, tau )  operation
  Returns:  a morphism in \mathrm{Hom}(\mathrm{im}(\alpha), T)
  
  The arguments are a morphism \alpha: A \rightarrow B and a pair of morphisms
  \tau = ( \tau_1: A \rightarrow T, \tau_2: T \hookrightarrow B ) where \tau_2
  is  a  monomorphism  such  that  \tau_2  \circ \tau_1 \sim_{A,B} \alpha. The
  output  is  the morphism u(\tau): \mathrm{im}(\alpha) \rightarrow T given by
  the universal property of the image.
  
  6.11-11 UniversalMorphismFromImageWithGivenImageObject
  
  UniversalMorphismFromImageWithGivenImageObject( alpha, tau, I )  operation
  Returns:  a morphism in \mathrm{Hom}(I, T)
  
  The  arguments  are  a morphism \alpha: A \rightarrow B, a pair of morphisms
  \tau = ( \tau_1: A \rightarrow T, \tau_2: T \hookrightarrow B ) where \tau_2
  is  a  monomorphism  such that \tau_2 \circ \tau_1 \sim_{A,B} \alpha, and an
  object  I  =  \mathrm{im}(  \alpha  ).  The  output is the morphism u(\tau):
  \mathrm{im}(\alpha)  \rightarrow  T  given  by the universal property of the
  image.
  
  6.11-12 AddImageObject
  
  AddImageObject( 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 ImageObject. F:
  \alpha \mapsto I.
  
  6.11-13 AddImageEmbedding
  
  AddImageEmbedding( 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 ImageEmbedding. F:
  \alpha \mapsto \iota.
  
  6.11-14 AddImageEmbeddingWithGivenImageObject
  
  AddImageEmbeddingWithGivenImageObject( 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
  ImageEmbeddingWithGivenImageObject. F: (\alpha,I) \mapsto \iota.
  
  6.11-15 AddCoastrictionToImage
  
  AddCoastrictionToImage( 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
  CoastrictionToImage. F: \alpha \mapsto c.
  
  6.11-16 AddCoastrictionToImageWithGivenImageObject
  
  AddCoastrictionToImageWithGivenImageObject( 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
  CoastrictionToImageWithGivenImageObject. F: (\alpha,I) \mapsto c.
  
  6.11-17 AddUniversalMorphismFromImage
  
  AddUniversalMorphismFromImage( 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
  UniversalMorphismFromImage. F: (\alpha, \tau) \mapsto u(\tau).
  
  6.11-18 AddUniversalMorphismFromImageWithGivenImageObject
  
  AddUniversalMorphismFromImageWithGivenImageObject( 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
  UniversalMorphismFromImageWithGivenImageObject. F: (\alpha, \tau, I) \mapsto
  u(\tau).
  
  
  6.12 Coimage
  
  For  a  given morphism \alpha: A \rightarrow B, a coimage of \alpha consists
  of four parts:
  
      an object C,
  
      an epimorphism \pi: A \twoheadrightarrow C,
  
      a morphism a: C \rightarrow B such that a \circ \pi \sim_{A,B} \alpha,
  
      a dependent function u mapping each pair of morphisms \tau = ( \tau_1:
        A  \twoheadrightarrow  T, \tau_2: T \rightarrow B ) where \tau_1 is an
        epimorphism  such  that  \tau_2  \circ  \tau_1  \sim_{A,B} \alpha to a
        morphism  u(\tau):  T  \rightarrow  C such that u( \tau ) \circ \tau_1
        \sim_{A,C} \pi and a \circ u( \tau ) \sim_{T,B} \tau_2.
  
  The  4-tuple ( C, \pi, a, u ) is called a coimage of \alpha if the morphisms
  u(  \tau  ) are uniquely determined up to congruence of morphisms. We denote
  the  object  C  of  such a 4-tuple by \mathrm{coim}(\alpha). We say that the
  morphism u( \tau ) is induced by the universal property of the coimage.
  
  6.12-1 MorphismFromCoimageToImage
  
  MorphismFromCoimageToImage( alpha )  attribute
  Returns:  a       morphism       in      \mathrm{Hom}(\mathrm{coim}(\alpha),
            \mathrm{im}(\alpha))
  
  The  argument  is  a  morphism  \alpha:  A  \rightarrow B. The output is the
  canonical   morphism   (in   a  preabelian  category)  \mathrm{coim}(\alpha)
  \rightarrow \mathrm{im}(\alpha).
  
  6.12-2 MorphismFromCoimageToImageWithGivenObjects
  
  MorphismFromCoimageToImageWithGivenObjects( alpha )  operation
  Returns:  a morphism in \mathrm{Hom}(C,I)
  
  The  argument  is  an object C = \mathrm{coim}(\alpha), a morphism \alpha: A
  \rightarrow  B,  and  an  object  I = \mathrm{im}(\alpha). The output is the
  canonical morphism (in a preabelian category) C \rightarrow I.
  
  6.12-3 AddMorphismFromCoimageToImageWithGivenObjects
  
  AddMorphismFromCoimageToImageWithGivenObjects( 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
  MorphismFromCoimageToImageWithGivenObjects.  F:  (C,  \alpha, I) \mapsto ( C
  \rightarrow I ).
  
  6.12-4 InverseMorphismFromCoimageToImage
  
  InverseMorphismFromCoimageToImage( alpha )  attribute
  Returns:  a        morphism       in       \mathrm{Hom}(\mathrm{im}(\alpha),
            \mathrm{coim}(\alpha))
  
  The  argument  is  a  morphism  \alpha:  A  \rightarrow B. The output is the
  inverse    of    the   canonical   morphism   (in   an   abelian   category)
  \mathrm{im}(\alpha) \rightarrow \mathrm{coim}(\alpha).
  
  6.12-5 InverseMorphismFromCoimageToImageWithGivenObjects
  
  InverseMorphismFromCoimageToImageWithGivenObjects( alpha )  operation
  Returns:  a morphism in \mathrm{Hom}(I,C)
  
  The  argument  is  an object C = \mathrm{coim}(\alpha), a morphism \alpha: A
  \rightarrow  B,  and  an  object  I = \mathrm{im}(\alpha). The output is the
  inverse of the canonical morphism (in an abelian category) I \rightarrow C.
  
  6.12-6 AddInverseMorphismFromCoimageToImageWithGivenObjects
  
  AddInverseMorphismFromCoimageToImageWithGivenObjects( 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
  MorphismFromCoimageToImageWithGivenObjects.  F:  (C,  \alpha, I) \mapsto ( I
  \rightarrow C ).
  
  6.12-7 IsomorphismFromCoimageToCokernelOfKernel
  
  IsomorphismFromCoimageToCokernelOfKernel( alpha )  attribute
  Returns:  a    morphism    in   \mathrm{Hom}(   \mathrm{coim}(   \alpha   ),
            \mathrm{CokernelObject}( \mathrm{KernelEmbedding}( \alpha ) ) ).
  
  The  argument  is  a  morphism  \alpha:  A  \rightarrow B. The output is the
  canonical      morphism      \mathrm{coim}(     \alpha     )     \rightarrow
  \mathrm{CokernelObject}( \mathrm{KernelEmbedding}( \alpha ) ).
  
  6.12-8 AddIsomorphismFromCoimageToCokernelOfKernel
  
  AddIsomorphismFromCoimageToCokernelOfKernel( 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
  IsomorphismFromCoimageToCokernelOfKernel. F: \alpha \mapsto ( \mathrm{coim}(
  \alpha   )  \rightarrow  \mathrm{CokernelObject}(  \mathrm{KernelEmbedding}(
  \alpha ) ) ).
  
  6.12-9 IsomorphismFromCokernelOfKernelToCoimage
  
  IsomorphismFromCokernelOfKernelToCoimage( alpha )  attribute
  Returns:  a     morphism     in    \mathrm{Hom}(    \mathrm{CokernelObject}(
            \mathrm{KernelEmbedding}( \alpha ) ), \mathrm{coim}( \alpha ) ).
  
  The  argument  is  a  morphism  \alpha:  A  \rightarrow B. The output is the
  canonical morphism \mathrm{CokernelObject}( \mathrm{KernelEmbedding}( \alpha
  ) ) \rightarrow \mathrm{coim}( \alpha ).
  
  6.12-10 AddIsomorphismFromCokernelOfKernelToCoimage
  
  AddIsomorphismFromCokernelOfKernelToCoimage( 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
  IsomorphismFromCokernelOfKernelToCoimage.     F:     \alpha     \mapsto    (
  \mathrm{CokernelObject}(  \mathrm{KernelEmbedding}(  \alpha  ) ) \rightarrow
  \mathrm{coim}( \alpha ) ).
  
  6.12-11 Coimage
  
  Coimage( alpha )  attribute
  Returns:  an object
  
  The  argument is a morphism \alpha. The output is the coimage \mathrm{coim}(
  \alpha ).
  
  6.12-12 CoimageProjection
  
  CoimageProjection( C )  attribute
  Returns:  a morphism in \mathrm{Hom}(A, C)
  
  This  is a convenience method. The argument is an object C which was created
  as  a  coimage  of  a  morphism  \alpha:  A \rightarrow B. The output is the
  coimage projection \pi: A \twoheadrightarrow C.
  
  6.12-13 CoimageProjection
  
  CoimageProjection( alpha )  attribute
  Returns:  a morphism in \mathrm{Hom}(A, \mathrm{coim}( \alpha ))
  
  The  argument  is  a  morphism  \alpha:  A  \rightarrow B. The output is the
  coimage projection \pi: A \twoheadrightarrow \mathrm{coim}( \alpha ).
  
  6.12-14 CoimageProjectionWithGivenCoimage
  
  CoimageProjectionWithGivenCoimage( alpha, C )  operation
  Returns:  a morphism in \mathrm{Hom}(A, C)
  
  The  arguments  are  a  morphism  \alpha:  A \rightarrow B and an object C =
  \mathrm{coim}(\alpha).   The   output  is  the  coimage  projection  \pi:  A
  \twoheadrightarrow C.
  
  6.12-15 AstrictionToCoimage
  
  AstrictionToCoimage( C )  attribute
  Returns:  a morphism in \mathrm{Hom}(C,B)
  
  This  is a convenience method. The argument is an object C which was created
  as  a  coimage  of  a  morphism  \alpha:  A \rightarrow B. The output is the
  astriction to coimage a: C \rightarrow B.
  
  6.12-16 AstrictionToCoimage
  
  AstrictionToCoimage( alpha )  attribute
  Returns:  a morphism in \mathrm{Hom}(\mathrm{coim}( \alpha ),B)
  
  The  argument  is  a  morphism  \alpha:  A  \rightarrow B. The output is the
  astriction to coimage a: \mathrm{coim}( \alpha ) \rightarrow B.
  
  6.12-17 AstrictionToCoimageWithGivenCoimage
  
  AstrictionToCoimageWithGivenCoimage( alpha, C )  operation
  Returns:  a morphism in \mathrm{Hom}(C,B)
  
  The  argument  are  a  morphism  \alpha:  A  \rightarrow B and an object C =
  \mathrm{coim}(  \alpha  ).  The  output  is  the  astriction to coimage a: C
  \rightarrow B.
  
  6.12-18 UniversalMorphismIntoCoimage
  
  UniversalMorphismIntoCoimage( alpha, tau )  operation
  Returns:  a morphism in \mathrm{Hom}(T, \mathrm{coim}( \alpha ))
  
  The arguments are a morphism \alpha: A \rightarrow B and a pair of morphisms
  \tau  =  (  \tau_1:  A \twoheadrightarrow T, \tau_2: T \rightarrow B ) where
  \tau_1  is  an  epimorphism such that \tau_2 \circ \tau_1 \sim_{A,B} \alpha.
  The  output  is  the morphism u(\tau): T \rightarrow \mathrm{coim}( \alpha )
  given by the universal property of the coimage.
  
  6.12-19 UniversalMorphismIntoCoimageWithGivenCoimage
  
  UniversalMorphismIntoCoimageWithGivenCoimage( alpha, tau, C )  operation
  Returns:  a morphism in \mathrm{Hom}(T, C)
  
  The  arguments  are  a morphism \alpha: A \rightarrow B, a pair of morphisms
  \tau  =  (  \tau_1:  A \twoheadrightarrow T, \tau_2: T \rightarrow B ) where
  \tau_1  is  an  epimorphism such that \tau_2 \circ \tau_1 \sim_{A,B} \alpha,
  and  an  object  C  =  \mathrm{coim}(  \alpha  ). The output is the morphism
  u(\tau): T \rightarrow C given by the universal property of the coimage.
  
  6.12-20 AddCoimage
  
  AddCoimage( 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 Coimage. F: \alpha
  \mapsto C
  
  6.12-21 AddCoimageProjection
  
  AddCoimageProjection( 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 CoimageProjection.
  F: \alpha \mapsto \pi
  
  6.12-22 AddCoimageProjectionWithGivenCoimage
  
  AddCoimageProjectionWithGivenCoimage( 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
  CoimageProjectionWithGivenCoimage. F: (\alpha,C) \mapsto \pi
  
  6.12-23 AddAstrictionToCoimage
  
  AddAstrictionToCoimage( 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
  AstrictionToCoimage. F: \alpha \mapsto a
  
  6.12-24 AddAstrictionToCoimageWithGivenCoimage
  
  AddAstrictionToCoimageWithGivenCoimage( 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
  AstrictionToCoimageWithGivenCoimage. F: (\alpha,C) \mapsto a
  
  6.12-25 AddUniversalMorphismIntoCoimage
  
  AddUniversalMorphismIntoCoimage( 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
  UniversalMorphismIntoCoimage. F: (\alpha, \tau) \mapsto u(\tau)
  
  6.12-26 AddUniversalMorphismIntoCoimageWithGivenCoimage
  
  AddUniversalMorphismIntoCoimageWithGivenCoimage( 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
  UniversalMorphismIntoCoimageWithGivenCoimage.  F:  (\alpha,  \tau,C) \mapsto
  u(\tau)