- 論域が大きい場合〈large domain of discourse〉を考える。
- 複アロー構成と多アロー構成、そのときのパラメータとしてのコレクションモナド
- コレクションモナドの一種としてのバンチモナド
- 型コンテキストと指標は同一概念であること。
- 命題コンテキストはフィイバー方向の型コンテキスト
- ベース方向とファイバー方向の“切れ目”を変えること。
- バンチの分配法則
- 色々な多圏様構造と色々なシーケント計算
- リーズニング・プログラミング： メタリーズニングは Apply, Comp, Prod があるCCC（かな？）
- 導出を対象として、リーズニングを射とするCCC（かな？）での計算がリーズニング・プログラミング
