“真に意味のある同一視は、要素の完全一致（strict equality）ではなく、構造保存的な可逆性＝equivalence によって与えられる”

論点は、

• 古典的集合論では = が最も強い同一性
• 圏論では isomorphism
• 高次圏・HoTT では equivalence

なぜ Voevodsky や Lurie のように、strict equality より equivalence を本質的同一視の基準に上げることが、公理論的（axiomatic）に正当化されるのか。

1. 条件

Homotopy Type Theory や Higher Category Theory的なアプローチに axiomaticity がある 理由は、

A. 数学的対象は「内部要素」より「構造と保存」で特徴づけられる

したがって、対象の同一性を = に固定するより、可逆な構造保存写像で捉えるとより一般化される。

B. 単なる哲学ではなく、公理として閉じた推論体系を作れる

• Voevodsky: Univalence Axiom
• Lurie: ∞-category / higher topos 的基礎

equivalence を中心にした推論が一貫した形式体系として動く。

C. 古典的数学にある「不変量による数学」と一致する

「同型まででよい」「同値まででよい」という暗黙の慣習を、後から厳密に基礎づけた。

2. 伝統的基礎における同一性

古典的集合論では、対象 a,b の同一性は

[a=b]

で与えられます。これは 要素が完全に一致する という extensional equality です。

たとえば集合 (A,B) が同型でも、普通は

[A ≅B ⇏ A=B]

です。

これは集合論では自然です。なぜなら集合の存在は、その要素そのもので決まるからです。しかし数学の多くの分野では、実際に重要なのは集合そのものではなく、その上の構造です。

• 群
• 位相空間
• 多様体
• 圏
• スペクトラム

対象の「本質」は内部実現ではなく、構造保存写像の可逆性で表されます。つまり実践的には

[A ≃B]

≃が構造上重要なファクターになることがほとんどであり、A = B は表現の特殊化にすぎないことが多い。

3. なぜ strict equality では不十分か

命題 1

数学的対象の多くは、表現依存ではなく不変量依存で扱われる。

例:

• 2つの群は、台集合が違っても群同型なら同じ群として扱う
• 2つの位相空間は、同相なら同じ空間として扱う
• 2つの圏は、同値なら同じ圏として扱う

このとき、= を本質的基準に置くと、毎回

• 定義を transport し
• 表現の差を調整し
• 「実は同じ」と言い換える

必要が出る。つまり strict equality は過剰に細かい。

命題 2

本質的対象論では、同一性は“区別不能性”に対応すべきである。

Leibniz 的に言えば、真の同一性は「すべての性質に関して置換可能」であるべきです。

ところが、構造数学での「区別不能性」はしばしば strict equality ではなく isomorphism / equivalence です。だから、数学実践の本質を反映するには

identity≈equivalence

という方向へ基礎を持っていく必然がある。

4. ここでいう axiomaticity とは何か

「axiomaticity がある」とは単に雰囲気ではなく、

1. 基本対象を定める
2. それらに対する基本関係・基本操作を定める
3. その上で推論規則が閉じる、構造が保存される
4. 既存数学を再構成できる

ということです。

5. Voevodsky の場合: Univalence がなぜ公理的か

5.1 型理論では identity type がある

Martin-Lof 型理論では、任意の型 (A) と要素 (a,b:A) に対し

Id_A(a,b)

という同一性型があります。

これは「(a) と (b) が同じである証拠」の全体です。同一性が単なる真偽値ではなく、構造を持つ対象になるため、冗長な条件記述を減らして抽象表現をすることができる。

5.2 型そのものの間にも identity がある

宇宙 ( 𝓊 ) を考えると、型 (A,B: 𝓊) に対して

Id_𝓊(A,B)

が存在。これは「型 (A) と (B) が等しい」。一方、型の間には equivalence

A≃B

もある。ここで古典的には、普通　A = B → A ≃ B　は成り立つが、逆は一般に成り立たない。

5.3 Univalence Axiom

Voevodsky の univalence は

Id_𝓊(a,b) ≃ Equiv(A,B)

を主張します。

