「論理計算のための宇宙と型、二種類の述語」において、二元の宇宙 $`{\bf Prop}`$ を次のように定義しました。
$`\quad {\bf Prop} := |{\bf Bool}|`$
$`{\bf Bool}`$ は2つの対象 $`{\bf 0}, {\bf 1}`$ だけを持つ集合圏の充満部分圏です。
しかし実際の証明支援系などでは、$`{\bf Prop} = |{\bf Set}|`$ としています。このことについては、以下の過去記事で書いています。
スローガンは「真偽値は、なんだっていいのだ」です。
...[snip]...
宇宙全体を真偽値だと考えましょう。C言語の「数値が真偽値」の場合と同じように、真偽の解釈規則を与えます。
$`{\bf Prop} = |{\bf Set}|`$ のときは、任意のファミリー〈indexed family of sets〉が述語になります。$`\newcommand{\In}{\text{ in }}
\newcommand{\mrm}[1]{\mathrm{#1} }
\newcommand{\twoto}{\Rightarrow }
`$
$`\quad P \text{ が } X \text{ 上の述語} \iff P : X \to |{\bf Set}| \In {\bf SET}`$
値が $`{\bf 0}, {\bf 1}`$ とは限らないファミリーからグロタンディーク構成をすると〈要素の圏を作ると〉、ファイブレーションはモノ射〈単射〉とは限りません。値が $`{\bf 0}, {\bf 1}`$ のときは、薄いバンドルが出来ていたのですが、厚みがあるバンドルになるかも知れないのです。
しかし、$`|{\bf Bool}|`$ でも $`|{\bf Set}|`$ でも同じように論理ができるので、次の仕掛けがあるのでしょう。
- $`{\bf Bool}`$ と $`{\bf Set}`$ は、何らかの意味で同値である。
- 薄いバンドルと厚いバンドルは、何らかの意味で同値である。
内容：
クラッシュ・モナド
次のような、集合圏上の自己関手 $`\mrm{Crush}`$ を考えます。
- 集合 $`X`$ に対して、
$`\mrm{Crush}(X) := \text{if }X = {\bf 0}\text{ then }{\bf 0} \text{ else } {\bf 1}`$ - 写像 $`f:X \to Y`$ に対して、$`\mrm{Crush}(f):\mrm{Crush}(X) \to \mrm{Crush}(Y)`$ は自明に定まる。
自己関手 $`\mrm{Crush}`$ は、次が成立するのでベキ等〈idempotent〉です。アスタリスクは、関手の図式順結合記号とします。
$`\quad \mrm{Crush} * \mrm{Crush}= \mrm{Crush}`$
自然変換 $`\mu :: \mrm{Crush}*\mrm{Crush} \twoto \mrm{Crush}`$ を、次の成分で定義します。この成分は自明に定まります。
$`\text{For }X \in |{\bf Set}|\\
\quad \mu_X : \mrm{Crush}(\mrm{Crush}(X)) \to \mrm{Crush}(X) \In {\bf Set}`$
自然変換 $`\eta :: \mrm{Id} \twoto \mrm{Crush}`$ を、次の成分で定義します。この成分も自明に定まります。
$`\text{For }X \in |{\bf Set}|\\
\quad \eta_X : X \to \mrm{Crush}(X) \In {\bf Set}`$
$`(\mrm{Crush}, \mu, \eta)`$ は集合圏上のモナドになります。このモナドのクライスリ圏を $`{\bf SetThin}`$ とします。
$`\quad {\bf SetThin} := \mrm{Kl}( \,(\mrm{Crush}, \mu, \eta)\,)`$
$`|{\bf SetThin}| = |{\bf Set}|`$ ですが、$`{\bf SetThin}`$ はやせた圏〈thin category〉になります。つまり、ホムセットは単元集合か空集合です。
自然に決まる埋め込み関手 $`{\bf Bool} \to {\bf SetThin}`$ があります。埋め込み関手は、充満忠実〈fully faithful〉かつ本質的に全射〈essentially surjective〉です。したがって圏同値です。
この圏同値が、先の主張（以下に再掲）の内容です。
- $`{\bf Bool}`$ と $`{\bf Set}`$ は、何らかの意味で同値である。
像集合
ここでのバンドルは単なる写像のことです。全射であることを特に仮定はしません。バンドル $`p:A \to B`$ が薄いとは次のことだとします。
$`\quad \forall b\in B.(\, p^{-1}(b) \cong {\bf 1} \lor p^{-1}(b) \cong {\bf 0} \,)`$
バンドル-ファミリー対応により、ファミリーとして実現した述語はバンドルに対応します。バンドル-ファミリー対応については以下の記事達にあります。
値が $`{\bf 0}, {\bf 1}`$ であるファミリー〈述語〉は薄いバンドルに対応し、そうとは限らないファミリー〈述語〉は薄いバンドルになるとは限りません。
が、ファミリーを述語として解釈するなら、“厚み”は問題ではないのです。バンドル $`p`$ も写像なので、その像集合 $`\mrm{Img}(p)`$ がとれます。$`B`$ 上のバンドルに限ると、像集合をとる操作は次のような写像になります。
$`\quad \mrm{Img} : |{\bf Bun}[B]| \to \mrm{Pow}(B) \In {\bf SET}`$
$`\mrm{Pow}(B)`$ は $`B`$ のベキ集合ですが、伝統的なブール値述語の集合と同型になります。
$`\quad \mrm{Pow}(B) \cong \mrm{Map}(B, \{0, 1\}) \In {\bf Set}`$
$`\mrm{Img}`$ はバンドルの厚みを無視しますが、それによって、うまいことブール値述語との対応がとれます。バンドルが薄くても厚くても同じ像集合／ブール値述語に対応すれば同一視できます。
この同一視可能性が、先の主張（以下に再掲）の内容です。
- 薄いバンドルと厚いバンドルは、何らかの意味で同値である。
