ラフ・ロードマップ -- 拡張版マイヒル／ネロード定理
遷移変換系を調べる手順（予定）をざっと書いておく。
まず、何を目標にするかというと、遷移変換系に関するマイヒル／ネロード定理。
- システムの圏（高次圏）Sysを定義する。
- 代数的な圏（高次圏）Algを定義する。
- 振る舞い関手B:Sys→Algを構成する。
- 実現関手（マイヒル／ネロード関手）N:Alg→Sysを構成する。
このとき：
上記の状況を、マイヒル／ネロード随伴（Myhill/Nerode adjunction）と呼びたい。
道具立て、副産物に関して：
- 振る舞い関手の構成にクリーネ／ファインマン公式を使う。
- 実現関手の構成には余代数を使う。
- 最小化の関係で、可到達代数と可観測代数が登場する（といいが？）。
- 振る舞いの値の圏はコゥゼン圏？
- ストーン双対が使えるといいな。
- ビドゥイット／ヘンニッカー／カーツ（Bidoit/Hennicker/Kurz）双対も使えるといいな。
- ゴールドブラッド（Goldblatt）双対も使えるといいな。
- 模倣（シミュレーション）、2方向模倣、双模倣が必要だろう。
- 一様性原理がどこかで登場しないか？
- ホーア論理に関するインスティチューションが登場するといいな。
- 超越的な方法だけでなく、具体的・構成的な方法が使えるといいのだが…
