UniMath Coq
UniMath
通常の数学者が紙とペンで書く「定理と証明」が、Coqの世界ではどのように「型（Type）」と「項（Term）」に置き換わるのか。
1. 「証明」という名のプログラム
コードは関数型プログラミング（Haskellなど）に似ています。
たとえば、「ある型 A と B が同値である」という命題を証明する場合、以下のようなステップをCoqに打ち込みます。
Coq
Definition is_equivalence (f : A -> B) :=
exists (g : B -> A), (forall x, g (f x) = x) /\ (forall y, f (g y) = y).
- 何をしているか: 「関数 f が同値（逆写像を持つ）である」という定義を、「型」として宣言しています。
- Coqの反応: もし証明者がこの f を具体的に提示し、逆写像 g が存在することを示せなければ、Coqは「型が合いません（証明不十分です）」とエラーを出し、計算を停止させます。
2. h-level（ホモトピー・レベル）
Coqの中で、数学的対象をその「複雑さ」に応じて階層化するのがUniMathの設計思想です。
| レベル (h-level) | 数学的な意味 | Coqでの扱い |
| h-Prop (Level 0) | 命題（真か偽か） | 答えが一つしかない型（「はい」か「いいえ」） |
| h-Set (Level 1) | 集合 | 要素が区別できる（例：自然数 1, 2, 3…） |
| Groupoid (Level 2) | 群様（図形など） | 要素間の「等しさ」自体に複数の道（パス）がある |
低次元「論理」から高次元「幾何学」までを一つの言語（Coq）で記述できるようにしました。
3. 「一価性公理（Univalence）」のコード
Coq
Axiom univalence : forall (A B : UU), (A ≃ B) ≃ (A = B).
- 意味: 「型 A と B が同値であること（≃）」と「型 Aと B が同一であること（=）」は、計算機の上で全く同じ（等価）として扱ってよい。
- 効果: これにより、コンピュータは「構造が同じなら、それは同じものだ」と認識できるようになります。人間がいちいち「これは定義は違うけど本質的には同じだから、同じ議論が使えるよね」と説明する手間（＝摩擦）が消滅しました。
4. 人間とCoqの「対話」
- 人間: 「このトポロジー的な性質を証明したい（ゴールを設定）」
- Coq: 「現在の前提条件はこれらです。次にどの論理ステップ（Tactic）を使いますか？」
- 人間: 「
apply induction（帰納法を適用せよ）」 - Coq: 「適用しました。残る証明の課題（サブゴール）はあと2つです」
このやり取りの果てに、画面に Proof Completed（証明完了） と表示されたとき、それは「人間の主観的な納得」ではなく、「宇宙の論理構造と合致した」という物理的な証拠になります。