記法の監獄の例：マックレーンの一貫性

ラックス・モノイド関手をラクソイド（laxoid）と呼ぶことにする。オプラックス・モノイド関手はコラクソイド。タイト・ラクソイド＝タイト・コラクソイド。厳密は考えてもしょうがない。

結合律子とラクソイドの関係を長年気付かなかったのは、やはり記法の監獄だろう。

結合律子を (A, B, C).α と書くことにする。μはラクソイドの乗法。Rは右掛け算関手。

• (A, B).μ : A.R*B.R → AB.μ
• X.(A, B).μ : X.(A.R*B.R) → X.(AB.μ)
• X.(A, B).μ : (XA)B → X(AB)
• (X, A, B).α : (XA)B → X(AB)

結局：

• X.(A, B).μ := (X, A, B).α

(X, A, B).α を (X, (A, B)).α' とすれば、

• X.(A, B).μ := (X, (A, B)).α'

(A, B) = AB と置けば、

• X.AB.μ := (X, AB).α'
• AB.μ = λX.[(X, AB).α']

ラクソイドの乗法μは、結合律子αの左変数によるカリー化（ラムダ抽象）になっている。カリー化して本質が変わるわけではないので、

• ラクソイドの乗法とは結合律子である。

と言える。そして、ラクソイドの結合法則は、「結合律子の結合法則」となる。ところが、

• ラクソイドの結合法則＝マックレーン五角形等式

だったから、結合律子の結合法則＝マックレーンの五角形法則 となる。

結合法則を満たす代数系では、一般結合法則が成立する。ラクソイドにおける一般結合法則がマックレーンの一貫性定理となる。

となると、通常の一般結合法則の証明と並行したラクソイドの一般結合法則の証明があるはずで、それがマックレーンの一貫性定理の証明にもなるはず。

記法の監獄から抜け出れば、事情は簡明なのだ。記法が耐え難くゴチャゴチャしていただけ。