二分木と書き換えの圏

Melliesの"MacLane's coherence theorem expressed as a word problem"も、今読んでみると面白い。このなかでAという固有名詞で表記される圏が出てくる。Aを僕なりに再定義してみる。Aより弱い（構造が少ない）A（イタリックじゃない）を定義する。

リーフノードが0, 1である二分木の全体をTとする。文字LとRの並び（空列も認める）をパスと呼ぶ。パスpはノードを指す。空列はルートを指す。pが指すノードが二分木a内に存在するときは p↓a と書く。p↓aのとき、a[p]はpが指すノードそのもの。

1. pL↓a で、a[pL]がリーフでないとき、α[p](a)が定義できる。
2. p↓a で、a[p]がリーフでなく、a[pL]が0のとき、λ[p](a)が定義できる。
3. p↓a で、a[p]がリーフでなく、a[pR]が0のとき、ρ[p](a)が定義できる。

1. α[p](a)は、ツリーaのノードa[p]に関して結合律書き換えを適用した結果。
2. λ[p](a)は、ツリーaのノードa[p]に関して左単位律書き換えを適用した結果。
3. ρ[p](a)は、ツリーaのノードa[p]に関して右単位律書き換えを適用した結果。

α^-1, λ^-1, ρ^-1 も同様に定義する。

ξを、α, λ, ρ, α^-1, λ^-1, ρ^-1 のどれかだとして、(a, ξ[p], ξ[p](a)) の3つ組をすべて考える。Tを頂点、この(a, ξ[p], ξ[p](a))を辺とする有向グラフが出来る。このグラフから自由生成された圏をTとする。

Tに、五角形／三角形条件で規定される射の同値関係を入れる。すると、TをE圏（各ホムセットに同値関係を持つ圏）とできる。Tを同値関係（合同）で割ると再び圏となる。対象は変わらない。T/≡ をAとする。

圏Aは、単一の生成元から生成された自由モノイド圏となる。このモノイド圏は厳密ではない。厳密にするには、対象類に同値関係を入れて割り算する必要がある。