「カン拡張ラムダ計算化計画」より：
この記事ではこれ以上の内容は述べませんが、引き続く記事達でカン拡張ラムダ計算化計画をちょっとずつ実行する予定です。
というわけで、ちょっと書きます。
内容：
使う道具・技術・枠組み
「カリー vs. カン、双対 vs. 随伴」において、通常のラムダ計算をカリー計算〈Curry calculus〉、カン拡張に関わる計算をカン計算〈Kan calculus〉と呼びました。引き続き「カリー計算」「カン計算」を使いますが、この2つを対比する話はしません。
「カン拡張ラムダ計算化計画」より：
カン拡張とラムダ計算の比較対照はしてきたのですが、どうもこれでは物足りなくて、カン拡張とラムダ計算を同じ枠組み内で展開したい気がしてきました。つまり、「カン拡張とラムダ計算は似てる」ではなくて「カン拡張とラムダ計算は同じだ」と言いたいのです。
カリー計算とカン計算を統合した計算体系をカリー／カン計算〈Curry-Kan calculus〉と呼ぶことにして、話題はカリー／カン計算です。
カリー／カン計算を組み立てるにあたって使う道具・技術・枠組みは次のものです。
- テンプレート充填問題
- 関手の表現可能性
- グロタンディーク構成
- 随伴系
テンプレート充填問題〈template filling problem〉とは、以前はフレーム充填問題〈frame filling problem〉と呼んでいたものです（「圏論におけるフレーム充填問題」、「フレーム充填問題と解空間関手」参照）。フレームは、テンプレートのなかで既に決まっている部分で、埋める〈fillする〉のは、フレーム以外の未定の部分です。なので、テンプレート充填問題のほうが適切かな、と。
ストリング図やペースティング図として描かれたテンプレートを“穴埋め問題〈filling problem〉”と考えて解を求める、この行為を基本に据えたいと思います。
関手の表現可能性〈representability〉とは、別な言い方をすると圏論的普遍性〈category-theoretic universal property〉です。「普遍性」という言葉はだいぶ分かりにくいです（「圏論の普遍性が難しい理由」参照）。
普遍性を、前層の表現可能性（双対的に余前層の余表現可能性）から理解すると、幾分は事情がハッキリするでしょう。例えば以下の過去記事達（古い順）で、普遍性を表現可能性から扱っています。
カリー／カン計算の構成においても、テンプレート充填問題を関手の表現可能性問題と関係付けます。
表現可能な関手（前層または余前層）のグロタンディーク構成〈Grothendieck construction〉（要素の圏とも呼ばれます）は、関手の表現系〈representation system for a functor〉（「圏論の普遍性が難しい理由」、「前層の表現可能性 再論：指標による記述」参照）の情報をすべて保持しています。例えば、関手のグロタンディーク構成〈要素の圏〉の終対象は、表現対象と普遍元をエンコードしています。
関手の表現系を調べることと、関手のグロタンディーク構成（である圏）を調べることはほぼ同じです。
随伴系〈adjunction | adjoint system〉は、カリー／カン計算の中心概念と言えます。カリー／カン計算で扱う随伴系は、テンソル・ホム随伴系〈tensor-hom adjunction〉と呼ばれるタイプ〈類型〉の随伴系*1です。ひとつのテンソル・ホム随伴系から、1-双対〈1-dual〉、2-双対〈2-dual〉というニ種の双対により、全部で4種類の随伴系ができます。これらの随伴系を詳しく調べることが、カリー／カン計算の主たる課題だと言えます。
使う具体例
カリー／カン計算を展開する環境となる圏／2-圏／二重圏として、次のような具体例を適宜参照しようと思います。
- デカルト閉圏としての、集合圏
- デカルト閉圏としての、命題論理
- モノイド閉圏としての、実数体上のベクトル空間達の圏
- 2-圏としての、順序集合達と単調写像達の圏
- 圏達の2-圏
- 自然数不等式達と行列達の二重圏
- 二重圏としての、単純古典テンソル計算
- 集合のあいだのスパン達の二重圏
- 単射達と関係達の二重圏
- 関手達とプロ関手達の二重圏
バエズ／ドーラン曲面（「バエズ／ドーラン曲面の意義と使い方」参照）達のドクトリン（「補足と続き： ベックの分配法則に基づく“一般化圏の製造工場” // ドクトリン」参照）も二重圏、あるいは三重圏を形成しそうですが、事例に使えるほどにハッキリと分かっているわけじゃないです。もしハッキリ分かれば、これもカリー／カン計算の事例になり得る可能性があります。
他にも（例えば依存型理論から）何か具体例が見つかれば追加します。具体例はなんぼあってもいいですからね！
*1:「ラムダ計算の自然性とお絵描き」「モノイド閉圏： カリー化からニョロニョロまで」では、指数随伴系〈exponential adjunction〉という言葉を使っています。
