Globular探り 16：可換モノイド
日本語を入れるとダメだった。日本語なしに書き換えて公開したらロードできた。
v2は公理のみ、v3は定理をひとつだけ証明。
v2の公理群は見ればわかると思うが、定理の証明がすぐに忘れそうだから書いておく。v3で追加した定理は、右単位律。通常はモノイドの公理だが、可換律があるので不要だからv2の公理に入れてなかった。
定理が正しいことの確認はたぶん次の2つの段階がある。
- 行為として、前提から結論に至る遷移系列を経験する。
- その行為の経験を、空間化／図形化／対象化する。
行為として経験するには、
- 前提となる図を作る。(M
unit);mult の絵だ。
- これを変形して、結論であるM（正確に言えば、^をbump-up演算子として M^）まで持っていく。
- 結論の絵を眺めて満足する。
以上の時間的な行為列である経験を空間化するには、
- 前提となる図を作る。これは同じ。
- bump-upする。これで次元が1増えて、増えた次元を時間とみなす。
- bump-upした前提は、空間図形の加工の原材料（未加工状態）とみなす。
- モースレベルが0の始端をビューする。「ビューする」とは、適当な射影とスライスを選ぶこと。
- このビューに対して、経験のときと同じ行為を遂行する。
- この行為は、この状況では図形（空間的存在物）の加工になっている。
- 行為が済んだら、パラメータであるモースレベルを動かして確認する。
- 時間的な行為を閉じ込めた n + 1 次元の図形が出来る。
- この図形にサロゲートで名前を付ける。この場合は「右単位律」を意味する名前。
- この図形のリライターは、サロゲートと証明行為（の空間化）をリンクさせて、相互変換する。
