このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

［参照用 記事］

パルムグレンによる、型理論の複前層モデル

雑記／備忘

パルムグレン〈Erik Palmgren〉は、圏の“前層の圏”を作る操作を繰り返し適用することにより、依存型理論の圏論的モデルを構成しました。パルムグレンのモデルは、カートメル〈John Cartmell〉のコンテキスト圏〈contextual category〉の“印象的な具体例”を与えます。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\In}{\text{ in }}
%\newcommand{\base}[1]{ {{#1}\!\lrcorner} }
%\newcommand{\Imp}{\Rightarrow}
\newcommand{\Iff}{\Leftrightarrow}
%\newcommand{\u}[1]{\underline{#1}}
\newcommand{\op}{ \mathrm{op} } % used
\newcommand{\hyp}{\text{－} } % used
%\newcommand{\o}[1]{\overline{#1}}
\newcommand{\twoto}{ \Rightarrow } % used
\newcommand{\ILT}{ \triangleleft } % immediately less than
`$

複前層

この記事の内容は、パルムグレンの次の論文に基づきます。

$`\cat{C}`$ は小さい圏とします。$`\cat{C}`$ 上の前層の圏は、$`\cat{C}`$ から集合圏 $`{\bf Set}`$ への反変関手達の関手圏です。$`\cat{C}`$ 上の前層の圏を $`\mrm{PSh}(\cat{C})`$ と書きます。

$`\quad \mrm{PSh}(\cat{C}) := [\cat{C}^\op, {\bf Set}] = {\bf CAT}(\cat{C}^\op, {\bf Set}) \;\In {\bf CAT}`$

$`\mrm{PSh}(\cat{C})`$ は $`\cat{C}^\wedge`$ または $`\widehat{\cat{C}}`$ と書くこともあります。

パルムグレンは、前層の圏 $`\mrm{PSh}(\cat{C})`$ の拡張として、（$`\cat{C}`$ 上の）複前層の圏〈category of multi-presheaves〉 $`\mrm{MPSh}(\cat{C})`$ を定義しました。複前層の圏の対象は、前層を成分とする依存リストです。次の形で書きます。

$`\quad \vec{P} = [P_1, \cdots, P_n]`$

最初に、圏 $`\sigma_\cat{C}(\vec{P})`$ を、リストの長さに関して帰納的に*1定義します。

  • $`\vec{P} = [ ]`$ （空リスト）のとき： $`\sigma_\cat{C}([ ]) = \sigma_\cat{C}() := \cat{C}`$
  • $`P`$ を $`\cat{C}`$ 上の前層として $`\vec{P} = [P]`$ （単項リスト）のとき： $`\sigma_\cat{C}([P]) = \sigma_\cat{C}(P) := \int(\cat{C} \mid P)`$

ここで、$`\int(\cat{C} \mid P)`$ は、前層 $`P`$ を特殊なインデックス付き圏とみなしてのグロタンディーク構成です。$`\int(\cat{C} \mid P)`$ は、前層 $`P`$ の要素の圏〈category of elements〉と呼ばれます。どのような前層に対しても要素の圏〈グロタンディーク構成〉を作れます。$`\cat{C}`$ が小さい圏なら、要素の圏もまた小さい圏になります。$`\cat{C}`$ が小さい離散圏、つまり単なる集合のときは、要素の圏はファミリーのシグマ型になります。

自然数 $`n`$ に対して、次の圏は定義できていると仮定します。

$`\quad \sigma_\cat{C}(\vec{P}) = \sigma_\cat{C}([P_1, \cdots, P_n]) = \sigma_\cat{C}(P_1, \cdots, P_n)`$

この状況で、前層 $`P_{n+1} : \sigma_\cat{C}(\vec{P})^\op \to {\bf Set}`$ に対して、以下の圏を定義できます。（ナカグロ '$`\cdot`$' はリストの最後に成分〈項目〉を追加する操作の演算子記号です。）

$`\quad \sigma_\cat{C}(\vec{P}\cdot P_{n+1}) = \sigma_\cat{C}([P_1, \cdots, P_n, P_{n + 1}]) = \sigma_\cat{C}(P_1, \cdots, P_n, P_{n+1})`$

この圏の定義は以下のとおりです。

$`\quad \sigma_\cat{C}(\vec{P}\cdot P_{n+1}) := \int (\sigma_\cat{C}(\vec{P}) \mid P_{n + 1})`$

例えば、長さ2のリストに対する定義は：

$`\quad \sigma_\cat{C}(P, Q) := \int (\sigma_\cat{C}(P) \mid Q)
= \int ( \int (\cat{C} \mid P) \mid Q)\\
\text{Where}\\
\quad P : \cat{C}^\op \to {\bf Set} \In {\bf CAT}\\
\quad Q : (\int (\cat{C} \mid P) )^\op \to {\bf Set} \In {\bf CAT}
`$

圏 $`\sigma_\cat{C}(\vec{P})`$ が構成可能な、前層の依存リスト $`\vec{P}`$ を複前層〈multi-presheaf〉と呼びます*2。長さ $`n`$ のリスト $`\vec{P}`$ が（$`\cat{C}`$ 上の）複前層であることは次のように書けます。

$`\quad \forall( 1 \le k \le n) .\, P_k \in |\mrm{PSh}(\sigma_\cat{C}(P_1, \cdots, P_{k - 1}))|
`$

$`n`$ が3以上なら、次のような条件の並びに展開できます。

$`\quad P_1 \in |\mrm{PSh}(\cat{C} )|\\
\quad P_2 \in |\mrm{PSh}(\int( \cat{C} \mid P_1) )|\\
\quad P_3 \in |\mrm{PSh}(
\int ( \int (\cat{C} \mid P_1) \mid P_2)
)|\\
\quad \cdots
`$

複前層のあいだの射

複前層が何であるかはわかりました。複前層達を圏に編成するためには、二つの複前層のあいだの射が必要です。この節で複前層の射を定義します。小さい圏 $`\cat{C}`$ は前節と同様で固定しています。

$`\cat{C}`$ 上の前層 $`P`$ に対して $`\int(\cat{C} \mid P)`$ を要素の圏と呼ぶので、$`\cat{C}`$ 上の複前層 $`\vec{P}`$ に対して $`\sigma_\cat{C}(\vec{P})`$ を複要素の圏〈category of multi-elements〉と呼ぶことにします。複要素の圏の対象である複要素〈multi-element〉は、$`\cat{C}`$ の対象と集合の要素達の依存リストの形で書けます。

（リストとして）長さ $`n`$ の複前層 $`\vec{P} = [P_1, \cdots, P_n]`$ の各成分 $`P_k`$ に対して、射影関手 $`\pi_{P_k}`$ を定義できます。

$`\quad \pi_{P_k} : \int(\sigma_\cat{C}([P_1, \cdots, P_{k - 1}]) \mid P_k ) \to \sigma_\cat{C}([P_1, \cdots, P_{k - 1}]) \In {\bf Cat}`$

これは、グロタンディーク構成に伴う標準射影です。$`k = 1, 2`$ に関しては次のようです。

$`\quad \pi_{P_1} : \int(\cat{C} \mid P_1 ) \to \cat{C} \In {\bf Cat}\\
\quad \pi_{P_2} : \int( \int( \cat{C} \mid P_1) \mid P_2) \to \int( \cat{C} \mid P_1) \In {\bf Cat}
`$

定義から、射影関手達 $`\pi_{P_1}, \cdots, \pi_{P_n}`$ はこの順で結合可能です。関手の図式順結合をアスタリスクで書くことにして、射影達の結合を次のように書きます。

$`\quad \pi^*_{\vec{P}} := \pi_{P_1} * \cdots * \pi_{P_n}: \sigma_\cat{C}(\vec{P}) \to \cat{C}
\In {\bf Cat}
`$

$`\vec{P}`$ が長さ0のリスト〈空リスト〉のときは、$`\pi^*_{\vec{P}} = \pi^*_{[]}`$ は、圏 $`\cat{C}`$ の恒等関手です。

これで、複前層のあいだの射を定義する準備ができました。$`\vec{P},\vec{Q}`$ を2つの複前層（長さは異なっても構わない）として、以下の図式を可換にする関手 $`f`$ が複前層のあいだの射です。

$`\quad \xymatrix{
\sigma_\cat{C}(\vec{P}) \ar[r]^f \ar[d]_{\pi^*_{\vec{P}} }
& \sigma_\cat{C}(\vec{Q}) \ar[d]^{\pi^*_{\vec{Q}} }
\\
\cat{C} \ar@{=}[r]
&\cat{C}
}\\
\text{commutative }\In {\bf Cat}
`$

射の結合と恒等射の定義は明らかでしょう。こうして作られた、複前層を対象として複前層のあいだの射を射とする圏を複前層の圏〈category of multi-presheaves〉と呼びます。$`\cat{C}`$ 上の複前層の圏を $`\mrm{MPSh}(\cat{C})`$ と書きます。場合によっては短く $`\mrm{M}^\cat{C}`$ とも書きます。

$`\vec{P}, \vec{Q}`$ が両方とも長さ1のリストのときは以下のようになります。

$`\quad \xymatrix{
\int(\cat{C} \mid P) \ar[r]^f \ar[d]_{\pi_{P} }
& \int(\cat{C} \mid Q)\ar[d]^{\pi_{Q} }
\\
\cat{C} \ar@{=}[r]
&\cat{C}
}\\
\quad \text{commutative }\In {\bf Cat}
`$

$`\vec{P}`$ が長さ1、$`\vec{Q}`$ は長さ0のときは以下のようになります。

$`\quad \xymatrix{
\int(\cat{C} \mid P) \ar[r]^-f \ar[d]_{\pi_{P} }
& \cat{C} \ar@{=}[d]
\\
\cat{C} \ar@{=}[r]
&\cat{C}
}\\
\text{commutative }\In {\bf Cat}
`$

つまり、$`f = \pi_P`$ です。実は、長さ0のリストは複前層の圏の終対象となります。

$`\vec{P}`$ が長さ0、$`\vec{Q}`$ は長さ1のときは以下のようになります。

$`\quad \xymatrix{
\cat{C} \ar[r]^-f \ar@{=}[d]
& \int(\cat{C} \mid Q)\ar[d]^{\pi_{Q} }
\\
\cat{C} \ar@{=}[r]
&\cat{C}
}\\
\text{commutative }\In {\bf Cat}
`$

つまり、$`f`$ は射影 $`\pi_Q`$ に対するセクションになります。次のように、複前層の圏のホムセットはセクションの集合になります。

$`\quad \mrm{M}^\cat{C}([ ], [Q]) = \mrm{Sect}(\pi_Q)`$

前層の圏と複前層の圏

「複前層の圏は前層の圏の拡張である」という主張を合理化するには、前層の圏から複前層の圏への埋め込み関手を構成する必要があります。実際、前層の圏は、複前層の圏の部分圏とみなせます。

複前層の圏 $`\mrm{M}^\cat{C}`$ の対象（複前層）はリストの形に書けるので、“リストの長さ”の概念があります。長さがちょうど $`n`$ の対象からなる充満部分圏は次のように書きます。

$`\quad \mrm{M}^\cat{C}_n \;\in |{\bf CAT}|`$

長さが $`n`$ 以下の対象からなる充満部分圏なら次のようです。

$`\quad \mrm{M}^\cat{C}_{\le n} \;\in |{\bf CAT}|`$

小さい圏 $`\cat{C}`$ 上の前層の圏 $`\mrm{PSh}(\cat{C})`$ は、長さ1の複前層の圏 $`\mrm{M}^\cat{C}_1`$ と同一視可能です。圏同値（実際には圏同型になる）を与える関手を $`J:\mrm{PSh}(\cat{C}) \to \mrm{M}^\cat{C}_1`$ とします。

対象の集合上での $`J`$ は簡単で次の一対一対応を与えます。

$`\quad |\mrm{PSh}(\cat{C})| \ni P \overset{J}{\longleftrightarrow} [P]\in \mrm{M}^\cat{C}_1`$

問題は $`J`$ の射パート／ホムパートです。前層の圏の射は、次のような自然変換でした。

$`\quad \varphi :: P \twoto Q : \cat{C}^\op \to {\bf Set} \In {\bf CAT}`$

一方で、長さ1の余前層のあいだの射は、次の図式を可換にする関手でした。

$`\quad \xymatrix{
\int(\cat{C} \mid P) \ar[r]^f \ar[d]_{\pi_{P} }
& \int(\cat{C} \mid Q)\ar[d]^{\pi_{Q} }
\\
\cat{C} \ar@{=}[r]
&\cat{C}
}\\
\quad \text{commutative }\In {\bf Cat}
`$

$`J`$ によりホムセットの同型が与えられることは次のように書けます。

$`\quad \mrm{PSh}(\cat{C})(P, Q) \overset{J}{\cong} \mrm{M}^\cat{C}_1([P], [Q])`$

ところが、この同型はグロタンディーク構成と逆構成により与えられます。$`\mrm{PSh}(\cat{C})\cong\mrm{M}^\cat{C}_1`$ は、グロタンディーク構成に関する基本的な事実だったわけです。

$`\mrm{PSh}(\cat{C})\cong\mrm{M}^\cat{C}_1`$ より強い結果が言えます。長さ1の複前層からなる部分圏ではなくて、すべての複前層からなる圏 $`\mrm{M}^\cat{C}`$ と $`\mrm{PSh}(\cat{C})`$ が圏同値になるのです。

$`\quad \mrm{PSh}(\cat{C}) {\simeq} \mrm{M}^\cat{C} \In {\bf CAT}`$

'$`\simeq`$' は圏同値を表すとします。複前層から前層への対応は、複前層 $`\vec{P}`$ の $`\pi^*_{\vec{P}}`$ で与えられます（詳細はパルムグレン論文を参照）。

カートメル構造

カートメル〈John Cartmell〉は、型理論／型システムのモデルとなる圏としてコンテキスト圏〈contextual category〉を導入しました。名前の一部である "contextual" という形容詞は一般的過ぎてちょっと使いにくいですね。「指標の圏はコンテキストの圏の反対圏」より：

型理論的圏の下部構造を形成する圏をコンテキストの圏〈category of contexts〉と呼ぶことにします。コンテキスト圏〈contextual category〉と紛らわしいですが、コンテキスト圏は型理論的圏の一種で、“コンテキスト圏のコンテキストの圏”〈the category of contexts of a contextual category〉があります。

ここでは、コンテキスト圏が持つ構造をカートメル構造〈Cartmell structure〉と呼ぶことにします。カートメル構造は、カートメルが定義したコンテキスト圏以外に対しても考えることができます。つまり、カートメル構造は、既存の圏にアタッチできる構造なのです。

とある圏がカートメル構造を持つという性質をコンテキスト性〈contextuality | 文脈性〉と呼び、カートメル構造を載せることをコンテキスト化〈contextualize | 文脈化）と呼んだりしています。が、こういう言葉を使うとなんか“いわくありげ”な印象を与えてよろしくないと思います。代わりに、カートメル性〈Cartmell property〉、カートメル化〈Cartmellize〉を使います。

小さい圏 $`\cat{D}`$ がカートメル構造を持つとは、概略的・直感的に言えば次のことです。

  1. $`\cat{D}`$ に終対象があり、ひとつの終対象が特定されている。
  2. $`\cat{D}`$ の対象は、なんらかの意味でリストと考えることができる。空リストは特定された終対象である。
  3. $`\cat{D}`$ の対象（リスト）の末尾に項目（リストの成分）を追加する操作が（潜在的にでも）存在する。この操作を拡張〈extension〉と呼ぶ。
  4. $`\cat{D}`$ の対象の集合 $`|\cat{D}|`$ は、特定された終対象をルートとするツリー構造を持つ。対象がツリーノードであり、ノードの“高さ”はリストの長さで与えられる。
  5. 対象（リストであり、ツリーノードでもある）の拡張に伴い、射も拡張できる。

圏 $`\cat{D}`$ がカートメル構造を持つとして、その構成素（の一部）は次のものです。

  • 特定された終対象 $`{\bf 1} = {\bf 1}_\cat{D}`$
  • 対象の長さ〈length〉（ツリーノードの高さ）を与える関数 $`\ell : |\cat{D}| \to {\bf N}`$
  • ツリーノードとしての親ノードを与える関数 $`\mrm{ft}: |\cat{D}|\setminus\{ {\bf 1}\} \to |\cat{D}|`$

関数 $`\mrm{ft}`$ は father の略らしいです。いまどき、性別を明示するのはどうかな？ と思うので、呼び名は親関数〈parent function〉とします。次の性質を（カートメル構造の公理として）要求します。

  • $`\ell(X) = 0 \Iff X = {\bf 1}`$
  • $`\ell(\mrm{ft}(X)) = \ell(X) - 1 \;\text{ where }X \ne {\bf 1}`$

対象（リストと考えてよい）のあいだの関係 $`\ILT`$ を次のように定義します。

$`\text{For } X, Y \in |\cat{D}|\\
\quad X \ILT Y :\Iff \mrm{ft}(Y) = X
`$

$`X \ILT Y`$ は次のように読みます（どれも同じ意味）。

  1. $`Y`$ は $`X`$ の拡張〈extension〉である。誤解を避けたいときは直接拡張〈immediate extension〉。
  2. $`Y`$ は $`X`$ の後者〈successor〉である。
  3. $`X`$ は $`Y`$ の前者〈predecessor〉である。

関係 $`\ILT`$ を、拡張関係〈extension relation〉、あるいは直接拡張関係〈immediate extension relation〉と呼びます*3。拡張関係 $`\ILT`$ を含む最小の反射的・推移的関係をとると、それは $`|\cat{D}|`$ 上のツリー順序になります。

$`|\cat{D}|`$ のツリー構造は、長さ（高さ）関数と親関数、あるいは拡張関係により記述できます。それだけでなく、圏の射を有向辺と考えた有向グラフ構造としても実現されます。それは以下のようなものです。

  • $`X\ILT Y`$ である $`X, Y`$ に対して、$`\cat{D}`$ の射 $`\rho^Y_X : X\to Y`$ が一意的に定まっている。

$`X\ILT Y`$ なら $`X = \mrm{ft}(Y)`$ なので、$`\rho^Y_X`$ を $`\rho^Y`$ と書いても問題ありません。$`Y \mapsto \rho^Y`$ は次の写像になります。

$`\quad \rho^\hyp : |\cat{D}|\setminus\{{\bf 1}\} \to \mrm{Mor}(\cat{D}) \In {\bf Set}`$

$`\rho^Y`$ の形の射はディスプレイ射〈display {map | morphism}〉と呼びます。ディスプレイ射を標準射影〈canonical projection〉と呼ぶこともあります。

ディスプレイ射の全体を $`\mrm{Disp} \subseteq \mrm{Mor}(\cat{D})`$ とすると、$`\mrm{Disp}`$ を辺の集合、$`|\cat{D}|`$ を頂点の集合とする有向グラフ $`(|\cat{D}|, \mrm{Disp}, \mrm{src}, \mrm{trg})`$ が定義できます。

$`\quad \xymatrix{
\mrm{Disp} \ar@/^1pc/[r]^{\mrm{src}} \ar@/_1pc/[r]_{\mrm{trg}}
& |\cat{D}|
}\\
\quad \In {\bf Set}\\
\text{Where}\\
\quad \mrm{src} := \mrm{dom}|_{\mrm{Disp}}\\
\quad \mrm{trg} := \mrm{cod}|_{\mrm{Disp}}
`$

この有向グラフが、$`|\cat{D}|`$ のツリー構造を正確に反映します。ただし、有向辺の向きはルートに向かう方向なので注意してください。

$`\quad X \ILT Y \Iff (\rho^Y : Y \to X \In \cat{D})`$

カートメル構造は、拡張関係 $`\ILT`$ が射に対しても定義できることを要求します。任意の射 $`f:X \to Y \In \cat{D}`$ と、$`Y`$ の拡張 $`Y\ILT Y'`$ に対して、次のプルバック四角形の可換図式が対応しています。

$`\quad \xymatrix {
X' \ar[r]^{f^\uparrow} \ar[d]_{ \rho^{X'} }
\ar@{}[rd]|{ \text{p.b.} }
& Y' \ar[d]^{\rho^{Y'}}
\\
X \ar[r]_f
& Y
}\\
\quad \In \cat{D}
`$

ここで、$`X'`$ と $`f^\uparrow`$ は、与えられた $`f`$ と $`Y'`$ から一意的に決まります。$`f^\uparrow`$ は、$`f`$ の拡張〈extension〉、持ち上げ〈lift〉、連結射〈connecting {map | morphism}〉などと呼ばれます。上記のプルバック四角形は、標準プルバック四角形〈canonical pullback square〉と呼びます*4。

拡張 $`Y \ILT Y'`$ と $`f:X \to Y`$ に対して、$`X`$ の拡張 $`X\ILT X'`$ と $`f`$ の拡張 $`f\ILT f^\uparrow`$ が決まることになります。「対象の拡張に伴い、射も拡張できる」とは、こういうことです。

対象の拡張に伴う射の拡張は（厳密に）関手的〈functorial〉に振る舞います。そのことを大雑把に表現すれば：

  • $`(f ; g)^\uparrow = f^\uparrow ; g^\uparrow`$
  • $`(\mrm{id}_X)^\uparrow = \mrm{id}_{X'}`$

標準プルバック四角形の存在から、ディスプレイ射を、任意の射に沿ってファイバー引き戻し（「ファイバーの計算の動機としてのプルバック公式 // プルバックってなに？」参照）することができます。つまり、ディスプレイ射のクラス（「射のクラスと制約付きスパン // 圏の射のクラス」参照）は、ファイバー引き戻しに関して閉じています。しかし、（一般的には）結合に関しては閉じていません。

複前層の圏のカートメル構造

カートメル構造は、圏の対象達がツリー状に編成されていることを表現する、かなり具体性が高い構造です。複前層の圏 $`\mrm{M}^\cat{C}`$ はカートメル構造を持ちます。つまり、複前層達は、全体としてツリー状に編成されているのです。

複前層はリストの形をしているので、長さ関数 $`\ell`$ は自明に定義できます。長さ0の唯一の対象〈複前層）は空リスト $`[ ]`$ です。空リストは複前層の圏 $`\mrm{M}^\cat{C}`$ の終対象です（それを証明する必要はあります）。リストの最後に成分〈項目〉を追加する演算として $`\cdot`$ がありました。これは、明示的な拡張演算となります。$`\ell(\vec{P}) = n`$ のとき：

$`\quad \vec{P} \ILT \vec{P'} \Iff \vec{P'} = \vec{P}\cdot P_{n + 1}`$

$`\vec{P} \ILT \vec{P'}`$ のときのディスプレイ射 $`\rho^{P'}`$ は、グロタンディーク構成の標準射影だとします。

$`\quad \rho^{P'} := \pi_{P_{n + 1}} : \int( \sigma_\cat{C}(\vec{P}) \mid P_{n+1}) \to \sigma_\cat{C}(\vec{P})`$

カートメル構造のツリー構造に関する部分は容易に確認できます。「対象の拡張に伴い、射も拡張できる」の部分は、それなりの議論が必要です。詳細はパルムグレンの原論文を参照してください。

おわりに

複前層とそのあいだの射は、プログラム意味論として利用可能です。複前層は、$`\cat{C}`$ の対象をパラメータとする依存リスト型とみなせます。型のインスタンス・データは複要素です。多相依存型のあいだの多相依存関数は、複前層のあいだの射によってモデル化できます。

$`\vec{P}`$ の長さが $`n`$ だとして、複前層の射 $`f: \vec{P} \to [Q]`$ は、多相パラメータ以外に $`n`$ 個の引数を持つ多相依存関数をモデル化しています。複前層の圏から前層の圏への圏同値は、$`n`$ 個の引数をひとつの引数にまとめてしまう操作に対応します。

複前層モデルは、小規模な計算系のモデルにも、大きなサイズのモデルにも使えそうです。

*1:「帰納」と「再帰」の使い方は「再帰的構成のために： 順序数の圏 // 再帰と帰納」参照

*2:パルムグレンは "multivariable presheaf" と呼んでますが、"variable" は不要でしょう。

*3:パルムグレンは「直接拡張関係」を使っています。

*4:"connecting map" は、「型理論とインスティチューションの周辺」で引用した論文[Sub21-]で使われていた用語、"canonical projection", "canonical pullback square" は[AENR23-24]で使われていた用語です。