圏ΩΟ、モデル論、ambient category
ΩΟに空集合を入れるのは止めた。直和が定義できないのだから始対象だけあってもしょうがない。
なんかのモデル論をやるとき、その内部でモデルを構成する側の圏を背景圏（ambient category）と呼んでおこう。Set、Ord（順序集合）、Vect（線形空間）なんかが背景圏によく使われますね。ΩΟ（Omega-Omicron）も背景圏のために定義した。
- ΩΟは具象的である。手で触れる。
- ΩΟは直積と終対象を持つ。
- ΩΟは指数を持ち、デカルト閉である。
- ΩΟは自分自身でenrichされている。
- ΩΟは共変、反変のpower monadを持つ。
- ΩΟは集合圏からの自然な埋め込み関手を持つ。
- ΩΟはConway不動点オペレータを持つ。
- ΩΟはトレース付きモノイド圏である。
あと、dualityがあるといいんだけどな。
教訓
今までやって気が付いたことを再確認しておこう。
- 代数構造にこだわりすぎない。
- 順序を忘れるな、順序が本質。
- 不動点⇔μオペレータ⇔トレース -- つまりCSHH定理を使え。
- 対称σの扱いに注意。
- 直和の扱いに注意。
Sequenceの代数は確かにクリーニ（クリーネ）代数になるのだが、他の領域もきれいな代数になるとは限らない。実は代数構造がなくてもなんとかなるし、演算の選び方も激しく恣意的。順序さえあればいいのだ。だから順序に注目すべき。
不動点は順序から構成する。不動点概念とμ記法による表現とトレースを使った意味論、となる。表現の圏のほうが扱いが難しい。表現の圏では、対称や直和がみえにくくなるので注意。人間が手で扱う表現とモデルとのあいだに、適当な圏（二圏、hom-catは表現の書き換えの圏）をはさむと良いだろう。α変換とμ計算の形式的体系が必要だ。
Conway不動点のμ表現
- 不動点：f† = <f†, A>;f -- μx.f(x, a) = f(μx.f(x, a), a)
- 自然性：[(g×X);f]† = g;f† -- μx.(f(x, g(b)) = (μx.f(x, a))[g(b)/a]
- 対角自然性：(f;g)† = [(A×g);f]† -- μx.g(f(x, a)) = μt.f(g(t), a)
- 対角性（ダブルダガー）：(f†)† = [(A×Δ);f]† -- μx.(μx'.f(x', x, a)) = μx.f(x, x, a)
μで書くと、また違った味わい。
ちなみに、Conwayのdouble iteration identities, composition identitiesは、t = t(x, y, z1, ...), s = s(x, z1, ...), r=r(x, z1, ...) として、
（http://citeseer.ist.psu.edu/bloom00iteration.htmlより。）
普通の自然性はどうなっているんだ？
それはそうと、λ記法やμ記法を使うと簡単になるのかな？ 圏論にあわせると、なんだか風変わりなラムダになってしまう気もする。Katyだって、まーラムダみたいなもんだしな。
