「依存積型」と「依存和型」に関しては、もうサンザンだよー、あったく‥‥（昨日の記事「依存型と総称型の圏論的解釈」の冒頭を参照）
ふんとに「依存ナントカ型」って紛らわしいよねぇ。それで、「依存ナントカ型」と言うのはやめます。
なんかまた
間違える混乱する気がするので、今後は見たままのパイ型／シグマ型を使おうと思います。
パイ〈Π〉とかシグマ〈Σ〉って呼び名にすると、思い出すことがあります -- $`\Sigma \dashv \Delta \dashv \Pi`$ という随伴の系列です。依存型のパイ型／シグマ型も、この“Σ-Δ-Π随伴”の事例です。パイ型／シグマ型をもう少し一般化することができて、それはカン拡張になります。
てな話を手短かにします。昨日の記事「依存型と総称型の圏論的解釈」の続きです。
内容：
錐と、定数関手からの自然変換
「依存型と総称型の圏論的解釈」と同様、Cは集合圏Setの部分圏であるデカルト閉圏とします（この仮定はあまり使いませんが）。F:J(A) → C は、J(A)をインデックス域とするC-ファミリーとします。これは単に「Fは関手だ」と言っているのと同じです。ψは、X∈|C| を頂点として、Fを底面とする錐だとします。
錐ψについてもっと詳しく言うと； a∈A ごとに ψa:X → F(a) in C が割り当てられているときに、その全体を錐〈cone〉というのです。ただし、今回の錐はちょっと特殊で、底面である関手 F:J(A) → C が離散圏からの関手なので、図式可換性に関する条件が何もありません。域が離散圏じゃなければ図式可換性の条件が加わります。
「錐ψ、頂点X、底面F」なんて呼び名をするのは次のような感じだからです。A = {a, b, c} の絵です*1。
$`
F: \{a, b, c\} \to \mathcal{C} \mbox{ in }{\bf CAT}\\
\:\\
\mbox{in }\mathcal{C}\\
\xymatrix@R+1pc {
{}
&*{X} \ar[dl]_-{\psi_a} \ar[d]|-{\psi_b} \ar[dr]^-{\psi_c}
&
\\
*{F(a)}
&*{F(b)}
&*{F(c)}
}
`$
頂点から底面に向かう射を、僕は“成分線”と呼んでいます。すぐ下で説明するように、自然変換の成分〈component〉だからです。
J(A)のすべての対象（集合Aの要素）を特定対象Xに対応させる関手を KA(X):J(A) → C とします。
- すべての a∈A に対して、KA(X)(a) = X
Xを頂点、Fを底面とする錐ψは、定数関手KA(X)からFへの自然変換と同じです。ちょっと考えればわかることだと思います。
上の事実から、錐ψを自然変換の記法で書くことにします。
- ψ::KA(X) ⇒ F:J(A) → C in CAT
CATの2-射である自然変換は、関手圏の射〈1-射〉なので次のようにも書けます。
- ψ:KA(X) → F in [J(A), C]
ここで、[J(A), C] は、J(A)からCへの関手を対象として自然変換を射とする関手圏です。関手圏[J(A), C]のホムセットを使って次のように書いても同じことです。
- ψ∈[J(A), C](KA(X), F)
右随伴Πと左随伴Σ
ファミリー〈関手〉F:J(A) → C のパイ型 ΠA(F) とは、極限 Limj(A)(F) のことでした。極限の定義から、錐 ψ:KA(X) → F in [J(A), C] と射 f:X → ΠA(F) は1：1対応するのでした。この1：1対応は次のように書けます。左辺は錐の集合、右辺は射の集合です。
- $` [J(A), \mathcal{C}](K_A(X), F) \cong \mathcal{C}(X, \Pi_A(F))`$
実際には関手性とか自然性とかのチェックが必要なんですが、上記の同型は、関手KAと関手ΠAが随伴関手ペアであることを主張しています。
- $` K_A:\mathcal{C} \to [J(A), \mathcal{C}] \mbox{ in }{\bf CAT} `$
- $` \Pi_A:[J(A), \mathcal{C}] \to \mathcal{C} \mbox{ in }{\bf CAT} `$
- $` K_A \dashv \Pi_A`$
同様に、ファミリーFのシグマ型は次のホムセット同型を与えます。右辺のホムセットは、余頂点Yで底面がFである余錐の集合とみなせます（余錐は錐の矢印の向きを逆にしたものです）。
- $` \mathcal{C}(\Sigma_A(F), Y) \cong [J(A), \mathcal{C}](F, K_A(Y)) `$
関手ΣAと関手KAが随伴関手ペアになります。
- $` K_A:\mathcal{C} \to [J(A), \mathcal{C}] \mbox{ in }{\bf CAT} `$
- $` \Sigma_A:[J(A), \mathcal{C}] \to \mathcal{C} \mbox{ in }{\bf CAT} `$
- $` \Sigma_A \dashv K_A`$
カン拡張によるパイ型とシグマ型
関手 KA:C → [J(A), C] が、関手 Δ!A:[J(1), C] → [J(A), C] と事実上同じであることを見ましょう。まずはΔの意味を説明する必要があります。
射 f:A → B in C があるとき、反レイフィケーション関手Jにより、関手 J(f):J(A) → J(B) in CAT が誘導されます。J(f) をプレ結合〈pre-compose〉することは、[J(B), C] → [J(A), C] という関手（関手圏のあいだの関手）を定義します。その関手を Δf とします*2。
- $` \Delta_f(\mbox{-}) := J(f)\ast \mbox{-} `$
- $` \Delta_f:[J(B), \mathcal{C}] \to [J(A), \mathcal{C}] \mbox{ in }{\bf CAT}`$
引数〈argument〉が下付きだったり丸括弧だったりは、習慣や気まぐれで意味はありません。プログラミング言語だと、引数渡し構文が一種類だけのものがありますが、それはそれで見にくい（視認性が悪い）もんです。下付き・上付き・括弧・併置などをテキトーに（根拠なく）使い分けるのは視認性向上にはなります。
さて、C内で、Aから終対象1への唯一の射を !A:A → 1 in C とすると、これは J(!A):J(A) → J(1) in CAT を誘導し、さらにJ(!A)のプレ結合により次の関手（関手圏のあいだの関手）が作られます。
- $` \Delta_{!_A}:[J({\bf 1}), \mathcal{C}] \to [J(A), \mathcal{C}] \mbox{ in }{\bf CAT}`$
Δ!AとKAは、次の可換図式の意味で“事実上同じ”です。
$`\require{AMScd}
\begin{CD}
[J({\bf 1}), \mathcal{C}] @>{\Delta_{!_A}}>> [J(A), \mathcal{C}] \\
@V{\cong}VV @| \\
\mathcal{C} @>>{K_A}> [J(A), \mathcal{C}]
\end{CD}\\
\mbox{commutes in }{\bf CAT}
`$
KAの代わりにΔ!AとKAを使って先の“随伴を定義するホムセット同型”を書いてみます。
- $` [J(A), \mathcal{C}](\Delta_{!_A}(X), F) \cong [J({\bf 1}), \mathcal{C}](X, \Pi_A(F))`$
- $` [J({\bf 1}),\mathcal{C}](\Sigma_A(F), Y) \cong [J(A), \mathcal{C}](F, \Delta_{!_A}(Y)) `$
これを見ると、パイ型とシグマ型の新しい特徴付けが分かってきます。それは次のようです。
- $` \Pi_A(F) = Ran_{J(!_A)}(F)`$
- $` \Sigma_A(F) = Lan_{J(!_A)}(F)`$
つまり、J(!A)に沿ったFの右カン拡張がFのパイ型で、J(!A)に沿ったFの左カン拡張がFのシグマ型です。
となると、!Aという特別な射ではなくて、一般の射 f:A → B in C に沿った左右のカン拡張を考えてもいいでしょう。次のように定義します。
- $` \Pi_f(F) := Ran_{J(f)}(F)`$
- $` \Sigma_f(F) := Lan_{J(f)}(F)`$
fに沿ったパイ型／シグマ型を特徴付けるホムセット同型は次のようになります。
- $` [J(A), \mathcal{C}](\Delta_f(X), F) \cong [J(B), \mathcal{C}](X, \Pi_f(F))`$
- $` [J(B),\mathcal{C}](\Sigma_f(F), Y) \cong [J(A), \mathcal{C}](F, \Delta_f(Y)) `$
今述べたことを簡潔に言うと、
- $` \Sigma_f \dashv \Delta_f \dashv \Pi_f`$
あるいはもっと短く：
- $` \Sigma \dashv \Delta \dashv \Pi`$
以上は、単に定義を書いただけで、型理論的意味付けを与えていません。が、型理論（あるいは論理やデータベース）としても意味があると思えます。
