「贅沢なグロタンディーク宇宙とPropositions-As-Types」に対して、老婆心的な補足をします。$`\newcommand{\mrm}[1]{\mathrm{#1} }
\newcommand{\mbf}[1]{\mathbf{#1} }
\newcommand{\In}{\text{ in }}
`$
内容：
「命題」を排除したい！
「贅沢なグロタンディーク宇宙とPropositions-As-Types」より：
"logic"はそのまま形容詞的にも使います。logical〈ロジカル〉を使って、「論理的な人」とか「論理的に考える」とかを連想されるとチョット困るからです。言葉の印象による誤解・曲解は非常に多いので、気を使ってます。
テクニカルタームとして使う言葉の選択には気を使います。テクニカルタームは定義により約束される符牒（同業者内、仲間内でのみ通用する言葉 →Wikipedia項目）なんだから、なんだっていいじゃないか -- と、そう思うでしょ。僕もそう思っていました。が、実際はそうもいかないのです。
テクニカルタームを見て、国語辞書的意味が最初に連想されることがどうも多いのです。形式的定義がチャンとあると分かっていても、言葉の解釈が国語辞書的意味にどんどん寄っていってしまい、正確な形式的定義からはズレてしまう、という現象を僕はけっこう観察します（サンプルの絶対数は少ないですが）。
また、テクニカルタームが曖昧多義語（オーバーロードされた言葉）だと、曖昧性解決〈オーバーロード解決〉にしくじったときにトンデモナイ誤解・曲解をまねいたりします。
テクニカルタームは次のような方針で選んでいます。
- 国語辞書、日常的用法、他分野での用法などが連想されやすい言葉は避ける。当該分野とかけ離れた分野の言葉の借用はむしろリスクが少ない。例えば、型理論で「宇宙」を使っても、天文学用語だとして解釈する人はいないだろう。が、型理論で「インスタンス」や「項」を使うと、既存の知識で解釈されるリスクが高い。
- 曖昧多義語はできるだけ使わない。“2つの意味を持つ言葉”くらいはまー許容するとしても、“3つ以上の意味を持つ言葉”は避ける。
この基準から言うと、「命題」は使いたくないよね。
「贅沢なグロタンディーク宇宙とPropositions-As-Types」より：
「命題」の意味は曖昧で、少なくとも次の3つの用法があります。
- 真偽値
- 述語
- 論理式
数学の本や論文では、定理の意味で「命題」を使うこともあります； 「命題 2.3 より‥‥」とか。日常的用法としては、「課題」とか「ミッション」の意味で「我々に課せられた命題は‥‥」とか言うし。
上の引用のように、「真偽値」「述語」「論理式」を使って、「命題」を（テクニカルタームとしては）使用禁止にしてしまえば曖昧性は回避できます。が、「真偽値」がクセモノです。
「真」「偽」「値」の三文字から、多くの人は「真〈True〉と偽〈False〉の二つの値からなる二値ブール型」と解釈するでしょう。それは間違いではないです。それでいいんです； 多くの場面では。しかし、Propositions-As-Types について語る文脈においては、真偽値が二値だとは言えません。だからといって、真でも偽でもない中間（シロクロはっきりしない）を認めているわけでもないのです。
ベリティ型とその型宇宙
Propositions-As-Types において使う真偽値に相当するモノをベリティ型〈verity type〉と呼ぶことにします。これは、「贅沢なグロタンディーク宇宙とPropositions-As-Types」で「論理型〈locig type〉」と呼んでいたモノと同じです。「ベリティ」は聞いたことない言葉でしょうから、「論理」に比べて余計な連想を避けられます。
"verity" は英語辞書的に "truth" の（ほぼ）同義語です。"truth value"〈「真偽値」〉から、"truth" → "verity"、"value" → "type" と置き換えて "verity type"〈ベリティ型〉です*1。初見では「意味不明」「何も連想できない」ところがメリットです。
ベリティ型は、実体としてはデータ型と同じです。集合論ベースの意味論では単に集合です。
ベリティ型 ＝ データ型 ＝ 集合
集合圏 $`\mbf{Set}`$ を使って表すなら：
$`\quad \mbf{Verity} = \mbf{Type} = |\mbf{Set}|`$
「贅沢なグロタンディーク宇宙とPropositions-As-Types」で $`\mbf{Logic}`$ と書いていた型宇宙を $`\mbf{Verity}`$ にリネームしました。
- $`\mbf{Verity}`$ は、ベリティ型達が住む宇宙（「住む」に関しては「型・インスタンス・宇宙とタルスキ宇宙系列 // 居住関係」参照）
- $`\mbf{Type}`$ は、データ型達が住む宇宙
- $`\mbf{Verity}`$ と $`\mbf{Type}`$ は実際は同じ。
「贅沢なグロタンディーク宇宙とPropositions-As-Types」では、「実際は同じだけど、用途が違う」と説明しました。宇宙の上部構造である銀河を考えると、用途の違いが実際の違いとなって現れます。
銀河〈型銀河 | {type}? galaxy〉は圏のことです。型理論において、（特に宇宙と一緒に使うとき）適切な構造を備えた圏を銀河と呼ぶ、という用法です（以下の過去記事参照）。
$`\mbf{Logic}`$ → $`\mbf{Verity}`$ とリネームしたので、$`\mbf{Logic}`$ に別な意味を与えます。宇宙 $`\mbf{Verity}`$ の上部構造である銀河を $`\mbf{Logic}`$ とします。次が成立します。
$`\quad \mbf{Verity} = |\mbf{Logic}|`$
銀河〈圏〉 $`\mbf{Logic}`$ は、銀河〈圏〉 $`\mbf{Set}`$ と同じではありません。クラッシュモナドのクライスリ圏が $`\mbf{Logic}`$ です。
$`\quad \mbf{Logic} := \mbf{SetThin} := \mrm{Kl}(\,(\mrm{Crush, \mu, \eta}) \,)`$
クラッシュモナドについては：
モナドやクライスリ圏を知らなくても、圏 $`\mbf{Logic}`$ は次のように定義できます。
- 対象の集合： $`|\mbf{Logic}| = |\mbf{Set}|`$
- ホムセット：
- $`\mbf{Logic}(\emptyset, \emptyset)`$ は単元集合
- $`X`$ が空でないとき $`\mbf{Logic}(X, \emptyset)`$ は空集合
- $`Y`$ が空でないとき（$`X`$ は空でもよい） $`\mbf{Logic}(X, Y)`$ は単元集合
述語 ＝ ベリティ型ファミリー
Propositions-As-Types の立場・手法で論理を行うときは、$`0, 1`$ の2つの値からなる二元集合 $`\mbf{B} = \{0, 1\}`$ に代えて、ベリティ型からなる宇宙 $`\mbf{Verity}`$ を使います。そうなると、Propositions-As-Types の立場・手法における述語〈predicate〉は次の形になります。
$`\quad p : X \to \mbf{Verity} \In \mbf{SET}\\
\quad \text{where }X \in \mbf{Type}
`$
銀河〈圏〉を使って書けば：
$`\quad p : X \to |\mbf{Logic}| \In \mbf{SET}\\
\quad \text{where }X \in |\mbf{Set}|
`$
圏〈銀河〉としては、$`\mbf{Set}`$ と $`\mbf{Logic}`$ は違いますが、対象の集合は同じなので、次のようにも書けます。
$`\quad p : X \to |\mbf{Set}| \In \mbf{SET}\\
\quad \text{where }X \in |\mbf{Set}|
`$
$`p`$ は述語だと言いましたが、実際には $`p`$ は型ファミリー（集合論的には集合達のインデックス付きファミリー〈indexed family of sets〉）に過ぎません。データ型とベリティ型は、同じ宇宙に住んでますが、異なる銀河に住んでいる型です。データ型が同型であることは、集合のあいだの全単射があることですが、ベリティ型が同型であることは、「空集合かそうでないか」だけで決まります。
データ型とベリティ型は“同じだけど違う”のです。矛盾しているわけではなくて、ある観点からは同じだが、別の観点からは区別できるだけです。同様に、型ファミリーと述語（ベリティ型ファミリー）は“同じだが違う”のです。
同義語・曖昧多義語
型理論のように、非常に多くの観点〈POV | Point Of View | perspective〉から記述・観察ができる対象物では、観点を文脈としてたくさんの同義語・曖昧多義語が発生します。同義語・曖昧多義語をさばいて整理するのはなかなか大変です。事前に多少なりとも整理しておきたいとは思うのですが、それもけっこう大変（愚痴）。
*1:Verity が人名でもあるところがちょっと問題です。Dominic Verity にちなんだなにかに、形容詞としての Verity が付くかも知れません。
