「カリー／ハワード／ランベック対応の辞書： 推論規則再論」で次のように書いています。
$`A, B, X, Y`$ などは圏 $`\mathcal{C}`$ の対象を表します。$`I, J`$ なども $`\mathcal{C}`$ の対象ですが、これらを“集合とみなす方法”〈dereification〉があるとします*1。
[脚注 *1] この仮定は、パワーリング／テンソリングを使って取り除くことができるかも知れません。現状、よくわからない。
「よくわからない」のは、圏の外部にあるモノを圏の内部に入れ込む方法／あるいは逆に圏の内部にある対象を圏の外部に引っ張り出す方法です。わからない部分は保留として、わかっていることを書きます。$`\newcommand{\Imp}{\Rightarrow}
\newcommand{\cat}[1]{ \mathcal{#1} }
\newcommand{\mrm}[1]{ \mathrm{#1} }
`$
内容：
準備
$`\cat{C}`$ は圏、$`I`$ は集合として、$`A:I \to |\cat{C}|`$ を“$`I`$ でインデックス付けられた $`\cat{C}`$ の対象の族”〈$`I`$-indexed family of objects of $`\cat{C}`$〉とします -- 長たらしいので単に「族」または「ファミリー」といいます。$`i \mapsto A_i`$ という書き方をして、インデックス〈引数〉が入る場所を黒丸で示した $`A_\bullet`$ も使います。
上記のごとき族〈ファミリー〉の全体がなす圏を $`{\bf Fam}[I, \cat{C}]`$ とします。対象は族で、射は“族のあいだの準同型写像”です。族のあいだの準同型写像 $`\alpha : A_\bullet \to B_\bullet`$ は次のように与えられます。
- $`\alpha : I \to \mrm{Mor}(\cat{C})`$
- $`\text{for }i\in I,\; \mrm{dom}(\alpha_i) = A_i`$
- $`\text{for }i\in I,\; \mrm{cod}(\alpha_i) = B_i`$
$`\alpha`$ は、$`I`$ を離散圏とみなしての自然変換です。
$`X \in |\cat{C}|`$ に対して、定数族〈constant family〉$`\mrm{K}^X_\bullet`$ を次のように定義します。
- $`\text{for }i\in I,\; \mrm{K}^X_i = (\mrm{K}^X)_i := X`$
すると、$`\beta : \mrm{K}^X_\bullet \to A_\bullet`$ は、頂点 $`X`$ で底面が $`A_\bullet`$ の錐〈cone〉を表します。
$`\prod`$ を集合圏でのパイ構成（無限個かも知れない集合達の直積）として次が成立します。
$`\quad {\bf Fam}[I, \cat{C}](\mrm{K}^X_\bullet, A_\bullet)
\cong \prod_{I} \cat{C}(X, A_\bullet) = \prod_{i\in I} \cat{C}(X, A_i)
`$
この同型は、カリー化と直接的な関係はないですが、カリー化と共に（同じ場面で）使われます。
外部バージョンの依存カリー同型
族 $`A_\bullet : I \to |\cat{C}|`$ を関手とみなしての極限が存在するとします。次のように書きます。
$`\quad \Pi_I A_\bullet := \mrm{lim}_I A_\bullet = \mrm{lim}_{i\in I} A_i`$
$`\prod`$ と $`\Pi`$ に本質的な違いはありませんが、$`\prod`$ は集合圏での具体的な構成物、$`\Pi`$ は極限の別記法として使います。
外部バージョンの依存カリー同型は次の同型です。極限の定義を知っていれば自明になります。
$`\quad \prod_I \cat{C}(X, A_\bullet) \cong \cat{C}(X, \Pi_I A_\bullet)
`$
「外部バージョン」と言っているのは、$`I`$ が圏 $`\cat{C}`$ の内部に居る対象とは限らないからです。
前節の同型と組み合わせると、次の3つの集合が同型になります。
- $`{\bf Fam}[I, \cat{C}](\mrm{K}^X_\bullet, A_\bullet) `$
- $`\prod_I \cat{C}(X, A_\bullet)`$
- $`\cat{C}(X, \Pi_I A_\bullet)`$
通常の（非依存な）カリー同型と繋ぐためには、$`I`$ を“内部化”する必要があります。外部バージョンの依存カリー同型は、極限の定義をなぞっているだけなので、内部化しないと面白くはありません。面白くすることは、今考え中です。
