にんじんと読む「Homotopy Type Theory」①

　Homotopy type theory（ホモトピー・型理論）は、集合論の代替になりうる。

　集合論は第一階述語論理の証明システム→ZFC集合論の二層から成り立っているが、型理論は第一階述語論理といった上位層の内部として理論を位置付ける必要がない。なぜなら命題は特定の型であり、定理の証明とは単にその特定の型をいじくる特殊操作にすぎないからである。

【ChatGPTによる要約】

型理論と集合論の主な違いは次のとおりです：

1. 基本的な概念:

   • 集合論: 集合論は集合と命題の2つの基本的な概念に基づいています。集合は対象の第2の層であり、命題は第1の層であり、集合と命題の間の相互作用が中心です。
   • 型理論: 型理論は型という1つの基本的な概念に基づいています。命題は特定の型と関連付けられ、証明はその型の要素として表現されます。型理論は独自の証明体系を持ち、第1の層の命題と第2の層の集合の相互作用が必要ありません。

2. 等号の取り扱い:

   • 集合論: 集合論では等号は命題として扱われます。すなわち、等号を否定または仮定できます。
   • 型理論: 型理論では等号は型として扱われ、2つの要素が等しいかどうかは「a =A b」という型が存在するかどうかにより判断されます。また、判断的等号または定義による等号も存在し、等号を定義によって制御できます。命題とは異なり、判断的等号は単に定義を展開することによって決定され、アルゴリズム的に決定可能です。

3. メタ言語:

   • 集合論: 集合論は通常の数学を記述するためのメタ言語（数学の「外部言語」）としてのみ使用されます。
   • 型理論: 型理論は自己完結的な証明体系であり、通常の数学の表現に直接使用できます。したがって、型理論はメタ理論としてのみ使用されず、通常の数学を記述するための形式言語としても使用されます。

これらの違いにより、型理論と集合論は数学的なアプローチに異なる視点を提供し、異なるニーズに対応します。

TYPE THEORY

• 　変数：a,b,c……
• 　型変数：A,B,C,……
• 　記号：→,：,=,（,）

　型変数は「型」であり、A,Bが型ならばA→Bは「型」である。これによって帰納的に「型」が定義される。

　あるaが型Aを持つと主張したい場合、「a：A」と書く。また、aとbが特定の型Aにおいて等しいと主張したい場合、「a=b：A」と書く。=については次のルールが定められている。

• 反射性: 型Aとa : Aが与えられた場合、a = a : A
• 対称性: 型Aとa ≡ b : Aが与えられた場合、b = a : A。
• 推移性: 型Aが与えられた場合、a = b : A および b = c : A の場合、a = c : A。

• 型の等価性: 型 A と B が与えられ、また a : A の場合、もし A = B : U であるならば、a : B である。

  ※型理論においてはすべてが型をもつので型にも型がある。型の型も型を持つので、型の型たちをまとめたUという型を考えている。universeという概念で、理解が難しい。要するにA:Uというのを見たら、Aは型なのだなというのがわかる。

　集合論においては関数は定義域と値域の直積の部分として定義されるが、型理論においてはより原始的な概念である。型理論における関数とは順序対の集合ではなく単なるルールの一つである。私たちには本来まだなにもいうことはできないが、たとえばf(x)=x+xは3という数字を入れた時には単に3+3を出力する規則と考えられる。

　その出力規則をΦとしたい場合（上の例ではx+x）、それにx:Aを適用した場合、A→Bという型を持つ関数は（λ（x:A）.Φ）：A→Bと書かれる。「いちいちこんなめんどくさい表記にしなくても」というのはもっともだが、f(x)=x+xと定義すると、これが関数を表示するものなのか、Bのオブジェクトについて表示したものなのかがまったくわからない。すべてのオブジェクトの型をはっきりさせる型理論にとってこの曖昧さは不便なのである。型A→Bの関数は（λ（x:A）.Φ）：A→Bのようにx:Aと指定されなくてもAのオブジェクトすべてにわたっているため、単にλx.Φ：A→Bとかき、これにa:Aを適用すると、（λx.Φ）(a）：Bと言う風になる。

型システム入門 プログラミング言語と型の理論