型の等しさの証拠は、型の equivalence の証拠と同じだけある

重要点

これは「同値でも等しいと雑に言おう」という話ではないです。
むしろ、

• equality をより高次的に理解し
• その内容が equivalence と一致するように
• 宇宙の同一性を公理化する

という精密な主張です。

5.4 なぜこれが axiomatic なのか

なぜなら univalence は以下を満たすからです。

(i) 明示的な公理

体系に付け加える明確な原理である。

(ii) 推論を閉じる

equivalent な型に対して構成・定理・性質を transport できる。

(iii) モデルを持つ

Kan simplicial sets などでモデル化され、一貫性の見込みがある。

(iv) 実践数学を反映する

「同型な構造は同じものとして扱う」を形式化する。

6. Lurie の場合: なぜ equivalence 中心が公理的か

Lurie では舞台が ∞-category になります。

6.1 普通の圏での問題

1-圏では対象 (X,Y) の「同じさ」は通常

• strict equality (X=Y)
• isomorphism (X ≅ Y)

の二段階があります。

だが圏論では実際には = より ≅ の方が重要です。
さらに 2-圏以上になると、

• 対象間の射
• 射の間の 2-射
• 2-射の間の 3-射
• …

が出てきて、strict equality を土台にすると不自然になります。

6.2 ∞-category では “equal” より “equivalent”

∞-category では、対象の一致はしばしば
可逆な 1-射、さらに高次ホモトピーを含んだ形で捉えられます。

つまり本質は X ≃Y であり、これは単なる set-level の等号ではない。

Lurie の世界では、数学的対象は「高次の関係込み」で存在するため、strict equality はもはや本質的ではなく、equivalence class ではなく equivalence space が自然です。Timeの問題ではなく、Spaceの問題を扱うNP-completeのverify方法に類似しています。

6.3 なぜそれが公理的なのか

∞-category theory は、

• composition
• associativity
• units

を strict law としてではなく、coherent homotopy として公理化するからです。

厳密な等式で縛る代わりに、整合的な高次可逆データを公理にする。

これも明確な axiomatic reformulation です。

普通の公理化

(fg)h = f(gh)

高次公理化

(fg)h ≃ f(gh)
ただしこの ≃は勝手な緩和ではなく、さらにその上の整合条件を無限段階で満たす。

つまり Lurie 的公理性は“等号を捨てた” のではなく、“整合性の階層を公理化した”ところにあります。

7. 論理的展開としての「証明」

命題

命題：構造数学において、strict equality の代わりに equivalence を本質的同一性として採用するアプローチは、公理論的正当性を持つ。

証明の骨子

Step 1

数学的対象 (X) の本質が、その内部実現ではなく構造保存可能性にある場合、対象の同一性判定は局所的な = よりもより広域な equivalence に依存する。

Step 2

このとき、= を基礎に据える体系では、実践上必要な不変性がメタレベル処理に押し出される。したがって基礎体系として冗長である。

Step 3

もし identity 自体を equivalence に対応させる公理を導入すれば、数学的推論は本質的不変量に直接沿う。

• Voevodsky: Id_𝓊(a,b) ≃ Equiv(A,B)
• Lurie: strict law の代わりに higher coherent equivalence

Step 4

この公理化は

• 形式的推論規則を持ち
• モデルを持ち
• 既存数学を再構成し
• 数学実践の invariant viewpoint を内部化する

ので、公理系として成立する。

結論

ゆえに、equivalence を本質的同一性に引き上げる立場は、単なる哲学的態度ではなく、十分に axiomatic である。

8. 注意

注意 1

“同型なら何でも等しい” ではない。

Voevodsky でも Lurie でも、雑に「全部同じ」と言っているわけではありません。

• 何が equivalence なのか
• どのレベルでの equivalence なのか
• その整合条件は何か

を精密に定めます。

注意 2

strictness を否定しているのではない。

むしろ、

• strict equality は残る
• しかし本質的分類には equivalence を使う
• そのこと自体を公理に織り込む

という形です。

注意 3

“同値でなくても同型なら equivalence 等価” という言い方は文脈依存

