「おー、$`\Delta`$ と $`\nabla`$ を組み合わせたら $`\diamondsuit`$ になるな、むふふふふ」と、ダジャレな記法を思いついて悦にいっている今日このごろ。
何の話かというと； カリー／ハワード／ランベック対応によれば、型と命題は事実上同じものなので、区別する必要はないです -- と言われても、「型と命題はなんか違うような気がする」と思うでしょ。その気持ちへの対処を考えました。
それは、型を命題へと“キャストする”オペレーターを導入する、という方法です。このオペレーターは、拡がり・大きさを持つ集合を一点（単元集合）に潰してしまうオペレーターなのでクラッシュ・オペレーターと呼びましょう。そして、クラッシュ・オペレーターを $`\nabla`$ と書きます。すると、「おー、$`\Delta`$ と $`\nabla`$ を組み合わせたら $`\diamondsuit`$ になるな、むふふふふ」なのです。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
%\newcommand{\twoto}{\Rightarrow }
%\newcommand{\thrto}{\Rrightarrow }
\newcommand{\In}{\text{ in }}
\newcommand{\op}{\mathrm{op}}
%\newcommand{\id}{\mathrm{id}}
%\newcommand{\u}[1]{\underline{#1}}
%\newcommand{\o}[1]{\overline{#1}}
\newcommand{\hyp}{ \text{－} }
%\newcommand{\Iff}{ \Leftrightarrow }
\newcommand{\Imp}{ \Rightarrow }
`$
内容：
※色付きテキストは次の約束で使います。
- 青い文字： 重要な概念・用語だがこの記事内では定義・説明してないもの。
- 赤い文字： この記事内で導入・定義した概念・用語。過去の定義の再掲・繰り返しのときもある。
- マゼンタの文字： この記事内の後方で定義されるか参照〈リンク〉される概念・用語。
薄い前層と述語
集合 $`X`$ は離散圏とみなせます。「集合を離散圏とみなす」といちいち断るのは面倒くさいので、「集合」を「離散圏」の同義語として使います。同様に、「プレ順序集合」は「やせた圏」の同義語だし、「順序集合」はとてもやせた圏の同義語です。
圏に関する概念は、すべからく集合（プレ順序集合、順序集合）にも適用可能です。例えば、$`X`$ を集合（すなわち離散圏）として関手圏 $`[X^\op, \mbf{Set}]`$ を考えることができます（$`{^\op}`$ は意味ないけど）。これは $`X`$ 上の 前層圏です。離散圏上の前層圏は、ファミリーの圏と同じです。
$`\text{When }X \text{ is discrete}\\
\quad \mrm{PSh}(X) = \mrm{Fam}(X) = [X^\op, \mbf{Set}] = [X, \mbf{Set}]
`$
主に、集合〈離散圏〉上の前層を考えますが、枠組みとしては前層の一般論を使います。
前層 $`P:\cat{C} \to \mbf{Set}\In \mbf{CAT}`$ が薄い〈sheer〉とは、次のことです。
$`\quad \forall X\in |\cat{C}|.\, P(X) = \emptyset \lor P(X) \cong \mbf{1}`$
つまり、$`\cat{C}`$ の任意の対象の関手値（値は集合）が空集合か単元集合であるとき、前層は薄いのです*1。$`\cat{C}`$ 上の薄い前層の全体から誘導される $`\mrm{PSh}(\cat{C})`$ の充満部分圏を $`\mrm{SheerPSh}(\cat{C})`$ とします。
集合〈離散圏〉 $`X`$ 上の薄い前層は、論理的述語と同じことです。$`x\in X`$ に対して、薄い前層 $`P`$ の値が空集合なら“偽”、値が単元集合なら“真”とみなします。今の文脈では、「薄い前層」と「述語〈predicate〉」は同義語として扱います。
この節の内容がピンとこなかったら、次の過去記事を読んでみるといいかも知れません。
クラッシュ・オペレーター
圏 $`\cat{C}`$ に対して、次のようなクラッシュ・オペレーター $`\nabla`$ を考えます。
$`\quad \nabla_\cat{C} : \mrm{PSh}(\cat{C}) \to \mrm{SheerPSh}(\cat{C}) \In \mbf{CAT}`$
まず、以下の約束をします。
- $`\mbf{0} := \emptyset`$
- $`\mbf{1} := \{\mbf{0}\} = \{\emptyset\}`$
任意の前層 $`P \in |\mrm{PSh}(\cat{C})|`$ に対して、$`\nabla_\cat{C} P = \nabla_\cat{C}(P)`$ は次のように定義します。
$`\text{For }X\in |\cat{C}|\\
\quad (\nabla_\cat{C} P)(X) :=
\left\{
\begin{array}{l}
\mbf{0} \text{ if }P(X) = \mbf{0}\\
\mbf{1} \text{ if }P(X) \ne \mbf{0}
\end{array}
\right.
`$
対象での値を決めれば、$`\nabla_\cat{C}(f:X \to Y)`$ の値は自動的に決まってしまいます。定義より、$`\nabla_\cat{C} P`$ は薄い前層です。文脈より明らかなら、下付きの $`{_\cat{C}}`$ は省略して単に $`\nabla`$ と書きます。
クラッシュ・オペレーターは、集合圏上のクラッシュモナド〈crush monad〉の台関手を前層に拡張したものです。クラッシュ・モナドについては、以下の過去記事を参照してください。
前層のあいだの自然変換 $`\alpha : P \to Q \In \mrm{PSh}(\cat{C})`$ についても、
$`\quad \nabla \alpha : \nabla P \to \nabla Q \In \mrm{PSh}(\cat{C})`$
もほぼ自明に決まります。自然変換の定義に基づいて確認してみてください。
こうして決まる関手 $`\nabla_\cat{C}`$ を、$`\cat{C}`$ 上のクラッシュ・オペレーター〈crush operator〉と呼びます。クラッシュ・オペレーターは、前層や自然変換に作用して、薄い前層とそのあいだの自然変換を生成します。
クラッシュ・オペレーターは、$`\mrm{PSh}(\cat{C}) \to \mrm{SheerPSh}(\cat{C})`$ の関手ですが、包含関手 $`\mrm{SheerPSh}(\cat{C}) \to \mrm{PSh}(\cat{C})`$ をポスト結合すれば、$`\mrm{PSh}(\cat{C}) \to \mrm{PSh}(\cat{C})`$ という自己関手とみなせます。
$`\quad \nabla_\cat{C} : \mrm{PSh}(\cat{C}) \to \mrm{SheerPSh}(\cat{C}) \In \mbf{CAT}\\
\text{or}\\
\quad \nabla_\cat{C} : \mrm{PSh}(\cat{C}) \to \mrm{PSh}(\cat{C}) \In \mbf{CAT}
`$
前層（特にファミリー）は型理論の型とみなせるので、クラッシュ・オペレーターは型を述語〈命題〉へと変換すると言えます。真と偽の二値以外の値を、真偽に正規化するという発想は昔からよく使われた発想です。興味があれば、次の過去記事を見てください。
論理演算と限量子
$`\cat{C}`$ 上の前層 $`P, Q`$ に対する直積、直和、指数は、点ごと〈pointwize〉に、集合圏の直積、直和、指数を使って定義します。それぞれ次のように書きます。$`\lambda`$ はラムダ記法のラムダ、$`x\In \cat{C}`$ は、$`x`$ が対象でも射でもいいラムダ変数ということです。
$`\quad P \times Q := \lambda\, x\In \cat{C}.\, P(x) \times Q(x)\\
\quad P + Q := \lambda\, x\In \cat{C}.\, P(x) + Q(x)\\
\quad [P, Q] := \lambda\, x\In \cat{C}.\, [P(x), Q(x)]
`$
点ごとに定義した指数は、圏上の前層の一般論としての指数〈内部ホム対象〉になるとは限らないので注意してください。離散圏上の前層に限ればうまく働きます。
他に、前層に対してシグマ型とパイ型が構成できるとします。シグマ型とパイ型の高水準な定義は、$`f:X \to Y`$ （離散圏間の関手とみなした関数）によるプレ結合引き戻し関手 $`\Delta_f`$ の左随伴関手がシグマ型、右随伴関手がパイ型です。次の随伴トリプルがあります。
$`\quad \sum_f \dashv \Delta_f \dashv \prod_f`$
具体的・構成的に $`\sum_f, \Delta_f, \prod_f`$ を定義することもできます。具体的表示のためには、きちんと記法を整備する必要があります。モヤッとした記法では正確な定義は無理です。今回は具体的表示は割愛しますけど。
前層 $`P, Q`$ に対する論理演算と限量子を、クラッシュ・オペレーターを使って次のように定義します。（$`\mrm{K}^\mbf{0}`$ は常に値 $`\mbf{0}`$ を取る定数値関手です。）
$`\quad P \land Q := \nabla (P \times Q)`$
$`\quad P \lor Q := \nabla (P + Q)`$
$`\quad P \Imp Q := \nabla ( [P, Q])`$
$`\quad \lnot P := \nabla ( [P, \mrm{K}^\mbf{0}])`$
$`\quad \exists_f P := \nabla ( \sum_f P)`$
$`\quad \forall_f P := \nabla ( \prod_f P)`$
上記の定義は任意の $`P, Q`$ に対して有効ですが、$`P, Q`$ を特に薄い前層〈述語〉に限ると、論理演算と限量子は、薄い前層に薄い前層を対応させる関手になります。
離散圏〈集合〉 $`X`$ 上の薄い前層達の圏 $`\mrm{SheerPSh}(X)`$ を（述語達の圏だから） $`\mrm{Pred}(X)`$ とも書くことにして、論理演算と限量子のプロファイルを書くと次のようです。
$`\quad (\land) : \mrm{Pred}(X) \times \mrm{Pred}(X) \to \mrm{Pred}(X) \In \mbf{CAT}`$
$`\quad (\lor) : \mrm{Pred}(X) \times \mrm{Pred}(X) \to \mrm{Pred}(X) \In \mbf{CAT}`$
$`\quad (\Imp) : {\mrm{Pred}(X)}^\op \times \mrm{Pred}(X) \to \mrm{Pred}(X) \In \mbf{CAT}`$
$`\quad (\lnot) : {\mrm{Pred}(X)}^\op \to \mrm{Pred}(X) \In \mbf{CAT}`$
$`\quad \exists_f : \mrm{Pred}(X) \to \mrm{Pred}(Y) \In \mbf{CAT}`$
$`\quad \forall_f : \mrm{Pred}(X) \to \mrm{Pred}(Y) \In \mbf{CAT}`$
ダイアモンド・オペレーター
過去記事「圏論的述語論理とお絵描き」、「最近の型理論： 型判断／シーケントの意味論に向けて」などで、述語論理の随伴トリプルを次のように書いています。
$`\quad \exists_f \dashv \diamondsuit_f \dashv \forall_f`$
記号 $`\diamondsuit`$ を使ったことに、たいした意味はありませんでした。論理の文脈では、一般的な記号 $`\Delta`$ を少し変えて使いたかっただけです。プレ結合引き戻し関手 $`\Delta_f`$ の論理バージョンが $`\diamondsuit_f`$ です。
ところが、$`\diamondsuit_f`$ は次のように定義できるのです。（アスタリスクは関手の図式順結合です。）
$`\quad \diamondsuit_f := \Delta_f * \nabla_X \;: \mrm{Pred}(Y)\to\mrm{Pred}(X)\In \mbf{CAT}`$
実は偶然なのですが、「ダイアモンド形は、上の三角形と下の三角形を繋げて作っている」という解釈ができて、たいへんに具合が良いことになりました。むふふふふ。
$`X,Y`$ は離散圏〈集合〉、$`f:X\to Y`$ を関手〈関数〉、前層圏は $`\mrm{PSh}(\hyp)`$ 、薄い前層圏〈述語達の圏〉は $`\mrm{Pred}(\hyp)`$ として、状況を示す図式は以下のようです。
$`\quad \xymatrix {
{\mrm{PSh}(Y)} \ar[r]^{\Delta_f}
&{\mrm{PSh}(X)} \ar[d]^{\nabla_X}
\\
{\mrm{Pred}(Y)} \ar@{^{(}->}[u] \ar[r]_{\diamondsuit_f}
&{\mrm{Pred}(X)}
}\\
\quad \text{commutative }\In \mbf{CAT}
`$
正確に言えば、包含関手も絡んでいます。包含関手、プレ結合引き戻し関手、クラッシュ・オペレーターをこの順で結合するとダイアモンド・オペレーター〈diamond operator〉になります。
存在限量子、全称限量子は、ダイアモンド・オペレーターの左随伴関手、右随伴関手としても定義できます。それは、シグマ型構成子、パイ型構成子にクラッシュ・オペレーターを適用した定義と同じになります。
述語論理ではあまり強調されないのですが、$`\diamondsuit_f`$ は極めて重要です。これがあるから、限量子も定義可能となるのであり、述語論理の要〈かなめ〉と言えます。$`\Delta_f`$ や $`\diamondsuit_f`$ は、$`f`$ による水増しオペレーター〈thinning operator〉とも呼ばれます。$`f`$ が直積の射影のときに、述語の変数水増しになるからです。よく知られた論理演算と限量子と共に、水増しオペレーター $`\Delta_f`$ にも注意を向けましょう。
シグマ型とパイ型を含む型理論的体系のなかで、クラッシュ・オペレーターとダイアモンド・オペレーターを明示的に使うと、型と命題の区別を付けることになります。型だけでも困ることはないのですが、「型と命題を区別したい」という要求に応えるメカニズムとしてクラッシュ・オペレーターとダイアモンド・オペレーターは適切です。
*1:基数 1 以下の集合達の圏を $`\mbf{Set}_{\le 1}`$ とすると、$`\mbf{Set}_{\le 1}`$ に値を取る前層が薄い前層です。「「命題」の曖昧性から前層意味論へ」では $`\mbf{Set}_{\le 1}`$ を $`\mbf{Logic}`$ と書いています。
