型 がどこまで複雑な等しさを持つかを測る指標を h-level と呼び、可縮空間（1 点に潰せる空間）を 0 として数えます。h-level が 1 上がるごとに、「等しさの間の等しさ」が１段深くなります。
はじめに
この記事は、ホモトピー型理論（HoTT、Homotopy Type Theory） を分かりやすく解説する連載シリーズの初回記です。
学部レベルの数学の予備知識だけを前提知識として、平易に分かりやすく解説することを心がけます。
「ホモトピー型理論」という名前だけを聞くと、抽象的な数学の話に思われるかもしれません。
しかし HoTT は、すでに実学上の成果を生んでいます。
たとえば、みなさんがリファクタリング（内部実装の書き換え）を行うとき、必ず気にされていることがあるはずです。
それは、書き換えの前後で、コードの振る舞いが変わっていないか、という点です。
for ループで書いた実装と、再帰で書いた実装。
コードはまったく違うのに、同じ入力に対して同じ出力を返すなら、両者は「等しい」と言ってよいはずです。
この「等しさ」を、機械が検証できる形で書き下したものが、HoTT の関数外延性にあたります。
さらにHoTT は、「同型な構造は同じものとして扱う」という数学者の慣習も、Univalence Axiom という公理として明文化しました。
これにより、ある型で証明した性質を、同型な別の型へそのまま運べるようになります。
証明しやすい素朴な実装で定理を証明し、その証明を効率のよい実装へ移す
── そうした分業が、形式的に正当な操作として実行できるのです。
こうした規則は、証明支援系（定理証明を計算機に検証させるシステム）の中で、実際に動いています。
とくに Cubical Agda は、Univalence を「計算できる」形で実装した言語です。
公理として置くだけでなく、実際にプログラムとして走らせられる
── ここが画期的でした。数学の証明が、計算機の上で実行可能なコードになった のです。
純粋数学の側でも、具体的な成果が出ています。
代表的なものを３つ挙げます。
第１に、古典数学に新しい定理が還流しました。
代数トポロジーの古典的な結果である Blakers-Massey の定理を HoTT の中で証明しようとしたとき、位相空間の細かい構造に頼らない、まったく新しい証明が見つかりました。
その論法が任意の ∞-トポスで通用することが判明し、古典的な定理よりも一般的な形の Blakers-Massey 定理が 2020年に発表されています。
制約の多い環境で証明を探したことが、結果として数学そのものを前進させた事例です。
第２に、計算できなかった量が計算されました。
球面のホモトピー群 $π_4(S^3) ≅ ℤ/nℤ$ の $n$ について、Guillaume Brunerie が HoTT の内部で定義を与え、$n = 2$ であることを証明しました（2016年）。
2022年には、これが Cubical Agda で形式化され、コンピュータが実際に $n$ の値を計算するところまで到達しています。
第３に、証明の再利用が現実的になりました。
「同型なら等しい」を保証する構造同一性原理により、群 $G$ で証明した定理を、$G$ と同型な任意の群へそのまま運べます。
UniMath のような大規模な形式化ライブラリで、証明の重複が大きく減ることが期待されており、実際に成果が出はじめています。
一方で、過大な期待は禁物です。
数論、解析学、確率論といった分野で、HoTTが直接の道具として使われている例は、2026年7月現在、ほとんどありません。
いま成果が出ているのは、もともとホモトピー論的な構造を持つ領域
── 代数トポロジー、高次圏論、そしてその形式化 に集中しています。
この記事では、その範囲を正確に見極めながら、「型」を「空間」として捉え、「2点を結ぶ経路」の数だけ「異なる等しさ」を識別するホモトピー型理論（HoTT）と何なのか？
そして、そのHoTTが何を変えつつあるのかを見ていきます。
HoTTとは何か
HoTT は、まだ産声を上げてから20年弱の新しい数学分野です。
歴史を簡単に振り返ると、2007年に初期の基礎論文の１つ（ Awodey-Warren,"Homotopy Theoretic Models of Identity Types"）が arXiv に提出されました。
ほぼ同時期に、Vladimir Voevodsky も独立に関連する研究を並行して進めており、両者の研究は独立してほぼ並行して発展しました。
その後、次のような経緯をたどって、今日 ホモトピー型理論（HoTT、Homotopy Type Theory）と呼ばれる新しい数学理論が形成されるに至りました。
-
2010年 ── Voevodsky が Univalence Axiom を提唱
-
2012-2013年 ── Univalent Foundations Program の立ち上げ（米国 Princeton の Institute for Advanced Study で開催）
- 2013年 ── 体系書 "Homotopy Type Theory: Univalent Foundations of Mathematics"（通称 HoTT Book）が刊行
このHoTT理論が、「型」を「空間」として捉え、「2点を結ぶ経路」の数だけ「異なる等しさ」を認識することを見ていきます。
そして、そのようなものの見方 を採用することによって、数学や情報学の分野で、どのような新たな成果が得られつつあるのか** にも、光を当てます。
「型」を「空間」として捉える
HoTTは、「型」を空間として捉える見方をします。
さらに、２つの数学的対象が等しいことを、２点を結ぶ「経路」（道）が一つ以上、存在すること として定義します。
ここで、互いに連続変形して移り合える２つの経路は、経路そのものとしては別のものですが、経路を連続的に動かせば互いに重ね合わせられるので「同じ等しさを表している」とみなします。
ただし、この「同じ等しさを表している」ということが認識できるのは、実は１つ上の次元での話です。
つまり、２つの経路そのもの（１段目の等しさ）を並べて比べているのではなく、その２つの経路をつなぐ「経路と経路の間の変形」（２段目の等しさ）が存在するということを見て、はじめて２つの経路が「同じ等しさを表している」と判定できるのです。
*2本の経路そのものを並べて見比べても、同じ等しさを表しているかは判定できない。
両者をつなぐ変形 $H$ が存在することを、1つ上の次元から見て初めて判定できる。*
２つの点の間に、互いに連続変形しあうことができない複数の「異なる」経路が存在するとき、その２つの点の間には、同じ１段目の階層の中に、互いに異なる複数の「等しさ」が存在する と捉えます。
さらに、２つの経路の間をつなぐ変形方法が存在する場合、両者（２つの経路）は一つ上の２段目の次元の階層で「等しい」 と認識されます。
同様にして、その変形方法と、別の変形方法の間をつなぐより高次の変形は、3段目の次元の階層における「等しさ」の成立として認識されます。
このような 「等しさ」の階層が無限に続く というのがHoTTの中心的な発見です。
つまり、HoTTでは、「等しい」ということの中に次の２つの豊かさが生じます。
-
同じ階層の中に、互いに変形で移り合わない複数の「等しさ」（=複数の経路）が存在しうる
-
「等しさ」の階層が、1段目・2段目・3段目・...と、無限に続く
この豊かな「等しさ」の構造を互いに区別して認識できるところに、HoTTが持つ優れた特徴があります。
この記事では、HoTTが持つこの優れた特徴が、数学や物理学、量子コンピュータの領域で、いま研究レベルでどのように威力を発揮しつつあるのか、研究の最前線で起きていることも紹介します。
想定読者
大学理系学部生
数学・物理・化学・生物・工学・情報科学のいずれかを専攻された方。
集合論、位相空間、群論の初歩は学んでいる。しかしCurry-Howard対応、圏論、ホモトピー型理論(HoTT)は初見。
記事の中心の問い
ホモトピー型理論(HoTT)は、数学と情報科学でどう役立ち、他分野へどこまで広がりうるのか?
TL;DR
ホモトピー型理論（Homotopy Type Theory、以下 HoTT） は、集合や群、位相空間などの数学的対象について「A と B が等しい」かどうかを問うとき、その等しさには、等しさのあり方が異なる、レベルの異なる複数の"等しさ"がありうる、という視座を提示するまだ新しい数学理論です。
基盤となる考え方は、2006-2010年頃 に、Awodey-Warren と Voevodsky が独立の視点から築き、2013年にいわゆる"HoTT Book"が刊行されたことで、正式な数学の分野として立ち上がりました。
HoTT が「型」を「空間」として扱うとは、どういうことか？
数学における**「空間」というのは、大まかに言えば、「点（要素）の集まり」と「点の間の何らかの構造」を持つ対象のこと** です。
位相空間なら開集合系(近さのルール)、距離空間なら距離関数、ベクトル空間なら加法とスカラー倍、というふうに、空間の種類ごとに構造の中身が変わります。
HoTTでは、値の分類を表す「型（type）」を、そのまま空間の一種として扱います。
ここで「型」とは、プログラミングでも使われる概念で、たとえば 整数の型 $Int$（要素は 1、2、3、...）、真偽値の型 $bool$ （要素は true と false の２つ）、群の型 $Group$（要素は具体的な個々の群、たとえば整数の加法群、対称群 $S_3$ など）、といった、値を分類する枠のことです。
これらそれぞれの型を、HoTTは空間として捉え直します。
型の要素（$Int$ なら 1、2、3、...、$bool$ なら true と false、Group なら個々の群）が、その空間の「点」 にあたります。
そして、点の間の構造として、
「点と点を結ぶ経路の集まり」
「経路と経路をつなぐ変形の集まり」
「変形と変形をつなぐ変形の集まり」
...
という無限に続く階層構造 を持ちます。
この経路の階層構造が、位相空間の開集合系や距離関数とは種類の違う構造 として、「点の間に構造がある」という空間の定義を満たしています。
Int、bool、Group といった値を分類する枠を、HoTT は空間として捉え直す。型の要素が空間の点となり、点の間には経路・変形・高次の変形という階層構造が入る。これが、開集合系や距離関数とは種類の違う「点の間の構造」にあたる。
この階層構造は、位相空間論 の言葉と対応させると、次のように整理できます。
位相空間 X の中の 2 点 a、b を、切れ目のない道でつなぐこと
── 数学的には「連続写像 $γ : [0,1] → X$ で $γ(0) = a$、$γ(1) = b$ を満たすもの」がある状態、これを「$a$ と $b$ が道でつながっている」と表現します
── を、HoTT ではそのまま「$a$ と $b$ が等しい」と扱います。
さらに、$a$ から $b$ に至る２本の道 $p$、$q$ があったとき、$p$ を少しずつ動かして $q$ に重ねられるかどうか(位相空間論では「$p$ と $q$ がホモトピックか」と呼ぶ、道と道の間の変形のこと)を、HoTT では「$p$ と $q$ が等しい」という 1 段高い等しさとして扱います。
この階層は、変形と変形の間の変形、さらにその間の変形、というふうに、無限に続きます。
位相空間 $X$ から、点の細かい位置の情報や、正確な距離、細かい形状といった、伸ばしたり縮めたりで変わってしまう情報を捨てて、「どの点とどの点が道でつながっているか」「その道はどう変形で移り合うか」といった、伸ばしたり縮めたりしても変わらない情報だけを残したもの を、位相空間$X$のホモトピー型（homotopy type） と呼びます。
HoTTの型が持つ経路の階層構造は、この位相空間のホモトピー型と、本質的に同じ情報を持つと考えられています。
どういうことか、順に説明します。
位相空間から、伸縮で消える情報（距離や次元）を捨てて、骨組みだけを取り出したもの
── それがホモトピー型でした。
一方、HoTTの型 が持っているのは、
点と、点を結ぶ経路と、経路と経路をつなぐ変形と・・・
という階層構造 でした。
この２つが、実は同じものを別の言葉で述べたものだ、というのが、ここでの主張です。
片方は位相空間から出発して、余計なものを削って骨組みにたどり着く。
もう片方は、はじめから骨組みだけを持っている
── 出発点は正反対ですが、たどり着く先が一致する、ということです。
この見通しの源流にあるのが、Alexander Grothendieck が 1983年に草稿 "Pursuing Stacks" で述べた、ホモトピー仮説（homotopy hypothesis）です。
どのような主張なのか、確認しておきましょう。
この仮説は、まったく違う２つの分野で作られた対象が、実は同じものである と述べるものです。
片方は、代数の側から組み立てられたものです。
点があり、点と点を結ぶ矢印があり、矢印と矢印を結ぶ矢印がある・・・ と、階層を無限に積み上げた構造です。
これを ∞-亜群（infinity-groupoid）と呼びます。
位相空間のことは何も考えず、演算の規則だけで組み立てた、純粋に代数的な対象です。
もう片方は、幾何の側から取り出されたものです。
位相空間から、伸縮で消える情報をすべて捨て、残った骨組みだけを見たもの。
これが ホモトピー型（homotopy type）でした。
両者は、出発点も、扱う道具も、まったく違います。
にもかかわらず、Grothendieck は次のように予想しました。
∞-亜群の全体と、ホモトピー型の全体は、本質的に同じものである。
代数の言葉で書いたものと、幾何から取り出したものが、過不足なく対応する
── そう述べたのです。
これが正しければ、空間を調べることと、代数的な階層構造を調べることが、同じ作業になります。
そしてHoTT の型 は、まさにこの ∞-亜群の構造を持っています。
だからこそ、HoTT が位相空間のホモトピー型と同じ情報を扱えると考えられるわけ です。
ただし、ここには注意が必要です。
ホモトピー仮説は、予想であって、証明された定理ではありません。
また、Grothendieck が語ったのは ∞-亜群についてであって、HoTT についてではありません。
1983年の時点で、HoTT はまだ存在していないからです。
HoTT の型と位相空間の対応を実際に裏づけているのは、Vladimir Voevodsky による単体的集合を使ったモデルの構成（2009年） 以降の研究です。
ホモトピー仮説は、この対応が成り立つはずだ、という見通しの源流にある発想として位置づけるのが正確です。
（この点については、記事末尾の補遺でも改めて整理しています）
たとえば、１点（自明な空間 ${*}$）と、円盤 $D^2$ と、実数直線 $ℝ$ と、平面 $ℝ^2$ は、位相空間として互いに同相ではありません（次元がそれぞれ違います）が、いずれも１点に連続変形で潰せるため、ホモトピー型としては同じもの（１点のホモトピー型、可縮な空間のホモトピー型）と扱います。
同じように、円周 $S^1$ と、円柱の側面($S^1 × [0, 1]$)と、平面から原点を除いたもの $ℝ^2$ \ {0} は、位相空間として互いに同相ではありませんが、いずれも円周に連続変形で潰せるため、ホモトピー型としては同じもの（円周のホモトピー型） と扱います。
つまり、HoTTの型は、位相空間そのものではなく、位相空間からこの骨組み（=ホモトピー型）だけを取り出した対象として、数学における空間の一種を実現している のです。
「同じ」の粗さを変えると、次元は残らない
ここで、位相空間論の標準的な「同じ」と、HoTT が採用する「同じ」の違いを整理しておきます。両者の違いは、次元という情報を保つかどうかに、はっきり現れます。
同相 ── 細かい見方
位相空間論で「２つの空間が同じ」という場合、まず思い浮かぶのは 同相（homeomorphic） です。
これは、２つの空間の間に、連続な全単射があり、その逆写像も連続であること、と定義されます。
点と点が１対１に対応し、近さの構造（開集合系）も完全に対応します。
同相はきわめて細かい見方で、点の個数も、開集合の構造も、そして次元も、すべて保たれます。
次元は同相不変量なので、円盤 $D^2$ と実数直線 $ℝ$ が同相になることはありません。
そして、１点空間そのものを除けば、どんな空間も同相写像で 1 点に潰すことはできません。
全単射である以上、点の個数が変わらないから です。
ホモトピー同値 ── 粗い見方
一方、ホモトピー同値（homotopy equivalent） は、これよりずっと緩い関係 です。
要求されるのは「連続変形で互いに移り合えること」だけで、全単射である必要がありません。
たとえば、円盤 $D^2$ を中心の１点に潰す写像を考えると、これは 無数の点を１点に送るので、まったく単射ではありません。しかしホモトピー同値の意味では、これで構わない のです。
その結果、次元は保たれません。
円盤 $D^2$ も、実数直線 $ℝ$ も、平面 $ℝ^2$ も、いずれも１点に連続変形で潰せるので、すべて１点とホモトピー同値になります。次元が 0、1、2 とばらばらであるにもかかわらず、です。
２つの見方の落差
つまり、同じ４つの空間 ${*}$、$D^2$、$ℝ$、$ℝ^2$ を前にして、
-
同相という細かい見方では、これらは全部別物です（次元がそれぞれ違う）
-
ホモトピー同値という粗い見方では、これらは全部同じです（どれも1点に潰れる）
という落差が生じます。
ホモトピー型（homotopy type） とは、この後者の粗い見方で残る情報のことです。伸ばしたり縮めたりすれば消えてしまう情報（正確な距離、細かい形状、そして次元）をすべて捨て、それでも消えない「骨組み」だけを取り出したもの、と言い換えられます。
位相幾何学・ホモトピー論・HoTT の違い
ここまで読まれて、次のような疑問を持たれた方がいるかもしれません。
「位相幾何学と HoTT の違いは、次元の差を乗り越えられるかどうか、ということなのか？」
この問いは、半分は当たっていますが、半分はずれています。
整理しておきましょう。
"次元を保つかどうか？" で見ると
たしかに、$D^2$（２次元の円板）と $ℝ$（１次元の直線）が同じホモトピー型を持つということは、次元の差を乗り越えた同一視 です。
しかし、この乗り越えを行っているのは HoTTには限られません。
| 次元を保つか | |
|---|---|
| 位相空間論の同相 | 保つ |
| 位相幾何学のホモトピー同値 | 保たない |
| HoTT の型 | 保たない |
つまり、次元を捨てるという操作は、HoTT が独自に始めたことではなく、位相幾何学のホモトピー論がすでに持っていた道具なのです。
ホモトピー論は位相幾何学の一分野ですから、「位相幾何学 対 HoTT」という対立軸はそもそも意味を成しません。
ここで、両者の関係を確認しておきましょう。
位相幾何学（topology）は、「切ったり貼ったりせず、連続的に変形して移り合えるものは同じとみなす」という立場に立つ幾何学の総称です。
長さや角度は無視します。
コーヒーカップとドーナツを同じとみなす、あの世界です。
ホモトピー論（homotopy theory）は、その中でも、同一視をさらに一段ゆるめた分野です。
では、何を緩めたのでしょうか？
緩めたものは、同一視に使う写像に対する要求です。
位相幾何学で、何かと何かが「同じ」と言うとき、２つの空間の間には連続な全単射が要求されます。
点と点が１対１に対応し、余った点も、重なった点もあってはなりません。
ホモトピー論では、この全単射という条件を外します。
「連続的に変形して移り合えればよい」とだけ要求し、写像が１対１である必要はありません。
この一点をゆるめた結果として、次元が保たれなくなります。
全単射なら、点の個数が変わらないので、次元も変わりようがありません。
しかし、全単射でなくてよいなら、無数の点を１点に潰す写像も許されます。
だから、円板（２次元）を一点（０次元）に潰してよいことになるのです。
次元を乗り越えられるようになったのは、結果として得られたことです。
ここを取り違えないでください。
「次元が同じかどうか」で、同相とホモトピー同値を区別することはできません。
たとえば $ℝ^2$ と $ℝ^2 \setminus {0}$ は、どちらも２次元ですが、ホモトピー同値ではありません（原点の穴が残るからです）。
逆に、円周 $S^1$（１次元）と $ℝ^2 \setminus {0}$（２次元）は、次元が違うのにホモトピー同値です。
判定の基準は、あくまで連続変形で移り合えるかどうかであって、次元ではない のです。
つまり、位相幾何学という大きな枠の中に、ホモトピー論という、より粗い見方をする分野がある、という関係です。
なぜ、全単射の条件を外したのか ── ２つの分野の成り立ち
「連続な全単射で同じ」という基準を、なぜわざわざゆるめたのでしょうか。
歴史をたどると、その理由がはっきりします。
位相幾何学の成立
位相幾何学の出発点は、1895年に Henri Poincaré が発表した論文 "Analysis Situs" です。
Poincaré が取り組んでいたのは、天体力学の三体問題でした。
惑星の運動を微分方程式で解こうとしたとき、厳密な解の公式は得られないという壁に突き当たります。
そこで彼は、発想を切り替えました。
解を数値として求めるのではなく、解が描く軌道の「形」を調べるという方向です。
軌道が閉じるのか、どこかに巻きつくのか、いくつの穴のまわりを回るのか。
このとき必要になったのが、長さや座標に依存しない、形の分類でした。
これが、位相幾何学の出発点です。
Poincaré はこの論文で、基本群（fundamental group）を導入しています。
空間の中のループを分類する道具で、まさにこの記事で扱ってきた**「経路」の話**です。
ホモトピー論の成立
ところが、当のPoincaré自身がすぐに問題に気づきます。
同相かどうかを判定するのは、極めて難しいのです。
２つの空間が同相であることを示すには、実際に連続な全単射を構成せねばなりません。
同相でないことを示すには、あらゆる全単射が存在しないことを示さねばならない。
どちらも困難です。
そこで、基本群のような不変量（同相な空間なら必ず一致する量）を計算して、間接的に判定する方法が取られました。
ここで、決定的な観察が生まれます。
基本群は、同相よりずっと弱い条件でも保たれるのです。
円板を一点に潰しても、基本群は変わりません（どちらも自明群）。全単射でない写像を使っているのに、不変量は生き残る。
つまり、同相という強い条件は、形を調べるうえで必要以上に厳しかったのです。
この認識から、「連続変形で移り合えればよい」というゆるい同一視 ── ホモトピー同値 ── が定式化されていきます。
1935年、Witold Hurewicz が高次ホモトピー群 $π_n$ を導入したことで、ホモトピー論は独立した分野として確立しました。
表で整理すると
| 位相幾何学 | ホモトピー論 | |
|---|---|---|
| 成立の年 | 1895年（Poincaré "Analysis Situs"） | 1935年前後（Hurewicz の高次ホモトピー群） |
| きっかけ | 三体問題の軌道を、解の公式なしに調べたい | 同相の判定が難しすぎた |
| 当初の目的 | 長さや座標に依存しない、形の分類 | 計算できる不変量で、形を捉える |
| 同一視の基準 | 連続な全単射（同相） | 連続変形で移り合う（ホモトピー同値） |
| 次元 | 保つ | 保たない |
| 代償として捨てたもの | 長さ・角度・座標 | さらに、次元と、詰まった中身 |
一貫している動機
２つの分野を並べると、同じ動機が二段階で働いていることが分かります。
扱いにくい情報を捨てて、扱える情報だけを残す。
位相幾何学は、長さと角度を捨てました。ホモトピー論は、さらに次元を捨てました。
そのたびに、区別できるものは減ります。しかし、残った情報は計算しやすくなり、より多くの空間を統一的に扱えるようになる。
HoTT が「はじめから骨組みだけを持つ」という設計を選んだのも、この流れの延長線上にあります。捨てられる情報は、最初から持ち込まない ── そういう判断です。
ホモトピー論とHoTTは何が違うのか
違いは、次元ではありません。
扱い方の順序です。
ホモトピー論は、まず位相空間を先に用意します。
そのうえで 開集合系を決め、連続写像を定義し、その特別な場合として「経路」を定義し、さらに経路どうしの変形として「ホモトピー」を定義していきます。
$位相空間 → 開集合系 → 連続写像 → 経路 → ホモトピー$
HoTT は、この出発点を持ちません。
位相空間を用意せず、開集合系も経由しません。
「経路」（道）を、はじめから型に備わった構造として持っていいるからです。
$型 → 経路（恒等型）$
が最初からある
HoTT は、そもそも位相空間という出発点を持たない
── ここが決定的な違いです。
では、なぜHoTTは考案されたのか？
位相幾何学とホモトピー論には、それぞれ明確な動機がありました。
HoTTが考案（発見）されるにいたった背景にも、動機と目的がありました。
きっかとなったのは、証明の検証
Vladimir Voevodsky は、代数幾何学の研究で 2002年に Fields 賞を受賞した数学者です。
その彼が、深刻な問題に直面しました。
自分の発表した論文に、長年気づかれなかった誤りが見つかったのです。
1990年に発表した論文に含まれていた主張が、2013年に反例を示されて否定されてしまったのです。
さらに困難は重なります。
Michael Kapranov との共著論文（1991年）で示したはずの結果も、誤りだと判明しました。
皮肉なことに、その論文が扱っていたのは、まさに Grothendieck のホモトピー仮説に関わる内容でした。
現代数学は、人間が査読で正しさを保証できる限界を超えつつある
── Voevodsky はそう考え、コンピュータによる証明検証 へと向かいます。
集合論では、なぜ足りなかったのか
ところが、既存の証明支援系を使ってみると、大きな障害にぶつかりました。
「同型な構造は同じものとして扱う」という数学者にとって当たり前の操作が、機械の上では自明ではなかったのです。
集合論 を土台にすると、同型な２つの群は「同型ではあるが、等しくはない」という扱いになります。
ですから、片方で証明した定理を他方に移すたびに、移し替えの作業を明示的に書かねばなりません。
この手間が、大規模な形式化を現実的でないものにしていました。
そこで、「等しさ」の定義を設計しなおす
Voevodsky が選んだのは、等しさの概念そのものを設計し直すという道でした。
この再設計を目指す作業を行うに際して、すでに準備が整えられていました。
1990年代、Martin Hofmann と Thomas Streicher が、型理論の恒等型を亜群として解釈できることを示していました。
__「等しさの証拠が複数ありうる」ことが、型理論の規則と矛盾しないと分かった** のです。
2006年から2009年にかけて、Steve Awodey と Michael Warren が、この解釈をホモトピー論の言葉へと拡張します。
型が空間として、恒等型が経路の空間として振る舞うことが、モデルによって裏づけられました。
そして 2009年、Voevodsky が単体的集合を使ったモデルを構成し、Univalence Axiom を提唱します。
単体的集合（simplicial set）とは、点・線分・三角形・四面体・・・を貼り合わせて空間を組み立てる、組合せ的な仕組みです。
粘土をこねる代わりに、レゴブロックで形を作るようなものというイメージでしょうか。
連続的な図形を、有限個の部品の貼り合わせとして扱えうことができるため、コンピュータで扱いやすいという利点があります。
ここでようやく、「同型なら等しい」を、公理として書き下されるようになりました。
その結果、数学者が暗黙に行っていた操作が、機械が適用できる規則になったのです。
表で整理すると
| 位相幾何学 | ホモトピー論 | HoTT | |
|---|---|---|---|
| 成立の年 | 1895年 | 1935年前後 | 2009-2013年 |
| きっかけ | 三体問題の軌道を、解の公式なしに調べたい | 同相の判定が難しすぎた | 自分の論文の誤りが、長年見過ごされた |
| 当初の目的 | 長さや座標に依存しない、形の分類 | 計算できる不変量で、形を捉える | 数学の証明を、機械に検証させたい |
| したこと | 長さと角度を捨てた | さらに全単射の条件を外した | 等しさを、経路として作り直した |
動機の違いに注目してください
位相幾何学とホモトピー論は、幾何学の内部から生まれました。
形をどう捉えるか、という問い への答えです。
しかし、HoTTは異なります。
出発点は、数学の営みそのものへの疑問でした。
私たちが正しいと信じている証明は、本当に正しいのか。
それを機械に確かめさせるには、何が足りないのか。
その答えを探した結果、幾何学の道具立てに行き着いた
── これが HoTT の成り立ちです。
HoTTは当初から、機械が扱える形の骨組みだけを持つよう設計されているのです。
まとめ
３者の関係を、あらためて整理します。
| 出発点 | 次元 | 経路の位置づけ | |
|---|---|---|---|
| 位相空間論（同相で見る） | 位相空間 | 保つ | 開集合系から定義する |
| ホモトピー論（ホモトピー同値で見る） | 位相空間 | 保たない | 開集合系から定義する |
| HoTT | 型 | 保たない | 型に最初から備わっている |
位相空間論とホモトピー論の違いは、「同じ」の粗さにあります。
ホモトピー論と HoTT の違いは、経路（道）が、どの段階で現れるかにあります。
ホモトピー論では、経路は後から定義されるものでした。
まず位相空間があり、開集合系があり、連続写像が定義され、その特別な場合として経路が現れます。
HoTT* \では、経路は最初からそこにあるものです。
型を用意した時点で、点と点を結ぶ経路が、型の構造としてすでに備わっています。
つまり、ここまで見てきた３者の関係は、性質の違う２つの区別が重なったものです。
- 位相空間論とホモトピー論： 同じ位相空間を扱いながら、「同じ」とみなす基準の粗さが違う
- ホモトピー論と HoTT ： 同じ粗さで見ながら、経路が後から定義されるか、最初から備わっているかが違う
前者は同一視の基準の話、後者は経路が現れる段階の話です。
この２つを混同してしまうと、「HoTT は位相幾何学と違って次元を無視する理論だ」という誤った理解に陥ってしまいます。
しかし、次元を無視するのはホモトピー論も同じ です。
HoTTの独自性は、位相空間を経由せず、経路を最初から持っているという点の方なのです。
潰れ方が止まる場所が、骨組みを決める
HoTTでは、何が骨組みとして残るのでしょうか。
円周 $S^1$ を考えてみてください。
円周は１点まで潰せません。
真ん中に穴が空いているため、輪をどう縮めても、穴を通り抜けることはできず、輪のまま止まってしまいます。
円柱の側面 $S^1 × [0, 1]$ も、平面から原点を除いたもの $ℝ^2 \setminus {0}$ も、同じ理由で1点までは潰れません。
いずれも同じ１つの穴を持ち、潰していくと同じ「円周」の形で止まります。
だからこれら３つは、位相空間として互いに同相ではないにもかかわらず、**同じホモトピー型（円周のホモトピー型）**を持つことになります。
どこまで潰れるか、どこで止まるか
ホモトピー型が捉えているのは、この情報です。
HoTTの型が実現しているもの
冒頭で述べたとおり、HoTTの型が持つ経路の階層構造は、このホモトピー型と本質的に同じ情報を持ちます（Grothendieck のホモトピー仮説）。
HoTTの型は、位相空間そのものではありません。
位相空間から骨組みだけを取り出した対象として、数学における空間の一種を実現しているのです。
言い換えれば、HoTT は最初から粗い見方の側に立っている理論です。
次元や距離といった、伸縮で消える情報を、そもそも持ち込まない。
その代わりに、「どの点とどの点が経路でつながるか」「その経路どうしは変形で移り合うか」という、伸縮しても消えない情報だけを、型の構造として直接扱います。
*HoTT の型は位相空間そのものではなく、そこから骨組みだけを取り出した対象である。
次元や距離といった伸縮で消える情報を持ち込まず、経路のつながり方と変形の可能性だけを型の構造として直接扱う。*
そして、こうやって「型」を空間として捉え直したとき、HoTTの中心的な発見が浮かび上がります。
それは、「$a$ と $b$ が等しい」ということの意味に、レベルの異なる複数の"等しさ"があるということです。
具体的には、「$a$ と $b$ が等しい」という主張は、HoTT では「$a$ から $b$ への経路が存在する」ことに対応します。
そして、経路は１本だけとは限らず、複数存在しうる のです。
しかも、それら複数見つかった経路は、連続変形によって互いに移り合わない かもしれません。
これ が、同じレベルの階層における「等しさ」の概念です。
さらに、２つの経路 $p$、$q$ が、互いに連続変形することで移り合えるとき、その連続変形の道筋自体が、１段上の「等しさ」の証拠になります。
この意味で、「経路 $p$ と経路 $q$ が等しい」という１段上の等しさが認識できます。
この階層は、無限に続きます。
*「$a$ と $b$ が等しい」ことを、$a$ から $b$ への経路として捉える。
経路は複数ありうるが、間に穴があると互いに変形で移り合わない（1段目）。
移り合う場合は、その変形 $H$ 自体が1段上の等しさになる（2段目）。
この階層は無限に続く。*
20世紀の数学（集合論の上で組み立てられた大部分の数学）は、「等しい」を真か偽の２択で扱ってきました。
しかし、実際の数学の営みでは、「集合として要素が同じ」「同型として同じ」「振る舞いとして同じ」「経路の集まりとして同じ」といった複数のレベルの等しさが、暗黙のうちに使い分けられていました。
（この４つが、HoTT の言葉ではそれぞれ何段目の話になるのかは、Univalence を紹介したあとの補足でまとめて整理します）
「振る舞いとして同じ」というのは、内部の実装や具体的な中身が違っていても、外側から見て同じ結果を返す状態を指します。
たとえば、階乗を計算する関数を、for ループで書いた実装と、再帰で書いた実装は、内部のコードは違いますが、同じ入力に対して同じ出力を返すので、「振る舞いとしては等しい」と言えます。
プログラマがコードをリファクタリング（内部実装の書き換え）したときに、「振る舞いが変わっていないか」を気にするのは、まさにこの意味の等しさです。
ここで、ひとつ確認しておきましょう。
for ループ版の $f$ と再帰版の $g$ は、そもそも何の要素なのでしょうか。
関数もまた、ある型の要素です
$f$ も $g$ も、自然数を受け取って自然数を返す関数です。
型で書けば、どちらも $ℕ → ℕ$ という型に属しています。
$3$ が $ℕ$ の要素であるのと同じように、$f$ は $ℕ → ℕ$ の要素なのです。
そして、記事の前半で述べたとおり、HoTTでは型を空間として眺めます。
この意味で、$ℕ → ℕ$ もまた、ひとつの空間です。
そこに住んでいる点のひとつひとつが、自然数から自然数への関数、ということになります。
「関数を並べた空間」 を思い浮かべてください。
階乗を計算する関数も、２倍する関数も、常に $0$ を返す関数も、すべてこの空間の点です。
fとgは、別の点です
さて、この空間の中で、$f$ と $g$ は同じ点でしょうか。
異なる点です。
実装が異なるのですから、これは当然のことです。
コンパイラから見れば、片方は繰り返しの命令列、もう片方は自分を呼び出す命令列。
まったく別のものです。
しかし、２点は経路で結ばれます
しかし、この２点の間には経路があります。
$f(0) = g(0)$、
$f(1) = g(1)$、
$f(2) = g(2)$、
・・・
と、すべての入力について値が一致するからです。
各点での一致を集めて、関数の空間における１本の経路へと束ね上げる
── これが、後で紹介する関数外延性の役割です。
別の点でありながら、経路で結ばれている。
これが、リファクタリングで守られている「等しさ」の正体です。
（なお、この場合の経路は１本しかありません。複数の等しさが生じるのは、また別の場合です。詳しくは後の補足で扱います）
HoTT は、この「暗黙のレベル」を明示的な型として書き下し、機械が扱える形に整えました。
「機械が扱える形に整えた」というのは、数学者が「同型なら同じ」「振る舞いが同じなら同じ」といった思考習慣を頭の中の暗黙の約束事として思い描くだけではなく、コンピュータのプログラム（定理証明支援系） がその慣習を正しく認識し、証明の中で自動的に適用できる形式的なルール（公理）として、明文化した、ということです。
これによって、数学者の暗黙の思考慣習を、コンピュータが１ステップずつ厳密にチェックする機械証明の対象にできるようになりました。
HoTT が「レベルの異なる複数の等しさを分けて議論できる視座」を提示してくれたことで、こうしたことが実現したのです。
「同型なら同じ」「振る舞いが同じなら同じ」は、経路の言葉でどう表されるのか
ここまで、HoTT では「$a$ と $b$ が等しい」ことを「$a$ から $b$ への経路が存在すること」として扱う、と述べてきました。
では、数学者やプログラマが日常的に使っている「同型なら同じ」「振る舞いが同じなら同じ」という２つの思考慣習は、この経路の枠組みの中でどう位置づけられるのでしょうか。
問題は、「経路がある」と言い切れないこと
まず、素朴に考えたときの困難を確認します。
たとえば、整数の加法群 $(ℤ, +)$ と、偶数全体の加法群 $(2ℤ, +)$ を考えます。
この２つは群として同型です（$n \mapsto 2n$ が同型写像）。
数学者は、これらを「同じ群」として扱います。
しかし、HoTT の枠組みで「$(ℤ, +)$ と $(2ℤ, +)$ が等しい」と主張するには、群の型 $\mathrm{Group}$ という空間の中で、この２点を結ぶ経路が存在することを示さねばなりません。
ところが、手元にあるのは同型写像 $n \mapsto 2n$ という「写像」であって、「経路」ではありません。
写像と経路は別物です。
同型写像があるからといって、経路があることが自動的に従うわけではないのです。
同じ問題が、関数 についても起こります。
階乗を for ループで書いた実装 $f$ と、再帰で書いた実装 $g$ があるとき、手元にあるのは「すべての入力 $n$ について $f(n) = g(n)$ である」という事実です。
これは各入力ごとの等しさ、つまり出力の空間の中の経路たちです。
しかし主張したいのは「関数の空間の中で $f$ と $g$ を結ぶ経路がある」という、一段違うことです。
Univalence Axiom ── 同型に経路を与える
この隔たりを埋めるのが、Voevodskyが2010年に提唱した Univalence Axiom です。
この公理が述べているのは、おおまかに言えば次のようなことです。
型 $A$ と型 $B$ の間に同値（対応がついていること）があるなら、それに対応する経路が $A$ から $B$ へ存在する
つまり Univalence は、「同型であること」を経路に翻訳するのではありません。
「同型があるのならば、経路があることにする」と宣言するのです。
公理とは、そういうもの です。
これによって、$(ℤ, +)$ から $(2ℤ, +)$ への同型写像は、$\mathrm{Group}$ という空間の中の１本の経路を与えます。
数学者が暗黙に行っていた同一視が、経路の存在という形で、型の中に書き下された ことになります。
関数外延性 ── 振る舞いの一致に経路を与える
関数の側を担うのが 関数外延性（function extensionality） です。
こちらは、
すべての入力 $n$ について $f(n)$ と $g(n)$ を結ぶ経路があるなら、$f$ と $g$ を結ぶ経路が存在する
と述べます。
forループ版と再帰版の階乗関数は、各入力ごとに同じ値を返します。
関数外延性は、この 「各点での経路の集まり」を、関数の空間における「１本の経路」へと束ね上げます。
リファクタリング前後のコードが「同じ」だと言えるのは、この意味において です。
内部実装は別物でも、関数という空間の中では、両者は１本の経路で結ばれた同じ点として扱うことができるのです。
２つの慣習が、同じ形に収まる
こうして整理すると、２つの慣習は同じ構図を持っていることが分かります。
| 慣習 | 手元にあるもの | 与えられる経路 | 根拠 |
|---|---|---|---|
| 同型なら同じ | $A$ と $B$ の間の同値 | $\mathrm{Type}$ の中の $A \rightsquigarrow B$ | Univalence Axiom |
| 振る舞いが同じなら同じ | 各点での経路の集まり | 関数の空間の中の $f \rightsquigarrow g$ | 関数外延性 |
どちらも、「別の形で与えられた同一視の証拠」を「経路の存在」へと引き上げる規則 です。
そして重要なのは、これらが規則として明文化されているという点です。
数学者の頭の中の約束事であれば、証明のどこでそれを使ったかは記録されません。
しかし、公理として 書き下されていれば、証明支援系はその適用を１ステップとして認識し、検証できるのです。
これが、「機械が扱える形に整えた」ということの中身 です。
図中の証明スクリプトについて、２点補足しておきます。
１.
introとassumeの混在についてRocq（旧 Coq）には
introはありますが、assumeはありません。Lean にはintroがあり、assumeは古い記法として存在しました。つまりこのスクリプトは、実在の言語をそのまま模したものではなく、擬似コードとして書かれています。
図中でも
.による区切りがなく行番号だけになっているとおり、特定の言語のコードというより「証明スクリプトのイメージ」として提示したものです。２.
QEDについてRocq では
Qed.は証明の終端を宣言するコマンドであり、introやapplyといったタクティクの列とは区別されます。図では５行目として並べていますが、厳密には性質の違う行です。
いずれも、この図の主眼である「各行が記録され、１ステップずつ検証される」という点には影響しません。実際に動くコードをご覧になりたい方は、記事の続編で Cubical Agda の実例を扱う予定です。
「どの同型を使ったか」が経路として残る
もう１点、経路として扱うことの帰結を補足しておきます。
$(ℤ, +)$ と $(2ℤ, +)$ の間には、$n \mapsto 2n$ という同型のほかに、$n \mapsto -2n$ という別の同型もあります。
Univalence のもと では、この２つはそれぞれ別の経路を与えます。
つまり「$(ℤ, +)$ と $(2ℤ, +)$ は等しい」という主張には、少なくとも２通りの異なる証拠があることになります。
これはまさに、前節で見た 「同じ階層の中に複数の等しさが存在する」状況 です。
集合論の枠組みで「同型だから同じ」と言ってしまうと、どの 同型を使ったかという情報は消えます。HoTTでは、それが経路として残ります。
この違いが、後に紹介する応用の場面で効いてきます。
補足：４つの「等しさ」は、HoTT の言葉では何段目にあたるのか
この節は、HoTT の指標である h-level を使って、記事の前半で挙げた４つの「等しさ」を整理し直すものです。
やや細かい話になりますので、先を急ぐ方は読み飛ばしていただいて差し支えありません。
「いま自分が扱おうとしている型の h-level が分かれば、その型の値（つまり、その型の要素）どうしの等しさがどの段で論じられるか分かる」
── ここだけ持ち帰っていただければ十分です。なお、ここで言う「値どうしの等しさ」と、「型どうしの等しさ」は、別の話です。
たとえば群の型 $Group$ を考えると、
値どうしの等しさ ── $(ℤ, +) = (2ℤ, +)$。個々の群を比べる話で、この節の主題です
型どうしの等しさ ── $Group = Ring$。群の型と、環の型そのものを比べる話で、宇宙（型を値として持つ、特別な型）の中の議論になります
この節で扱うのは、前者だけです。
後者は、階層がもうひとつ上に乗った話になります。
この節では、次の順に整理します。
- h-level の定義と、番号が下がる理由
- ４つの「等しさ」の整理
- プログラミングのデータ型の h-level
- 数学の概念の h-level
- 複数の等しさが生じる型と、その意義
必要な箇所だけ拾い読みしていただいて構いません。
この記事の前半で、実際の数学の営みでは、複数のレベルの等しさが暗黙に使い分けられてきた、と述べました。
-
「集合として要素が同じ」
-
「同型として同じ」
-
「振る舞いとして同じ」
-
「経路の集まりとして同じ」
の４つです。
これらはHoTTの言葉では、それぞれ何段目の話に該当するのでしょうか？
この記事のサムネイルの図で紹介した h-level という指標を使うと、この問いに答えることができます。
ただし、その前前に、ひとつ確認しておかねばならないことがあります。
h-level は、「等しさ」ではなく「型」に付く番号です
これは間違えやすいところです。
h-level は、「この等しさは何段目か」を測る番号ではありません。
「この型は、どこまで豊かな等しさを持っているか」を測る番号です。
定義は、次のようになっています。
型 $A$ の h-level が $n+1$ であるとは、$A$ の任意の２つの要素 $a$、$b$ について、恒等型 $a =_A b$ の h-level が $n$ であること。
より厳密な定義は、nLab の項目をご参照ください。
なお、文献によっては、h-level と番号が２つずれる $n$-type という記法も使われます。リンク先で数字を読むときは、ご注意ください。
出発点は、h-level $0$ です。
これは可縮空間、つまり本質的に１点だけからなる型を指します。
この定義から、ひとつ大事な結論が導き出されます。
型の h-level が $N$ なら、その要素どうしの等式の h-level は $N - 1$ です。
つまり、等しさを問うと、番号はひとつ下がるのです。
番号は下がるのであって、上がるのではありません。
ここは直感に反するかもしれませんので、理由を述べておきます。
型 $A$ 全体を考えるときは、どの要素についても自由に議論することができます。
しかし、 $a =_A b$ を考えるときには、すでに両端の点が $a$ と $b$ に固定されています。
自由に動ける余地が減っている分だけ、構造が単純になる ── だから番号が下がるのです。
したがって、「この等しさは何段目か」と問うときは、「その等式が住んでいる型は、h-level いくつか」 に読み替えて考えることになります。
１. 「集合として要素が同じ」── 舞台は h-level 2、等式は h-level 1
たとえば、自然数の型 $ℕ$ の中で、$2 + 2 = 4$ を考えます。
$N$ は 集合（set）であり、h-level は 2 です。
なぜ 2 になるのか、定義に戻って確かめておきましょう。
h-level は、下から順に決まっていきます。
h-level $0$ ── 可縮
本質的に１点だけからなる型です。
「要素がちょうどひとつあり、しかもすべての要素がその一点に等しい」ことが要求されます。
要素がひとつだけの型（ユニット型）が、これにあたります。
h-level 1 ── 命題
h-level $0$ が何であるかは決まりました。
この h-level $0$ を使って、h-level $1$ が何であるかを決めます。
型 $A$ が h-level $1$ であるとは、$A$ のどの２つの要素 $a$、$b$ をとっても、恒等型 $a =_A b$ が h-level $0$（可縮）になるということです。
これが何を意味するか、順に読み解いてみましょう。
$a =_A b$ が可縮である、というのは、「$a$ から $b$ への道が、ちょうど１本だけ存在する」 ということでした。
ここで大事なのは、これが $A$ のどの２要素についても成り立たねばならない、という点です。
$a$ と $b$ を、どう選んでも、です。
$a$ と $b$ を別々の要素として選んだ場合を考えてみてください。
その場合も、$a$ から $b$ への道が存在せねばなりません。
つまり、$A$ の中のどの２要素も、必ず等しいということになります。
「どの２要素も必ず等しい」型とは、どんな型でしょうか。
要素が２つ以上あるように見えても、それらが全部等しいのですから、実質的には要素は１種類しかないことになります。
したがって、h-level 1 の型は、次のどちらかです。
- 要素がひとつもない型（空の型）── 「どの２要素も」と言われても、２要素が取れないので、条件は自動的に満たされます
- 要素が本質的にひとつだけの型
この２つをまとめて、「要素が高々ひとつしかない型」 と言います。
命題（mere proposition）と呼ぶのは、これが「真か偽か」の２択に対応するからです。
要素があれば真、なければ偽。
そして、真である場合、その証拠は本質的にひとつしかない
── ふだん私たちが「命題」と言うときの感覚と、ぴたりと重なります。
h-level 2 ── 集合
同じやり方で、今度は h-level 1 を使って、h-level 2 が何であるかを決めます。
型 $A$ が h-level 2 であるとは、**任意の２要素 $a$、$b$ について、恒等型 $a =_A b$ が h-level 1（命題）であること です。
$a =_A b$ が命題であるとは、どういうことでしょうか。
命題とは、要素が高々ひとつしかない型でした。
つまり、「$a$ と $b$ が等しいことの証拠は、あっても１本だけ」 ということです。
これを $N$ で確かめてみます。
$2 + 2 = 4$ の証拠は、何通りあるでしょうか。
$2 + 2$ を計算すれば 4 になる ── それだけです。
「別の経路をたどって 4 になった」という区別すべき第２の証拠は存在しません。
その一方で、$2 + 2 = 5$ の証拠は、１本もありません。
つまり $N$ では、どの２つの要素をとっても、その等式の証拠は ０本か１本。これはまさに、恒等型が命題であるということです。
したがって $N$ は h-level $2$、すなわち集合になります。
なぜ「集合」と呼ぶのか
この名前は、私たちがふだん使っている集合の性質を、そのまま言い当てているからです。
集合論では、「$2 + 2$ と $4$ は等しい」と言ったとき、どう等しいかは問いません。
等しいか等しくないか、それだけです。
h-level $2$ の型*は、まさにこの性質を持っています。
だから HoTT では、h-level $2$ の 型 のことを 集合（set）、あるいは $h$-集合（h-set）と呼ぶのです。
逆に言えば、私たちが慣れ親しんできた集合論**は、HoTT の階層の中では、下から３段目にあたる特別な場合だったということになります。
したがって、$2 + 2 =N 4$ という等式そのものは、h-level $1$ になります。これが、命題（mere proposition）です。
命題とは、要素が高々ひとつしかない型 のことでした。
これが何を意味するかというと、「$2 + 2 = 4$ の証拠は、本質的にひとつしかない」 ということです。
証明の書き方は何通りもあるでしょう。
しかし、どの証明を持ってきても、それらは互いに等しいものとみなされます。 証拠の違いが、意味のある違いを生まない。
これが、20 世紀の数学が扱ってきた「真か偽かの２択」の等しさの正体です。
HoTTの言葉 で言えば、h-level 1 の等しさにあたります。
$Z$、bool、String ・・・皆様が日常的に扱うデータ型の多くが、この h-level $2$ の集合であり、その要素どうしの等しさは h-level $1$ に落ちます。
２. 「同型として同じ」── 舞台は h-level 3、等式は h-level 2
次に、群の型 $Group$ の中で、$(Z, +)$ と $(2Z, +)$ を比べます。
$Group$ は 亜群（groupoid）であり、h-level は ３ です。
なぜ 3 になるのか、確かめておきましょう。
定義に従えば、h-level $3$ とは、「どの２つの要素の間に成立する等式も、h-level $2$（集合）になる」ことでした。
そこで、群 $G$ と $H$ が等しいことの証拠を数えます。
Univalence のもとでは、その証拠は $G$ から $H$ への群同型そのものです。同型がひとつ見つかれば、それが等しさの経路を１本与えます。
では、群同型を全部集めたものは、どんな型でしょうか。
同型写像は、台集合の間の写像です。
２つの同型写像が等しいかどうかは、「すべての元で同じ値を返すか」で決まり、その答えは真か偽の２択です。証拠が複数あることはありません。
つまり、群同型の全体は集合（h-level 2） です。
したがって、$Group$ の h-level は $2 + 1 = 3$ になります。
なぜ「亜群」と呼ぶのか
h-level $3$ の型には、点（群）と、点を結ぶ道（同型）があります。
道が複数あれば、それらは互いに区別されます。
$(ℤ, +) = (ℤ, +)$ の証拠が、恒等写像と符号反転の２つに分かれたのが、その例でした。
では、そこからもう一段上がって、「２本の道が等しいか」を問うとどうなるでしょうか。
ここで話が終わります。
２つの群同型が等しいかどうかは、真か偽かで決まってしまい、その答えの証拠が何通りあるか、という問いは立ちません。
つまり、点と道までは豊かだが、その先には何もない
── この形の構造を、亜群と呼びます。
「点と、点を結ぶ可逆な矢印」だけで、構造が尽きているのです。
「点と、可逆な矢印」だけで構造が尽きている
── これが亜群の姿です。だから h-level 3 の型を、亜群 と呼びます。
したがって、$(ℤ, +) =_{Group} (2ℤ, +)$ という等式は、h-level $2$
── 集合です。
命題ではなく集合になった、というのが重要な変化です。
命題なら、証拠は本質的にひとつでした。
しかし集合であれば、要素が複数あってよい のです。
実際、$(ℤ, +)$ から $(2ℤ, +)$ への同型写像は、$n \mapsto 2n$ のほかに $n \mapsto -2n$ もありました。
Univalence のもとでは、この２つはそれぞれ別の経路を与えます。
つまり「$(ℤ, +)$ と $(2ℤ, +)$ は等しい」という主張の証拠が、２つある。
より一般に、群 $G$ と $H$ が等しいことの証拠の集まりは、$G$ から $H$ への同型写像全体の集合と一致します。
たとえば $G = H = ℤ$ とすると、$ℤ$ から $ℤ$ への群同型は、恒等写像と符号反転の２つだけです。
したがって、$ℤ =_{Group} ℤ$ という等式の型は、ちょうど２元からなる集合になります。
「$ℤ$ は $ℤ$ に等しい」という、一見あたりまえの主張に、２通りの異なる証拠がある ── これが h-level 2 の等しさの世界です。
数学用語に関する注意喚起 ── 「亜群」には、まったく別の意味がある
ここで「亜群」と呼んでいるのは、圏論の意味での亜群（groupoid）です。
対象（点）と、対象を結ぶ矢印（道）からなり、すべての矢印が可逆である構造を指します。
ところが、日本語の数学用語における**「亜群」**には、これとは別の意味があります。
代数学では、集合と、その上の二項演算ひとつだけからなる構造 ── 結合律も単位元も要求しないもの ── を、かつてgroupoid と呼びました。日本語訳が、同じく「亜群」です。
こちらは現在、Bourbaki（ブルバキ）の用語である マグマ（magma）と呼ばれることが多くなっています。
両者は、まったく無関係な概念です。
| 代数学の亜群（＝マグマ） | 圏論の亜群 | |
|---|---|---|
| 中身 | 集合ひとつと、二項演算ひとつ | 対象と、可逆な矢印 |
| 公理 | 演算が閉じていること、それだけ | 結合律、単位元、逆元 |
| 位置づけ | 群から公理をすべて外したもの | 群を、複数の対象へ広げたもの |
| 別名 | マグマ | グルーポイド |
方向が、正反対です。
代数学の亜群は群より条件がゆるく、圏論の亜群は群より対象が多い。
この記事で扱っているのは、後者だけです。
紛れを避けたい場合は、グルーポイドとカタカナで書く流儀もあります。
３. 「振る舞いとして同じ」── これは「段」ではなく「手段」です
ここで、注意していただきたいことがあります。
「振る舞いとして同じ」ことは、h-level の階段 を一段上がった話ではありません。
記事で挙げた例で確かめてみましょう。
階乗を計算する関数には、for ループで書いた実装 $f$ と、再帰で書いた実装 $g$ の２通り存在します。
この関数の型は $ℕ → ℕ$ です。
$ℕ$ が集合（h-level $2$）ですから、$ℕ → ℕ$ もまた集合であり、h-level は $2$ です。（関数外延性を認めれば、こうなります）
したがって $f =_{ℕ → ℕ} g$ は、h-level $1$
── 命題です。
つまり、１つ目の「集合として要素が同じ」と、まったく同じ段（h-level） に落ちるのです。
では、「振る舞いとして同じ」 こととは、何だったのでしょうか。
これは、段（h-level）の話ではなく、等しさを示すための ”手段の話” です。
-
h-level ── その型が、どれだけ豊かな等しさを持つか（縦の軸）
-
関数外延性 ── 等しさを、どうやって示すか（横の軸）
$f$ と $g$ が等しいことを直接示すのは困難です。
実装が違うのですから。
そこで、各点ごとの等しさ（$f(0) = g(0)$、$f(1) = g(1)$、...）を集めて、関数全体の等しさへと持ち上げる。それが関数外延性の役割でした。
階段を上がっているのではなく、同じ段に到達するための別の登り口を用意している ── そう理解してください。
なお、２つ目の「同型として同じ」にも、同じ構図があります。
「同型なら等しい」を保証する構造同一性原理も、手段の側の話です。
ただしこちらは、舞台となる $Group$ が実際に h-level $3$ であるという、段（h-level）の違いも同時に効いています。
ですから３つ目ほど混同は起きません。
４. 「経路の集まりとして同じ」── 舞台は h-level 3 以上、あるいは有限の段を持たない
最後に、位相空間そのものに近い型を考えます。
円周 $S^1$ を、HoTT の中で型として構成することができます。
$S^1$ の h-level は 3 です。
したがって、基点 $base$ について、$base =_{S^1} base$ という等式は h-level * $2$、つまり集合*になります。
そしてこの集合が何かというと、整数全体 $ℤ$ と一対一に対応します。
これが、記事の後半で紹介する $π_1(S^1) = ℤ$ の内容です。
「基点が基点に等しい」という主張の証拠が、整数の個数だけ、つまり無限にある。何周したかが、そのまま証拠の違いになるわけです。
さらに球面 $S^2$ になると、事情が変わります。
$S^2$ は、どの $n$ についても有限の h-level を持ちません。
$π_2(S^2) = ℤ$、$π_3(S^2) = ℤ$、... と、高次のホモトピー群が無限に非自明であり続けるからです。
階段のどの段にも収まらない ── これが、記事の冒頭で述べた「階層が無限に続く」ということの、具体的な現れです。
４つのまとめ
以上を表にまとめます。
| 記事の表現 | 具体例 | 舞台となる型 | 型の h-level | 等式自体の h-level |
|---|---|---|---|---|
| 集合として要素が同じ | $2 + 2 = 4$ | $ℕ$、$ℤ$、bool
|
2（集合） | 1（命題） |
| 同型として同じ | $(ℤ, +) ≅ (2ℤ, +)$ | $\mathrm{Group}$、$\mathrm{Ring}$ | 3（亜群） | 2（集合） |
| 振る舞いとして同じ | for 版と再帰版の階乗 | $ℕ → ℕ$ | 2（集合） | 1（命題） |
| 経路の集まりとして同じ | $π_1(S^1) = ℤ$ | $S^1$ | 3（亜群） | 2（集合） |
| $π_n(S^2)$ | $S^2$ | 有限の段なし | 有限の段なし |
ここから、実務的な見通し が立ちます。
いま手元で取り扱っている型の h-level が $N$ だと分かれば、その要素どうしの等しさは、h-level $N-1$ の世界で議論される。
bool、$ℕ$、$ℤ$、String といった、プログラマが日常的に扱うデータ型は、いずれも h-level $2$ の集合です。
ですから、値どうしの等しさは h-level $1$ ── 命題であり、証拠の違いを気にする必要はありません。
その一方で、型そのものを要素として扱う世界に入ると、話が変わります。
群、環、位相空間といった数学的構造を「型の要素」として並べたとき、その舞台は h-level $3$ 以上 になります。
等しさは命題ではなく集合になり、どの証拠を使ったかが意味を持ちはじめるのです。
「同型だから同じ」で済ませていた場面で、どの同型を使ったかを記録しておかねばならなくなる
── その境目が、h-level $2$ と $3$ の間にあります。
注意：「１つ上の次元へ」と、h-level は逆向きに動きます
ここで、記事の前半で紹介した図を、もう一度ご覧ください。
ここは混乱しやすいところですので、再掲した上の図を眺めながら、注意点をご説明します。
この図が示しているのは、議論の舞台が上がることです。
h-level が上がることではありません。
むしろ、そこでは h-level は下がっています。
図の中身を、型の言葉で書き直してみましょう。
１段目
舞台は $a =_A b$ という型です。
図の中の経路 $p$ と $q$ は、この型の要素にあたります。
２段目
「$p$ と $q$ が変形で移り合うか」を問うということは、$p =_{(a =_A b)} q$ という新しい型を考えることです。
図の中の変形 $H$ は、この型の要素になります。
つまり、１段目で要素だったもの（$p$、$q$）が、２段目では点として置かれ、それらを結ぶ新しい型が立つ。
これが、「１つ上の次元へ」ということの中身 です。
先ほど紹介した**「経路が点になり、変形が経路になる」の図が、まさにこの構造を描いています。**
その一方で、h-level は、この移動と逆向きに動きます。
型 $A$ の h-level が $N$ だとすると、
- $a =_A b$ の h-level は $N - 1$
- $p =_{(a =_A b)} q$ の h-level は $N - 2$
というふうに、段を上がるほど、型は単純になっていきます。
理由は、先に述べたとおりです。
両端が固定されて、動ける余地が減っていくからです。
なぜ混同が起きやすいのか。
原因は、用語の重なりにあります。
この記事では「１段目」「２段目」という言い方を、恒等型を何回入れ子にしたかという意味で使っています。こちらは、上がっていく方向です。
他方で、h-level は、その型がどこまで豊かな等しさを持つかの指標です。入れ子を深くすると、こちらは減っていきます。
同じ「段」という言葉で、逆向きの２つの量を指していた
── ここが、混線の元になります。
ですから、上の表で h-level を読むときは、図の「１つ上の次元へ」という矢印とは、いったん切り離して考えてください。
舞台は上がる。しかし、その舞台に立つ型は、単純になっていく。
この２つが同時に起きている、というのが正確な理解です。
プログラミングのデータ型は、h-level いくつか
ここまでの話を、皆様が日常的に触れているデータ型で確かめてみましょう。
Int、Str ── h-level 2（集合）
整数型 Int と文字列型 Str は、どちらも h-level 2、つまり集合です。
なぜそう言えるのでしょうか。
ここで、Hedberg の定理（1998 年）という便利な結果が使えます。
型 $A$ について、任意の２要素 $a$、$b$ が「等しいか、等しくないか」を機械的に判定できるならば、$A$ は集合（h-level 2）である。
Int の２つの値が等しいかどうかは、比較すれば必ず分かります。
Str も、一文字ずつ照合すれば判定できます。
したがって、どちらも集合です。
集合であるということは、その要素どうしの等式は h-level 1、つまり命題になります。
3 = 3 の証拠は、本質的にひとつしかない。
「どういう経緯で 3 と 3 が等しいと分かったか」を区別する必要はない、ということです。
プログラマの感覚で言えば、等値比較 == が bool を返せば済む世界が、ここにあたります。
List ── 中身の h-level を、そのまま引き継ぐ
リスト型はどうでしょうか。
結論から言うと、List A の h-level は、要素の型 $A$ の h-level と同じになります。
$A$ が集合（h-level 2）なら、List A も集合です。
直感的には、次のように考えると腑に落ちると思います。
２つのリストが等しいことの証拠とは、「長さが等しい」ことの証拠と、「各位置の要素が等しい」ことの証拠を、束ねたものです。
各要素の等しさが命題（証拠がひとつ）なら、それを束ねたリストの等しさも命題になります。
証拠の選び方に自由度が生まれないから です。
したがって、List Int、List Str、List (List Int)
── いずれも h-level $2$ です。
Set ── ここで用語の罠があります
Set は注意が必要です。
プログラミングの Set と、数学の「集合全体の型」は、h-level が違います。
プログラミングの Set（重複のない要素の集まり、というデータ構造）を考えます。
Set Int は、「$ℤ$ の各要素について、それが入っているかいないか」を指定したものです。
型で書けば $ℤ → Prop$ にあたります。
命題の型 $Prop$ は h-level $2$（集合） であり、関数型の h-level は行き先で決まりますから、Set Int も h-level $2$ です。
一方、数学で言う「集合全体の型」$hSet$
── つまり、個々の集合をひとつの点として並べた型
── は、h-level 3 です。
同じ「Set」という語で、まったく違う段のものを指してしまうので、ここは意識して区別してください。
-
Set Int（$ℤ$ の部分集合ひとつ）── h-level $2$ -
$hSet$（集合という数学的対象を並べた型）── h-level $3$
理由は、後の「数学の概念」の節で説明します。
Func ── 行き先だけで決まります
関数型は、ここで一番おもしろい振る舞いをします。
関数型 $A → B$ の h-level は、行き先 $B$ の h-level だけで決まります。
出発点 $A$ は、まったく関係しません。
驚かれるかもしれませんが、理由は単純です。
関数外延性を思い出してください。
$f = g$ を示すには、各入力 $x$ について $f(x) = g(x)$ を示せばよいのでした。
つまり、$f = g$ の証拠とは、「各点での等しさの証拠」を集めたものです。
各点での等しさは、$B$ の中の等式です。
ですから、$B$ がどれだけ豊かな等しさを持つかが、そのまま $f = g$ の豊かさを決めます。
$A$ は「何点ぶん集めるか」を決めるだけで、豊かさには寄与しません。
具体例で確かめましょう。
引数も返り値もひとつの関数
$$ℕ → ℕ$$
行き先 $ℕ$ は h-level 2 なので、この型も h-level 2。したがって $f = g$ は命題です。
先ほど見た、for ループ版と再帰版の階乗関数の例が、これにあたります。
引数が複数ある関数
$$ℕ → ℕ → ℕ$$
これは、括弧を補うと $ℕ → (ℕ → ℕ)$ です。２引数の関数は、「ひとつ受け取って、残りを待つ関数を返す関数」として表せます（カリー化）。
行き先は $ℕ → ℕ$ で、これは h-level 2。
したがって全体も h-level 2 です。
引数を何個に増やしても、最後にたどり着く行き先が $ℕ$ である限り、h-level 2 のまま です。
引数が関数である高階関数
$$(ℕ → ℕ) → ℕ$$
行き先は $ℕ$ で h-level 2。
したがって、この型も h-level 2 です。
引数が複雑な関数であっても、出発点は h-level に影響しません。
返り値が関数である高階関数
$$ℕ → (ℕ → ℕ)$$
行き先 $ℕ → ℕ$ が h-level 2 なので、全体も h-level 2。
行き先が豊かな場合
では、いつ h-level が上がるのでしょうか。
その答えは、行き先を変えたとき です。
$$ℕ → Group$$
これは「それぞれの自然数に、群をひとつ対応させる」型です。
行き先 $\mathrm{Group}$ は h-level 3 ですから、この関数型も h-level 3 になります。
まとめると、こうです。
関数型の h-level を知りたければ、矢印を右へ右へとたどって、最後に何が来るかだけを見ればよい。
プログラマが日常的に書く関数は、最後に Int や String や bool といった h-level 2 の型に着地します。ですから、実務で扱う関数型は、ほぼすべて h-level 2 です。
数学の概念は、h-levelいくつか
次に、数学で扱う概念を見ていきます。
ここで、区別すべき大事なポイントがあります。
「構造の中の要素」を見ているのか、「構造そのものを並べた型」を見ているのか。両者を区別する視点です。
この違いで、*h-level が変わります。
要素を見るとき ── h-level 2
まず、構造の中の個々の要素 を扱う場合です。
ベクトル
３次元ベクトル $v = (1, 2, 3)$ は、型 $ℝ^3$ の要素です。
$ℝ$ は集合（h-level $2$）であり、その直積も集合ですから、**$ℝ^3$ は h-level $2$ です。
したがって、２つのベクトルが等しいことは命題であり、証拠はひとつ。
成分が全部一致するか、しないか、それだけです。
行列
$m \times n$ 行列の全体 $\mathrm{Mat}(m, n, ℝ)$ は、実質 $ℝ^{mn}$ ですから、h-level $2$ です。
テンソル
テンソルも同様です。
階数を上げても、成分が実数である限り、その全体は h-level $2$ の集合になります。
関数（写像として）
$f : ℝ → ℝ$ のような写像を要素として見る場合、先ほどの規則どおり、**行き先 $ℝ$ が h-level 2 なので h-level $2$ です。
つまり、線形代数や解析学でみなさんが計算している対象は、ほぼすべて h-level $2$ の世界の住人**です。
「等しいか、等しくないか」の２択で足りる。
これが、20 世紀の数学の大部分が動いていた地平です。
構造そのものを並べるとき ── h-level 3
ここから、話が変わります。
集合の型 $hSet$
個々の集合を点として並べた型を考えます。
$hSet$ の中で「集合 $A$ と集合 $B$ が等しい」とは、何でしょうか。
Univalence によれば、$A$ から $B$ への全単射があることです。
しかも、どの全単射を使ったかが、そのまま等しさの証拠になります。
$A = B$ の証拠の集まりは、$A$ から $B$ への全単射全体の集合です。
これは集合（h-level 2）ですから、
$hSet$ の h-level は $2 + 1 = 3$
となります。
具体例を出しましょう。$A = B = {1, 2, 3}$ とします。
「この集合はこの集合に等しい」という主張の証拠は、${1,2,3}$ から ${1,2,3}$ への全単射、つまり ３次対称群 $S_3$ の元、全部で６個あります。
あたりまえに見える等式に、６通りの証拠があるわけです。
群の型 $\mathrm{Group}$
同じ構図です。$G = H$ の証拠は、$G$ から $H$ への群同型全体。これは集合ですから、$\mathrm{Group}$ は h-level 3。
環の型 $\mathrm{Ring}$、体の型 $\mathrm{Field}$
これらも同様に h-level 3 です。
等しさの証拠は、環同型・体同型の全体になります。
ベクトル空間の型 $\mathrm{Vect}$
こちらも h-level 3。
等しさの証拠は、線形同型（正則な線形写像）の全体です。
たとえば $ℝ^n = ℝ^n$ の証拠は、$n$ 次一般線形群 $GL_n(ℝ)$ の元すべて、ということになります。
さらに上へ ── 圏の型は h-level 4
圏（category）まで来ると、もう一段上がります。
圏の型 $\mathrm{Cat}$ の h-level は 4 です（２-亜群にあたります）。
理由を追ってみましょう。
圏 $\mathcal{C}$ と $\mathcal{D}$ が等しいことの証拠は、圏同値（equivalence of categories）です。
ところが、圏同値どうしにも「等しさ」があります。
自然同型（natural isomorphism）です。
つまり、$\mathcal{C} = \mathcal{D}$ の証拠の集まりは、命題でも集合でもなく、亜群（h-level $3$） になっているのです。
したがって、
$Cat$ の h-level は $3 + 1 = 4$
です。
数学の対象が抽象度を上げるにつれて、「等しさの証拠」自体が構造を持ちはじめる ── その最初の実例が、圏です。
なお、ここで言う「圏」は、HoTT Book で言う univalent category（対象の同型と等式が一致する圏）を指します。
この条件を外した precategory では、事情が変わります。
一覧
| 対象 | 型として | h-level | 等式の h-level | 等しさの証拠 |
|---|---|---|---|---|
| 整数 |
Int、$ℤ$ |
2 | 1 | 一致するかしないか |
| 文字列 | Str |
2 | 1 | 一致するかしないか |
| リスト | List Int |
2 | 1 | 長さと各要素の一致 |
| 集合（データ構造） | Set Int |
2 | 1 | 同じ要素を含むか |
| 関数 | $ℕ → ℕ$ | 2 | 1 | 各点での値の一致 |
| 高階関数 | $(ℕ → ℕ) → ℕ$ | 2 | 1 | 各点での値の一致 |
| ベクトル | $ℝ^3$ | 2 | 1 | 成分の一致 |
| 行列 | $\mathrm{Mat}(m,n,ℝ)$ | 2 | 1 | 成分の一致 |
| テンソル | 成分表示 | 2 | 1 | 成分の一致 |
| 集合（数学的対象） | $hSet$ | 3 | 2 | 全単射の全体 |
| 群 | $\mathrm{Group}$ | 3 | 2 | 群同型の全体 |
| 環 | $\mathrm{Ring}$ | 3 | 2 | 環同型の全体 |
| 体 | $\mathrm{Field}$ | 3 | 2 | 体同型の全体 |
| ベクトル空間 | $\mathrm{Vect}$ | 3 | 2 | 線形同型の全体 |
| 圏 | $\mathrm{Cat}$ | 4 | 3 | 圏同値の全体（亜群） |
境目はどこにあるか
この表を眺めると、h-level 2 と 3 の間に、はっきりした断層があることが分かります。
h-level 2 の世界（要素を扱う世界）では、等しさは命題です。
証拠はひとつ。
「等しいか、等しくないか」だけを気にすればよい。
h-level 3 以上の世界（構造を並べる世界）では、等しさは集合です。
証拠が複数ある。
どの証拠を使ったかを、記録しておかねばなりません。
そして、この断層をまたぐ操作が、実はよく行われています。
$ℝ^3$ の中でベクトルを計算しているうちは h-level $2$ の世界にいます。
しかし「$ℝ^3$ というベクトル空間」を、他のベクトル空間と比べはじめた瞬間*に、h-level $3$ の世界へ移っている**のです。
補足：どんな型なら、何本の道があるのか
ここまでh-level という指標を使って、議論を整理してきましたが、同じことを**「道の本数」**の側から眺めると、また違った見通しが立ちます。
この点については、別の連載記事 で、Cubical Agda のコードを交えながら詳しく扱いました。
その記事から、要点を引きながら整理しておきます。
「型」と「道の種類（数）」との対応関係
「どんな型なら、何種類の道があるのか」 を、代表的な５つの型で並べると、次のようになります。
| 型（空間） | ２点を結ぶ道の「種類」の数 |
|---|---|
| 円周 $S^1$ | 整数の数だけ（0 周・1 周・2 周・…） |
| トーラス（ドーナツの表面） | 整数のペアの数だけ（縦に○周・横に○周） |
| ８の字（２つの輪） | さらに多い（左右どちらの輪を、どの順で回るか、まで効く） |
| 球面 $S^2$ | 道のレベルでは １種類（どの輪も縮む）。ただし「道と道の等しさ」の段で、整数の数だけ現れる |
宇宙の中の Bool
|
２種類（「そのまま」と「true/false を入れ替える」） |
逆に、Nat や Bool のような素朴な型（中身が集合である型）では、２点を結ぶ道は、あっても たかだか１本です。
複数の道が現れるのは、穴・ねじれ・高次の構造を持った型に限られます。
この表を、h-level の言葉に翻訳すると
いま述べたことを、これまでの h-level の言葉に置き換えてみましょう。
「道がたかだか１本」= 等式の型が命題（h-level 1）= 元の型が集合（h-level 2）
Nat、Bool、String がここに入ります。
証拠がひとつしかないので、区別のしようがありません。
「道が整数の数だけある」= 等式の型が集合（h-level 2）= 元の型が亜群（h-level 3）
円周 $S^1$、トーラス、８の字がここです。
証拠が複数あり、しかも互いに区別できます。
「道と道の段で、はじめて豊かになる」= 有限の h-level を持たない
球面 $S^2$ がこれにあたります。
１段目は静かでも、２段目で整数が現れる。以降も止まりません。
つまり、「道の本数」と「h-level」は、同じ事実を別の角度から述べたものなのです。
豊かさが顔を出す段は、型ごとに違う
ここで、もうひとつ面白い事実があります。
型によって、最初の"豊かさ"が顔を出す段が、一段ずつ高くなっていくのです。
円周 $S^1$ ── １段目で豊かになる
円周の一点を起点にすると、**１段目（道のレベル）**で、もう違いが出ます。「0 周・1 周・2 周……」という、整数の数だけの道。
いちばん下の段で、塔が太くなる例です。そのかわり、$S^1$ では２段目から上は、つぶれて自明になります。
だからこそ $S^1$ の h-level は 3 で止まるわけです。
球面 $S^2$ ── ２段目で豊かになる
球面では、１段目は静かです。表面に置いた輪ゴムは、どこに置いても一点まで縮みきってしまい、道のレベルでは違いが出ません。
ところが**２段目（道と道の等しさ）**で、突然ゆたかになります。
風船をボールに何回ぶんかぶせるか ── 0 回・1 回・2 回…… が、整数の数だけ別物として区別される。
豊かさが、一段上にずれて現れるわけです。
３次元球面 $S^3$ ── ３段目で豊かになる
さらにその上です。$S^3$ では、１段目も２段目も静かで、３段目で初めて、整数の数だけの違いが顔を出します。
円周は１段目、球面は２段目、$S^3$ は３段目
── 「いちばん下の、面白い等しさが住んでいる階」が、型ごとに違うのです。
Nat や String のような素朴な型は、この塔がいちばん下（点の段）で終わってしまう、いわば「平屋」だったわけです。
なぜ、この階段は無限に続くのか
そして、ここが HoTT の核心につながります。
別記事では、次のように書きました。
ここが HoTT の面白さの入口です
等しさを「道」とみなすと、道どうしの間に、さらに 「道と道をつなぐ道」（ホモトピー、homotopy）を考えられます。
さらにその上に、また道を……と、構造が どこまでも高く積み上がっていく。
この**「無限に積み上がる等しさの構造」を扱えることが、HoTT が幾何学（ホモトピー論）と結びつく理由**です。
規則そのものは、拍子抜けするほど機械的です。
いま見ている段の"もの"（点／道／ずらし方／…）を、次の段では新しい"点"とみなし、それらのあいだの「移し合い」を考える
── これを延々と繰り返すだけ。
先ほど「注意」の節で見た、$p$ と $q$ が２段目では点になる、という話が、まさにこれです。
そして、この繰り返しがいつ止まるかを測っているのが、h-level なのです。
- 有限回で止まる型 ── h-level が有限（
Natは 2、$S^1$ は 3、$\mathrm{Cat}$ は 4）
- いつまでも止まらない型 ── 有限の h-level を持たない（$S^2$、$S^3$）
「型」を空間に、「値」を点に、「等しさ」を道に読み替えることで可能になったこと
ここまでの整理の土台になっているのは、以下の読み替えでした。
型は空間、値は点、等しさ（恒等型）は、点と点を結ぶ道。
そして、そのすべてが、ひとつの型（空間）の内側で起きる出来事です。
この読み替えを受け入れた瞬間に、位相幾何学の道具立てが、そっくりそのまま型理論の中で使えるようになる
── h-level という指標も、その恩恵のひとつです。
ふだんのプログラミングで True ひとつに潰れていた等しさが、HoTT では、こんなにも豊かな世界だったわけです。
複数の等しさが生じる型 ── 具体例と、その意味
「穴やねじれを持った型でだけ、複数の道が現れる」と述べました。
では、それは具体的にどんな型なのでしょうか。
プログラミングの世界と、数学の世界に分けて挙げてみます。
プログラミングの世界
はじめに、範囲をはっきりさせておきます。
**Python や Java、C++ といった一般的なプログラミング言語で日常的に扱う型は、ほぼすべて h-level $2$ の集合です。
ここで複数の等しさが問題になることは、まずありません。
複数の等しさが顔を出すのは、依存型（dependent type）を持つ言語です。
依存型という言葉が初めて出てきましたので、説明しておきます。
依存型とは、値によって中身が変わる型のことです。
たとえば「長さ $n$ のリスト」という型を考えてみてください。
$n$ という値が、型の一部になっています。Vec 3 と Vec 5 は、別の型です。
ふつうの言語では、リストの長さは型に含まれません。
List[int] と書けるだけで、長さは実行時に確かめるしかありませんでした。
依存型があれば、「長さが合わないリストどうしは、そもそも足せない」ということを、コンパイル時に保証できます。
このような型を扱える言語が、Agda、Coq/Rocq、Lean、Idris です。
とりわけ、Cubical Agda は、HoTT を直接扱えるように設計されています。
そのうえで、実際に複数の等しさが現れる場面を挙げてみます。
１. 型そのものを値として扱うとき（宇宙）
いちばん基本的な例が、これです。
ここで 宇宙（universe）という言葉を説明しておきます。
ふつうの型の値は、3 や true といったデータでした。
これに対して、「型そのものを値として持つ、特別な型」 を考えることができます。これを宇宙と呼び、Type と書きます。
宇宙を空間とみなすと、その点のひとつひとつが、ひとつの型になります。
$ℕ$ も Bool も、宇宙という空間の中の点なのです。
さて、Bool という型を、この宇宙の中の点として見てみましょう。
「Bool は Bool に等しい」という等式に、２本の道があります。
- 「そのまま対応させる」道（恒等）
- 「`true` と `false` を入れ替えて対応させる」道（否定）
どちらも Bool を Bool に移す同値ですが、入れ替えたか、しなかったかは、明らかに別の情報です。
Univalence のもとでは、これが２本の異なる経路として残ります。
より一般に、型 $A$ を $A$ 自身に移す同値（自己同値）が複数あれば、宇宙の中で $A = A$ の道も、その数だけあります。
２. 同じデータの、別表現を行き来するとき
実務に近い例です。
自然数を、素朴な zero/suc 表現と、計算の速い二進表現の２通りで定義したとします。
この２つは同値ですから、Univalence によって「等しい」と言えます。
すると、素朴な表現で証明した定理を、そのまま速い表現へ運べます。
「証明しやすい型で証明し、使いやすい型で動かす」という分業が可能になる わけです。
形式手法（formal methods、プログラムの正しさを数学的に証明する手法）では、これを リファインメント（refinement）と呼びます。
証明しやすい仕様と、効率のよい実装との間に橋を架ける作業のことです。
その理論的な土台が、ここにあります。
３. 対称性を持つデータ構造
順序を持たないデータを考えます。
たとえば「$n$ 個の要素からなる集合」という型を考えると、その要素どうしの等式は、$n$ 次対称群 $S_n$ の元の数だけあります。
対称群（symmetric group）$S_n$ とは、$n$ 個のものを並べ替える方法すべてを集めた群のことでした。
$S_3$ なら、３個の並べ替えが $3! = 6$ 通りあります。
つまり、要素をどう並べ替えて対応させたか、が等しさの証拠として残るわけです。
グラフを「同型なものは同じ」として扱う型も同様で、等式の証拠はグラフ同型の全体 になります。
４. バージョン管理を型で表す
やや意外な応用として、パッチ理論（patch theory）があります。
パッチとは、ソースコードの差分のことです。
Git で言えばコミットにあたります。
Angiuli、Morehouse、Licata、Harper による "Homotopical Patch Theory"（2014 年）では、リポジトリの状態を点、パッチを道として、型の中に記述しました。
すると、パッチの適用順を入れ替えても同じ結果になるという「可換性」が、道と道をつなぐ変形として表現されます。
バージョン管理システムが暗黙に扱っていた等しさの構造が、型の階層として書き下されたわけです。
数学の世界
数学では、幾何学的な対象そのものが、複数の等しさの供給源になります。
順に見ていきましょう。
円周 $S^1$
基点から出て戻る道が、巻いた回数だけあります。
等式の型は $ℤ$ と一対一に対応します（$π_1(S^1) = ℤ$）。
トーラス $T^2$（ドーナツの表面）
縦回りと横回りの２方向があり、その組み合わせで無数の道ができます。
等式の型は $ℤ \times ℤ$ に対応します。
「縦に $m$ 周、横に $n$ 周」という整数の組が、そのまま道の種類になるわけです。
８の字（２つの輪をつないだ図形）
ここから先は、可換ですらありません。
左の輪を回ってから右の輪を回るのと、右を回ってから左を回るのとでは、別の道になります。
このような、順序が効く道の集まりを、自由群（free group）と呼びます。
自由群とは、いくつかの生成元から、可換性などの余計な関係をいっさい課さずに作った群のことです。８の字の場合は、２元生成の自由群になります。
クラインの壺
基本群が非可換になる、もうひとつの例です。
実射影平面 $ℝP^2$
球面の、向かい合う点どうしを同一視して作られる曲面です。
ここでは、等式の型が $ℤ/2ℤ$ に対応します。「２周すると元に戻る」道が現れる、有限の例として興味深いものです。
球面 $S^2$、$S^3$、…
１段目は静かでも、上の段で豊かになります。
しかも $π_n(S^m)$ の全体像は、いまだに分かっていません。
群 $G$ の分類空間 $BG$
これは幾何学的にも代数的にも重要な型です。
分類空間（classifying space）$BG$ とは、点がひとつだけの空間でありながら、その点から自分自身への道が、群 $G$ の元の数だけあるような対象のことです。
たとえば $G = ℤ/2ℤ$ なら、道は２本。$G = ℤ$ なら、道は整数の数だけあります。
群という代数的な対象を、空間として実現したものだと思ってください。
HoTTの中では、$BG$ をひとつの型として直接構成できます。
モジュライ空間
最後に、現代数学で大きな役割を果たしている対象を挙げます。
モジュライ空間（moduli space）とは、ある種類の数学的対象を、同型なものは同じとみなして、すべて並べた空間のことです。
たとえば「種数 $g$ の閉曲面の複素構造」をすべて集めて並べたものが、曲線のモジュライ空間 $\mathcal{M}_g$ です。
楕円曲線のモジュライ空間も、数論や代数幾何学で中心的に扱われます。
ここで問題になるのが、並べられた各点が、自分自身への同型（自己同型）を持つことです。
たとえば楕円曲線には、必ず「符号を反転する」という自己同型があります。
特別な楕円曲線では、さらに多くの自己同型を持ちます。
集合として並べようとすると、この自己同型の情報が消えてしまいます。
「点が１個」としか言えなくなるのです。
しかし、HoTT の型として並べれば、自己同型は、その点から自分自身への道として、そのまま保存されます。
複数の等しさが「発見された」ことは、研究をどう変えたのか
ここが本題です。
等しさが複数あると分かったこと
── より正確には、それを型の言葉で直接扱えるようになったこと
── は、数学の研究に何をもたらしつつあるのでしょうか。
現時点で見えているものを、４つ 挙げます。
第１に、代数トポロジーを、集合論を経由せずに展開できるようになりました
従来、ホモトピー群を計算するには、位相空間を集合として構成し、連続写像を定義し、同値類を取り……という手続きが必要でした。
HoTTでは、円周や球面を型として直接定義し、その恒等型を調べるだけで済みます。
Licata-Shulman による $π_1(S^1) = ℤ$ の機械証明（2013 年）が、その最初の実例でした。
以降、van Kampen の定理、Freudenthal のサスペンション定理などが、この方式で証明されています。
この分野は 合成ホモトピー論（synthetic homotopy theory）と呼ばれています。
「合成」（synthetic）とは、対象を、より基本的なものから組み立てるのではなく、はじめから公理で与えて扱う立場を指す言葉です。
ユークリッド幾何学で、点や直線を座標で定義せずに、公理だけで扱ったのと同じ発想だと思ってください。
第２に、古典数学の側へ、新しい定理が還流しました
これが、いちばん注目すべき成果だと思います。
Blakers-Massey の定理という、代数トポロジーの古典的な定理があります。
空間を貼り合わせたとき、そのホモトピー群がどこまで元の空間の情報を保つかを述べる定理です。
HoTT の中でこの定理を証明しようとしたとき、Finster と Lumsdaine は、位相空間の細かい構造に頼らない、まったく新しい証明を見つけました。
集合論的な道具が使えないため、そうせざるを得なかったのです。
ところが、その証明を読んだ Anel、Biedermann、Finster、Joyal が、同じ論法が任意の ∞-トポスで通用することに気づきます。
こうして、古典的な定理よりも一般的な形の Blakers-Massey 定理が、2020年 に発表されました。
HoTTという制約の多い環境で証明を探したことが、結果として古典数学に新しい定理をもたらした
── これは、この分野が単なる「証明の書き換え」ではないことを示す決定的な事例です。
第３に、計算できなかった量が、計算できるようになりました
Guillaume Brunerie は 2016 年の学位論文で、$π_4(S^3) \cong ℤ/nℤ$ となる $n$ を、HoTT の内部で定義しました。
そして $n = 2$ であることを、長い議論の末に証明しています。
その後 2022 年、Ljungström と Mörtberg が Cubical Agda でこれを形式化し、コンピュータに $n$ の値を実際に計算させることに成功しました。
答えは 2 でした。
定理の証明が、そのままプログラムとして走る
── これは、Cubical Agda が** Univalence を計算規則として実装したからこそ可能になったこと**です。
第４に、「同型なら同じ」が、証明の再利用として機能するようになりました
数学者は昔から「同型な構造は同一視してよい」と考えてきました。
しかし集合論の上では、これは厳密には成り立たないため、いちいち移し替えの作業が必要でした。
Univalence と構造同一性原理によって、この移し替えが自動化されます。
群 $G$ で証明した定理は、$G$ と同型な任意の群へ、そのまま運べる。
環でも、位相空間でも同じです。
UniMath のような大規模な形式化ライブラリで、証明の重複が大きく減ることが期待されており、実際に成果が出はじめています。
展望 ── これから期待されていること
さらに先を見ると、次のような方向が議論されています。
モジュライ問題との相性
先ほど紹介したモジュライ空間には、各点が自己同型を持つという問題がありました。
代数幾何学では、この問題に スタック（stack）という道具で対処してきました。
スタックとは、大まかに言えば、「点の集まり」ではなく「点と、点の自己同型の集まり」を同時に扱う空間のことです。
集合の代わりに亜群を貼り合わせて作る、と言い換えてもよいでしょう。
1960年代に Grothendieck と Deligne-Mumford らによって整備され、モジュライ理論の標準的な言語になりました。
HoTTの型は、はじめから同型を経路として保持しています。
ですから、スタックの言葉を、より自然に扱えるのではないかと期待されています。
高次圏論の内部言語として
Shulmanの2019 年の結果が示したとおり、∞-トポスはHoTTのモデルになります。
∞-圏論は現代数学の中心分野のひとつですが、その計算は極めて煩雑です。
対象と対象の間の射、射と射の間の 2-射、さらにその上……と、無限の階層をすべて追いかけねばならないからです。
HoTTの言葉 で書けば、その煩雑さの多くを型システムが引き受けてくれるのではないか？
── これが、圏論側からHoTTに対して寄せられている期待です。
ただし、慎重に
一方で、過大な期待は禁物です。
数論、解析学、確率論といった分野で、HoTT が直接の道具として使われている例は、2026年7月現在、ほとんどありません。
いま成果が出ているのは、もともとホモトピー論的な構造を持つ領域
── 代数トポロジー、高次圏論、そしてその形式化
── に集中しています。
HoTTはまだ 20 年に満たない理論です。
その応用可能性の射程がどこまで広がるかは、これからの数十年間の取り組みが、答えを出すことになります。
なぜ、等しさの舞台は「ひとつ下」になるのか
最後に、この節で繰り返し出てきた「等しさを問うと h-level がひとつ下がる」ことの理由を、丁寧に説明させてください。
理由１：定義がそう言っている
まず、いちばん素直な理由です。
h-level の定義そのものが、
型 $A$ の h-level が $n+1$ である ⟺ 任意の $a, b : A$ について $a =_A b$ の h-level が $n$
という形をしています。
ですから、「等式の h-level は、元の型より１つ小さい」 は、定義から直ちに従うことです。
しかし、これでは「なぜそう定義するとうまくいくのか」が分かりません。もう少し踏み込みましょう。
理由２：両端が固定されるぶん、自由度が減る
型 $A$ 全体を眺めているとき、私たちは どの点についても自由に議論できます。
ところが $a =_A b$ を眺めるときには、状況が変わります。
すでに両端の点が $a$ と $b$ に固定されているのです。
道の全体を考えるのではなく、「$a$ から出て $b$ に着く道」だけを考える。
動ける範囲が、はっきり狭まっています。
具体例で見ましょう。
$\mathrm{Group}$（h-level 3）では、点として置ける群は無数にあります。
$ℤ$、$S_3$、$GL_n(ℝ)$、... 何でも来い、という状態です。
しかし $ℤ =_{\mathrm{Group}} S_3$ を考えた瞬間、話は $ℤ$ と $S_3$ の間に限定されます。
ここで問うことができるのは、「$ℤ$ から $S_3$ への同型はどれか」だけです。
実際には同型がないので、この型は空です。
$ℤ =_{\mathrm{Group}} ℤ$ なら、答えは２つの同型（恒等と符号反転）。有限個です。
両端を固定するたびに、扱う対象が痩せていく ── これが「ひとつ下がる」ことの実感です。
理由３：証拠は、元の対象より単純である
もうひとつ、別の角度から。
一般に、「$X$ である」ことの証拠は、$X$ そのものより単純になります。
$\mathrm{Group}$ の点は、群そのものです。台集合、演算、単位元、逆元、そして結合律や逆元律の成り立つことの証拠 ── これらを全部束ねた、重たい対象です。
一方、$G =_{\mathrm{Group}} H$ の点は、同型写像ひとつです。台集合の間の写像に、演算を保つという条件がついただけ。ずっと軽い。
さらに、２つの同型写像 $f$、$g$ が等しいかどうかを問うと、これは「すべての $x$ で $f(x) = g(x)$ か」という、命題にまで痩せます。
群（重い） → 同型（軽い） → 同型どうしの一致（命題） → 何もない
このように、等しさを問うたびに構造が削ぎ落とされ、最後は命題に行き着いて止まります。
h-level が有限であるとは、この階段が有限回で底に着く、ということなのです。
理由４：ループ空間との対応
位相幾何学を学び始めた方には、この対応が一番しっくりくるかもしれません。
位相空間 $X$ と基点 $x_0$ に対し、$x_0$ を出て $x_0$ に戻るループ全体の空間を、ループ空間 $\Omega X$ と呼びます。
ループ空間には、よく知られた性質があります。
$$π_n(\Omega X) \cong π_{n+1}(X)$$
つまり、ループ空間を取ると、ホモトピー群の番号がひとつずれるのです。$\Omega X$ の $n$ 次の情報は、$X$ の $n+1$ 次の情報にあたります。
HoTT の恒等型 $x_0 =_X x_0$ は、まさにこのループ空間に対応します。
そして h-level についても、同じずれが起きます。
$X$ が $n$-type ならば、$\Omega X$ は $(n-1)$-type
恒等型を取ることは、ループ空間を取ることであり、次元をひとつ下げることである
── これが、位相幾何学の言葉で見たときの答えです。
球面 $S^2$ が有限の h-level を持たないのも、同じ理由から理解できます。$\Omega S^2$、$\Omega^2 S^2$、... と取り続けても、$π_n(S^2)$ が非自明であり続けるため、いつまでも底に着かないのです。
実務的なまとめ
以上を、使える形にまとめます。
手元の型の h-level が $N$ なら、その要素どうしの等しさは、h-level $N-1$ の舞台で論じられる。
Int、String、List、ふつうの関数 ── これらは h-level 2 ですから、等しさは h-level 1、つまり命題です。
「等しいか、等しくないか」だけを見ればよく、どうやって等しいと分かったかは気にしなくてよい。 これが、私たちが慣れ親しんだ世界です。
一方、群、環、体、ベクトル空間、集合そのもの
── これらを並べた型は h-level 3 です。等しさは h-level 2、つまり集合になります。
証拠が複数あり、どれを選んだかが後の議論に影響する。 ここから先が、HoTT が本領を発揮する領域です。
そして圏まで来ると h-level 4。等しさの証拠自体が亜群の構造を持ちはじめ、「証拠の証拠」まで管理する必要が出てきます。
みなさんが手元の対象を見たとき、まず問うべきは次のことです。
私はいま、要素を扱っているのか。それとも、構造そのものを並べて比べているのか。
前者なら h-level 2 の世界。後者なら h-level 3 以上の世界です。
この境目を意識できるようになることが、HoTT の視座を身につける第一歩になります。
HoTT が注目されているコミュニティ
2026年7月現在、HoTTは以下の６つの研究者コミュニティから注目されています。
分野ごとに、HoTT + Univalence Axiom が直接応用されているのか、それとも構造的なアナロジーにとどまっているのかを、明示的に区別しながらご紹介します。
数学基礎論
20 世紀の数学は、Cantorが創始し、ZFC集合論 として整えられた集合論を、共通の土台として発展してきました。
しかし、20 世紀後半以降、圏や ∞-圏、ホモトピー型のような高次の構造を扱う数学が発展するにつれ、集合論の上ではこれらを自然な形で扱えない、機械証明との相性が悪い、幾何学的な直観と形式のズレがある、といった問題が露わになってきました。
ZFC集合論に代わる、あるいは補完する数学の新しい土台の候補として、HoTTは活発に研究されています。
Voevodsky が提唱した Univalent Foundations Program （UF Program） がその中心で、HoTT + Univalence Axiom が直接使われている、HoTTの直接応用の分野です。
圏論・∞-圏論
Michael Shulman が 2019 年に定理 "All (∞,1)-toposes have strict univalent universes" を証明し、任意の Grothendieck ∞-トポスの内部言語が HoTT である、という結びつきを確立 しました。
Grothendieck ∞-トポスとは、∞-圏論の中で扱われる、特別な種類の ∞-圏です。
集合論が、「集合を作ったり、集合の間の関係を扱ったりできる、数学の基本的な舞台」を提供するのと同じように、Grothendieck ∞-トポスは、「その内部で、対象を作ったり、対象の間の高次の関係を扱ったり、論理的な推論を進めたりできる、豊かな数学の舞台」を提供します。
20 世紀後半に Grothendieck が代数幾何学のために導入した通常のトポス(1-トポス)を∞-圏として拡張したもので、現代数学の様々な分野(代数幾何、代数トポロジー、数理物理)で舞台として使われています。
また、「内部言語」とは、その舞台の中で使われる論理・言語のことです。
20 世紀後半、Lawvere らが「通常のトポスの内部言語は直観主義高階論理である」ことを示しました。トポスと論理との関係性については、以下の記事で取り上げています。
Shulman の 2019 年の定理は、この主張を一段持ち上げて、「∞-トポスの内部言語は HoTT である」ことを示しました。
これは、HoTT が、現代数学の中心分野である ∞-圏論（圏論を無限の階層まで拡張した数学）の中で標準的に使われる言語として位置づけられたという記念碑的な成果です。
詳細は次回の記事で扱います。
ここで 圏(category) は「対象と、対象を結ぶ矢印(射)」を扱う数学的な枠組み（1945 年、Eilenberg-Mac Lane が体系化）、∞-圏（infinity category） は、その階層(対象→射→2-射→3-射→...)を無限まで拡張したもの(Jacob Lurie が 2009 年の "Higher Topos Theory"で体系化)です。
Shulmanの2019年の定理は、HoTT + Univalence Axiom の意味論と ∞-圏論の関係についての、確立された数学的な定理 です。
定理証明支援系・形式証明
-
UniMath（Coq 上の HoTT ライブラリ、2014 年-）、
-
Cubical Agda（Univalence を計算規則として実装した Agda の拡張、2019 年-）、
-
HoTT-Coq
などで、HoTT + Univalence Axiom を直接使った数学の主要定理の 機械証明（machine-checked proof、数学者が書いた証明をコンピュータが１ステップずつ厳密にチェックし、正しいことを機械的に確かめること。証明支援系（proof assistant）というソフトウェアを使う）が実用段階に入っています。
代表例は、Licata-Shulman による 円周の基本群 π₁(S¹) = ℤ の HoTT 内機械証明です。
これは、円周 S¹ 上に基点(スタート地点)を決め、そこから同じ基点に戻る道を考えると、円周を何周したかで道の種類が区別でき、その周回数の集まりが整数 ℤ と 1 対 1 に対応する、という代数トポロジーの古典的結果(Poincaré が 1895 年に発見)を、HoTT の内部だけで機械証明したものです。
なお、同じ「定理証明支援系」の分野でも、Lean/mathlib(古典的な依存型理論、2025 年時点で 200 万行以上)は、HoTT の直接応用ではなく、依存型理論の別系譜での大規模ライブラリです。
Perfectoid 空間の形式化(2019 年、Kevin Buzzard ら)、Terence Tao の多変数解析の形式化(2023 年-)などは、いずれも Lean/mathlib での成果で、HoTT + Univalence Axiom を直接使ってはいません。
プログラミング言語理論・関数型プログラミング
依存型プログラミングの基礎理論として注目されています。
この分野で、HoTT + Univalence Axiom を直接実装しているのは Cubical Agda(2019 年-)です。
他の依存型プログラミング言語(Idris、F*)や、実用段階の検証済みソフトウェアの代表例(CompCert、RustBelt、seL4)は、いずれも古典的な依存型理論(Coq/Iris)や高階論理(Isabelle/HOL)の枠組みで書かれており、HoTT + Univalence Axiom を直接使ってはいません。これらは HoTT の応用ではなく、依存型理論・高階論理の別系譜の実用例として、明確に区別しておく必要があります。
数理物理・量子計算
HoTT + Univalence Axiom の直接応用が、2023-2024 年に確立しました。
Myers-Sati-Schreiber による”Topological Quantum Gates in Homotopy Type Theory”(Communications in Mathematical Physics、2024)が、トポロジカル量子ゲート
── 量子コンピュータの計算のステップを、粒子の位置ではなく、粒子（エニオン）の軌跡の編み方（２次元空間内での交差の仕方）に符号化して表現する仕組み（Alexei Kitaev が 1997 年頃に提案）
── を、HoTT の言語で直接記述し、Cubical Agda で機械証明可能な形にまとめた成果として、量子コンピュータの領域に、HoTTを直接的に応用した事例の代表例 になっています。
加えて、Linear Homotopy Type Theory(LHoTT)が、Proto-Quipper と相互翻訳可能な量子プログラミング言語の設計・検証言語として、Sati-Schreiber(2023-2025)らによって定式化されています。
詳細は次回の記事で紹介します。
AI 研究・AI 安全性
HoTT + Univalence Axiom を直接使ったモデルや実装は、2026年7月現在、事実上ありません。
この分野で議論されているのは、Univalence Axiom の「振る舞いが同じなら等しい」という原則と、AI モデルの等価性（蒸留、量子化、リファクタリング後のモデルが実質的に同じかどうか）の実務的な感覚が似ている、という構造的なアナロジーにとどまっています。
この構造的な結びつきは、HoTT + Univalence Axiom そのものの直接応用されたものではありません。
「レベルの異なる複数の等しさ」を識別する視座が、どの分野でどう役立っているか？
「同じ２点を結ぶ経路（道）が、互いに変形で移り合わない形で複数存在しうる」というHoTTの中心的な発見と、それを型システムで扱える言語としてのHoTTが、実際にもたらした発展は、次の３点にまとめられます。
（発想レベル・比喩レベルのつながりを除外し、HoTT + Univalence Axiom が実際に道具として使われている応用のみを列挙します）
第１に、HoTT の内部における「同型な構造は等しい」という考え方の公理化です。
20世紀の数学者が暗黙の慣習で使っていた「同型な構造は同じもの」というものの考え方を、Voevodsky が 2010 年に Univalence Axiom として明示の公理に書き下しました。
UniMath、Cubical Agda、HoTT-Coq の中で、この公理が実装され、機械が「同型なら等しい」を自動的に扱って証明を進められるようになりました。
第２に、HoTT の内部での代数トポロジーの主要定理の機械証明です。
ここで 代数トポロジー(algebraic topology) とは、位相空間の「つながり方」や「穴のあり方」を、代数(群、環、体などの、足し算・掛け算のできる数学的な構造)の言葉に翻訳して調べる位相空間論の一分野(1895 年、Poincaré が”Analysis Situs”で始めた)です。
Licata と Shulman が 2013 年に、上で紹介した円周の基本群 π₁(S¹) = ℤ を、HoTT の内部だけで機械証明することに成功しました。
以降、球面のホモトピー群の一部、van Kampen の定理、Blakers-Massey の定理、Freudenthal のサスペンション定理などが、HoTT の中で機械証明されています。
「レベルの異なる複数の経路」を型システムで直接扱えるようになったことが、この進展を可能にしました。
さらにこの延長線上で、Cubical Agda での 合成コホモロジー理論(synthetic cohomology theory)
── 代数トポロジーの主要な道具のひとつである「コホモロジー」（位相空間の"穴"を、群・環という代数の言葉で捉える手法）を、集合論的な迂回を経由せず、HoTT の言語だけで組み立てる理論
── の完全な機械証明（Brunerie-Ljungström-Mörtberg 2022、Ljungström-Mörtberg 2024/2025）や、simplicial HoTT（単体的 HoTT）（有向 Univalence 公理（directed univalence axiom）を含む HoTT の変種）。
通常のHoTTでは、「等しさ」が可逆（逆向きにたどることができる）であるのに対し、逆向きにたどることができない「向き付きの矢印」も型システムで扱えるように拡張したもの）での ∞-圏の Yoneda 補題の機械証明（Kudasov-Riehl-Weinberger 2024）なども、この視座から得られた成果です。
詳細は次回の記事で紹介します。
第３に、数学の新しい土台の提案として、HoTT は集合論に代わる/補完する基礎付けの候補になっています。
集合論では、技術的迂回が必要だった高次の構造(上で紹介した圏・∞-圏、そして位相空間から細かい距離や形状の情報を捨てて、点のつながり方や道の変形の情報だけを残した対象である ホモトピー型(homotopy type) など)を、直接扱うことのできる言語として、HoTTはいま、数学基礎論の新しい候補として注目されています。
HoTT + Univalence Axiom そのものが実際に使われている応用:
UniMath、Cubical Agda、HoTT-Coq などの HoTT を直接使う数学ライブラリ、Licata-Shulman による π₁(S¹) = ℤ の機械証明(2013 年)、その後の HoTT 内での代数トポロジーの主要定理の機械証明(球面のホモトピー群の一部、van Kampen の定理、Blakers-Massey の定理、Freudenthal のサスペンション定理など)。
以下は、HoTT の応用事例ではなく、依存型理論・高階論理の応用事例になります。
HoTTの応用事例ではないことに、ここで注意を促しておきます。
-
CompCert（Coq/古典的な依存型理論、Airbus 航空機ソフトで実用）
-
RustBelt（Coq/Iris、Rust の型システムの安全性の理論的裏づけ）
-
seL4（Isabelle/HOL、AWS Firecracker の一部で使用されるマイクロカーネル）
-
mathlib（Lean/古典的な依存型理論）
-
Perfectoid 空間の形式化
-
Terence Tao の多変数解析の形式化
-
Idris・F*（古典的な依存型理論の系譜）
など。
これらは HoTT の直接応用ではなく、依存型理論・高階論理の別系譜の実用例です。
一方、物理学、化学、生物学、機械工学・電気工学のような伝統的工学、社会科学では、
HoTT + Univalence Axiom が実際にモデル(数学的な描き方)として使われている例は、
2026 年 7 月現在、事実上ありません。
HoTT はまだ若い理論(2006-2013 年頃に基盤確立)であり、今後数十年で他分野への応用が広がる可能性があります。
それでは次の記事では、HoTTの各論点について、詳しく解説していきます。
補遺：より厳密な言い方について
本文では、学部レベルの予備知識だけで読めることを優先し、いくつかの箇所で意図的に簡略化した書き方をしました。
この分野に詳しい読者から見ると、そのままでは正確でない表現が残っています。ここでまとめて補正しておきます。以下の記述が、本文より優先されます。
１. Grothendieck のホモトピー仮説は「仮説」であって定理ではない
本文で「HoTT の型が持つ経路の階層構造は、位相空間のホモトピー型と本質的に同じ情報を持つことが分かっています」（1983年、Grothendieck のホモトピー仮説）と書きましたが、この言い方には２つの不正確さがあります。
第１に、これは予想であって、証明された定理ではありません。
Grothendieck が 1983 年の草稿 "Pursuing Stacks" で述べたのは、「∞-亜群の圏と、位相空間のホモトピー型の圏は同値であるはずだ」という 予想（homotopy hypothesis） です。
∞-亜群の定義を１つ固定すれば、その定義のもとで定理として証明できる場合もありますが、「∞-亜群とは何か」の定義自体が複数あるため、包括的な形では今日も予想のままです。
第２に、これは HoTT について述べたものではありません。
1983 年の時点で HoTT は存在しません。Grothendieck が語ったのは ∞-亜群についてであり、HoTT の型についてではありません。
HoTT の型と位相空間のホモトピー型の対応を実際に数学的に裏づけているのは、Voevodsky による 単体的集合を使ったモデルの構成（2009 年） 以降の一連の研究です。
ホモトピー仮説は、この対応が成り立つはずだという見通しの 源流にある発想 として位置づけるのが正確です。
したがって本文の該当箇所は、次のように読み替えてください。
HoTT の型が持つ経路の階層構造は、位相空間のホモトピー型と本質的に同じ情報を持つと考えられています。
この見通しの源流にあるのが、Grothendieck のホモトピー仮説（1983 年）です。HoTT の側でこの対応を裏づけているのは、Voevodsky の単体的集合モデル（2009 年）以降の研究です。
２. Univalence Axiom の正確な主張
本文では Univalence を、次のように紹介しました。
型 $A$ と型 $B$ の間に同値があるなら、それに対応する経路が $A$ から $B$ へ存在する
「おおまかに言えば」と断ったとおり、これは Univalence の 帰結の一部 であって、公理そのものではありません。
この言い方だと、「経路を１本付け加えるだけ」の、はるかに弱い主張でも満たせてしまいます。それでは Univalence の内容になりません。
Univalence が実際に主張しているのは、次のことです。
型 $A$ と型 $B$ について、「$A$ から $B$ への経路の全体」と「$A$ から $B$ への同値の全体」が、過不足なく対応する
より正確には、経路から同値を作る標準的な写像
$$idtoeqv : (A =_{\mathcal{U}} B) \longrightarrow (A ≃ B)$$
が、それ自身 同値である、というのが Univalence Axiom です。
つまり、単に「同値があれば経路がある」だけでなく、経路と同値が同じだけある ことまで主張しています。
この「同じだけある」という部分が本質的です。
本文の最後で述べた「$(ℤ, +)$ と $(2ℤ, +)$ の間の $n \mapsto 2n$ と $n \mapsto -2n$ が、それぞれ別の経路を与える」という話は、まさにこの一致から従うものです。弱い方の言い方では、この結論は出てきません。
３. 「同型なら等しい」は Univalence から導かれる結果
本文では、群 $(ℤ, +)$ と $(2ℤ, +)$ の同型を例に Univalence を説明しましたが、この２つは厳密には別の階層の話です。
Univalence が直接述べているのは、型の同値についてです。
一方、群のような 構造を持つ対象 について「同型なら等しい」が成り立つことは、Univalence から 導かれる 結果であり、構造同一性原理（structure identity principle, SIP） と呼ばれます。
群の同型は、台集合の間の同値に加えて、演算が保たれることを要求します。
この「構造も対応している」という条件を込めたうえで、群の型 $\mathrm{Group}$ における経路が得られる、という段取りになります。
本文の説明は、この導出の過程を省いて結論だけを述べたものです。
４. 関数外延性は Univalence から導出できる
本文では、Univalence と関数外延性を並列の規則として扱いました。
役割の違いを示すうえではこの整理が分かりやすいのですが、事実としては、関数外延性は Univalence から導出できる ことが知られています（Voevodsky）。
つまり、両者は独立した２本の公理ではありません。
本文であえて分けて書いたのは、「同型なら同じ」と「振る舞いが同じなら同じ」という２つの慣習が、それぞれ異なる場面で働くことを明示するためです。
５. Shulman の定理が示したこと
本文で「任意の Grothendieck ∞-トポスの内部言語が HoTT である、という結びつきを確立した」と書きましたが、これはやや強い言い方です。
Shulman が 2019 年に証明したのは、任意の Grothendieck ∞-トポスが、strict univalent universe を持つモデル圏によって表示できる、ということです。
これは「∞-トポスは HoTT のモデルになる」という方向、すなわち 健全性 にあたります。∞-トポスの中で HoTT の言葉を使って議論してよい、という保証が得られたわけです。
一方、その逆方向 ── HoTT の構文が ∞-トポスの内部言語として過不足ない、という主張（内部言語予想）── は、一般には未解決です。
したがって、「∞-トポスの内部言語は HoTT である」と言い切るのではなく、「∞-トポスが HoTT のモデルになることが示され、内部言語として HoTT を使える保証が得られた」と述べるのが正確です。
記念碑的な成果であることに変わりはありません。
６. ∞-圏の体系化の帰属
本文では「∞-圏は Jacob Lurie が 2009 年の "Higher Topos Theory" で体系化した」と書きましたが、これは経緯を簡略化しすぎています。
∞-圏のモデルの１つである 擬圏（quasi-category） は、Boardman-Vogt が 1973 年に導入し、André Joyal がその理論を大きく整備しました。
Lurie の "Higher Topos Theory"（2009 年）は、この基礎のうえに立って、∞-圏論を現代数学で使える規模まで大規模に展開した仕事です。
「Boardman-Vogt と Joyal による基礎づけを経て、Lurie が 2009 年に大規模に展開した」とするのが正確です。
７. simplicial HoTT と有向 Univalence 公理
本文で「simplicial HoTT（有向 Univalence 公理を含む HoTT の変種）」と書きましたが、有向 Univalence は、この体系に最初から組み込まれている公理ではありません。
Riehl-Shulman の simplicial type theory（2017 年）は、単体的な構造を型理論の中で扱えるようにした体系で、有向 Univalence はそのうえで 追加の公理として議論されている 段階にあります。
また、Kudasov-Riehl-Weinberger による ∞-圏の Yoneda 補題の形式化（2024 年）も、有向 Univalence を使わずに行われています。
「有向 Univalence を含む体系」ではなく、「有向 Univalence が議論されている体系」とするのが正確です。
８. Lean/mathlib の規模について
本文で「2025 年時点で 200 万行以上」と記しましたが、この数字は確認が取れていません。
mathlib の規模は日々変動するため、正確な数字は公式リポジトリの統計をご確認ください。「数百万行規模の大規模ライブラリ」という理解で差し支えありません。
９. seL4 の採用事例について
本文で seL4 について「AWS Firecracker の一部で使用されるマイクロカーネル」と記しましたが、この記述は裏づけが取れていません。
Firecracker は AWS が Rust で開発した VMM であり、seL4 とは別系統のプロジェクトです。両者の間に採用関係があるという公開情報は確認できませんでした。
seL4 については、「Isabelle/HOL によって機能正当性が形式検証されたマイクロカーネル」という記述のみが正確です。この点をお詫びして訂正します。
以上の補正は、いずれも本文の主張の骨格を変えるものではありませんが、専門的な正確さの観点からは重要な違いです。
本文は入門的な見通しを優先した記述であり、厳密な定式化については、"Homotopy Type Theory: Univalent Foundations of Mathematics"（HoTT Book, 2013）の該当章をご参照ください。