[0076] 統一された正しい同一視の概念

ホモトピー型理論を数学の言語(数学の基礎付けまたは圏の内部言語)と見た場合、長所として「統一された正しい同一視の概念」が挙げられる。比較のために、事実上標準的な数学の基礎付けである公理的集合論では同一視の概念が「正しい」とは言い難いことを説明する。公理的集合論では、あらゆる数学的対象は集合として実装される。二つの集合が同一であるのはそれらが全く同じ要素を持つ場合である。この同一視の概念は統一されてはいるが、「正しい」同一視ではない。数学者が実際に二つの集合を同一視するのはそれらの間に全単射がある時である。また、なんらかの構造(例えば群構造)を持った二つの集合を同一視するのはそれらの間に同型写像(例えば群同型)がある時であるし、場合によっては同型よりも弱い概念(例えば圏同値やホモトピー同値)によって二つの対象を同一視する。つまり、言語が提供する同一視の概念と数学者が本当に求めている同一視の概念が乖離している。

集合としての同一性よりも弱い同一視の概念を使うということは、各種概念が弱い同一視の下で不変であるかどうかを常に気にしなければならない。例えば、二つの集合の間に全単射があればそれらの濃度は同じなので、濃度は全単射の下で不変であり、濃度について論じる時は集合を全単射の下で同一視しても問題はない。一方、集合\(X\)についての性質「\(X\)は空集合を要素に持つ」は全単射の下で不変ではない。このように、公理的集合論の言語を使う限り、全単射の下で不変でないような性質は簡単に書けてしまい、そのような性質に言及した場合には全単射による同一視は(一般には)正当化されない。「空集合を要素に持つ」はやや人工的な例だが、もう少し自然な例だと「圏が有限個の対象と射を持つ」といった性質は圏同値で不変でないにもかかわらず圏論の教科書に登場することがある。

対して、ホモトピー型理論には統一された同一視の概念があり、あらゆる性質はその同一視の下で不変であり、かつその同一視の概念は「正しい」ものであることを証明できる。一価性公理は二つの型の間に同値があればそれらは同一視されるというものであったが、実はこの公理があればあらゆる構造について同一視の概念が「正しい」ものであることが導出される。この現象は構造同一原理(structure identity principle)と呼ばれる。例えば、二つの群の間に群同型があればそれらは同一視され、二つの圏の間に圏同値があればそれらは同一視される、などが定理として得られる。よって、あらゆる性質は群同型や圏同値の下で不変である。群同型や圏同型の下で不変でないようなものはそもそも書けないように言語が設計されていると言ってもよい。