• 1-圏では isomorphism が equivalence
• 2-圏では equivalence は isomorphism より弱い
• ∞-圏では equivalence はさらに高次的

なので、isomorphism = equivalence は一般には 1-圏的な言い方です。

Lurie 的には、isomorphism というよりinvertible morphism up to coherent higher homotopyが equivalence 等価です。

9. まとめ

古典的基礎は存在者が先にあり、その一致が等号で決まるという存在論に近い。

Voevodsky / Lurie 的基礎は

対象は関係の網の中で現れ、その本質は可逆な構造保存性で与えられる

というホモトピカルコヒーレンス。“何を primitive に取るか” が、要素から構造へ、構造から関係へ、関係から高次整合へ移った。

Voevodsky や Lurie の公理性は、strict equality を捨てたことにあるのではなく、数学の本質が invariant structure にあるという事実を、identity の側へ持ち上げて公理化したことにある。

Voevodsky的・Lurie的にZFCを定義するとしたらどうなるか

• ZFC: 集合が基本
• Voevodsky/Lurie: より高次の構造が基本で、集合はその特殊例

1. ZFCでは何が基本か

ZFCの基礎は大きく言えば3つです。

1. 対象としての集合
2. 基本関係としての「∈」
3. 基本的同一性としての「=」

ZFCでは、すべての数学対象は最終的には集合として表されます。
そして、集合の同一性は外延性によって決まります。

要するに「同じ要素を持つなら同じ集合である」という立場です。

しかし数学では、「同型だが等しくない」ということが普通に起こります。
たとえば2つの群が群として完全に同じ構造を持っていても、台集合の実現が違えば別物です。

2. Voevodsky的な置き換え

Voevodskyの方向では、集合の代わりにまず「型」が基本になります。
そして、要素が集合に属するというより、「ある型の項である」と考えます。

ZFC的な書き方:

• x ∈ A

HoTT的な書き方:

• x : A

ここでAは集合というより「型」です。

さらに重要なのは、等号の意味が変わることです。

ZFCでは、

• x = y
  は単なる真偽です。

HoTTでは、

• Id_A(x, y)
  は「xとyが同じである証拠の型」になります。

つまり、同一性がただの2値ではなく、構造を持つものになります。

3. Univalenceで何が起こるか

Voevodskyの決定的な点は Univalence です。

直感的にはこうです。

• 型Aと型Bが本質的に同じ構造を持つなら
• それらは等しいものとして扱ってよい

ただしこれは雑な同一視ではありません。
厳密には、「等しさの空間」と「equivalenceの空間」が対応する、という主張です。

普通の集合論では、

• A = B なら AとBは同型
• でも AとBが同型でも A = B とは限らない

となります。

Univalenceでは、このギャップを埋めます。

すると、「同型をいちいち経由して移す」という冗長な記述が減り、構造不変な記述がそのまま基礎言語になります。

4. その中で集合はどう定義されるか

HoTTでは、すべてが最初から集合ではありません。
型には高次の同一性があり、同一性の証拠どうしにもさらに同一性がありえます。

そこで、ZFC的な意味での集合に対応するものは、次のような特別な型として定義されます。

• 0-truncated type
• h-set

意味は、

• 要素どうしの同一性はある
• しかしその同一性の証拠どうしには、もう面白い高次構造がない

ということです。

言い換えると、パスやホモトピーのような高次情報が潰れていて、古典的集合にかなり近いレベルまで落ちている型です。

したがって、Voevodsky的にZFCを作るなら、

• 世界全体 = 型の宇宙
• 集合 = その中の0-truncatedな型

となります。

5. Lurie的な置き換え

Lurieの方向では、型理論よりも∞-圏や∞-toposが中心になります。

ここでは公理系は、単なる集合の集まりではなく、対象と射と高次射を持つ構造として扱われます。

ZFCでは対象が最初から集合ですが、Lurie的にはまず

• ∞-topos

のような大きな構造があり、その中に対象が存在します。

そして集合に相当するものは、その中の

• 0-truncated object

です。

これはVoevodskyの0-truncated typeとほぼ同じ方向の発想です。

