Awodey本から離れて久しい。圏論(16) - らんだむな記憶が実質最後に触れた箇所だ。
arrow category $\mathbf{C}^\to$
\begin{equation}
\begin{CD}
A @> g_1 >> A^\prime @> h_1 >> A^{\prime\prime} \\
@V f VV \circlearrowright @VV f^\prime V \circlearrowright @VV f^{\prime\prime} V \\
B @>> g_2 > B^\prime @>> h_2 > B^{\prime\prime}
\end{CD}
\end{equation}
ということで、 $g = (g_1,g_2),\ h = (h_1,h_2)$ に対して、
\begin{equation}
h \circ g = (h_1,h_2) \circ (g_1,g_2) = (h_1 \circ g_1, h_2 \circ g_2)
\end{equation}
という感じで良いかな。また、
$$ 1_f = (1_{\mathrm{dom}(f)},1_{\mathrm{cod}(f)})$$
となる。
functors として $\mathbf{C} \xleftarrow{\mathrm{dom}} \mathbf{C}^\to \xrightarrow{\mathrm{cod}} \mathbf{C}$ を持つとあるので、 $\mathrm{dom}$ のほうだけ見ておこう。
- $\mathbf{C}^\to \ni f \overset{\mathrm{dom}}{\mapsto} \mathrm{dom}(f) \in \mathbf{C}$
- $\mathbf{C}^\to \ni g = (g_1,g_2) \overset{\mathrm{dom}}{\mapsto} g_1 \in \mathbf{C}$
とすると、
(a) $\mathrm{dom}(g: f \to f^\prime) = g_1: \mathrm{dom}(f) \to \mathrm{dom}(f^\prime)$
(b) $\mathrm{dom}(1_f) = 1_{\mathrm{dom}(f)}$
(c) $\mathrm{dom}(h \circ g) = h_1 \circ g_1 = \mathrm{dom}(h) \circ \mathrm{dom}(g)$
で確かに functor になっている。 $\mathrm{cod}$ については $\mathbf{C}^\to \ni g = (g_1,g_2) \overset{\mathrm{cod}}{\mapsto} g_2 \in \mathbf{C}$ と定めて、あとは上記で $\mathrm{dom}$ を$\mathrm{cod}$ に置き換えて読めば良い。
