型理論／論理／インスティチューション理論の引っ越し準備 - 檜山正幸のキマイラ飼育記 (はてなBlog)

どこに引っ越すのか？それは“コンテキスタッドの世界”への引っ越しです。コンテキスタッドが型理論／論理／インスティチューション理論に対して、統合的・整合的な枠組みを与えるだろう、と思っています。それは、最近の記事達の内容や動機になっています。

型理論、論理、インスティチューション理論をすべて、コンテキスタッドの枠組みで定式化して同時に扱いたいのです。現状の用語・記号のコンフリクトや不整合をある程度は解消しておかないと困ったことになります。引っ越しの準備として、コンフリクト・不整合の解消をしておきます。共通に／一律に使う概念・記法・図法についても説明します。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
%\newcommand{\mbb}[1]{ \mathbb{#1} }
\newcommand{\twoto}{\Rightarrow }
\newcommand{\op}{\mathrm{op} }
\newcommand{\In}{\text{ in }}
\newcommand{\id}{\mathrm{id}}
%\newcommand{\u}[1]{\underline{#1}}
%\newcommand{\o}[1]{\overline{#1}}
\newcommand{\hyp}{ \text{－} }
%\newcommand{\Iff}{ \Leftrightarrow }
%\newcommand{\Imp}{ \Rightarrow }
\newcommand{\ctxpair}[2]{ \begin{pmatrix}#1 \\ #2\end{pmatrix} }
\newcommand{\mapsot}{\style{display: inline-block; transform: rotate(180deg)} {\mapsto} }
`$

内容：

宣言
具現化
随伴トリプル
モデル関手
ファイブレーション的プルバック四角形と変種達
依存ペア
トータル射

ハブ記事：

コンテキスタッド、包括圏、ハイパードクトリン

宣言

次の概念は、統合すれば同じことです。

型理論の型〈type〉
論理の命題〈proposition〉
インスティチューション理論の文〈sentence〉

これらを表す一般用語として、ステップ〈step〉が色がなくていいかと思ったのですが、色が無さすぎるみたいです。宣言〈declaration〉にします、とりあえず。型理論のコンテキスト〈型コンテキスト〉は、実際に型宣言のリストで、コンテキスト拡張で追加されるモノ（拡張ステップ）も型宣言とみなせるので、「宣言」は違和感がないでしょう。

インスティチューション理論の文関手〈sentence functor〉に相当する一般用語は宣言関手〈declaration functor〉です。宣言関手は、コンテキスト〈指標〉に宣言達の圏（小さい圏に限定）を対応させます。

$`\quad \mrm{Decl} : \cat{C}^\op \to \mbf{Cat} \In 2\mbf{CAT}\\
\text{or}\\
\quad \mrm{Decl} : \cat{S} \to \mbf{Cat} \In 2\mbf{CAT}
`$

宣言関手の関手戻り値関手（「型理論周辺、何で混乱するのか？ // 関手が値である反変関手・共変関手」参照）の略記は、$`\cat{C}`$ 上では $`f^*`$ 、$`\cat{S}`$ 上では $`f_*`$ です。

コンテキスト達の圏 $`\cat{C}`$ と指標達の圏 $`\cat{S}`$ （型理論周辺、何で混乱するのか？ // コンテキスト達の圏と指標達の圏）の両方を使うので、$`f^*`$ と $`f_*`$ が必要です。この結果、随伴トリプルに対する以下の略記法は諦めます。

$`\quad f_! \dashv f^* \dashv f_*`$

宣言関手には紆余曲折があり、「コンテキストの圏と指標の圏と限量子 // エス関手」で導入した用語「エス関手〈ess functor〉」（「述語論理：ハイパードクトリンとパルムクイスト二重圏 // エス関手」も参照）をしばらく使ってましたが、ステップ〈step〉と同様、色が無さすぎなので、型理論／論理／インスティチューション理論の文脈では宣言関手にします。なお、「k-特性関手とk-特性付き圏」で述べた特性関手は完全に一般的概念なので、そのままとします。

具現化

次の概念も同じことです。

型理論のインスタンス〈instance〉
論理の証明〈proof〉

インスタンスを表す構文的対象物〈syntactic object〉がインスタンス項〈instance term〉、証明を表す構文的対象物が証明項〈proof term〉ですが、型理論では、「インスタンス項」を単に「項」と呼ぶ習慣があります。この習慣には従いません（「型理論へのファイブレーション的アプローチ：インスタンスとは // 「インスタンス」を「項」と呼ぶのはやめよう」参照）。ただし、構文論の話をしているときは、「インスタンス項」を単に「インスタンス」、証明項を単に「証明」と呼びます。ほとんどの場合、「インスタンス」「証明」は、構文論内で構文的対象物と解釈されます。

さて、インスタンス／証明に相当する一般用語ですが、具現化〈manifestation〉とします。具現化は定義と言っても同じことですが、「定義」が使われすぎなので、少し珍しい言葉にします。ルオが以下の論文で扱った manifest field は、ほぼ具現化〈manifestation〉のことです。

[Luo09]
Title: Manifest Fields and Module Mechanisms in Intensional Type Theory
Author: Zhaohui Luo
Year: 2009
Pages: 19p
URL: https://www.cs.rhul.ac.uk/~zhaohui/Modules08.pdf

型理論における宣言と具現化が“型とインスタンス”、論理における宣言と具現化が“命題と証明”です。インスティチューション理論における宣言は文ですが、具現化相当の概念はあまり出てこないようです（π-インスティチューション（「演繹系と閉包系」参照）で少し現れますが）。

一般論	型理論	論理	インスティチューション理論
宣言	型	命題	文
具現化	インスタンス	証明	-

随伴トリプル

随伴トリプルに $`f_! \dashv f^* \dashv f_*`$ を使うのは諦めざるを得ません。代わりに、次の形式を使うことにします。

$`\quad \sum_f \dashv \Delta_f \dashv \prod_f`$
$`\quad \Sigma_f \dashv \Delta_f \dashv \Pi_f`$
$`\quad \exists_f \dashv \diamondsuit_f \dashv \forall_f`$

最初の2つの記法は依存型理論でお馴染みです。三番目の記法は論理の文脈で使います。$`\diamondsuit_f`$ は論理の水増し〈thinning〉ですが、その由来は「型を命題にクラッシュさせる：ダイアモンド・オペレーターの由来」に書いています。

$`f_! \dashv f^* \dashv f_*`$ のメリットは簡潔に書けることです。このメリットを得るために、次の新しい記法も使うかも知れません。

$`\quad f_\sigma \dashv f^* \dashv f_\pi`$

随伴トリプルは、依存型理論のシグマ型／パイ型と、ハイパードクトリン（「述語論理：ハイパードクトリンとパルムクイスト二重圏」参照）の存在限量子／全称限量子に現れます。

モデル関手

インスティチューション理論に出てくるモデル関手は、モデル理論におけるモデルの抽象的定式化（モデル関手の関手戻り値対象である圏の対象がモデル）です。モデル関手は通常 $`\mrm{Mod}`$ と書かれますが、加群〈module〉の圏と誤認されないように、$`\mrm{Model}`$ を使います。

$`\quad \mrm{Model}: \cat{S}^\op \to \mbf{CAT} \In 2\mathbb{CAT}`$

インスティチューション理論のモデル関手は、「型理論周辺、何で混乱するのか？ // 構文論的意味論と意味論的意味論」の意味論の分類で言えば、形式的意味論的意味論を圏論的に定式化したものです。

モデル関手の関手戻り値関手を $`f^*`$ と書くのも諦めざるを得ないので、アスタリスクの代わりにダイアモンドを使って $`f^\diamond`$ と書くことにします。充足関係〈satisfaction relation〉の記述などでバランスが悪くなりますが、まー仕方ないです。

指標達の圏 $`\cat{S}`$ の反対圏であるコンテキスト達の圏 $`\cat{C} = \cat{S}^\op`$ では、モデル関手は共変関手になります。

$`\quad \mrm{Model}: \cat{C} \to \mbf{CAT} \In 2\mathbb{CAT}`$

行きがかり上、共変モデル関手の関手戻り値関手は $`f_\diamond`$ と書きます。

モデル関手の関手戻り値関手はリダクト関手〈reduct functor〉と呼びます。一方、宣言関手の関手戻り値関手は翻訳関手〈translation functor〉です。

指標達の圏 $`\cat{S}`$ 上では、反変モデル関手のリダクト関手が $`f^\diamond`$ 、共変宣言関手の翻訳関手が $`f_*`$
コンテキスト達の圏 $`\cat{C}`$ 上では、共変モデル関手のリダクト関手が $`f_\diamond`$ 、反変宣言関手の翻訳関手が $`f^*`$

モデル関手は勝手な関手というわけではなくて、満たすべき条件がありますが、今回は割愛します。

ファイブレーション的プルバック四角形と変種達

依存型理論においてファイブレーション〈ファイバー付き圏〉は必須です。ファイブレーションの定義に現れるファイブレーション的プルバック四角形（「包括コンテキスタッドに向けて // ファイブレーション的プルバック四角形」参照）はとても重要です。

ファイブレーション的プルバック四角形は次のように書きます。

$`\quad \xymatrix{
B' \ar[r]^{f'} \ar@{|->}[d]
\ar@{}[dr]|{\text{f.p.b.}}
& B \ar@{|->}[d]
\\
X \ar[r]_f
&Y
}\\
\quad \In \pi:\cat{D} \to \cat{C}
`$

ここで：

$`\pi:\cat{D} \to \cat{C}`$ はファイブレーション
ラベルがない $`\mapsto`$ は関手 $`\pi`$ の値割り当て（関手引数対象と関手戻り値対象）
$`f\in\mrm{Mor}(\cat{C})`$ はベース射
$`f'\in\mrm{Mor}(\cat{D})`$ はトータル射で、$`f`$ のデカルト持ち上げ。適当な亀裂子（「包括コンテキスタッドに向けて // デカルト持ち上げと亀裂子／分裂子」参照）を使って $`f' = f^{\Uparrow B}`$ と書ける。

ファイブレーション的プルバックよりも弱い条件を満たす四角形として、ファイブレーション的可換四角形〈fibrational commutative square〉もたまに使います。次のように書き〈描き〉ます。

$`\quad \xymatrix{
B' \ar[r]^{f'} \ar@{|->}[d]
\ar@{}[dr]|{\text{f.comm.}}
& B \ar@{|->}[d]
\\
X \ar[r]_f
&Y
}\\
\quad \In \pi:\cat{D} \to \cat{C}
`$

これは次の意味です。

$`\quad \pi(f') = f`$

単に、$`f'`$ が $`f`$ の上にあるトータル射だと言っているだけです。

ファイブレーション的プルバック四角形の別な書き方〈描き型〉として次があります。

$`\quad \xymatrix{
B' \ar@{|->}[d]
\ar@{}[dr]|{\text{f.p.b.}}
& B \ar@{|->}[d] \ar@{|->}[l]_{f^*}
\\
X \ar[r]_f
&Y
}\\
\quad \In \pi:\cat{D} \to \cat{C}
`$

ここで、$`f^*`$ は反変の宣言関手（一般論ではインデックス付き圏）の翻訳関手（一般論では再インデキシング関手）です。逆グロタンディーク構成のアットマーク記法（「包括コンテキスタッドに向けて // グロタンディーク構成と逆グロタンディーク構成」参照）を使えば次のように書けます。

$`\quad f^* = \mrm{Decl}(f) = \cat{D}@(f)`$

ファイブレーション〈ファイバー付き圏〉 $`\cat{D}`$ とファミリー〈インデックス付き圏〉 $`\cat{D}@`$ は相互に置き換え可能なので、デカルト持ち上げ $`f'`$ の代わりに翻訳関手（宣言関手 $`\cat{D}@`$ の関手戻り値関手）の値割り当て（関手引数対象と関手戻り値対象）を使っています。ファイブレーション的プルバック四角形の上段に、デカルト持ち上げを書いても、翻訳関手の値割り当てを書いても、どっちでも同じです。

ファイブレーションの射影関手（ファイブレーションそのものだが）の値割り当て $`B' \mapsto X`$ を $`X \Vdash B'`$ とも書きます。これは、論理や型理論の「文法的に許容できる宣言」という概念との整合性・一様性を確保するための記法の約束です。この記法を使えば、ファイブレーション的プルバック四角形は次のようになります。

$`\quad \xymatrix{
B'
\ar@{}[dr]|{\text{f.p.b.}}
& B \ar@{|->}[l]_{f^*}
\\
X \ar@{||-}[u] \ar[r]_f
&Y \ar@{||-}[u]
}\\
\quad \In \pi:\cat{D} \to \cat{C}
`$

概念に対する呼び名・書き方・描き方が変わったところで、内容的には何も変わらないことに注意しましょう。

依存ペア

依存ペアとは、ファイブレーションのトータル対象を書き表す手法です。以下の図の状況の表現です。

$`\quad \xymatrix{
A \ar@{|->}[d]
\\
X
}\\
\quad \In \pi:\cat{D} \to \cat{C}
`$

ここで：

上段は、$`A \in |\cat{D}|`$ であることを示している。
下段は、$`X \in |\cat{C}|`$ であることを示している。
矢印は $`\pi(A) = X`$ であることを示している。

上記の状況を書き下すために、次のような書き方が使われます。

$`A = (X, A)`$
$`A = {_X A}`$
$`A = (X \mid A)`$
$`A = \ctxpair{A}{X}`$ （カプチ／マイヤースの記法）
$`A = A@X`$

事態・状況としては、トータル対象 $`A`$ がベース対象 $`X`$ 上のファイバー〈局所圏〉に入っていることですから、次のような所属命題を書いても同じことです。

$`A\in |\cat{D}_{X}|`$
$`A\in |\cat{D}_{@X}|`$
$`A\in |\cat{D}@(X)|`$
$`A\in |\mrm{Decl}(X)|`$

もちろん、
$`\quad \cat{D}_X = \cat{D}_{@X} = \cat{D}@(X) = \mrm{Decl}(X)`$
です。宣言関手 $`\mrm{Decl}`$ は、ファイブレーションの逆グロタンディーク構成でしたから、$`\mrm{Decl} = \cat{D}@`$ です。

そして、$`A\in |\mrm{Decl}(X)|`$ とまったく同じことを次のようにも書きます。

$`\quad X \Vdash A`$

この節の最初の図式の内容を簡潔に書くなら $`X \overset{\pi}{\mapsot} A`$ ですから、次の同値性が成立します。

$`\quad X \Vdash A \iff X \overset{\pi}{\mapsot} A\iff \mrm{Decl}(X)\ni A`$

トータル射

依存ペア $`(X, A) = (X\mid A)`$ はトータル対象を書き表わすための手法でした。トータル射も依存ペアとして書けますが、図式により理解しておいたほうがいいでしょう。まずは次の図式です。

$`\quad \xymatrix{
A \ar[r]^F \ar@{|->}[d]
\ar@{}[dr]|{\text{f.comm.}}
&B \ar@{|->}[d]
\\
X \ar[r]_f
&Y
}\\
\quad \In \pi: \cat{D}\to \cat{C}
`$

これは、$`F:A \to B`$ がトータル射（$`\cat{D}`$ の射）で、$`\pi(F) = f`$ であることを示しています。つまり、$`F`$ は $`f`$ 上のトータル射〈total morphism over $`f`$〉です。

$`F`$ が $`f`$ 上に居るからといって、デカルト持ち上げとは限りません。デカルト持ち上げとの差は、局所射 $`\varphi`$ で表すことができます。

$`\quad \xymatrix{
A \ar[d]_{\varphi}
&{}
\\
B' \ar[r]^{f'} \ar@{|->}[d]
\ar@{}[dr]|{\text{f.p.b.}}
&B \ar@{|->}[d]
\\
X \ar[r]_f
&Y
}\\
\quad \In \pi: \cat{D}\to \cat{C}
`$

上記の図式の状況を $`F = (f,\varphi)`$ と書きます。単なるペアで書いてますが、あくまで図式の状況の略記としてペアを使っているだけです。$`f`$ が $`F`$ のベースパート〈base part〉、$`\varphi`$ が $`F`$ のファイバーパート〈fiber part〉です。

トータル射の結合の計算法は、「包括コンテキスタッドに向けて // トータル射の結合公式と図示」に書いてあります。

ファイブレーション的プルバック四角形を翻訳関手を使って書けば次のようです。

$`\quad \xymatrix{
A \ar[d]_{\varphi}
&{}
\\
B' \ar@{|->}[d]
\ar@{}[dr]|{\text{f.p.b.}}
&B \ar@{|->}[d] \ar@{|->}[l]_{f^*}
\\
X \ar[r]_f
&Y
}\\
\quad \In \pi: \cat{D}\to \cat{C}
`$

無名の矢印記号 '$`\mapsto`$' の形を別バージョンにすると：

$`\quad \xymatrix{
A \ar[d]_{\varphi}
&{}
\\
B'
\ar@{}[dr]|{\text{f.p.b.}}
&B \ar@{|->}[l]_{f^*}
\\
X \ar[r]_f \ar@{||-}[u]
&Y \ar@{||-}[u]
}\\
\quad \In \pi: \cat{D}\to \cat{C}
`$

どれも、$`F = (f,\varphi)`$ ということを表しています。図式により記述されている概念的事物が何であるかが問題であって、使われている矢印記号はどうでもいいです。ましてや、テキストによる略記なんぞに注目してもしょうもないです。なにかしらのテキストエンコーディングをせざるを得ないからテキトーにエンコードしているだけです。