6. Lurie的には「∈」はどうなるか

ZFCでは要素 belonging が基本です。Lurie的には、要素はしばしば「終対象からの射」として理解されます。

つまり、

• x ∈ A

は素朴な帰属関係というより、

• 1 → A

という射で表されます。

ここで1は終対象です。

言い換えると、要素とは「一般化された点」です。これは層やトポスの考え方とも一致します。

7. Lurie的には等号はどうなるか

Lurieの世界では、対象の一致は strict equality よりも path, homotopy, equivalence によって理解されます。

つまり対象AとBが「同じ」とは、単に記号上同一というより、

• 可逆な射があり
• その可逆性が高次整合性を伴って成立している

ということです。

1-圏なら「同型」に近いですが、∞-圏ではもっと強く、

• 射の間のホモトピー
• ホモトピーの間のホモトピー
• そのさらに上

まで含めて整合している必要があります。だからLurie的基礎は、「等号を緩めた」というより、「等号の代わりに高次整合性を公理化」しています。

8. Voevodsky的ZFCのイメージ

Voevodsky的ZFCは次のような感じです。

基本公理

• すべての対象は集合ではなく型である

membership

• x ∈ A ではなく x : A

equality

• 等号は単なる真偽ではなく、同一性の証拠の型を持つ

集合

• 集合とは、型のうち高次の同一性が潰れたもの
• つまり 0-truncated type

本質的同一性

• 型どうしの equivalence は、等しさと対応する
• これを保証するのが univalence

「集合を基本にする」のではなく、
「型とその高次同一性を基本にし、その一番平坦な部分を集合と呼ぶ」

という構図です。

9. Lurie的ZFCのイメージ

Lurie的に言うと次のようになります。

基本公理

• すべての対象は ∞-topos の中にある

membership

• 要素は belonging というより generalized point
• つまり 1 → A という射

equality

• 等しさは strict equality より path / homotopy / equivalence が本質

集合

• 集合とは ∞-topos の中の 0-truncated object

論理

• 論理は単なる外部メタ言語ではなく、topos の内部論理として現れる

つまり、

「集合の宇宙」が先にあるのではなく、
「関係と高次整合性の宇宙」が先にあり、
集合はその中の離散的・平坦な層として出てくる

10. ZFCとの一番大きな違い

ZFCとVoevodsky/Lurieの差

ZFC

• 世界は要素の集まりからできている
• 同一性は外延的一致で決まる
• 同型は等号より弱い

Voevodsky/Lurie

• 世界は関係とその高次整合性からできている
• 同一性は証拠や経路やequivalenceを持つ
• 集合は高次構造を消した特別な場合にすぎない

したがって、ZFCの「集合中心宇宙」は、より一般化されたVoevodsky/Lurieでは「高次構造の特殊断面」という特殊解に変わります。

11. 一番圧縮した定義

Voevodsky的にZFCを再定義するなら:

• 集合 = 0-truncated type
• 属する = typing
• 等しい = identity type
• 本質的同一性 = equivalence
• 宇宙 = types の universe

Lurie的にZFCを再定義するなら:

• 集合 = ∞-topos における 0-truncated object
• 属する = 終対象からの射
• 等しい = path / homotopy / equivalence
• 宇宙 = ∞-topos

12. 哲学的に一言で言うと

ZFCでは、
「何が入っているか」
が対象の本体です。

Voevodsky/Lurieでは、
「どういう対象、階層、関係があるか」
が対象の本体です。

だからVoevodsky的・Lurie的にZFCを定義するとは、単に公理を書き換えることではなく、

集合の形而上学を、要素中心から構造・関係・高次整合性中心へ反転すること

を意味します。

13. まとめ

Voevodsky的・Lurie的にZFCを定義すると、集合は所与の存在者ではなくなる。
まず型や∞-toposがあり、集合はその中の 0-truncated な特別な対象として定義される。
等号は単なる記号的一致ではなく、identity, path, homotopy, equivalence の側で理解される。
つまり、ZFCの世界は「高次構造を持つ基礎」の特殊解、離散部分として回収される。