はじめに
「２つのものが等しい」という言い方には、実は複数の意味があります。
同じ書類で本人確認された「同じ顧客」と、メールアドレスの一致から推定した「同じ顧客」。この２つの「同じ」は、根拠がまったく違います。
それでも私たちの書くプログラムの多くは、この区別を捨てて、一本の「同じ」に潰してしまいます。
数学の世界には、「複数の等しさ」を潰さずに、区別したまま扱うための理論 があります。
ホモトピー型理論（HoTT、ホット） と呼ばれる、2013年前後に形になった新しい数学です。
そして、その理論を実際にコンピュータの上で動かせるプログラミング言語があります。
Cubical Agda（キュービカル・アグダ） です。
cubical は、「立方体の」という意味の英語 です。
等しさ を 「道」として 扱い、道どうしの関係を正方形や立方体の形に載せて計算する理論 を土台にしていることが、名前の由来です（由来の中身は、第３部で説明します）。
Cubical Agda の土台になっているのは、Agda（アグダ）という言語 です。
依存型（いぞんがた） という仕組みを使って、プログラムと数学の証明を同時に書くために作られました。
ふだんのアプリケーション開発ではなく、正しさを数学的に保証したい分野
── とりわけ、大学や研究機関でのプログラミング言語の研究 ──
で使われてきた言語です。
この言語には、ビジネスでの利用事例がほぼありません。
筆者はこれまで、定理証明やプログラム検証の言語について、ビジネスでの使い道まで含めた入門記事を書いてきました。
その筆者が調べても、Cubical Agda を製品開発に使った企業事例は見つけられませんでした。
では、なぜ紹介するのか。
事例が無い理由そのものが、この言語の設計思想を語っている からです。
詳しくは第１部で説明しますが、先に一言でまとめます。
この言語は、実務の資産を増やすことではなく、数学の理論そのものを試験する場であることを、自分の役割として選んでいます。
事例の無さは、言語として成功しなかったがゆえの結果ではなく、言語として何を優先したかの取捨選択の結果 です。
そして、企業事例が無いにもかかわらず、世界の研究者たちがこの言語の上で新しい数学を検証し続けている
── その理由を知ると、プログラミング言語と数学の関係が、一段深く見える ようになります。
本記事は、Agda も、定理証明も、HoTT も学んだことのない Python エンジニアの方に向けて、前提知識ゼロからこの言語の存在理由を説明する記事です。
この記事の全体像 ── 順路と結論を最初に
結論を先に述べます。
Cubical Agda は、「２つのものが等しい」という事実を、成り立つか成り立たないかの二択ではなく、「どんな根拠で等しいのか」という証拠ごと扱えるプログラミング言語の代表格です。
証拠は１つとは限らず、別々の証拠は別々のものとして扱われます。
ビジネス事例が無いのは欠陥ではなく、この言語が「理論の試作台」という役割を選んだ結果です。
そして、HoTT には、「同じ振る舞いをする２つのものは、等しいものとして取り替えてよい」という中心原理 があります（ 一価性（いっかせい） と呼ばれます）。
この文言は、一見すると「違いを潰して、一本の等しさにまとめる」話に聞こえます。
実際は逆 です。
一価性 は、等しさの証拠を増やす原理 です。
２つのものの振る舞いを同じにする、崩れの無い１対１の対応が見つかるたびに、その対応の１つ１つが、それぞれ別々の「等しさの証拠」になります。
別々の対応からは、別々の等しさの証拠が生まれる
── 先ほどの 「複数の等しさ」は、この原理から供給される のです。
多くの処理系は、この原理を公理として導入してきました。
公理 とは、自明のこととみなして、証明抜きで正しいと認める約束事です。
Python でいえば、関数名だけ決まっていて、中身が書かれていない状態です。
呼び出すことはできますが、「どう計算するか」が書かれていないので、そこから先へは進めません。
公理 も同じで、「これは正しい」と約束するだけで、「どう計算するか」という説明は与えません。
そのため、公理を使った証明は書けても、最後まで計算を進められないことがあります。
Cubical Agda は、この原理そのものを、中身のあるコードとして実装 しました。
つまり、「正しいと約束するだけ」だったものを、「どう計算するか」まで実装した のです。
だから、一価性を使った証明でも最後まで計算を進めることができます。
実物をお見せします。
「２つのものが等しい」ことの証拠が２通り あって、その違いが計算結果に現れる
── 最小の実演です。
Agda のコードを初めてご覧になる方に向けて、コードの下で全行を解説します。
{-# OPTIONS --cubical #-}
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Univalence
open import Cubical.Data.Bool
sameWay : Bool ≡ Bool
sameWay = refl
flipWay : Bool ≡ Bool
flipWay = ua notEquiv
checkSame : transport sameWay true ≡ true
checkSame = refl
checkFlip : transport flipWay true ≡ false
checkFlip = refl
最初に、語の区別を伝えます。
このコードのうち、sameWay、flipWay、checkSame、checkFlip の４つは、プログラマ（筆者）が自分の好きな名前を任意に付けた箇所 です。
別の名前に変えてもコードは同じように動きます。
それ以外の語は、予約語 か、読み込んだライブラリが提供する名前 で、どれがどれかは読みながらそのつど示します。
そのうえで、全体の形から説明します。
このコードは、「準備」「２つの等しさの定義」「２つの確認」の３つのブロック でできています。
そして、このコードに登場する定義はすべて、「名前 : 型」の行と、「名前 = 中身」の行の２行セット で書かれています。Agda で定義を書くときの、よく使われる形です。
Python の型ヒント付きの代入 x: int = 42 を、宣言と代入の２行に分けた形だと思ってください。
ただし、Python と決定的に違う点が１つあります。
Agda では、型 の欄に、「〜は〜と等しい」のような主張 を記述することができます。
そして、型 の欄に主張を書いた場合、中身の欄に書くべきものは、その主張の 証拠 です。
この対応 だけ頭に置いて、上から読んでいきます。
最初の１行は、機能の有効化です。
{-# OPTIONS --cubical #-} は「このファイルでは Cubical の機能を使う」という処理系への指定で、Python のファイル先頭に書く from __future__ import annotations のような役回りです。
続く３行は、道具の読み込みです。
open import は Python の import にあたります。
open が付いているので、読み込んだ部品をモジュール名なしでそのまま使えます（Python の from ... import * に近い書き方です）。
Cubical.Foundations.Prelude からは ≡ と refl と transport が、Cubical.Foundations.Univalence からは ua が、
Cubical.Data.Bool からは Bool と true と false と notEquiv が、それぞれ手に入ります。
sameWay の２行が、１つ目の等しさです。
宣言の行 sameWay : Bool ≡ Bool は、「sameWay の型は、『Bool と Bool は等しい』という主張である」と読みます。
中身の行の refl は、ライブラリの部品で、「左右を計算すると、まったく同じ形になる」ことを根拠にした、等しさの証拠 です。
つまりこの２行は、「Bool と Bool は等しい」という主張に、「そのまま重ねる」という証拠を与えています。
flipWay の２行が、２つ目の等しさです。
宣言の行の型は、sameWay とまったく同じ「Bool と Bool は等しい」という主張です。
違うのは中身です。
notEquiv は、ライブラリに登録済みの部品で、「true と false を入れ替える」という対応 と、その対応が崩れの無い１対１の対応であることの証明を、ひとまとめにしたもの です。
そして ua は、一価性の原理を利用して、崩れの無い１対１の対応から「等しさの証拠」を作り出す、ライブラリの関数 です。
この関数の名前には、小さな物語があります。
ua は、一価性 の英語名 univalence axiom（一価性の公理）の略に由来する名前 です。
公理だった時代の名前を受け継ぎながら、Cubical Agda の ua の中では、Glue（グルー）と呼ばれる機構が実際の計算を担っています。
公理の名前を継いだ関数が、中では計算で動いている
── この言語の発明は、名前のギャップにも刻まれています。
なお、Agda では関数の呼び出しを ua notEquiv のように空白で並べて書きます。
Python でいう ua(notEquiv) です。
つまり flipWay は、「入れ替え」という対応から ua が作り出した、もう１つの等しさの証拠 です。
同じ主張に、別々の根拠の証拠が２つ並びました。
checkSame の２行は、１つ目の確認です。
ここで transport が登場します。
transport は、２つの引数 ── 等しさの証拠と、値 ── を受け取る関数です。
この実演の範囲では、「証拠が表す対応にしたがって、受け取った値を変換する関数」と理解すれば十分 です。
宣言の行の transport sameWay true は、Python でいう transport(sameWay, true) で、「true を sameWay の対応で変換した結果」を指します 。
型の全体は「その結果は true と等しい」という主張 で、中身の refl が「実際に両辺を計算すれば、同じ値になる」という証拠 です。
最後の checkFlip の２行が、この実演の頂点です。
主張内容は、「true を flipWay で変換した結果は、false と等しい」 。
入れ替えの対応を通るので、答えが false に変わります。
どの証拠を渡したかによって、計算の答えが変わるのです。
そして、中身はここでも refl です。
refl は、機械が左辺の計算を実際に最後まで進めて、右辺と同じ値に到達したときにだけ、コンパイルに通ります。
一価性が公理（中身の無い関数）の処理系では、この計算が途中で詰まるため、同じ行は通りません。
checkFlip がコンパイルに通ること自体が、「一価性を使った証明を、最後まで計算できた」という動かぬ証拠なのです。
まとめると、このコードでプログラマが自分で名付けたのは、sameWay、flipWay、checkSame、checkFlip* の４つだけです。
open、import は 予約語、{-# OPTIONS --cubical #-} は 指定の書式 です。
残りの Bool、true、false、≡、refl、ua、notEquiv、transport は、いずれも読み込んだ Cubical ライブラリが提供する名前 です。
Bool と Bool のあいだの崩れの無い１対１の対応は、「そのまま」と「入れ替え」の２通り です。
一価性は、その１つ１つから、別々の等しさの証拠を作ります
── 一価性が証拠を供給する、という先ほどの話の、これが実物 です。
同じ「Bool と Bool は等しい」という主張に、計算結果まで違う２つの証拠が共存 する
── 冒頭の「複数の等しさ」は、このような形でコードになります。信じるだけだった原理を、動くコードに変えた ── これが、この言語の最大の発明です。
順路は次のとおりです。
本記事では、研究者が実際に行った実例と、筆者が独自に考えたアイディアを、読者が区別できるように書き分けます。
実例には出典を付けます。
筆者のアイディアには 【筆者の構想】 という標識を付けます。
標識の無い主張は、出典で確認できる範囲に限定します。
想定読者
- Python は書けるが、定理証明・形式検証の言語（Lean 4、Rocq、Agda など）は学んだことがない方
- 「等しさが複数ある」という言葉に、何のことか分からないなりに、引っかかりを感じた方
- AI と数学の関係、あるいはプログラミング言語の理論の最先端に関心がある方
数学の予備知識は仮定しません。本文中の専門用語は、登場する前にすべて日常の言葉で組み立てます。
この記事を読む価値
- Cubical Agda とは何か、なぜビジネス事例がほぼ無いのかを、理由の階層（設計目的・自動化・問題の性質）まで含めて説明できるようになる
- 「等しさの証明を、値のように持ち回る」という HoTT の中心発想を、コード例と日常の比喩で理解できるようになる
- 一価性という原理が「公理として置くと計算が止まり、Cubical Agda は計算できる形で実装した」という、この言語の存在理由が分かるようになる
- 円周 S¹ の定義など、他の主流言語では直接書けない種類のコードを、１行ずつ読めるようになる
- 球面のホモトピー群の機械計算や、バージョン管理の数理モデル化など、研究の実例を出典つきで知ることができる
- 「理論の実例」と「筆者の構想」を区別して受け取る読み方 ── 形式手法の記事を読むときの基本姿勢 ── が身につく
TL;DR
（この節の専門用語は、いずれも本文で説明します）
- Agda は、依存型という仕組みでプログラムと数学の証明を同時に書ける言語で、タクティク（証明の自動組み立ての指示）に頼らず、証明そのものを関数として直接書くスタイルに個性がある
- Cubical Agda は、プログラミング言語 Agda の拡張で、ホモトピー型理論（HoTT）を実際に動かせる処理系の代表格である
- HoTT は、「a と b は等しい」を、成り立つか成り立たないかの二択ではなく、「どんな根拠で等しいのか」という証拠ごと扱う数学である。証拠は複数ありえて、別々の証拠は別々のものとして区別される
- Cubical Agda の最大の発明は、HoTT の看板原理である一価性を、公理としてではなく計算できる部品として実装したことである
- HoTT の形式化には Rocq（旧名 Coq）側にも歴史あるライブラリ（Coq-HoTT と、創始者ヴォエヴォドスキー本人が始めた UniMath）がある。そちらは一価性を公理として置く。どちらが主流かを示す統計は無い。検査済みの理論を書き溜める役割を Rocq が、証明を実際に計算して動かす実験の役割を Cubical Agda が担う、という分業と見るのが正確である
- AI が定理証明を訓練場にする流れの中心は Lean 4 で、Agda を専業とする求人は筆者の調べた範囲で見当たらない。Agda で身につく素養が他の証明言語の仕事へ持ち運べる、というのが筆者の予想である
- ビジネス利用の公開事例は、筆者の知るかぎりほぼ存在しない。理由は、この言語が実務資産の蓄積ではなく理論の試作台という役割を選んでいるからである
- 研究の実例は存在する ── 球面のホモトピー群の機械計算、バージョン管理のパッチを「等しさの証拠」としてモデル化した研究（2014年）など
- 本記事の後半には、筆者が独自に考えたビジネスへの示唆を【筆者の構想】の標識つきで書く。実例と構想の区別は、標識で明示する
筆者のこれまでの記事について
本記事は単独で読めるように書いてあります。
この節は、筆者が書いてきた関連記事の地図です（読み飛ばして構いません）。
筆者はこれまで、「数学の証明を機械が検査する」という世界の言語たちを、Python エンジニア向けにひとつずつ紹介してきました。
-
Lean 4 とは何か ── 定理証明系の現在の主役。AI が数学オリンピックに挑む舞台裏と、業務要件の検証への応用を書きました。本記事と最も関係が深い一本です
-
λProlog とは何か ── 定理証明系 Rocq の内側で働く論理プログラミング言語の話です
-
F* とは何か ── 型に条件を書き込める言語（篩型）と、その業務応用の話です
- HoTT 連載（第１回）・HoTT連載（第２回） ── 本記事の主題である「複数の等しさ」の数学そのものを扱う連載です。本記事は、この連載の理論を「動かす」side story にあたります
本記事だけで話は完結しますが、Lean 4 の記事を先に読むと、本記事の「Lean 4 の標準の設計では採用されていないこと」という論点が、より立体的に見えます。
まず、Agda とはどんな言語か
Cubical Agda の話に入る前に、土台の Agda そのものの位置づけを説明します。
Agda を一言でまとめると、依存型という仕組みを使って、プログラムと数学の証明を同時に書くための言語 です。現在の Agda（Agda 2）は、スウェーデンのチャルマース工科大学で2007年に生まれました。
型が、値に依存する ── 依存型の威力を１つだけ
依存型とは、値を含んだ型 を書ける仕組みです。威力の分かる定番の例をお見せします。
Python でリストの先頭要素を取る関数を考えてください。空のリストを渡せば、実行時エラーになります。エラーが出るのは、動かした後です。
Agda では、次の型が書けます。
open import Data.Nat
open import Data.Vec
first : {A : Set} {n : ℕ} → Vec A (suc n) → A
first (x ∷ xs) = x
上から読みます。
最初の２行は、道具の読み込みです。
Data.Nat からは 自然数の型 ℕ が、
Data.Vec からは 長さつきリストの型 Vec と、先頭に要素を加える演算子 ∷ が手に入ります。
宣言の行を読みます。
波括弧の {A : Set} {n : ℕ} は 「A は型、n は自然数」という引数 です。
波括弧で囲まれた引数は、呼び出すときに書かなくても、機械が文脈から推測して埋めてくれます（暗黙の引数と呼ばれます）。
本体は、Vec A (suc n) → A の部分 です。
Vec A (suc n) は 「長さが suc n（＝何かの数 n に１を足した数、つまり１以上**）の、A のリスト」という型** です。
長さという値が、型の一部に入っています ── これが 依存型 です。
中身の行は、等式が１本だけです。
first (x ∷ xs) = x は、「先頭が x で、残りが xs のリストを受け取ったら、x を返す」という定義 です。
注目すべきは、空リストの場合の行が、書かれていない ことです。
型が「長さ１以上」と約束しているので、空リストの場合分けはそもそも起こりえず、書かなくても機械が網羅済みと認めます。
この型のおかげ で、first に空のリストを渡すプログラムは、実行する前に、コンパイルの段階で弾かれます。
実行時エラーを検査で捕まえるのではなく、間違ったプログラムを最初から書けないようにする ── correct by construction（構成による正しさ）と呼ばれる考え方です。
このコードの中で、プログラマが自分で名付けたのは、first、A、n、x、xs です。
open、import、波括弧、→、= は予約語と記号 です。
Data.Nat、Data.Vec、Set、ℕ、Vec、suc、∷ は、いずれもライブラリが提供する名前 です。
証明を、関数として直接書く ── タクティクを使わないスタイル
定理証明の言語 の多くは、タクティクという道具 を持っています。
「この方針で証明を組み立てよ」と機械に指示する命令の言葉 で、Lean 4 や Rocq の証明は、タクティクの列として 書かれます。
Agda の証明の書き方は、これと異なります。
タクティクに頼らず、証明そのものを関数（プログラムの部品）として、手で直接書きます。
途中の書きかけ部分は「穴」として残し、処理系と対話しながら埋めていく ── そういう作法です。
この個性は、教育の現場で実証されています。
プログラミング言語理論の教科書 PLFA （ Programming Language Foundations in Agda、ウォードラーらによる無料公開の教科書）は、それまでの定番だった Rocq（当時 Coq） ベースの教科書を「タクティクの学習に時間を取られ、肝心の言語理論の学習が薄くなる」という理由で Agda に置き換えた本です。
著者らは、タクティク無しでも証明の長さは同程度に収まり、しかも 証明を紙面の上でそのまま読める と報告しています。
ただし、同じ著者らはこうも認めています ── 本格的な数学の大規模な形式化には、タクティクを持つ処理系のほうが向いている、と。
この取引の話は、第１部でもう一度出てきます。
定理証明の言語たちの、住み分け
筆者がこれまで紹介してきた言語たちと並べると、Agdaの立ち位置 が見えてきます。
-
F* ：SMT ソルバという自動証明の火力を活用した、ソフトウェア検証（セキュリティ分野の実績）
-
Lean 4 ：数学ライブラリ Mathlib の蓄積を土台にした、数学の形式化と、業務検証への応用
-
Rocq（旧名 Coq） ：証明からプログラムを取り出す性質を生かした、コンパイラや暗号などの検証済みソフトウェア
-
Idris 2 ：依存型を日常のプログラミングに使うことを目指した、実務寄りの言語
- Agda ：依存型プログラミングそのものを、混ぜ物なしで学び、試すための言語。プログラミング言語の研究論文では、「証明は Agda で機械化した」と添えられることがあります
つまり Agda は、プログラムと証明を一体として設計する考え方を、いちばん純粋な形で体験できる言語 です。
この純度が、次の第１部で述べる「ビジネス事例の無さ」と、第３部で述べる「HoTT との相性」の、両方の源泉になっています。
第１部 ── なぜビジネス事例が、ほぼ無いのか
最初に、いちばん答えにくい問いに答えます。
Cubical Agda をビジネスの製品開発に使った公開事例を、筆者は見つけられませんでした。
これは調査不足ではなく、構造的な理由があります。
理由は３つの層に分かれます。
理由１：この言語は「理論の試作台」という役割を選んでいる
プログラミング言語には、それぞれ役割があります。
たとえば、定理証明系の主役である Lean 4 には、Mathlib（マスリブ）という巨大な数学ライブラリ があり、世界中の貢献者が検査済みの定理を毎日積み上げています。
実務で定理を使いたい人は、この蓄積をそのまま呼び出せます。
Agda のコミュニティは、これとは違う道を歩んできました。
Agda が磨いてきたのは、蓄積の量ではなく、言語の土台の純度 です。
新しい型システムの理論を思いついた研究者が、そのアイディアを最初に試す場所 ── それが Agda の役割でした。
試作台に求められるのは、余計な混ぜ物が無いことです。
実務の便利さのために理論の純度を落とす、という取引を、この言語は原則として行いません。
事例が無いのは、事例を作る方向に言語が向いていないからです。
これは欠陥ではなく、分業です。
理由２：自動証明の火力を、意図的に持たない
定理証明の言語には、「ボタンひとつで機械が証明を探してくれる」自動化の道具を持つものがあります。
自動化が強いほど、人間の書く量は減り、実務のコストは下がります。
逆に言えば、自動化の弱い言語で証明を書くことは、人件費の高い仕事になります。
Agda は、自動化の弱い側の言語です。
証明は基本的に、人間が手で、一歩ずつ書きます。
これも設計の選択です。
自動化の機械を強くするには、論理の側を automation 向きに単純化する取引が必要になることが多く、Agda はその取引よりも、土台の理論をそのまま書ける表現力を選びました。
研究者にとって、手で書けることは苦になりません。
理論の一歩一歩を自分の目で確かめることが、研究そのもの だからです。
しかし 企業にとって、証明の人件費は直接のコストです。
この一点だけでも、業務利用のハードルは高くなります。
理由３：HoTT が扱う問題を、産業は「潰す」ことで済ませてきた
３つ目の理由が、いちばん深いものです。
本記事の主題である HoTT は、「等しさが複数ある状況」を厳密に扱う数学です。
ところが産業の現場は、この状況を昔から知っていながら、理論で扱わずに、運用で潰してきました。
冒頭の顧客データの例を思い出してください。
本人確認による「同じ」と、メール一致の推定による「同じ」。
実務のシステムの多くは、この区別を保存せず、統合した結果だけを残します。
区別を潰しても、多くの場合は困りません。
困るのは、誤った名寄せが起きたときや、監査で統合の根拠を説明できないときです。
つまり、たまにしか困らない。
たまにしか困らない問題のために、人件費の高い言語と最先端の数学を導入する
── この投資判断が成立しないことは、ビジネスの側から見れば自然です。
事例が無いことは、理論が無価値であることを意味しません。
問題の痛みが、まだ投資に見合う形で顕在化していない、ということです。
以上の３層が、答えです。
ここから先は、「では、この言語は何のために存在し、何に使われているのか」という本題に入ります。
第２部 ── では、何に使われているのか
Agda の主戦場は、プログラミング言語と論理学の研究の世界 です。
新しい型システムを設計した研究者が、その性質を Agda の上で形式化して確かめる。
世界中の大学の研究室で、Agda はそういう試作台として動いています。
そして 2010年代、この試作台の上に、ひとつの大きな理論が載りました。
それが ホモトピー型理論（HoTT） です。
HoTT は、数学者ウラジーミル・ヴォエヴォドスキーらの仕事を起点に、2013年に共同執筆の教科書（通称 HoTT Book）としてまとまった、新しい数学の土台の候補 です。
この理論の検証実験の主要な現場になったのが、Agda とその拡張である Cubical Agda でした。
有志によるライブラリ（agda/cubical）が GitHub 上で育てられ、HoTT の定理が機械検査つきで積み上げられています。
なぜ、数ある言語の中で Agda だったのか。
答えは「相性」にあります。
次の第３部で、その相性を、専門用語を使わずに組み立てます。
第３部 ── Agda と HoTT の相性:「等しさの余地」の物語
型理論というアイディア ── 証明を、型検査として扱う
まず、土台の考え方をひとつだけ説明します。
定理証明系と呼ばれるソフトウェアは、数学の証明をプログラムのコードとして書き、その正しさをコンパイラのような検査器で確かめる道具です。
鍵になる発想は、「型」と「主張」を同じものとして扱う ことです。
Python の型ヒント int は「この変数には整数が入る」ことしか言えません。
しかし型の仕組みを深くすると、「すべての自然数 $n$ について $n + ０ = n$ が成り立つ」のような 数学の主張そのもの を、型として書ける ようになります。
そして、その型を持つプログラムを書けたなら、それが 証明 です。
この 「証明も計算も、同じ材料で書く」という設計 の元祖のひとつが、1970年代にスウェーデンの論理学者ペール・マルティン=レーフが作った理論です（ マルティン=レーフ型理論 と呼ばれます）。
Agda は、この理論をほぼそのまま言語にした処理系です。
混ぜ物の少なさが、第１部で述べた「試作台の純度」の正体です。
等しさの「余地」── Agda の土台に残されていた空き地
ここからが、相性の核心です。
「 $２ + ２ = ４$ 」を証明したとします。
証明のしかたは、原理的には何通りもありえます。
では、証明どうしは区別するべきでしょうか。
主流の定理証明系のひとつである Lean 4 は、「区別しない」と決めた設計 です。
等しさの証明は、何通り書いても同じ一個として扱う。
この割り切りのおかげで、検査は軽く、速くなります （この設計は「証明の無関係性」と呼ばれます）。
一方、マルティン=レーフの理論そのもの ── つまり Agda の土台 ── は、この点を 決め打ちしていません。
等しさの証明を、値のように区別して持ち回れる 余地が、理論の設計に最初から残されていた のです。
長いあいだ、この余地は「理論上の空き地」でした。区別できたとして、何に使うのか、誰も知らなかったからです。
HoTT が空き地に注いだもの ── 等しさは「道」である
2000年代後半、数学者たちがこの空き地の使い道を発見します。
等しさの証明を、２つの点を結ぶ「道」として読む ── という読み替えです。
$a$ と $b$ が等しいことの証明は、点 $a$ から点 $b$ への道である。
道は複数ありえる （山を北から回る道と、南から回る道）。
道と道のあいだにも「道の変形」が考えられる。
この読み替えを徹底すると、等しさの階層の全体が、ホモトピー論という幾何学の言葉と正確に対応する ── これが HoTT の出発点 です。
なぜ、論理の話をしていたはずなのに、図形の世界に入るのでしょうか。
理由は、語彙が同じ形をしているから です。
点があり、点と点を結ぶ道があり、道と道のあいだの変形がある
── この３つ揃いは、幾何学がゴムひもの伸び縮み（連続変形）で図形を調べるときの、基本の語彙そのものです。
等しさの証明を道と読み替えた瞬間に、型はひとつの図形と同じ構造を持ちはじめます
── 要素は点、等しさの証明は道、証明どうしの等しさは道の変形、という対応 です。
そして 幾何学の側 には、ホモトピー論 という、道と変形を１世紀以上調べてきた分厚い蓄積 があります。
構造が同じなら、その定理と道具をそのまま借りられる
── 図形の世界に入るのは、絵のためではなく、この蓄積を借りるため なのです。
Agda の空き地は、まさにこの読み替えの受け皿 でした。
等しさの証明を区別できる理論だけが、「複数の道」を語れる からです。
証明を区別しない設計（Lean 4）では、道は常に一本に潰れます。
だから Lean 4 の標準的な理論基盤の上では、HoTT は展開できません
── 軽さと速さを選んだ設計の、裏面です。
歴史的ないきさつについて、若干の補足をします。
旧世代の Lean 2 には、証明の区別を潰さない HoTT 用の動作モードがあり、その上で HoTT ライブラリが作られていました。
Lean 3 以降は現在の設計に一本化され、この道は閉じられています。
また、Cubical の仕組みを Lean に載せた処理系は、筆者の知るかぎり存在しません。
「Lean で HoTT はできないのか」という自然な疑問への、これが現在の答えです。
Cubical の発明 ── 公理ではなく、計算できる部品として
HoTT には、看板となる原理があります。
一価性（いっかせい、univalence） です。
日常の言葉に開けば、「同じ振る舞いをする２つの構造は、等しいものとして取り替えてよい」という原理です。
リストで実装した辞書と、木構造で実装した辞書
── 外から見た振る舞いが同じなら、数学の上でも等しいと扱ってよい、という許可証です。
全体像の節で述べたとおり、この許可証は、振る舞いを同じにする対応の１つ１つに発行されます。
対応が複数あれば、等しさの証拠も複数生まれる
── 一価性は、本記事の主題である「複数の等しさ」の供給源でもあります。
問題は、この原理の入れ方でした。
最初期の HoTT では、一価性を 公理 として置いていました。
公理 とは、「証明は示さないが、成り立つと認めてくれ」という宣言です。
公理には代償があります。公理に頼った証明は、そこで計算が止まる のです。
証明をプログラムとして実行しようとしても、公理の部分だけ中身が無いため、機械は先へ進めません。
2019年に発表された Cubical Agda は、この問題への回答でした。
等しさを「道」として扱う 計算規則を、言語の内部に直接組み込む。
その結果、一価性が、公理ではなく、証明できて計算もできる部品になった
── これが Cubical Agda の最大の発明です。
はじめにで予告した、名前の由来もここにあります。
道は１次元の線です。
道と道の変形は、２次元の正方形に張られます。
その変形どうしの関係は、３次元の立方体に
── と、あらゆる次元の立方体を基本部品にして計算の規則を定める理論（ キュービカル型理論 と呼ばれます）が、この言語の土台です。
cubical（立方体の）という名前は、この部品の形から来ています。
琥珀の中に空洞を作らず、一価性入りの証明が最後まで実行できる。
この一点が、世界中の HoTT 研究の実験がこの言語の上で行われている理由です。
HoTT の家は、もうひとつある ── Rocq のライブラリとの比較
正確を期すために、書いておくべきことがあります。
HoTT を形式化できる場所は、Agda だけではありません。
定理証明系 の世界には、Rocq （ロック。旧名 Coq （コック）として知られる、1980年代から続く老舗の言語）があります。
そして歴史の順で言えば、HoTT の形式化は Rocq 側のほうが先輩です。
HoTT Book がまとまった2013年前後、理論の検証の主要な現場は当時の Coq でした。
現在も、Coq-HoTT と UniMath という２つの大きなライブラリが Rocq の上で育てられています。
UniMath には、特筆すべき事実があります。HoTT の創始者であるヴォエヴォドスキー本人が始めたライブラリ だという点です。
理論の生みの親の本拠地は、Agda 側ではなく Rocq 側にあったのです。
では、両者は何が違うのか。
核心は、第3部でずっと話してきた一点 ── 一価性の入れ方 です。
-
Rocq 側（Coq-HoTT、UniMath） ：
一価性を 公理として置きます。
全体像の節の言葉でいえば、関数名だけあって中身の無い関数の扱いです。
理論を書き溜め、正しさを検査することはできますが、中身が無い部分で計算が止まるため、証明を実行して値を取り出せない場面が生まれます。
円周のような「道つきの型」も、言語の正式機能ではなく、工夫を重ねて実現しています
-
Cubical Agda ：
一価性が 証明できて、計算します。
道つきの型も言語の正式機能です。
代わりに、処理系としての歴史は2019年からと浅く、蓄積の規模と自動化の道具では Rocq の生態系に及びません
表にまとめます。
| 観点 | Rocq（Coq-HoTT / UniMath） | Cubical Agda |
|---|---|---|
| 一価性の扱い | 公理として置く（計算は止まる） | 証明できて、計算する |
| 道つきの型（高階帰納型） | 言語の正式機能ではなく、工夫で実現 | 言語の正式機能 |
| 蓄積の歴史 | 2013年前後からの大きな蓄積。創始者本人のライブラリを含む | 2019年からの若い蓄積 |
| 向いている仕事 | 理論を書き溜める、大規模な形式化 | 道の計算を、実際に実行する実験 |
なお、上記の比較表に Lean 4 が登場しない理由 は、先ほど述べたとおりです
── 標準的な理論基盤が証明の区別を潰す設計のため、公理側にも計算する側にも、席が無い のです。
では、どちらが HoTT の本命なのでしょうか。
利用者数や採用数の統計は存在せず、主流を断定することはできません。
筆者に言えるのは、役割の違いまでです。
検査済みの理論を書き溜めて保管する、図書館の書庫のような役割では、Rocq 側に歴史と規模があります。
一方、「一価性を計算させる」という研究課題の実験場としては、Cubical Agda が代表格です。
第５部で紹介するブルネリ数の機械計算のような、実行して値を取り出す種類の成果は、計算する側の Cubical Agda から生まれています。
本記事が Agda 側を主役に選んだ理由も、この一点にあります。
公理で止まる証明と、最後まで動く証明の違い
── それがこの記事の物語の背骨だからです。
両者は敵同士の関係ではなく、書庫と実験場という分業関係のもとにあります。
研究の現場では、どう使い分けられているのか
利用の統計はありませんが、それぞれのライブラリの上で実際に行われている仕事の性格から、使い分けの形は読み取れます。
定理を書き溜める仕事は、公理側のライブラリで行われています。
圏論や代数のような数学の体系を、一価性の言葉で大規模に形式化する
── UniMath が担ってきたのは、この種の仕事です。
この仕事では、証明を実行して値を取り出す場面がそもそも無いため、公理で計算が止まることは弱点になりません。むしろ、Rocq の成熟した処理系と自動化の支援が効きます。
値を取り出す仕事は、計算する側でしか行えません。
第５部で紹介する ブルネリ数の機械計算 のように、証明を実行した結果の数値そのものが成果になる研究です。
一価性が計算する Cubical Agda だけが、この種の仕事の道具になります。
そして、この使い分けの軸は、実は Rocq 対 Agda という言語の対立ではありません。
Agda の側にも、一価性を公理として置く書き溜め型の大きなライブラリ（agda-unimath）が育っています。
つまり研究者が選んでいるのは言語ではなく、その仕事に、実行して値を取り出す工程が要るか、要らないか です ── 要らなければ公理側の書庫へ、要るなら計算する側の実験場へ、という選び方なのです。
なお、学び方のロードマップの節で触れる HoTTEST Summer School では、公理側（agda-unimath） と計算する側（Cubical のライブラリと 1Lab） の両者の 教材が同じ講座に並んでおり、この分業が対立ではないことの傍証になっています。
第４部 ── Agda の読み方（最小限）と、コードの実例
【厳密を期すための注記】記号の扱いについて
本記事では、コードの語を「予約語と記号」「ライブラリが提供する名前」「プログラマが任意に付けた名前」の３つに分けて説明します。
ただし、この分け方には、正確を期すための但し書きが必要です。
data、where、open、import は、確かに Agda の予約語です。
しかし →、≡、∙、∷ といった記号の多くは、予約語ではありません。
これらは、ライブラリの中で定義された演算子です。
Agda では、記号を自分で定義できます。
_∙_ のように下線を交えた名前を付ければ、それが中置演算子になります。
本記事に登場する記号の大半は、この仕組みでライブラリが定義したものです。
つまり、記号は「予約語の側」ではなく「ライブラリが提供する名前の側」に属します。
それでも本記事が記号を予約語と並べて扱うのは、コードを読む際の実用上の目安としてです。
「自分で決めた名前ではないもの」と「自分で決めた名前」を見分けることが、初見のコードを読む助けになるからです。
厳密な境界ではなく、読解の手がかりとお考えください。
ここからは、コードを読んでいきましょう。
必要な読み方は、次の表だけです。
| 書き方 | 役割 | Python での近い感覚 |
|---|---|---|
| data 名前 : Set where | 新しい型を、作り方の一覧で定義する | Enum の定義に近い |
| 関数名 : 型 | 関数の型（引数と戻り値）の宣言 | 型ヒント付きの def の宣言部 |
| 関数名 引数 = 式 | 場合ごとの定義本体 | if 分岐を、等式の形で並べる |
| a ≡ b | 「a と b は等しい」という主張の型 | 近いものが無い（本記事の主役） |
| refl | 「定義どおり計算すれば同じ」という等しさの証明 | 近いものが無い |
コードの中の語は、本記事でも、
- 「予約語と記号」
- 「ライブラリが提供する名前」
- 「プログラマが任意の名前を付けられる箇所」
の３つに分けて、そのつど解説します。
実例１ ── まず、ふつうの Agda を１つ
data Bool : Set where
true : Bool
false : Bool
not : Bool → Bool
not true = false
not false = true
真偽値の型を自作し、否定の関数を定義しています。上から読みます。
最初の３行が、型の定義です。
data Bool : Set where は、「Bool という新しい型を、これから作り方の一覧つきで定義する」という宣言です。
Set はライブラリが提供する名前で、「型の型」── Bool のような型たち自身が住む場所 ── を指します。
where の下に字下げして並べた２行が作り方の一覧で、「Bool の値は true と false の２つだけで、それ以外は存在しない」と読みます。
Python の Enum の定義に近い形です。
残りの３行が、関数の定義です。
宣言の行 not : Bool → Bool は、「not は、Bool を受け取って Bool を返す関数」という型ヒントです。
続く２行は、Python の if 分岐を等式の形で並べたものです
── 引数が true なら false を返し、false なら true を返す。場合分けを、分岐の構文ではなく 等式の列 として書くのが、Agda の流儀です。
このコードでプログラマが自分で名付けたのは、Bool、true、false、not です。
data、where、:、=、→ は予約語と記号で、Set だけがライブラリが提供する名前です。
Agda は、まずはこのくらい普通の関数型言語です。
実例２ ── 等しさが「型」になる
open import Data.Nat
open import Relation.Binary.PropositionalEquality
sample : 2 + 2 ≡ 4
sample = refl
上から読みます。
最初の２行は、道具の読み込みです。
Data.Nat からは自然数と足し算が、
Relation.Binary.PropositionalEquality からは ≡ と refl が手に入ります。
全体像の節の実演では Cubical のライブラリを読み込みましたが、ここは Cubical 抜きの、素の Agda の標準ライブラリです。
残りの２行が、おなじみの２行セット（宣言と中身）です。
宣言の行では、sample の型が 2 + 2 ≡ 4 という主張そのもの になっています。
中身の行の refl は、「左辺を定義どおり計算すれば、右辺と同じ値になる」という等しさの証拠です。
機械は実際に $2 + 2$ を計算して $4$ に到達し、確かめたうえで、この２行をコンパイルに通します。
このコードでプログラマが自分で名付けたのは sample だけです。
open、import は予約語、Data.Nat、Relation.Binary.PropositionalEquality、≡、refl はいずれも、ライブラリが提供する名前です。
ここまでは、実は Lean 4 でも Rocq でも書ける内容です。
次から、Cubical Agda でしか書けない世界に入ります。
実例３ ── 円周を、点と道で定義する
Cubical Agda では、型の定義に「点の作り方」だけでなく 「道の作り方」 を書けます。
{-# OPTIONS --cubical #-}
open import Cubical.Foundations.Prelude
data S¹ : Type where
base : S¹
loop : base ≡ base
S¹（エスワン）は、数学でいう円周です。上から読みます。
最初の２行は、おなじみの準備です。
Cubical の機能を有効にし、基本道具（Type と ≡）を読み込みます。
data の行は、実例１の Bool と同じ形です。
「$S^¹$ という新しい型を、作り方の一覧つきで定義する」という宣言で、Type は Cubical ライブラリでの「型の型」── 実例１の Set と同じ役回りです。
名前が違うのには、理由があります。
Set という名前は「集合」を連想させますが、HoTT の世界では、型は道の構造を持ちうるため、集合とは限りません。
そこで Cubical や HoTT の文脈では、慣習として Type という中立な名前が使われます。
役割は Set と同じ、含意だけが違う名前 ── そう読んでください。
where の下の１行目、base : S¹ は、点の宣言です。
Bool の true と同じ形で、「 $S^¹$ には base という値がある」と読みます。
そして、その次の行が本記事の頂点です。
loop : base ≡ base ── 型の欄が、「base は base と等しい」という主張になっています。
つまりこの行は、値ではなく、base から base へ戻る「等しさの証拠（道）」を、型の作り方の一覧に直接並べています。
実例１の一覧に並んだのは値だけでしたが、Cubical Agda では、一覧に道も並べられるのです。
自明に見えるかもしれません。
しかし、refl（その場で動かない道）とは 別の証拠 として、loop が存在します。
一周まわって帰ってくる道と、動かない道は、区別される ── これが「等しさの証拠が複数ある」世界の、最小の入口です。
ここで、良い問いがひとつ生まれます。
loop は、プログラマが任意に付けた名前にすぎません。
では、「一周して、base という同じ地点に戻ってくる」という定義は、コードのどこに書かれているのでしょうか。
答えは、型の欄の base ≡ base です。
道の型では、≡ の左が出発点、右が到着点を表します。
その両方が base ── つまり「出発点と到着点が、同じ点 base である道が１本ある」。
コードに書かれている定義は、これがすべてです。
「ぐるっと一周する」という円の絵は、コードのどこにも書かれていません。
書かれているのは、base から出て base に戻る道が新しい部品として１本ある、ということだけです。
この道が refl に潰れない別の証拠であることも、この最小の定義の型が幾何学の円周と同じ振る舞いをすることも、定義した後から、定理として確かめられる性質 です。
だから、loop を別の名前に変えても、この構造は何ひとつ変わりません。
このコードでプログラマが自分で名付けたのは、S¹、base、loop です。
１行目の {-# OPTIONS --cubical #-} は「この機能を有効にせよ」という指定で、予約の書式です。
Type と ≡ は Cubicalライブラリが提供する名前です。
「道つきの型」 という部分について、ここで解説させていただきます。
ふつうの型の定義は、実例１の Bool のように、値（点）の一覧だけ を書く設計図です。
道つきの型 の 定義 は、それに加えて、「どの点とどの点が、どんな証拠で等しいか」という道の一覧 まで同じ設計図に書きます。
値の設計図と、等しさの設計図が同居している ── それが道つきの型 です。
このような道つきの型は、高階帰納型 と呼ばれます。
証明を区別しない言語では、この５行は原理的に書けません。
実例４ ── 等しさの証拠で、性質を運ぶ（transport）
等しさの証拠は、持っているだけでは道具になりません。使い道は、値の変換です。
carry : {A B : Type} → A ≡ B → A → B
carry p a = transport p a
上から読みます。宣言の行には、書き方が２つ登場します。
波括弧の {A B : Type} は、機械が文脈から推測して埋めてくれる暗黙の引数です（「Agda とはどんな言語か」の節の first にも出てきた書き方です）。
そして → の連なりは、複数の引数の書き方です
── Agda では、関数の型を「引数 → 引数 → 戻り値」と → で繋いで並べます。
あわせて読むと、「carry は、A と B が等しいという証拠と、A の値を受け取り、B の値を返す関数」という宣言です。
中身の行は、受け取った証拠 p と値 a を、そのまま transport に渡しています。
transport は、全体像の節の実演で使った、あの関数です
── 証拠が示す対応にしたがって、値を変換します。
ここでは「A と B が等しい」という証拠 p を根拠に、A の値 a から B の値を作っています。
このコードでプログラマが自分で名付けたのは、carry、A、B、p、a です。
transport と Type はライブラリが提供する名前、波括弧・→・= は予約語と記号です。
そして 一価性は、この transport への入場券を大量発行します。
「同じ振る舞いの２つの構造は等しい」が成り立つので、振る舞いの同じ実装 A と実装 B のあいだで、証明済みの性質を transport で引き継げる
── リスト実装の辞書で証明した性質が、木構造実装の辞書へ、証拠つきで運ばれる。これが一価性の実用面の顔です。
証拠どうしも、計算できる ── ねじれ２回は、そのまま
第４部の締めくくりに、Cubical Agda らしさが最もよく出る実演を置きます。
等しさの証拠は、値のように持ち回れるだけではありません。
証拠どうしをつないで、新しい証拠を作る演算 があります。
全体像の節のコードの続きとして、次の４行を足します。
twice : Bool ≡ Bool
twice = flipWay ∙ flipWay
checkTwice : transport twice true ≡ true
checkTwice = refl
∙ は、２つの証拠を順につなぐ演算です。
道の言葉でいえば、道の終点に次の道の始点を継ぎ足して、１本の道にします。
twice は、全体像の実演で作った flipWay ── true と false を入れ替える根拠の等しさ ── を、２回続けて繋いだ証拠 です。
プログラマが自分で名付けたのは twice と checkTwice で、∙ はtransport と Type はライブラリが提供する名前、波括弧・→・= は予約語と記号です。です。
そして checkTwice が、機械の答えです。
入れ替えを２回通せば、元に戻る ── true を twice で変換した結果は true である、という主張に、refl が通ります。
ねじれた糸を２回撚ると、まっすぐな糸と同じ運び方に戻る
── この直観を、機械が実際に計算を最後まで進めて、裏づけた のです。
公理の処理系では、この計算はねじれの部分で止まります。
証拠を作る、証拠と証拠をつなぐ、つないだ証拠で値を変換する
── その全工程が最後まで動く。
Cubical Agda でしか見られない景色として、本記事はこの４行を選びました。
第５部 ── 研究の実例（出典つき）
ここに挙げるのは、研究者が実際に行い、論文または公開実装で確認できる実例です。
実例A ── 球面のホモトピー群を、機械で計算する
HoTT の生まれ故郷である代数トポロジー には、「球面の上の道の絡まり方」を数える、ホモトピー群という計算対象 があります。
人間の手計算では何十ページにもなる繊細な議論の世界です。
この計算の一部が、Cubical Agda の上で形式化され、機械検査つきで実行されました。
$π_₄（ S^³ ）$ と書かれる群の計算（ブルネリ数と呼ばれる数値の機械計算） は、Cubical Agda の計算能力 ── 公理で止まらない、という第３部の話 ── の実証例として知られています。
実例B ── バージョン管理を、「道」でモデル化する
git のようなバージョン管理システムの基礎には、パッチ（リポジトリへの編集操作）という概念があります。
2014年の研究「Homotopical Patch Theory」（Angiuli、Morehouse、Licata、Harper）は、このパッチを 「リポジトリの状態どうしを結ぶ、等しさの証拠（道）」 として HoTT でモデル化しました。
パッチの合成、取り消し、順序の入れ替えの法則が、道の言葉で厳密に書けることを示した研究 です。
エンジニアが毎日触っている道具の数理が、最先端の等しさの数学と正確に対応していた
── 理論が道具を照らした好例です（なお、git そのものが HoTT で作られているわけではありません。理論によるモデル化と、道具の実装は別の話です）。
実例C ── 実装の取り替えで、証明を再利用する
第４部の transport の話の研究版です。
一価性を使うと、同型な構造のあいだで定理を輸送できるため、「単純だが遅い定義で証明し、速い実装へ性質を運ぶ」という証明の再利用が、言語の機能として成立 します。
この発想は Cubical Agda の原論文（2019年）でも動機のひとつとして示されています。
第６部 ──【筆者の構想】ビジネスへの示唆
この第６部は、研究の実例ではありません。
筆者が独自に考えた構想 であり、実在の事例と混同されないよう、この標識を付けて書きます。
【筆者の構想】
冒頭の顧客データの話に戻ります。
本人確認による「同じ顧客」と、メール一致の推定による「同じ顧客」
── この２種類の同一視を、潰さずに 別々の「等しさの証拠」として型で管理する 設計は、HoTT の transport の考え方と正確に同じ形をしています。
レコード $A$ の購入履歴を $B$ に引き継ぐとき、どの証拠を根拠に運んだのかがコードに残る
── 監査への説明が変わる可能性のある設計です。
この発想は、実務の言葉と地続きです。
データの世界で「データリネージ（来歴管理）」や「監査証跡」と呼ばれてきた要請
── どのデータが、どの根拠で、どう繋がれたかを後から辿れること
── は、「証拠を潰さない」という本記事の主題と、同じ方向を向いています。
たとえば金融のリスク管理では、VaR のような数値そのものと同じ重さで、その数値がどのデータの、どんな同一視から導かれたのかという来歴の説明が求められます。
規制対応や、AI の判断根拠の説明（XAI）のように、同一視の根拠まで問われる場面がもし増えていくなら
── これは予測ではなく、条件の話です ── 証拠ごと扱う型の設計は、その要請の理論的な土台の候補になります。
ただし、構想には線引きが要ります。
この枠に乗るのは 根拠のはっきりした同一視だけ です。「80パーセントの確度でたぶん同じ」という確率的な名寄せは、等しさの証拠（論理の構成物）では表現できません。
また、「本人確認の証拠のときだけ口座統合を許す」といった業務規則は、理論が与えるものではなく、設計者が型の設計で作り込む部分です。
そして、実現の形の見積もりです。
Cubical Agda がそのまま業務システムに入る未来を、筆者は予想していません。
あるとすれば、「等しさを証拠つきで扱う」という設計思想が、もっと普通の言語やデータ基盤の設計に薄まって届く 形でしょう。
理論の言葉がそのまま現場に降りることは稀でも、理論のまなざしは先に届くものだからです。
つまり、こういうことです。
Cubical Agda のコードや一価性という言葉が、業務システムに現れる日は来ないかもしれません。
それでも、「この２つの『同じ』は、根拠の違う別々の同一視ではないか」と問う ものの見方 は、言語や定理より先に、設計者の頭の中に届きます。
本記事の冒頭で、顧客データの２つの「同じ」を区別して読んだとき、あなたはすでにその見方を一度使っています。
AI エージェント時代に、Agda 人材の需要は広がるのか
キャリアの問いにも触れておきます。
問いは２つに分かれます
── AI エージェントの時代に、Agda を書けるエンジニアへの人材ニーズは広がるのか。
そして、その中でも Agda の HoTT ライブラリを扱える人材のニーズは高まるのか。
Agda エンジニアの需要 ── 確認できる事実と、筆者の予想
まず、確認できる現在の事実です。AI が定理証明を訓練場にする流れの中心には、Lean 4 がいます。
筆者の Lean 4 の記事で調べたとおり、AI 企業向けに Lean 4 の証明を書く仕事は実在し、報酬つきで募集されています。
その一方で、Agda を専業とする求人は、筆者の調べた範囲では見当たりません。
今後広がるかどうかを示す時系列のデータも、ありません。
構造的な理由も、第１部で述べたとおりです。
AI の訓練場には、大量の検査済みデータと自動化の道具が要ります。蓄積の量より土台の純度を選んだ Agda は、この要件と噛み合いにくい位置にいます。
ここからは、筆者の予想です。
「Agda の求人」が増えなくても、「Agda で鍛えた人」の価値は、別の経路で効く と筆者は考えています。
依存型を読み書きし、プログラムと証明を一体で設計する素養は、言語をまたいで持ち運べる技能です。
PLFA で Agda を学んだ人が、Lean 4 や Rocq や F* の仕事に移ることに、大きな段差はありません。
定理証明の書き手が少ないまま、証明を求める仕事は現に存在する
── この需給の形が続くかぎり、Agda はその市場への、遠回りに見えて足腰の強い入口になりえます。
HoTT ライブラリを扱える人材の需要 ── 研究職の世界の話
Agda の HoTT ライブラリ（agda/cubical や agda-unimath）を扱える人材への需要は、さらに範囲が狭くなります。
確認できる事実として、この技能が仕事になる場所は大学と研究機関で、その形は研究職です。
産業の側にこの技能を求める求人を、筆者は確認できていません。
理由も、第1部で述べたことの裏返しです
── 産業は「複数の等しさ」を、潰す運用で済ませてきました。
この状況が変わらないかぎり、産業のニーズは生まれません。変わる可能性のある場面は第6部で述べましたが、あれは【筆者の構想】であって、予測ではありません。
なお、ロボットや自動運転のような、物理世界で動く AI（Physical AI）の安全性検証は、形式手法への関心が高い分野です。
ただし、そこで主に研究されてきた道具は モデル検査 や 制御理論に基づく検証 で、Agda や HoTT が使われている事例を、筆者は確認できていません。
関心の高い分野と、この言語の現在地は、まだ接続していない
── これが、検証できる範囲の答えです。
何のために学ぶかで、答えが変わる
整理すると、こうなります。需要を追って学ぶなら、入口は Lean 4 です。
求人が実在し、日本語の学習資産があり、AI との接続が太いからです。
原理を深く掘るために学ぶなら、Agda と HoTT には代えが利きません。
依存型を混ぜ物なしで身につける素振り場として、そして「複数の等しさ」を実際に動かして確かめられる実験場の代表格として、です。
次の節の学び方は、後者の動機の読者に向けたものです。
学び方のロードマップ ── 知識ゼロから、どう学ぶか
最後に、この言語を実際に学ぶ場合の道筋を書いておきます。
日本語の本は、あるのか
現状をそのまま書きます ── Agda を主題にした日本語の入門書は、筆者の知るかぎり見当たりません。
有志の Web 記事や大学の講義資料は散在しますが、体系的な書籍は無く、腰を据えた学習は英語の教材が前提になります。
Lean 4 に日本語コミュニティの翻訳資産が育っているのと比べても、ここは差のある部分です。
英語の定番は、はっきりしている
代わりに、英語の定番は明確です。Agda の公式ドキュメントにチュートリアルの一覧ページがあり、そこに並ぶ顔ぶれが、そのまま定番のリストになっています。
- 教科書の定番は PLFA（Programming Language Foundations in Agda）です。
無料公開で、演習込みで頭から進める作りになっています。タクティク不要の言語だからこそ教科書が Coq から置き換えられた、という経緯は「Agda とはどんな言語か」の節で述べたとおりです
- 書籍では、"Certainty by Construction"（Maguire、2023年）と "Verified Functional Programming in Agda"（Stump、2016年）が、公式一覧の筆頭に挙がる Agda 専門書です
- 環境構築なしでブラウザから試したい場合は、"Let's Play Agda"（2025年）という演習サイトが公式一覧に載っています。参入コストの急落は、この言語にも来ています
- Cubical Agda と HoTT の側では、HoTTEST Summer School（2022年）の講義動画と演習が入口の定番で、その教材は本記事で紹介した agda/cubical ライブラリや、オンライン教科書 1Lab へ接続しています
現場の人は、どうやってゼロから学んでいるのか
「Agda を使う研究室や仕事に入った人は、どう学ぶのか」
── 学び方の統計はありませんが、公式のチュートリアル一覧そのものが実態を示しています。
一覧の大半は、世界各地の大学の講義資料 です。
Agda 誕生の地チャルマース工科大学の講義をはじめ、各大学の授業がそのまま教材として公開されており、研究の世界では「講義か教科書で基礎→自分の題材で小さな形式化→詰まったらコミュニティで質問」という経路が定番です。
この経路は、独学でもなぞれます。順路の形にすると次のとおりです。
- 本記事の第4部のコードを、ブラウザ（Let's Play Agda など）で手元再現する。書いて動かした行だけが、身につきます
- PLFA を頭から、演習込みで進める。Agda はタクティクの無い言語なので、穴を残して処理系と対話しながら埋める書き方そのものが、先生役になります
- 詰まったら、公式のコミュニティチャット（Zulip）で質問する。初学者の質問が日常的に流れている場所です
- Cubical に進む段階で、HoTTEST Summer School の演習と agda/cubical ライブラリの定義の読解に移る。ライブラリの定義へジャンプして読む習慣が、そのまま研究の現場の読み方です
学習リソース
- HoTT Book（"Homotopy Type Theory: Univalent Foundations of Mathematics"、2013年） ── 理論の原典。公式サイトで無料公開されています
- agda/cubical ライブラリ（GitHub） ── 本記事のコードの土台。定義と定理が全行公開されています
- Agda 公式ドキュメント ── 言語そのものの入門はこちらから
- PLFA（Programming Language Foundations in Agda） ── Agda で書かれたプログラミング言語理論の教科書。無料でオンライン公開されています
- Agda 公式のチュートリアル一覧（Agda documentation 内の A List of Tutorials） ── 定番書・講義資料・演習サイトの公式リスト。学び方のロードマップの節で述べた教材はここから辿れます
- HoTTEST Summer School 2022（GitHub） ── Cubical Agda と HoTT の講義動画・演習の定番。1Lab や agda/cubical への接続点でもあります
- 筆者の HoTT 連載（第１回・第２回） ── 「複数の等しさ」の数学を、コード無しの日本語で説明した連載です
まとめ
- Cubical Agda は、等しさの証明を値のように区別して扱える、HoTT の実用処理系の代表格である
- ビジネス事例がほぼ無いのは、この言語が理論の試作台という役割を選び、自動化の火力より土台の純度を優先し、そして HoTT の主戦場である「複数の等しさ」を産業がまだ運用で潰せているからである
- 最大の発明は、一価性を公理ではなく計算できる部品として実装したことにある。公理は計算を止めるが、Cubical Agda の証明は最後まで動く
- 円周 S¹ の５行の定義は、「等しさの証拠が複数ある」世界の最小の入口である
- 研究の実例（球面のホモトピー群の機械計算、パッチ理論）は出典つきで実在する。ビジネスへの示唆は、本記事では【筆者の構想】として実例と区別して述べた
関連記事
出典
- "Homotopy Type Theory: Univalent Foundations of Mathematics"（Univalent Foundations Program、2013年） ── HoTT の原典
- "Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types"（Vezzosi、Mörtberg、Abel、ICFP 2019） ── Cubical Agda の原論文
- "Homotopical Patch Theory"（Angiuli、Morehouse、Licata、Harper、ICFP 2014） ── パッチを等しさの証拠としてモデル化した研究
- agda/cubical（GitHub） ── Cubical Agda の標準ライブラリ
- "Programming Language Foundations in Agda"（Wadler、Kokke、Siek） ── タクティクを使わない Agda の証明スタイルと、その教育上の利点を示した教科書。「Agda とはどんな言語か」の節で参照
- Coq-HoTT（GitHub） ── Rocq 上の HoTT ライブラリ
- UniMath（GitHub） ── ヴォエヴォドスキーが始めた Rocq 上のライブラリ