PS

Identity natural transformation による functorial equality

命題

Natural transformation:

  •  (\tau _ A : FA \to F'A) _ {A \in \mathcal{A}}

について

  •  (\forall A \in \operatorname{Ob} \mathcal{A})(FA = F'A \wedge \tau _ A = 1 _ {FA}) \implies F = F'

証明


\begin{aligned}

F'(f: A \to B) &= F'(f) \circ \tau _ A \\
      & \lbrace \text{naturality of } \tau \rbrace \\
      &= \tau _ B \circ F(f) \\
      &= F(f)

\end{aligned}