「外部バージョンの依存カリー同型」にて：
外部バージョンの依存カリー同型は、極限の定義をなぞっているだけなので、内部化しないと面白くはありません。面白くすることは、今考え中です。
集合圏とは限らない圏 $`\mathcal{C}`$ に対して依存カリー同型を定義するのはけっこう面倒です。“今考え中”なんですが、そのための素材や道具を紹介します。$`\newcommand{\Imp}{\Rightarrow}
\newcommand{\cat}[1]{ \mathcal{#1} }
\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\hyp}{\text{-}}
\newcommand{\In}{\text{ in }}
\newcommand{\bto}{ \mathrel{\bullet\!\!\!\to} }
`$
内容：
パワーリングとコパワーリング
「カリー／ハワード／ランベック対応の辞書： 推論規則再論」にて：
$`A, B, X, Y`$ などは圏 $`\mathcal{C}`$ の対象を表します。$`I, J`$ なども $`\mathcal{C}`$ の対象ですが、これらを“集合とみなす方法”〈dereification〉があるとします*1。
[脚注 *1] この仮定は、パワーリング／テンソリングを使って取り除くことができるかも知れません。現状、よくわからない。
パワーリングとテンソリング（コパワーリングの同義語）はnLabに項目があります。
nLabでは、一般的な豊穣圏〈enriched category〉の文脈でパワーリング／コパワーリングが定義されてますが、ここでは通常の圏、つまり$`{\bf Set}`$-豊穣圏だけを考えます。この記事では、「コパワーリング」より「テンソリング」という言葉を使います。
単なるパワーリング／テンソリングではどうも足りないようなので、圏のモノイド作用〈monoidal action〉と組み合わせます。
圏のモノイド作用〈アクテゴリー〉
$`\cat{M} = (\cat{M}, \otimes, {\bf 1})`$ はモノイド圏とします。モノイド圏は必ずしも厳密〈strict〉とは限りませんが、律子 $`\alpha, \lambda, \rho`$ は省略します。
$`\cat{C}`$ は圏（とりあえずは単なる圏）だとして、二項関手〈双関手〉$`(\odot):\cat{C}\times \cat{M} \to \cat{C}`$ があって、次の同型があるとします。
- $`A\odot {\bf 1} \cong A`$
- $`A\odot (J\otimes K) \cong (A\odot J)\odot K`$
さらに、マックレーンの五角形／三角形の法則を満たすとき、複合構造 $`(\cat{M}, \cat{C}, \odot)`$ を右アクテゴリー〈right actegory〉といいます。モノイド圏 $`M`$ が圏 $`\cat{C}`$ に右モノイド作用〈right {monoid | monoidal} action〉するともいいます。あるいは、圏 $`\cat{C}`$ は（作用 $`\odot`$ により）モノイド圏 $`\cat{M}`$ 上の右加群圏〈right module category〉だともいいます。
左アクテゴリー〈left actegory〉も同様に定義できます。
ひとつの圏 $`\cat{C}`$ に対して、モノイド圏 $`M`$ が左から作用し、モノイド圏 $`\cat{N}`$ が右から作用しているとき、複合構造 $`(\cat{M}, \cat{N}, \cat{C}, \odot, \oslash)`$ を両側アクテゴリー〈two-sided category〉といいます。$`\cat{M} = \cat{N}`$ であって、次の同型が在るときは対称両側アクテゴリー〈symmetric two-sided category〉と呼ぶことにします。
$`\quad J\odot A \cong A \oslash J`$
対称両側アクテゴリーの場合は、左作用と右作用を同じ記号 $`\odot`$ で表すことにすれば：
$`\quad J\odot A \cong A \odot J`$
対称モノイド圏の場合と同様な法則も必要ですが割愛します。
デカルト圏へのモノイド作用
$`\cat{K}`$ は集合圏の部分圏だとします。例えば、$`\cat{K} = {\bf Set}`$ でもいいし、$`\cat{K} = {\bf FinSet}`$（有限集合だけからなる部分圏）とかです。$`\cat{K}`$ は単元集合 $`{\bf 1} = \{*\}`$ を含み直積で閉じているとします。つまり、$`(\cat{K}, \times, {\bf 1})`$ は直積によるモノイド圏とします。
圏 $`\cat{C} = (\cat{C}, \otimes, {\bf 1})`$ もデカルト圏とします。例えば、完備順序集合〈CPO〉と順序連続写像の圏がその例です。モノイド圏 $`\cat{K}`$ がデカルト圏 $`\cat{C}`$ に両側モノイド作用しているとします。左右のモノイド作用は対称で、複合構造 $`(\cat{K}, \cat{C}, \odot, \odot)`$ は対称両側アクテゴリーになっているとしましょう。
この状況だと、次の同型を要請するのは自然でしょう。
- $`J\odot (A \otimes B) \cong (J\odot A)\otimes B`$
- $`(A \otimes B)\odot K \cong A \otimes (B\odot K)`$
これらの同型と関連する法則を仮定します。
混乱の心配がなければ、$`\cat{C}`$ のモノイド積も $`\times`$ で書くことにします（デカルト積なので）。仮定する同型は次の形になります。
- $`J\odot (A \times B) \cong (J\odot A)\times B`$
- $`(A \times B)\odot K \cong A \times (B\odot K)`$
若干混乱の心配もありますが、モノイド圏の単位対象はすべて $`{\bf 1}`$ でオーバーロードします。$`\cat{C}`$ の単位対象と、$`\cat{K}`$ による対称両側作用により、次の定義をします。
$`\quad \hat{\hyp}: \cat{K} \to \cat{C}\\
\quad J \mapsto \hat{J} := J\odot {\bf 1} \cong {\bf 1}\odot J
`$
$`(\odot)`$ が二項関手〈双関手〉なので、片一方の引数を固定した $`\hat{\hyp}`$ は関手になります。この関手により、$`\cat{K}`$ を $`\cat{C}`$ の内部に取り込めます。$`\hat{\hyp}`$ が単射的になるとは限りませんが、実例では単射的なことが多いです。
$`J\in |\cat{K}|`$ に対して、$`\hat{J} \in |\cat{C}|`$ は、集合を $`\cat{C}`$ の対象とみなしたものです。$`\hat{J}`$ は $`J`$ のレイフィケーション〈reification〉*1とかコード化〈encoding〉と呼びます。
集合部分圏であるデカルト圏 $`\cat{K}`$ が作用しているデカルト圏 $`\cat{C}`$ では、$`\cat{K}`$ に属する集合／写像を $`\cat{C}`$ 内にレイファイ／コード化〈エンコード〉することができます。
テンソリング〈コパワーリング〉
テンソリングとモノイド作用は独立な概念です。テンソリングのためにモノイド作用が必要なわけではありません。しかしここでは、モノイド作用 $`(\odot)`$ がテンソリングにもなっている状況を考えます。
次の同型を考えます。
$`\text{ for }J\in |\cat{K}| \subseteq |{\bf Set}|\\
\text{ for }X, A\in |\cat{C}|\\
\quad \cat{C}(J \odot X, A) \cong {\bf Set}(J, \cat{C}(X, A) ) \In {\bf Set}`$
これがテンソリング〈コパワーリング〉を定義する同型です。$`\cat{K} = \cat{C} = {\bf Set}`$ の場合は、集合圏のカリー同型になるので、ここではテンソリング・カリー同型〈tensoring Curry isomorphism〉と呼んでおきます。
モノイド作用 $`\odot`$ の代わりにレイフィケーション $`\hat{J}`$ を使って書けば：
$`\quad \cat{C}(\hat{J} \times X, A) \cong {\bf Set}(J, \cat{C}(X, A) ) \In {\bf Set}`$
テンソリング・カリー同型がどの程度成立することを要求するか？ は考えなくてはならない問題です。とりあえず、$`J, X`$ をうまく選べば次のような関手の自然同型が成立することを要求しましょう。
$`\quad \cat{C}(\hat{J} \times X, \hyp) \cong {\bf Set}(J, \cat{C}(X, \hyp) ) \In {\bf CAT}(\cat{C}, {\bf Set})`$
パワーリング
$`\cat{K}, \cat{C}`$ は前節までと同じ設定で、パワーリングとは次の形の二項関手です。
$`\quad \cat{K}^\mathrm{op} \times \cat{C} \to \cat{C}`$
第一引数に関しては反変なことに注意してください。この形の反変・共変の二項関手を $`[\hyp \bto \hyp]`$ で表すことにします。
$`[\hyp \bto \hyp]`$ がパワーリング〈powering〉であるための同型は次のものです。
$`\text{ for }J\in |\cat{K}| \subseteq |{\bf Set}|\\
\text{ for }X, A\in |\cat{C}|\\
\quad \cat{C}(X, [J \bto A]) \cong {\bf Set}(I, \cat{C}(X, A) ) \In {\bf Set}`$
テンソリングの場合と同様に、$`J, X`$ をうまく選べば次のような関手の自然同型が成立することを要求します。
$`\quad \cat{C}(X, [J \bto \hyp] ) \cong {\bf Set}(I, \cat{C}(X, \hyp) ) \In {\bf CAT}(\cat{C}, {\bf Set})`$
おわりに
以上、対称両側モノイド作用、テンソリング、パワーリングを紹介しました。これらの素材・道具があれば、依存カリー同型を定式化できると思うのですが、全部必要かどうかはわかりません。不要な素材・道具が混じっているかも知れません。あるいは逆に、必要なものを見過ごしている可能性もあります。
やってみないとわかりません。ほぼ準備はできた気がするので組み立ててみます。
*1:抽象的なモノを具象化するのがレイフィケーションです。具体的な集合が圏の対象になってしまうと抽象化ですが、$`\cat{C}`$ の住人から見ると、得体の知れない外界のモノが自分たちの世界に降りてきたように見えるでしょう。
