λΠ＋CICによるリーズニング実現

まだ未整理だが、とりあえず備忘メモ。

まず、対称性がある操作達。

1. 無制限タプル構成
2. 無制限コタプル構成（無制限タプル構成の双対）
3. 有限タプル構成（無制限から制限）
4. 有限コプル構成（有限タプル構成の双対）
5. 依存カリー化
6. カリー化（依存カリー化の非依存版）
7. 依存反カリー化（依存カリー化の逆写像）
8. 反カリー化（カリー化の逆写像、依存反カリー化の非依存版）

これらは次のように還元される。

1. 無制限タプル構成 ⇒ 依存カリー化
2. 無制限コタプル構成
3. 有限タプル構成 ⇒ 無制限タプル構成 ⇒ 依存カリー化
4. 有限コプル構成 ⇒ 無制限コタプル構成
5. 依存カリー化
6. カリー化 ⇒ 依存カリー化
7. 依存反カリー化 ⇒ 依存評価射＋後結合 ⇒ 依存評価射＋結合
8. 反カリー化 ⇒ 依存反カリー化 ⇒ 依存評価射＋後結合 ⇒ 依存評価射＋結合

結局、必要なものは：

1. 依存カリー化
2. 無制限コタプル構成
3. 依存カリー化
4. 無制限コタプル構成
5. 依存カリー化
6. 依存カリー化
7. 依存評価射＋結合
8. 依存評価射＋結合

まとめると次の4種類：

1. 依存カリー化 λΠ（X |- λ.f : ΠA）
2. 無制限コタプル構成 ρΣ（ρは檜山が勝手に付けた ΣA |- ρ.f: Y）
3. 依存評価射 dep_ev
4. 結合 poly_comp

基本射も4種類：

1. 恒等射 id
2. 終射 !
3. 始射 θ
4. 依存評価射 dep_ev