Arrow の first が満たすべき公理が式だけだとわかりにくいので図式にしてみる。

first と pure は図式の中では関手っぽさを出すため First と Pure のように先頭大文字にしてみた。

多相なものには気分によって型を補足した。

１．［拡張］ first (pure f) = pure (f×id)

Hom(X,Y) で X から Y への射の集まりを表すと

              (-)×id_D
  Hom(B,C) --------------> Hom(B×D,C×D)
    ｜                            ｜
    ｜ Pure                       ｜ Pure
    ↓                            ↓
  Hom(B,C) --------------> Hom(B×D,C×D)
               First_D

上辺は通常の関数の世界、下辺は Arrow の世界。

first (pure f) = pure (f×id) で f = id とすると

first (pure id) = pure (id×id)

pure id も pure (id×id) も idA なので

first が関手であるための条件の一つ

first idA = idA

が導かれる。

２．［関手］ first (f >>> g) = first f >>> first g

図は略。

上記の first idA = idA とこの法則が成り立つので first は関手。

３．［交換］ first f >>> pure (id×g) = pure (id×g) >>> first f

        f
  B1 --------> B2

        g
  C1 --------> C2

とすると

           Pure (id_B1×g)
  B1×C1 -----------------> B2×C2
    ｜                       ｜
    ｜ First_C1 f            ｜ First_C2 f
    ↓                       ↓
  B2×C1 -----------------> B2×C2
           Pure (id_B2×g)

４．［単位］ first f >>> pure fst = pure fst >>> first f

           Pure fst
  B×D -----------------> B
   ｜                    ｜
   ｜ First_D f          ｜ f
   ↓                    ↓
  C×D -----------------> C
           Pure fst

５．［結合］ first (first f) >>> pure assoc = pure assoc >>> first f

        f
  A --------> B

とすると

                  Pure assoc
  (A×C)×D ---------------------> A×(C×D)
      ｜                              ｜
      ｜ First_D (First_C f)          ｜ First_{C×D} f
      ↓                              ↓
  (B×C)×D ---------------------> B×(C×D)
                  Pure assoc