「モナドとテンソル強度のサンプル」の前半と同じ記号法を使い、(C, +, 0) はモノイド圏だとします。
a∈|C| を固定して、λx∈|C|.(a + x), λf∈C.(a + f) で定義される対応を考えます。a + f は、ida + f の略記と思ってください。このような対応を、Haskellのセクション記法を借用して (a+) と書くことにします。(a+)(x) = a + x, (a+)(f) = a + f = ida + f です。(+a) も同様に定義できます。
(a+) は、C→Cの関手になります。それを示すには次のことを確認します。
- (a+)(f;g) = (a+)(f);(a+)(g)
- (a+)(idx) = id(a+)(x)
定義により展開すれば、次の2つの等式となります。
- a + (f;g) = (a + f);(a + g)
- a + idx = ida + x
これらはほぼ自明でしょう。
次に、f:a→b をCの射として、自然変換 (f+)::(a+)⇒(b+):C→C を定義します。自然変換は成分となる射を指定すればいいので、次のように定義します。
- [(f+)x:(a+)(x) → (b+)(x)] := [(f + idx):a + x → b + x]
(f+)が、関手(a+)から関手(b+)への自然変換であるためには、次の図が可換になる必要があります（自然性）。
u : x → y(a+)(x) --(a+)(u)--> (a+)(y)
| |
(f+)_x (f+)_y
| |
v v
(b+)(x) --(b+)(u)--> (b+)(y)
もう少し分かりやすい記法で書くなら：
a + x --(a + u)--> a + y
| |
f + x f + y
| |
v v
b + x --(b + u)--> b + y
(a + u);(f + y) = a;f + u;y = f + u, (f + x);(b + u) = f;b + x;u = f + u ですから、確かに可換図式となります。
これにより、λa∈|C|.(a+) = λa∈|C|.λx∈|C|.(a + x), λf∈C.(f+) = λf∈C.λx∈|C|.(f + idx) は関手となります。Cの対象を「Cの自己関手」に、Cの射を「Cの自己関手間の自然変換」にマップします。
実は、今述べたことはイチイチ定義を確認しなくても言えます。モノイド圏Cを上空から眺めると、それは圏Cat内に棲んでいます。C∈|Cat| ですね。Cのモノイド積+は二項関手（双関手）ですから、+:C×C→C in Cat です。
ところが、Catはデカルト閉圏なので、Cat(A×B, C) = Cat(A, [C←B])、Cat(A×B, C) = Cat(B, [A→C]) という同型が成立します。[C←B] と [A→C] はどちらも指数（ベキ）ですが左右を区別しています。これらの同型が、左カリー化 (f:A×B→C) |→ (f^:A→[C←B]) と右カリー化 (f:A×B→C) |→ (^f:B→[A→C]) を与えます。
特に、A = B = C として、二項関手+に左右のカリー化をほどこすと、+^:C→[C←C], ^+:C→[C→C] が出てきます。+^(a) = (a+), ^+(a) = (+a) だったのです。[C←C] と [C→C] を区別する必要はなくて、どちらも End(C) = CC、つまり自己関手の圏（射は自然変換）です。モノイド積+のカリー化 +^ または ^+ により、Cは関手圏CCに埋め込めることになります。正確に言えば、ただちに埋め込みかどうかはわかりませんが、実用的な多くのケースでは埋め込みになっています。
