5 Category 2-Cells
  
  
  5.1 Attributes for the Type of 2-Cells
  
  5.1-1 Source
  
  Source( c )  attribute
  Returns:  a morphism
  
  The  argument  is  a  2-cell  c: \alpha \rightarrow \beta. The output is its
  source \alpha.
  
  5.1-2 Range
  
  Range( c )  attribute
  Returns:  a morphism
  
  The  argument  is  a  2-cell  c: \alpha \rightarrow \beta. The output is its
  range \beta.
  
  
  5.2 Identity 2-Cell and Composition of 2-Cells
  
  5.2-1 IdentityTwoCell
  
  IdentityTwoCell( alpha )  attribute
  Returns:  a 2-cell
  
  The  argument  is  a  morphism  \alpha.  The  output  is its identity 2-cell
  \mathrm{id}_{\alpha}: \alpha \rightarrow \alpha.
  
  5.2-2 AddIdentityTwoCell
  
  AddIdentityTwoCell( 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 IdentityTwoCell. F:
  \alpha \mapsto \mathrm{id}_{\alpha}.
  
  5.2-3 HorizontalPreCompose
  
  HorizontalPreCompose( c, d )  operation
  Returns:  a 2-cell
  
  The  arguments  are  two  2-cells  c:  \alpha  \rightarrow  \beta, d: \gamma
  \rightarrow  \delta  between  morphisms  \alpha,  \beta: a \rightarrow b and
  \gamma,  \delta: b \rightarrow c. The output is their horizontal composition
  d \ast c: (\gamma \circ \alpha) \rightarrow (\delta \circ \beta).
  
  5.2-4 AddHorizontalPreCompose
  
  AddHorizontalPreCompose( 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
  HorizontalPreCompose. F: (c,d) \mapsto d \ast c.
  
  5.2-5 HorizontalPostCompose
  
  HorizontalPostCompose( d, c )  operation
  Returns:  a 2-cell
  
  The  arguments  are  two  2-cells  d:  \gamma  \rightarrow \delta, c: \alpha
  \rightarrow  \beta  between  morphisms  \alpha,  \beta:  a \rightarrow b and
  \gamma,  \delta: b \rightarrow c. The output is their horizontal composition
  d \ast c: (\gamma \circ \alpha) \rightarrow (\delta \circ \beta).
  
  5.2-6 AddHorizontalPostCompose
  
  AddHorizontalPostCompose( 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
  HorizontalPostCompose. F: (d,c) \mapsto d \ast c.
  
  5.2-7 VerticalPreCompose
  
  VerticalPreCompose( c, d )  operation
  Returns:  a 2-cell
  
  The  arguments  are  two  2-cells  c:  \alpha  \rightarrow  \beta,  d: \beta
  \rightarrow \gamma between morphisms \alpha, \beta, \gamma: a \rightarrow b.
  The  output  is  their  vertical  composition  d \circ c: \alpha \rightarrow
  \gamma.
  
  5.2-8 AddVerticalPreCompose
  
  AddVerticalPreCompose( 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 VerticalPreCompose.
  F: (c,d) \mapsto d \circ c.
  
  5.2-9 VerticalPostCompose
  
  VerticalPostCompose( d, c )  operation
  Returns:  a 2-cell
  
  The  arguments  are  two  2-cells  d:  \beta  \rightarrow  \gamma, c: \alpha
  \rightarrow  \beta between morphisms \alpha, \beta, \gamma: a \rightarrow b.
  The  output  is  their  vertical  composition  d \circ c: \alpha \rightarrow
  \gamma.
  
  5.2-10 AddVerticalPostCompose
  
  AddVerticalPostCompose( 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
  VerticalPostCompose. F: (d,c) \mapsto d \circ c.
  
  
  5.3 Well-Definedness for 2-Cells
  
  5.3-1 IsWellDefinedForTwoCells
  
  IsWellDefinedForTwoCells( c )  operation
  Returns:  a boolean
  
  The  argument  is  a  2-cell  c.  The  output  is true if c is well-defined,
  otherwise the output is false.
  
  5.3-2 AddIsWellDefinedForTwoCells
  
  AddIsWellDefinedForTwoCells( 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
  IsWellDefinedForTwoCells. F: c \mapsto \mathtt{IsWellDefinedForMorphisms}( c
  ).