昨日の記事「カリー／ハワード／ランベック対応とハイティング／ド・モルガン圏」で話題にしたハイティング圏について、もう少しダラッと述べます。$`
\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\cat}[1]{\mathcal{#1}}
%\newcommand{\msf}[1]{\mathsf{#1}}
%\newcommand{\mbb}[1]{\mathbb{#1}}
%\newcommand{\hyp}{\text{－} }
%\newcommand{\twoto}{\Rightarrow }
\newcommand{\In}{ \text{ in } }
%\newcommand{\ot}{\leftarrow}
%\newcommand{\op}{\mathrm{op}}
\newcommand{\Imp}{\Rightarrow }
`$
内容：
ネーミング
僕がネーミングに気をつけるようになったのは、名前の語感や連想から判断してしまう人が一定数いることを知ったからです。もちろん、分かりやすい名前がいいのですが、誤認・誤解を招きそうな名前はむしろ意味不明な名前に変えてしまったほうが安全だと思っています。意味不明な名前の素材によく使うのは人名です。
ハイティング〈Arend Heyting〉にちなんで名付けたハイティング圏〈Heyting category〉は、直和を持つデカルト閉圏のことです。直積〈デカルト積〉と直和〈デカルト余積〉の両方を持つ圏は双デカルト圏〈biCartesian category〉と呼ぶので、ハイティング圏＝直和を持つデカルト閉圏は双デカルト閉圏〈biCartesian closed category〉とも呼びます。
「双デカルト閉圏」だと、「双」や「閉」のかかり具合が分かりにくくて、「直和に関してもモノイド閉構造を持つ圏だろう」とか間違った推測をする人がいるかも知れません。もちろん、定義を確認せずに推測するほうが悪いのですが、字面からの推測も連想も出来ない「ハイティング圏」のほうが望ましいと僕は思います。
用語「ハイティング圏」の前に、次のような形容詞を付けた概念を考えます。
- やせた
- 小さい
- ド・モルガン
- ブール
- モノイド〈monoidal〉
「やせた」「小さい」は圏の一般論で使われる形容詞です。「ド・モルガン」と「ブール」はハイティング圏に対してしか意味を持たない形容詞です。形容詞「モノイド〈monoidal〉」は、直積〈デカルト積〉の代わりに一般的なモノイド積を考えることを意味します。
デカルト〈René Descartes〉やブール〈George Boole〉は、形容詞 Cartesian, Boolean がありますが、通常は、人名をそのまま形容詞にします。Heyting, De Morgan はそのままで形容詞です。
ハイティング前代数とハイティング代数
圏 $`\cat{C}`$ がやせている〈thin〉とは次のことです（必要なら、「はじめての圏論 その第3歩：極端な圏達 // 射が少ないやせた圏」参照）。
$`\text{For }A, B \in |\cat{C}|\\
\quad \text{Holds }\cat{C}(A, B) = \emptyset \lor \cat{C}(A, B) \cong \mbf{1}
`$
やせたハイティング圏はハイティング前代数〈Heyting prealgebra〉といいます。台圏〈underlying category〉がやせているので、プレ順序集合〈preordered set〉だとみなせます。台圏が順序集合とみなせるとき（とてもやせた圏〈very thin category〉のとき）、そんなハイティング圏はハイティング代数〈Heyting prealgebra〉と呼びます。なお、"preorder" を「プレ順序」と書くのは、口頭で「全順序〈total order〉」と区別がつかないからです。
ハイティング圏が小さい圏〈small category〉とは仮定してなかったので、上の定義のハイティング前代数もハイティング代数も小さいとは限りません。しかし、通常は小さい圏を想定している場合が多いでしょう。
多くの場面で：
- ハイティング前代数とは、小さなやせたハイティング圏である。
- ハイティング代数とは、小さなとてもやせたハイティング圏である。
ハイティング代数は、直観主義論理に対応する順序代数構造として古くから研究されてきた対象物です。ハイティング圏は、ハイティング代数の圏論化〈categorification〉と言っていいでしょう。
ハイティング圏の例
まず、集合圏 $`\mbf{Set}`$ はハイティング圏になっています。これは、小さくない圏だし、やせた圏でもありません。おおきな太ったハイティング圏です。
有限集合達の圏 $`\mbf{FinSet}`$ もハイティング圏です。これも、小さくない圏だし、やせた圏でもありません。有限集合しか入ってないので、圏 $`\mbf{FinSet}`$ のなかで無限の極限や余極限をとることは出来ません。
「「命題」の曖昧性から前層意味論へ // 真偽値と論理圏」において、論理圏 $`\mbf{Logic}`$ を定義しました。圏 $`\mbf{Logic}`$ は集合圏 $`\mbf{Set}`$ と類似した圏で、やはりハイティング圏になっています。集合圏とは違い、やせた圏です。しかし、とてもやせた圏ではありません。言うならば、大きなハイティング前代数です。
古典二値真偽値の二元集合 $`\mbf{B}`$ を圏だとみなすと、小さなとてもやせたハイティング圏になります。つまり、圏とみなした $`\mbf{B}`$ はハイティング代数です。$`\mbf{B}`$ はブール代数としてお馴染みですが、ブール代数はハイティング代数になります（逆は成立しません）。
$`X`$ を集合として、ベキ集合 $`\mrm{Pow}(X)`$ にしかるべき演算と順序を入れるとブール代数になります。したがって、しかるべき演算と順序を備えた $`\mrm{Pow}(X)`$ はハイティング代数でもあります。ハイティング代数は小さなとてもやせたハイティング圏のことでした。
$`T`$ を位相空間として、開集合の集合 $`\mrm{Open}(T)`$ にしかるべき演算と順序を入れるとハイティング代数、つまり小さなとてもやせたハイティング圏になります。しかし、$`\mrm{Open}(T)`$ がブール代数になるとは限りません。
単元集合 $`\mbf{1}`$ を自明な位相空間とみなして、次が成立します。
$`\quad \mrm{Open}(\mbf{1}) = \mrm{Pow}(\mbf{1}) \cong \mbf{B} \text{ as Heyting category}`$
ド・モルガンの法則と古典論理の法則
「カリー／ハワード／ランベック対応とハイティング／ド・モルガン圏 // 追記」で述べたように、ハイティング圏なら、選言〈直和〉の否定に関するド・モルガンの法則は成立するようです。しかし、連言〈直積〉の否定に関するド・モルガンの法則は必ずしも成立しないようなので、公理として要請します。ド・モルガンの法則が完全に成立するハイティング圏をド・モルガン／ハイティング圏〈De Morgan-Heyting category〉と呼びます -- 「カリー／ハワード／ランベック対応とハイティング／ド・モルガン圏」とは、人名形容詞の語順が逆ですが。
ド・モルガン／ハイティング圏があれば十分なことも多そうですが、ド・モルガン／ハイティング圏で古典論理の法則が成立することは保証できません。古典論理を特徴づける法則に次のようなものがあります。
- 二重否定の法則 $`\lnot \lnot A \equiv A`$
- 排中律 $` \lnot A + A \equiv 1`$
- 含意の古典的定義 $`[A, B] \equiv \lnot A + B`$
記法をより論理っぽくするなら：
- 二重否定の法則 $`\lnot \lnot A \equiv A`$
- 排中律 $` \lnot A \lor A \equiv \top`$
- 含意の古典的定義 $`A \Imp B \equiv \lnot A \lor B`$
これらを全部公理に入れる必要はなくて、どれか1つでもハイティングの公理系に付け加えれば、古典論理ができます。例えば、ハイティングの公理系＋二重否定の法則で、古典論理になります。
古典論理の法則のどれかを仮定した（追加した）ハイティング圏をブール／ハイティング圏〈Boolean Heyting category〉と呼ぶことにします。小さくてとてもやせたブール／ハイティング圏はブール代数です。
モノイド・ハイティング圏
ハイティング圏の定義において、直積〈デカルト積〉と直和〈デカルト余積〉はモノイド積として与えられています。直和はそのまま残して、直積を任意のモノイド積に置き換えた構造をモノイド・ハイティング圏〈monoidal Heyting category〉と呼ぶことにしましょう。関係圏 $`\mbf{Rel}`$ やベクトル空間の圏 $`\mbf{Vect}_K`$ は、モノイド・ハイティング圏の例になります。
モノイド・ハイティング圏を定義する際は、最初に余デカルト圏 $`(\cat{C}, +, 0)`$ を考えて、その上に直和を保存するモノイド積 $`\otimes`$ を載せるといいでしょう。モノイド積 $`\otimes`$ は直積とは限らないので、射影や対角が存在するとは限りません。単位対象 $`I`$ が終対象だとも言えません。
モノイド・ハイティング圏の典型的事例である $`\mbf{Rel}`$ や $`\mbf{Vect}_K`$ では、始対象と終対象は一致していて、直和は直積を兼ねています。直積（直和でもある）とは全然別物のモノイド積〈テンソル積〉があり、そのモノイド積に関するモノイド閉構造を持ちます。
こうなると、古典論理や直観主義論理とはまったく違った様相を呈しますが、それでも、“ある種の論理”と解釈することは出来ます。内部ホム〈指数〉は含意だし、双対操作〈dualizing〉が否定になります。
直和とモノイド積〈テンソル積〉を持つ圏に関して、以下の過去記事があります。
おわりに
デカルト閉圏は、カリー／ハワード／ランベック対応の最初に出てくる例ですが、論理をする環境として見ると、連言含意論理（AND と IMPLIES しかない論理）なので、物足りないし、実用にはなりません。
デカルト閉圏に直和が入ると、OR と NOT も使えるようになるので、だいぶ論理らしくなります。それがハイティング圏でした。ハイティング圏で古典論理が出来るわけではありませんが、「実用になる論理」の出発点としては適切でしょう。
ハイティング圏を強くして古典論理に向かう方向性があります。一方で、デカルト積を弱めてモノイド積にすることにより、古典論理とは全然違った世界を見せてくれます。
また、「命題」「真偽値」のような厄介な曖昧多義語をうまく解釈する道具としても、ハイティング圏は大変に有用です。命題実体＝述語 とは、ハイティング圏を余域とする関手のことだし、真偽値とはハイティング圏の対象だと定義すれば丸く収まります。
ハイティング圏は、論理／型理論／圏論を互いに結び合わせる良い位置に居る構造です。
