Goto Chapter: Top 1 2 3 4 5 6 7 8 9 10 11 12 13 Ind

### 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$$.

 ‣ 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)$$.

 ‣ 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)$$.

 ‣ 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$$.

 ‣ 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$$.

 ‣ 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.

 ‣ AddIsWellDefinedForTwoCells( C, F ) ( operation )
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 )$$.