想定読者と、この記事のねらい
- 高校で理系の数学を学んだものの、内容はだいぶ忘れてしまっている（大学の数学は未学習）
- 「位相幾何学」「ホモトピー理論」「圏論」は、名前も聞いたことがない、または名前だけ知っている
この記事は、そういう皆様に向けて、ホモトピー理論という数学の世界観を紹介するものです。
数式はほとんど使いません。中心になる言葉は、「点」と「道」 のふたつだけです。予備知識も要りません。必要なのは、広場を散歩する場面や、粘土をこねる場面を思い浮かべる想像力だけです。
そして記事の最後に、この幾何学の世界観が、意外な場所 ── プログラミング言語の世界 ── へ流れ込んでいることを、予告編として少しだけお見せします。
1. 「等しい」とは、そもそも何でしょうか
小学校以来、私たちは「等しい」という言葉を、当たり前のものとして使ってきました。2 + 3 と 5 は等しい。これは疑いようがなく、答えは「はい」か「いいえ」のどちらかに決まる、と感じられます。
ところが、図形の世界に足を踏み入れたとたん、「等しい」は当たり前ではなくなります。
三角定規を2枚、机に置いてみてください。片方を裏返すと、もう片方にぴったり重なるとします。
この2枚は「同じ形」でしょうか？
裏返しを許すなら同じですし、許さないなら別物です。
では、形はそっくりで大きさだけ違う2つの三角形は？
「相似」という緩い基準では同じ、「合同」という厳しい基準では別物です。
つまり図形の世界では、「等しい」の基準は 1 種類ではなく、目的に応じて選ぶもの なのです。
厳しい基準を選べば、区別は細かくなる代わりに、比べる作業は大変になります。
緩い基準を選べば、多くのものがひとまとめになり、見通しがよくなります。
この記事で紹介する ホモトピー理論 は、数学の歴史の中でも指折りに 大胆な緩め方 を選んだ分野です。
そして、その緩め方の中から、「等しい」という概念そのものについての、驚くほど豊かな風景が立ち上がってきます。
2. 宣言 — 「もの」は点、「等しさ」は道
ホモトピー理論の世界観は、次のふたつの宣言に凝縮できます。
考えたい「もの」たちを、ひとつの空間に、点として置く。
「a と b は等しい」という事実を、点 a と点 b をつなぐ道として描く。
「道」は、文字どおりの意味で受け取ってください。紙の上に点をふたつ打ち、鉛筆の先を紙から離さずに、片方からもう片方までなぞる。そのなぞった線が道です1。
途中で途切れていなければ、ぐねぐね曲がっていても、大回りしていても構いません。
この宣言の何が新しいのでしょうか？
それは、等しさを「はい / いいえ」の判定結果ではなく、証拠という実体を持つもの に変えた点です。
従来の感覚では、「a と b は等しいか」という問いの答えは、真か偽かのどちらかでした。
ところが道の見方では、a と b が等しいと主張したい人は、道を 1 本、実際に差し出す ことになります。
証拠の線が引けたら等しい。
どうやっても線がつながらないなら、等しくない。
等しさが、空間の中に置かれた目に見える物体になるのです。
自らの主張の正しさを証明するために、主張内容を体現する具体例を実際に作り出して差し出さなければならない数学は、プロの数学者たちの間では、構成主義の数学 と名付けられています。
実はこの構成主義の数学は、関数型プログラミング言語や、AI による数学定理の証明プロジェクトで活躍している定理証明言語の型理論を、深いところで支えています。
📌 中上級者向け補足：Lean の日々の証明は構成主義的なのか
AI 数学証明で使われる Lean の実際の数学ライブラリでは、排中律や選択公理といった古典論理の公理を上乗せして使うのが普通で、日々の証明が構成主義的に行われているわけではありません。
ただし、その土台にある型理論そのものは構成主義の系譜にある——という関係です。
本文の一文は「型理論を深いところで支えている」と、この土台の話に限定した言い方になっています。
「そんな言い換えをして、何が変わるのか」と思われるかもしれません。
実は、決定的なことが変わります。
証拠が実体になった瞬間、証拠を数える ことができるようになるのです。
次の節で、それを見ます。
3. 池のある広場 — 「等しさ」は 1 種類とは限らない
広い広場を想像してください。広場の中に、点 a と点 b があります。
まず、広場に何の障害物もない場合。a から b への道は、いくらでも引けます。
まっすぐな道、右に膨らむ道、大きく蛇行する道。
しかし、これらの道はどれも、地面から離さずに少しずつずらしていけば、互いにぴったり重ねられます。引ける道は無数でも、ずらして重なるものを同一視するなら、道は実質 1 種類です。
「a と b は等しい」ことの証拠は、あってもなくても 1 通り、という穏やかな世界です。
次に、広場のまんなかに 池 がある場合を考えます。池の中は歩けません。
すると、景色が一変します。a から b へ、池の 左側 を回る道と、右側 を回る道が引けます。
どちらも a と b をつなぐ正当な道、つまり「a と b は等しい」ことの正当な証拠です。
ところが、この 2 本は互いに重ねられません。
左回りの道を、地面から離さずにじわじわ動かして右回りの道に重ねようとすると、途中でどうしても池の上を通過しなければならず、そこで手が止まります。
池 ── 空間に開いた穴 ── が、2 本の道を、取り替えのきかない別々の証拠として区別させている のです。
さらに言えば、証拠は 2 通りでは済みません。
- 池のまわりをぐるりと 1 周してから b へ向かう道
- 2 周してから向かう道、逆向きに 1 周する道
巻きつく回数が違う道は、どれも互いに重ねられない、別々の証拠です。
穴がたった 1 つあるだけで、「a と b は等しい」という 1 つの主張の裏に、数えきれるが無限にある、異なる証拠の一覧表 がぶら下がることになります。
ここで、この記事でいちばん大事な一文を書きます。
ホモトピー理論では、「等しいか、等しくないか」だけでなく、「どのように等しいか」「その等しさ方は何種類あるか」までが、問いになる。
等しさの証拠を数える。
この一見奇妙な発想が、実は空間の形 ── 穴がいくつ、どこに開いているか ── を調べる強力な手段になります。
証拠の種類が枝分かれするのは、穴のあるところだけだからです。
証拠の一覧表は、空間ごとの「指紋」になる
いくつかの空間で、実際に証拠の一覧表を作り比べてみましょう。
同じ地点から出発して同じ地点に戻ってくる道（周遊コース）に話を絞ると、比べやすくなります。
障害物のない広場。
どんな周遊コースも、その場でじわじわ縮めていけば、出発点に立ち止まったままの「動かないコース」に潰せます。
一覧表の中身は、実質 1 行だけです。
池が 1 つある広場。 前に見たとおり、池のまわりを何周するか（右回りを負の数で数えることにします）でコースが枝分かれします。
一覧表は「…, -2 周, -1 周, 0 周, 1 周, 2 周, …」となり、整数の目盛りとぴったり同じ構造 をしています。
ドーナツの表面。
ドーナツ（浮き輪でも構いません）の表面を歩き回れる世界を考えると、周遊コースの巻きつき方は 2 方向あります。
輪をくぐる向きにぐるりと回る巻きつきと、輪に沿って大回りする巻きつきです。
コースは「くぐる向きに m 周、大回りの向きに n 周」という 整数のペア で分類されます。
一覧表が、2列の表になるのです。
池が 2 つある広場。
さらに面白いことが起きます。
左の池を回ってから右の池を回るコースと、右の池を回ってから左の池を回るコースは、互いに重ねられない別のコースになります。
回る順番までが証拠の違いとして記録される ので、一覧表は整数の目盛りのような素直な形には収まりません。
こうして並べると、見えてくることがあります。
空間の形が違えば、証拠の一覧表の構造が違う。
逆に言えば、一覧表は空間の指紋 なのです。
目で見ても区別しにくい 2 つの空間が本当に違う形かどうかを、証拠の一覧表を突き合わせて判定する ── ホモトピー理論 の実務は、おおよそこの形をしています。
ここまでの一覧表を、表にまとめておきます。
| 空間 | 周遊コースの一覧表（＝出発点が自分自身と「等しい」ことの証拠の一覧） |
|---|---|
| 障害物のない広場 | 実質 1 行（動かないコースだけ） |
| 池が 1 つある広場 | 整数の目盛りと同じ構造（…, -2 周, -1 周, 0 周, 1 周, 2 周, …） |
| ドーナツの表面 | 整数のペア（くぐる向きに m 周、大回りの向きに n 周） |
| 池が 2 つある広場 | 回る順番まで区別される、もっと複雑な構造 |
「等しさの証拠の一覧」と「空間の形」という、一見なんの関係もなさそうな 2 つのものが、1 枚の表の左右に並ぶ。
この対応こそが、ホモトピー理論という分野の土台です。
なお、形の情報をこうした数えられる情報に翻訳して調べる分野を、数学者たちは 代数トポロジー と呼びます（その代表的な手法のひとつには ホモロジー という名前もついています）。
名前だけ挙げておきますので、いつか専門書で再会したら思い出してください。
📌 中上級者向け補足：厳密性を担保した説明をすると ── 「道」そのものを数えているわけではない
本文では「道を数える」と説明しましたが、数学的には、文字どおり個々の道そのものを数えているわけではありません。
2 点を結ぶ道は、少し曲げたり、少し膨らませたりすることで無数に作れます。
そのため、個々の道をそのまま区別して数えるのではなく、「端点を固定したまま連続的に変形できる道どうし」を同じものとして扱います。
このとき、実際に分類しているのは、個々の道ではなく 道のホモトピー類 です。
たとえば、1 つの穴のある平面上で、基点から出発して基点へ戻るループを考えると、「穴を何周したか」によってホモトピー類を区別できます。
本文の「左回り」「右回り」「1 周」「2 周」といった説明は、このホモトピー類の違いを直感的に表したものです。
このように、複雑な曲線を一本ずつ調べるのではなく、連続変形で同じとみなせるものをまとめて分類する ことで、空間の形を代数的な情報として扱えるようになります。ここから 基本群 などの概念が登場します。
4. 道の上の道 — 等しさの階層は積み上がる
前の節で、「2 本の道を、ずらして重ねる」という操作を何度も使いました。この操作を、もう一段だけ注意深く見てみます。
道 p と道 q を重ねられるかどうか。
これは、言い換えれば 「道 p と道 q は等しいか」 という問いです。
点と点の等しさを問うていたはずが、いつのまにか、道と道の等しさを問うている。
舞台が一段、上がっています。
そして、p を q へじわじわ動かしていくときの、その 動かし方の全体（ずらしていく途中経過をぜんぶ束ねたもの）は、いわば「道 p から道 q への道」です。
1段目の等しさの証拠が道だったように、2 段目の等しさの証拠は、道と道をつなぐ 変形 なのです。
ちなみに、この 変形 こそが、ホモトピー（homotopy）と呼ばれるものです。
この記事で紹介している世界観の分野名は、ここから来ています。
ホモトピー と呼ばれる数学研究分野、と覚えてください。
すると当然、次の問いが生まれます。
２つの変形は等しいか？
その証拠は、変形と変形をつなぐ、さらに上の 変形です。
- 1 段目：点と点をつなぐ道。
- 2 段目：道と道をつなぐ変形。
- 3 段目：変形と変形をつなぐ、さらに上の変形。
- ……
この階段は、原理的に どこまでも続きます2。
等しさの上に等しさが、その上にまた等しさが積み上がっていく。
ホモトピー理論が扱う「空間の形」とは、点の配置のことではなく、この 無限に積み上がった等しさの構造全体 のことなのです。
階段を上がる仕組みそのものは、じつは拍子抜けするほど機械的です。
ひとつの段から次の段へ移るときのルールは、こう言い表せます。
いま見ている段の主役たち（1 段目なら道、2 段目なら変形）を、次の段では「点」とみなす。そして、その新しい点どうしをつなぐ道を考える。
1段目では、道 p や道 q が主役でした。
2 段目に上がると、p と q はそれぞれ 1 個の点に格下げされ、そのあいだをつなぐ変形が、新しい「道」の役を演じます。
前の段の主役が点になり、主役の座を次のものに譲る。
この世代交代を延々と繰り返すだけで、無限の階段が立ち上がります。
仕組みは単純なのに、そこから生まれる構造は空間ごとにまるで違う
── ここに、この分野の奥行きがあります。
📌 中上級者向け補足：厳密性を担保した説明をすると ── 「道の上の道」とは何か
本文では、道 p から道 q への連続的な変形を、いわば「道 p から道 q への道」と表現しました。
これはホモトピーを直感的に理解するための比喩です。
厳密には、2 本の道 p と q の間のホモトピーは、2 つのパラメータを持つ連続写像 として表されます。一方のパラメータは道の上の位置を表し、もう一方は変形がどこまで進んだかを表します。
つまり、1 本の道を別の道へ連続的に動かしていく過程全体を、ひとつの数学的対象として扱っているわけです。
そして、ここで終わりではありません。
2 つのホモトピーそのものをさらに連続的に変形することも考えられます。
すると、
点 → 道 → 道の間のホモトピー → ホモトピーの間のホモトピー → …
という階層が現れます。
本文で「等しさの証拠が、さらに別の等しさの証拠を持つ」と説明したのは、この構造を直感的に表したものです。
なお、空間によっては、この塔のどの階に「面白さ」が住んでいるかが違います。
池のある広場では、1段目（道の段）で早くも証拠が枝分かれしました。
一方、世の中には、1段目は退屈なのに、2段目で突然にぎやかになる空間もあります。
代表例は、風船の表面です。風船の表面に輪ゴムを置くと、どこに置いても、するすると滑らせて 1 点に縮めきれてしまいます。
周遊コースの段（1段目）では、障害物のない広場と区別がつきません。
ところが「縮め方どうしを比べる」2段目に上がったとたん、しぼんだ風船をボールに何回かぶせ直すか、という数えあげが顔を出し、一覧表がにぎやかになります。
1階は空き部屋なのに 2階に住人がいる
── そんな建物のような空間があるわけです。どの階がにぎやかかは、空間ごとの個性です。
📌 中上級者向け補足：厳密性を担保した説明をすると ── 風船の 2 段目で何が起きているのか
本文では、風船の表面では 1 段目の周遊コースがすべて1点に縮められる一方、2段目では「縮め方どうし」の違いが現れる、と説明しました。
数学的には、風船の表面、つまり 2次元球面 S² について、基本群 π₁(S²) は自明です。
これは、球面上の任意のループを1点へ連続的に縮められることを意味します。
ところが、さらに1段上の構造を見ると、違いが現れます。
2次元球面から2次元球面への写像を考えると、その写像を連続変形しても消せない違いがあり、それらは整数で分類できます。
この整数は 次数（degree） と呼ばれます。
その結果、2 次ホモトピー群について
π₂(S²) ≅ ℤ
が成り立ちます。
本文の「しぼんだ風船をボールに何回かぶせ直すか」というイメージは、この整数を直感的に捉えるためのものです。
厳密には、物理的な風船を実際に何回もかぶせるという操作を定義しているのではなく、球面から球面への写像のホモトピー類を分類しています。
この例の面白いところは、1段目では何も残らないように見える空間でも、2段目まで調べると豊かな構造が現れることです。
これが「等しさの階層」が単なる比喩ではなく、実際の数学的構造につながっていることを示しています。
5. この見方は、どこから来たのか — 形の分類という問題
さて、こんな風変わりな世界観を、数学者はなぜ採用するに至ったのでしょうか？
歴史を少しさかのぼります。
5-1. 解の式をあきらめて、軌道の形を見る
19 世紀の末、フランスの数学者 Henri Poincaré は、太陽・地球・月のような 3 つの天体が引き合いながら動くとき、その運動を予測するという難問（三体問題）に取り組んでいました。そして、運動を表す方程式の解を、きれいな式として書き下すことは望めない、という壁に突き当たります。
ここで Poincaré は、問いの立て方を変えました。
解の数値を求めるのはあきらめる。
その代わり、解の描く軌道が、大づかみにどんな「形」をしているか
── ぐるっと閉じて元に戻るのか、何かのまわりに巻きついていくのか ── を調べよう、と。
この方針転換に必要だったのは、長さや座標といった細かい数値に頼らずに、形どうしを比べ、分類する道具でした。1895 年に発表された彼の論文を出発点として、この道具立てはやがて 位相幾何学（トポロジー） と呼ばれる数学領域に育っていきます。
俗に「コーヒーカップとドーナツを同じとみなす幾何学」と紹介される、あの分野です。
カップの取っ手の輪とドーナツの輪が対応していて、あとは粘土のように連続的に変形すれば互いに移り合えるから、位相幾何学の目にはこの 2 つは同じ形に映る
── そういう世界です。
📌 中上級者向け補足：厳密性を担保した説明をすると ── Poincaré の仕事とホモトピー理論の歴史
本文では、Poincaré が三体問題などを背景として、個々の軌道をきれいな式で解くこととは別に、軌道の「形」そのものを調べる方向へ進んだ、という物語で紹介しました。
これは歴史の流れをつかむための説明ですが、実際の数学史はもう少し複雑です。
Poincaré の 1895 年の『Analysis Situs』は、今日の代数トポロジーにつながる重要な仕事のひとつです。ただし、そこから現在のホモトピー理論が一気に完成したわけではありません。
その後、多くの数学者によって基本群、ホモトピー群、ホモロジー、CW 複体などの概念が発展し、現在の位相幾何学・代数トポロジーへつながっていきました。
また、本文の「三体問題が解けない」という説明も、「解が存在しない」という意味ではありません。
一般に、三体問題では二体問題のような単純な閉形式の解を得ることが難しく、軌道の複雑な構造を調べる必要がありました。
したがって本文の歴史説明は、Poincaré の研究をきっかけの一つとして、「個々の形を直接計算するだけでなく、連続変形しても変わらない構造を調べる」という数学が発展していった大きな流れを示すもの、と捉えるのが適切です。
5-2. 「きっちり同じ」は、厳しすぎた
位相幾何学にも、「同じ形」の基準として厳しめのものと緩めのものがあります。
厳しい方の基準は、おおまかに言えば、2つの形のあいだで、点と点をひとつ残らず1対1に対応させ、しかもご近所関係（どの点とどの点が近くにいるか）まで完全に写し取れること を要求します3。
ところが、この基準は使ってみると厳しすぎました。
2つの形がこの意味で同じであることを示すには、条件を満たす対応をひとつ実際に組み立てる必要があり、同じでないことを示すには、あり得る対応をすべて否定する必要があります。ど
ちらも、たいへんな難行です。
そこで数学者たちは、要求を思い切って削りました。
点どうしの 1 対 1 対応は、もう求めない。連続的な変形で互いに移り合えさえすれば、同じとみなす4。
たった一箇所の緩和ですが、効果は劇的でした。
1対1でなくてよいなら、たくさんの点をまとめて1点に押し潰すような変形も許されます。
たとえば、ぴんと張った 1 枚の円盤（ふちも中身も含めた丸い膜）は、中心に向かってきゅっと縮めていけば、1点にまで潰せます。
厳しい基準では「2次元の膜」と「0次元の点」は決して同じになれませんが、緩い基準のもとでは、これら2つは堂々と同じ仲間です。
次元の違いすら、乗り越えてしまうのです。
この落差を、もう少し味わってみましょう。
1個の点、1本の線分、1枚の円盤、どこまでも広がる平面。
この4つは、次元だけ見ても 0、1、2、2 とばらばらで、厳しい基準ではすべて互いに別物です。
ところが緩い基準では、どれも1点に潰せるので、4 つとも同じ仲間 になります。
区別がここまで大胆に消えるからこそ、「では、それでも消えない違いとは何か」という次の問いが、くっきりと浮かび上がってきます。
📌 中上級者向け補足：厳密性を担保した説明をすると ── ホモトピー同値とは
本文では、「連続的な変形で互いに移り合えさえすれば、同じとみなす」と説明しました。
これはホモトピー同値を理解するための直感として有効ですが、数学的な定義はもう少し慎重です。
2つの空間 X と Y がホモトピー同値であるとは、X から Y への連続写像 f と、Y から X への連続写像 g が存在し、g と f を続けて適用したもの g∘f が X の恒等写像とホモトピックになり、f∘g が Y の恒等写像とホモトピックになることをいいます。
ここで重要なのは、「X を粘土のように直接変形して Y にする」ということが、ホモトピー同値の定義そのものではないという点です。
本文の「連続的な変形で互いに移り合う」という表現は、あくまでこの概念をイメージするための入門者向けの言い方です。
厳密には、2つの空間の間に連続写像を用意し、それらが互いに逆写像のように振る舞うことを、完全な逆ではなく「ホモトピーの意味で逆」であることによって表現しています。
本文では直感的に分かりやすい理解を優先し、正式な定義はこのコラム欄に記載させていただきました。
5-3. 潰しきれずに残るもの — 骨組み
「何でも潰せるなら、全部1点になって、区別が消えてしまうのでは？」と思われたでしょうか。
ここが、いちばん面白いところです。潰しきれない形が、あるのです。
輪っか（指輪の輪の部分だけを取り出した、中身のない 1 本の閉じた線）を考えてください。
これをどう縮めても、1点にはできません。
縮める途中で、まんなかの穴を線が横切らなければならなくなりますが、輪の外の空間は使えないというルールのもとでは、それができない。輪は、小さくはなっても、輪のままで止まります。
同じことが、いろいろな形で起こります。
トイレットペーパーの芯（筒）を潰していくと、やはり輪の形で止まります。
まんなかに丸い穴を開けた 1 枚の紙も、穴のふちに向かって縮めていくと、輪になって止まります。
膜としての円盤・筒・穴あきの紙は、見た目も次元もばらばらなのに、潰した先に残る形 で分ければ、筒と穴あき紙は「輪」の仲間、円盤は「点」の仲間、ときれいに二手に分かれるのです。
この、「連続変形でどこまで潰せて、どんな形で止まるか」という骨組みの情報 を扱う数学の正式な概念は、ホモトピー型 と呼ばれています。
「骨組み」という言い方は、それを直感的に言い表すための、この記事の比喩です。
長さも、角度も、次元も、潰す過程で消えてしまう情報はすべて捨てる。
それでも消えなかった骨組みだけで形を分類する
── これが、ホモトピー理論 という分野の名前の由来であり、その一貫した戦略です。
📌 中上級者向け補足：厳密性を担保した説明をすると ── 「骨組み」は比喩である
本文では、空間を連続変形して「どこまで潰せるか」「何が残るか」に注目し、その残ったものを「骨組み」と呼びました。
これはホモトピー型をイメージするための比喩です。
ホモトピー型そのものが、空間の中に実際の骨組みとして存在するわけではありません。
数学的には、ホモトピー同値という関係によって空間を分類 し、同じホモトピー型を持つ空間を同じ仲間として扱います 。
また、「空間を縮める」という現象にも、変形レトラクト や 強変形レトラクト など、より具体的な数学的概念があります。円盤を 1 点へ縮める、といった例は、こうした具体的な変形をイメージするのに適しています。
したがって、本文の「骨組み」という言葉は、厳密な専門用語ではありません。
「連続変形によって区別されなくなる細かな違いを捨てたとき、それでも残る本質的な形の情報」 を入門者向けに見える形へ翻訳した比喩です。
5-4. 骨組みと、道の数えあげが、つながる
ここで、第3節の「池のある広場」を思い出してください。
あの広場は、まさに「まんなかに穴を開けた紙」でした。
そして穴のせいで、2点をつなぐ道の種類が、巻きつき回数の分だけ枝分かれしていました。
つまり、こういうことです。
- 骨組みが「点」に潰れる空間（穴がない）では、道の種類は枝分かれしない。等しさの証拠は実質1通り。
- 骨組みに「輪」が残る空間（穴がある）では、道の種類が巻きつき回数の分だけ枝分かれする。等しさの証拠が無限に並ぶ。
形の骨組みを調べることと、等しさの証拠を数えあげることが、同じ作業の表と裏になっている
── これが、Poincaré に始まる形の分類の問題と、第2節の風変わりな宣言とが、がっちり噛み合う場所です。
ちなみに Poincaré 自身、1895 年のその論文で、まさに「空間の中のループを分類する」道具を導入しています。等しさの証拠を数えるという発想は、この分野の生まれた瞬間から、中心にあったのです。
6. まとめ — そして、意外な続きへ
この記事で見てきたことを、3つにまとめます。
-
ホモトピー理論 は、「もの」を空間の点として置き、「a と b は等しい」を a と b をつなぐ道 として描く世界観です。等しさは「はい / いいえ」の判定ではなく、数えられる証拠を持つ実体になります。
- 穴のある空間では、同じ2点のあいだに、互いに取り替えのきかない道が何種類も並び立ちます。さらに、道と道の等しさ、そのまた等しさ……と、等しさの階層はどこまでも積み上がります。
- この見方は、形をゆるく比べて分類したいという、19世紀末以来の問題意識から生まれました。連続変形で潰しきれずに残る 骨組み が形を分類し、その骨組みは、等しさの証拠の数えあげ として読み取れます。
ここまで、ずっと 数学の世界 を歩いてきました。
最後に、ひとつだけ予告をさせてください。
実は、この空間的な眼差しは、数学の外にも成立する場所があります。
プログラミング言語のデータ型 です。
整数型や文字列型といった、プログラマが毎日使っているあの「型」を空間とみなし、値を点、値どうしの等しさを道として扱う
── ここまで見てきた ホモトピー理論 を、プログラミング言語の型理論 に丸ごと取り入れた ホモトピー型理論（Homotopy Type Theory 、略して HoTT ）という理論があります。
2007 年頃から研究が始まった、まだ 20 年に満たない新しい理論です5。
型 が 空間 だとしたら、皆様が普段使っている型は、穴のない退屈な広場なのでしょうか。
それとも、池のある広場のような型も存在するのでしょうか。
詳しくは、次回の2回目の記事で扱います。
この先の議論のロードマップ
連載シリーズではないのですが、これから、それぞれ独立した単独記事を書いていきます。
単独記事ですが、各記事のテーマは数珠つなぎのように連なっています。
各記事を順番にお読みいただけると、関数型言語・定理証明言語の言語理論研究のひとつの最前線に広がっている景色まで、道がつながっていることを体験いただけます。
【ここから先のロードマップ】
脚注
参考文献・リンク
- The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics（通称 HoTT Book）, 2013. https://homotopytypetheory.org/book/
- Henri Poincaré, Analysis Situs, 1895.（位相幾何学の出発点となった論文。本文 5-1 節で触れたものです）
-
数学ではこの線のことを 道（path、経路とも訳されます）と呼びます。正式には「区間から空間への連続写像」として定義されますが、この連載の本文では「鉛筆を離さずになぞった線」という理解で通します。 ↩
-
この積み上がった階層のうち、どの高さまで実質的な中身が残っているかを数える指標が HoTT には用意されており、h-level と呼ばれます。本連載の地の文ではこの数え方に立ち入らず、「階層が積み上がる」という描像だけで話を進めます。 ↩
-
この厳しい基準は、正式には 同相 と呼ばれます。 ↩
-
この緩い基準は、正式には ホモトピー同値 と呼ばれます。 ↩
-
基礎となる研究は 2006 年から 2009 年頃にかけて複数の研究者によって独立に進められ、2013 年に刊行された解説書（通称 HoTT Book）によって、分野としての形が定まりました。 ↩