この記事は、連載シリーズの第３回目です
Arend という定理証明支援系について、全７回にわたってお伝えしています。
これまでの流れ
第１回では、Arend が HoTT（ホモトピー型理論）を公理としてではなく、計算して確かめる対象として扱っていることをお伝えしました。
第２回目では、Arend と Cubical Agda がどこで設計判断を分けたのかを扱いました。
区間 I を普通の型として扱うか、型の外に置くか。その一点で、両言語は分かれました。
今回（３回目）扱うこと
第１回と第２回では、次の３つを名前だけ挙げて先へ進みました。
- 移送
- 商型
- 関数外延性
本記事では、この３つを掘り下げます。
ところで、移送・商型・関数外延性は、ホモトピー型理論（HoTT）における「２つの対象の等しさ」の捉え方から、正当化されます。
そのため、この記事では、HoTT についての解説から始める順番で議論を展開していきます。
まず、HoTT がどういう発想なのかを扱います
ホモトピー型理論（HoTT）は、２つの対象が等しいとき、２つの対象を結ぶ経路（道、path）が存在していると捉える発想です。
タロウくん：
道、ですか。
専任講師：
順を追って説明します。
道には、向きがあります。 $a$ から $b$ への道があれば、それを逆にたどって $b$ から $a$ への道も作れます。
タロウくん：
・・・行きと帰りが対になっている。
専任講師：
その舞台となる「型」を、空間として解釈できることが分かっています。
型そのものが位相空間だ、という意味ではありません。型を空間として読み替えるモデルが、いくつも与えられているという意味です。
1998年の Hofmann と Streicher による解釈。2009年の Awodey と Warren によるモデル圏での解釈。そして Voevodsky による単体集合を用いた解釈。
単体集合とは、点・線分・三角形・四面体といった単純な図形を組み合わせて、空間を表すための道具です。図形を積み木のように組み上げて、複雑な形を表します。
タロウくん：
・・・複数の研究者が、別々にモデルを与えた。
専任講師：
そのため、次のようなイメージで捉えられます。
数学的に定義された空間があり、そのなかに２つの対象が点として置かれている。 そして、両者を結ぶ道がある。
その２つの対象が等しい理由（根拠）が複数見出されたとき、２つを結ぶ道が複数本、描かれます。
タロウくん：
・・・道が２本、３本と増えていく。
専任講師：
Bool の例が、まさにそれです。
Bool から Bool へ、過不足なく一対一に対応づける方法は２通りあります。何も変えない対応と、true と false を入れ替える対応です。
その２通りが、それぞれ別の道を与えます。
「等しさを空間内の経路（道、path）として捉える」ことが、移送・商型・関数外延性を支えています
専任講師：
道として捉えられるからこそ、この３つができます。
| できること | 道のどの性質を使うか |
|---|---|
| 移送 | 道に沿って、値を運べる |
| 商型 | 道を、型の定義に書き込める |
| 関数外延性 | 各点での道から、関数どうしの道を組み立てられる |
では、この発想はどこから来たのか。
唐突に現れたものではありません。
1998年に示された「グルーポイド解釈」という結果があり、それを受けて2006年に２組の研究者が独立に同じところへ至りました。
なぜ「等しさ」を空間内の経路として捉えることにしたのか。その経緯が分かると、移送・商型・関数外延性の理解も深まります。
そこで本記事では、第１部で HoTT の出自をたどります。
その過程で、依存型の考え方と、型理論にどんな系統があるのかも押さえます。
第２部以降で、移送・商型・関数外延性を順に見ていきます。
なお、本記事だけでも読めるように書きました。 第１回・第２回で扱った概念も、必要な範囲で改めて解説します。
本記事のExecutive Summary
本記事を読むと、何が分かるのか
第２回では、Arend と Cubical Agda の設計判断の違いを扱いました。
しかし、そもそも「等しさの根拠を区別できると、何が嬉しいのか」には触れていません。
本記事では、具体的にできることを３つ示します。
| できること | 何ができるようになるのか |
|---|---|
| 移送 | ある型について書いた証明を、別の型へ運べる |
| 商型 | 「$1/2$ と $2/4$ は同じ数だ」と型の定義に書き込める |
| 関数外延性 | 「どんな入力にも同じ値を返す２つの関数は、等しい」と言える |
そして、この３つを「公理として足す」方式を選んだ場合に何が起きるのかも扱います。
Arend は、この３つに計算規則を与えました。 そのため、証明を走らせると具体的な値まで到達します。
一方、Rocq／Coq 上の HoTT ライブラリは、この３つを公理として宣言する方式を採っています。
「一価性公理は、証明も検証もせずに、正しいものとして受け入れる」と宣言し、その上に議論を積み上げる。
証明そのものを記述することはできます。
しかし、一価性公理は、検証ぬきに正しいと受け入れる立場に立っています。そのため、一価性を具体的に検証し、計算するための計算規則が、Rocq の HoTT ライブラリには含まれていません。
そのため、HoTT に関して計算して、具体的な値を算出することができないのです。
なお、このことは、Rocq の HoTT ライブラリでは、一価性を前提とした数学的な主張を証明したり反証したりできない、という意味ではありません。
Rocq の HoTT ライブラリでも、一価性を前提とした数学的な主張を証明したり反証したりすることは、可能です。
しかし、具体的な値を求めることができないのです。理由は、HoTT に関する計算規則が Rocq の HoTT ライブラリでは定義されていないからです。
本記事では、両者を対比しながら、その違いがどこから生じるのかを扱います。
なお、本記事で比較するのは、通常の Haskell の等値判定 == と、依存型理論における同一視型です。 Haskell の高度な型拡張や外部ライブラリによる表現までを網羅的に比較するものではありません。
本記事には、Arend 以外の言語も登場します
本記事の主題は Arend です。
しかし、Arend の設計判断を理解するには、他の言語がどうしているかを見る必要があります。
「Arend はこうしている」とだけ述べても、それが何を選び、何を諦めたことなのかが分かりません。
比較の相手があってはじめて、判断の意味が見えてきます。
そこで本記事では、次の言語を引き合いに出します。
| 言語・処理系 | 本記事で登場する理由 |
|---|---|
| Arend | 本記事の主題。 HoTT の計算規則を言語に組み込んだ処理系 |
| Haskell | 記法の対比。 Arend のコードを読むときの手がかりとして使う |
| Cubical Agda | 設計判断の対比。 Arend と同じく計算規則を組み込んだが、区間の置き場所が違う |
| Lean 4 | 関数外延性の扱いの対比。 公理として足すのではなく、商型から定理として導いている。ただし代償がある |
| Rocq／Coq 上の HoTT ライブラリ （Coq-HoTT、UniMath） | 「公理として足す」道の代表例。 計算規則を持たないと何が起きるかを示す |
とりわけ Lean 4 は、第４部で重要な役割を果たします。
「どんな入力にも同じ値を返す２つの関数は等しい」という主張を、Lean 4 は公理として足すのではなく、定理として証明しています。
しかし、それでも計算が止まる場面が残ります。
その現象を、Lean 4 の公式ドキュメントの記載を引きながら確かめます。
本記事の議論の流れ
青い枠が出発点です。 依存型とは何か、型理論にはどんな系統があるか、HoTT はどこから来たのか。そこから始まります。
金色の枠が、本記事の中心となる移送・商型・関数外延性です。
赤い枠が、この３つを公理として足した場合に起きることです。
緑の枠が到達点です。 Arend が何を手放し、何を得たのかを述べます。
本記事の読み方
本記事は長いため、関心に応じた入口を示しておきます。
| 関心 | どこから読むか |
|---|---|
| 移送・商型・関数外延性だけ知りたい | 第２部〜第４部 |
| 公理として足すと何が起きるのかを知りたい | 第５部・第６部 |
| Arend と Cubical Agda の違いを知りたい | 第７部 |
| 依存型や型理論の系統から知りたい | 第１部から順に |
| 型理論の用語を整理したい | 第８部の対話篇 |
第１部 ── ホモトピー型理論は、どこから来たのか ── 依存型と型理論の系統から
HoTT の現在につながる重要な着想は、2006年ごろに現れました。
専門も所属も異なる２組の研究者が、独立に同じところへ至っています。
２つの研究が独立に出現した
（原文引用）
The idea of homotopy type theory arose around 2006 in independent work by Awodey and Warren and Voevodsky, but it was inspired by Hofmann and Streicher's earlier groupoid interpretation.
（筆者による日本語訳）
ホモトピー型理論の着想は、2006年ごろ、Awodey と Warren による研究、および Voevodsky による研究として、それぞれ独立に現れた。ただし、それは Hofmann と Streicher による、より早い時期のグルーポイド解釈に触発されたものであった。
Steve Awodey は、カーネギーメロン大学の哲学科に籍を置く数学者・論理学者です。
指導教官は圏論の創始者の１人 Saunders Mac Lane であり、圏論を用いた高階論理のモデル理論を専門としてきました。教科書 Category Theory（Oxford University Press）の著者としても知られています。
Michael Warren は、当時カーネギーメロン大学の博士課程にいました。
2008年の学位論文の題名が Homotopy Theoretic Aspects of Constructive Type Theory（構成的型理論のホモトピー論的側面）です。
両者の共著論文が、着想の中核をなしています。
Homotopy theoretic models of identity types（Mathematical Proceedings of the Cambridge Philosophical Society, 2009）。マーティン＝レーフ型理論が、任意のモデル圏のなかで健全に解釈できることを示した論文です。
タロウくん：
マーティン＝レーフ型理論とはなんですか？
また、モデル圏もなんのことかわかりません。
専任講師：
順に説明します。
まず、マーティン＝レーフ型理論から。
スウェーデンの数学者・論理学者である Per Martin-Löf が、1970年代に提唱した型理論です。
タロウくん：
型理論、というと。
専任講師：
プログラムの型と、数学の証明を、同じ枠組みで扱う体系です。
「この式はこの型を持つ」という判定と、「この命題は正しい」という判定を、同じ規則で行います。
タロウくん：
・・・型検査が、そのまま証明の検査になる。
専任講師：
そのとおりです。
このあたりは、本連載の過去の記事で、カリー＝ハワード同型対応という名前がついていることを含めて、解説しました。内容をまだお読みでない方や、読んだけど忘れてしまった方は、ぜひ過去の記事を参照ください。
タロウくん：
型理論についてはわかりました。カリー＝ハワード同型対応が根幹にあるのですね。
ところで、型理論は複数あるんですか？
どんな型理論があって、そのなかでマーティン＝レーフ型理論の位置づけと、マーティン＝レーフ型理論がどんな型理論かを知りたいです。
専任講師：
順を追って説明します。
まず、依存型理論という大きな枠組みがあります。
タロウくん：
依存型、というのは。
専任講師：
値によって型が変わる仕組みのことです。
Haskell の型は、値に依存しません。Int は常に Int です。
依存型を持つ言語では、値を受け取って型を返す関数を記述できます。
タロウくん：
・・・例を見せていただけますか。
例① ── 要素数を型に持つリスト
専任講師：
Haskell のリストを思い出してください。
[1, 2, 3] :: [Int]
この型は [Int] です。要素が何個あるかは、型に現れません。
要素が３個でも100個でも、型としては同じ [Int] です。
タロウくん：
・・・言われてみれば、そうですね。
専任講師：
依存型があると、要素数を型に書き込めます。
Arend で定義してみましょう。
\data Vec (A : \Type) (n : Nat) \elim n
| 0 => vnil
| suc m => vcons A (Vec A m)
Vec A n は、「型 A の要素を n 個持つリスト」 を表します。
タロウくん：
型に n という数が入っている。
専任講師：
そこが依存型です。
n は値であり、その値によって型が変わります。
実際に作ってみます。
\func v3 : Vec Nat 3 => vcons 1 (vcons 2 (vcons 3 vnil))
型検査を通過します。
タロウくん：
Vec Nat 3 ・・・「自然数を３個持つリスト」ですね？
専任講師：
そうです。
要素を２個しか入れなければ、型検査で弾かれます。
Haskell では、要素数の誤りを型で防ぐことができません。
依存型があれば、それができます。
例② ── 値によって、返る型が変わる関数
専任講師：
もう１つ、はっきりした例をお見せします。
\data Bool | true | false
\func F (b : Bool) : \Set0 \elim b
| true => Nat
| false => Bool
この F は、Bool の値を受け取って、型を返します。
| 呼び出し | 返る型 |
|---|---|
F true |
Nat |
F false |
Bool |
タロウくん：
・・・引数の値によって、返る「型」が違う。
専任講師：
使ってみます。
\func v1 : F true => 5
\func v2 : F false => true
F true は Nat なので、5 を入れられます。F false は Bool なので、true を入れられます。
型検査を通過します。
タロウくん：
Haskell には、この形がありませんね。
専任講師：
ありません。 型を返す関数を、値の上で場合分けして定義することはできません。
📌 中上級者向け：Haskell の型拡張と依存型の違いを厳密にいうと
本文では、通常の Haskell と依存型を持つ言語を対比しました。
GHC Haskell には、DataKinds、GADTs、型族（Type Families）、singleton パターンなどがあります。 これらを使えば、値に似た情報を型のレベルへ持ち上げたり、型のレベルで場合分けしたりできます。実際、Data.Type.Equality の (:~:) を使えば、型どうしの等しさを表す項を扱えます。
ただし、それらは一般の値 x を受け取って型 F x を返す依存関数を、言語の基本機能としてそのまま提供するものではありません。
型のレベルへ持ち上げた値についての等しさと、値そのものについての等しさは、別のものです。本文で扱っている 3 = 3 は後者にあたります。
本記事での比較対象は、通常の Haskell の等値判定 == と、Arend の同一視型（identity type）です。 GHC 拡張を含む Haskell の表現力全体を網羅的に比較することは目的としていません。
そして、3 = 3 も型になります
専任講師：
ここからが、この記事の主題につながります。
Haskell で 3 == 3 と記述すると、何が返りましたか。
タロウくん：
True です。真偽値ですね。
専任講師：
依存型を持つ言語では、3 = 3 は真偽値ではありません。
型そのものです。
\func T : \Type => 3 = {Nat} 3
型検査を通過します。 3 = 3 が、\Type に属する値として扱われています。
タロウくん：
・・・3 = 3 が、型。
専任講師：
そうです。
型である以上、その型に属する値を考えることができます。
\func pf : 3 = {Nat} 3 => idp
idp が、「３と３が等しいことの根拠」 にあたる値です。
タロウくん：
真偽値なら True が返って終わりでした。
専任講師：
型なら、その中に何が入っているかを問えます。
根拠が１つなのか、複数あるのか。
それを型として扱えるようになります。
タロウくん：
・・・だから、等しさの根拠を区別できる。
専任講師：
そこが、依存型理論と HoTT のつながりです。
なお、{Nat} という記法 が出てきました。
「どの型の値どうしを比べるのか」を明示する書き方 です。
通常は処理系が推論しますが、ここでは Nat と指定しています。
idp は、３と３が等しい理由のひとつです
専任講師：
idp は、３と３が等しい理由のひとつです。
タロウくん：
ひとつ、ということは・・・。
idp 以外にも３と３が等しい別の理由が見つかった場合は、
\func pf : 3 = {Nat} 3 => 別の理由
と記述するんですか？
専任講師：
記法としては、そのとおりです。
別の理由が見つかれば、そこに書き込みます。
ただし、3 = 3 については、そうなりません。
タロウくん：
・・・別の理由がない、ということですか？
専任講師：
理由が複数あっても、それらは互いに等しくなるんです。
実際に確かめてみましょう。
\func pf1 : 3 = {Nat} 3 => idp
\func pf2 : 3 = {Nat} 3 => idp
\func same : pf1 = pf2 => idp
型検査を通過します。
pf1 と pf2 という２つの根拠を作り、その２つが等しいことを idp で示せています。
タロウくん：
・・・別々に書いても、同じものになるということですか。
専任講師：
そうです。
Nat という型は、そういう性質を持っています。
Arend では、次のように確かめられます。
\func natIsSet0 : \Set0 => Nat
\Set0 に属する型は、等しさの根拠が高々１本です。
タロウくん：
・・・「高々１本」。
専任講師：
根拠がないか、あっても実質１本しかない、という意味です。
3 = 5 なら、根拠は存在しません。
3 = 3 なら、根拠は１本だけです。
根拠が複数ある例
タロウくん：
では、根拠が複数ある例はあるのですか？
専任講師：
あります。
値どうしではなく、型どうしを比べるとき です。
Bool = Bool が、その例です。
Bool から Bool へ、過不足なく一対一に対応づける方法は、２通りあります。
まずは、なにも変えない操作をしたとき です。
- TrueはTrueのまま。
- FalseはFalseのまま。
よって、
- TrueとTrueは等しい。
- FalseとFalseも等しい
次に、論理反転操作する場合 が考えられます。
- TrueはFalseになり、
- FalseはTrueになる。
その結果、
- TrueとTrueの比較は、FalseとFalseの比較になり、結果は等しい。
- FalseとFalseの比較は、TrueとTrueの比較になり、結果は等しい。
タロウくん：
・・・ どちらの操作でも、過不足なく対応がついていますね。
専任講師：
そうなんです。
だから、何も変えない操作をしたとき と、論理反転する操作をしたとき のそれぞれが、
Bool = Bool の （互いに異なる別々の）根拠 になります。
Arend では、こう記述します。
\func idPath : Bool = Bool => path (iso boolId boolId boolIdId boolIdId)
\func negPath : Bool = Bool => path (iso boolNeg boolNeg boolNegNeg boolNegNeg)
どちらも型は Bool = Bool です。しかし、中身が違います。
そして、それぞれの根拠に沿って true を運ぶと、結果が変わります。
coe は、等しさの根拠に沿って値を運ぶ操作です。
この記事の第２部で、あらためて扱います。
\func m1 : Bool => coe (\lam i => idPath @ i) true right
\func m2 : Bool => coe (\lam i => negPath @ i) true right
\func c1 : m1 = true => idp
\func c2 : m2 = false => idp
型検査を通過します。
タロウくん：
idPath で運ぶと true、negPath で運ぶと false ・・・。
専任講師：
運んだ結果が違います。だから、この２つは別の根拠です。
タロウくん：
・・・3 = 3 では、そういうことが起きない。
専任講師：
起きません。Nat の値どうしを比べる限り、根拠は１本です。
根拠が複数現れるのは、比べる対象がどんな型かによります。
タロウくん：
・・・型によって、事情が違う。
専任講師：
そこは、本記事の第８部であらためて扱います。
では、どんな型理論があるのか
専任講師：
依存型理論には、いくつかの系統があります。
タロウくん：
系統、ですか。
専任講師：
代表的なものが２つあります。
系統① ── CIC
専任講師：
１つは、CIC（ Calculus of Inductive Constructions 、帰納的構成の計算体系）です。
タロウくん：
長い名前ですね。
専任講師：
２つの部分からできています。
まず、CoC（ Calculus of Constructions 、構成の計算体系）という土台があります。
1988年に Thierry Coquand と Gérard Huet が提唱した体系です。
タロウくん：
CoC とは、どういうものですか？
専任講師：
Haskell の型システムを拡張していった先にあるもの だとお考えください。
順に見ていきましょう。
CoC への道のり ── ３つの拡張
専任講師：
出発点は、単純な関数です。
f :: Int -> Bool
値を受け取って、値を返す。
これだけなら、依存型は要りません。
タロウくん：
はい。
専任講師：
ここから、３つの方向に拡張できます。
第１の拡張は、値が型に依存することです。
length :: forall a. [a] -> Int
a という型を受け取って、その型のリストを扱う関数を返す。
タロウくん：
Haskell の forall ですね。
専任講師：
そのとおりです。多相性と呼ばれます。
第２の拡張は、型が型に依存することです。
Maybe :: * -> *
Maybe は、型を受け取って型を返します。
| 受け取る型 | できあがる型 |
|---|---|
Int |
Maybe Int |
Bool |
Maybe Bool |
String |
Maybe String |
タロウくん：
どの型が、どの型に依存しているのですか。
専任講師：
Maybe Int という型が、Int という型に依存しています。
Int を Bool に変えれば、できあがる型は Maybe Bool に変わります。
つまり Maybe Int は、Int が決まってはじめて決まる型です。
タロウくん：
・・・「依存する側」が Maybe Int、「依存される側」が Int。
専任講師：
そのとおりです。型のレベルの関数だと考えてください。
Haskell には、ここまであります。
そして第３の拡張が、型が値に依存することです。
タロウくん：
先ほどの Vec Nat 3 ですね。
専任講師：
それが依存型です。Haskell にはありません。
この３つの拡張をすべて備えた体系が、CoC です。
| 拡張 | 何ができるか | Haskell に | 例 |
|---|---|---|---|
| 第１ | 値が型に依存する | ある | forall a. [a] -> Int |
| 第２ | 型が型に依存する | ある | Maybe :: * -> * |
| 第３ | 型が値に依存する | ない | Vec Nat 3 |
タロウくん：
・・・全部乗せ、ということですか。
専任講師：
そう捉えていただいて構いません。
CoC に足りなかったもの
タロウくん：
では、CoC だけでは足りなかったのですか？
専任講師：
データ型を定義する仕組みがありませんでした。
Haskell の data にあたるものです。
data Nat = Zero | Suc Nat
data List a = Nil | Cons a (List a)
自然数、リスト、木構造。
そうしたデータ型を、構成子を並べて定義する仕組みです。
タロウくん：
CoC では、これを記述できなかった。
専任講師：
正確には、記述できないわけではありません。
関数として符号化する方法があります。
しかし、扱いにくいのです。
場合分けや再帰を、そのままの形で記述できません。
タロウくん：
・・・実用上、困る、と。
専任講師：
実用上、困ってしまうわけです。
そこで、CoC に帰納的型を加えたものが CIC です。
「Inductive」が、その帰納的型を指しています。
$$\text{CoC} + \text{帰納的型} = \text{CIC}$$
この CIC が、Rocq／Coq と Lean の土台になっています。
📌 中上級者向け：CoC の「３つの拡張」は教育的な見取り図です
本文では、CoC を「値が型に依存する」「型が型に依存する」「型が値に依存する」という３つの方向から説明しました。
これは、Haskell の読者が CoC の方向性をつかむための説明です。
CoC は Haskell を歴史的に拡張して得られた体系ではありません。
形式的には、CoC は依存積・多相性・型作用子などを含むラムダ計算の体系として発展してきました。
本文の３分類は、Barendregt cube と呼ばれる型付きラムダ計算の見取り図を、Haskell の読者向けに再構成したものです。
CoC の正式な構成要素を、歴史的な順序で並べたものではありません。
また、実際の GHC Haskell は Hindley–Milner 型推論、型クラス、GADTs、型族などを持ち、CoC と一直線に比較できる言語ではありません。
それでも、この見方をすると、通常の関数型プログラミング・多相型・依存型・命題と証明・定理証明が、ばらばらの機能ではなく、「型と項の関係をどこまで表現できるようにするか」という１つの軸の上に並んでいる ことが見えてきます。
系統② ── マーティン＝レーフ型理論
専任講師：
もう１つが、マーティン＝レーフ型理論（ Martin-Löf Type Theory、略して MLTT ）です。
先ほど名前を挙げた、Per Martin-Löf が1970年代に提唱した体系です。
タロウくん：
CIC より早いのですね。
専任講師：
そこは重要です。MLTT のほうが、10年以上先に提唱されています。
CoC が1988年ですから、MLTT は CIC の前身ではありませんし、CIC に何かを足したものでもありません。
別々に発展した、２つの系統だとお考えください。
タロウくん：
では、どこが違うのですか。
専任講師：
主な違いは、２つあります。
違い① ── 宇宙の階層の扱い
専任講師：
まず、宇宙という言葉から説明します。
タロウくん：
お願いします。
型にも、型がある
専任講師：
Haskell で考えてみましょう。
3 :: Int
3 という値の型は Int です。
タロウくん：
はい。
専任講師：
では、Int の型は何でしょうか。
タロウくん：
・・・型に、型があるのですか。
専任講師：
あります。Haskell では * と記述します。
Int :: *
Bool :: *
[Int] :: *
値に型があるように、型にも「どこに属するか」があるのです。
タロウくん：
考えたことがありませんでした。
専任講師：
この「型を集めた場所」を、宇宙（universe）と呼びます。
宇宙にも、型がある
専任講師：
ここで、次の問いが出てきます。
その宇宙自身は、どこに属するのか。
タロウくん：
・・・宇宙の型、ということですか。
専任講師：
そうです。２つの答え方があります。
答え方①：宇宙は、自分自身に属する。
$$\mathrm{Type} : \mathrm{Type}$$
答え方②：宇宙は、１つ上の宇宙に属する。
$$\mathrm{Type}_0 : \mathrm{Type}_1$$
タロウくん：
①のほうが単純に見えますが。
専任講師：
①を採ると、体系が矛盾します。
「自分自身を含まない集合の集合」を考えると矛盾が生じる、という話をご存じでしょうか。
タロウくん：
ラッセルのパラドックスですね。
専任講師：
型理論でも、同じ形の矛盾が生じます。
$\mathrm{Type} : \mathrm{Type}$ を許すと、「偽である」ことを証明できてしまうのです。
タロウくん：
・・・何でも証明できてしまう。
専任講師：
それでは、証明支援系として使えません。
そこで、②の方式が採られます。
📌 中上級者向け：なぜ `Type : Type` は危険なのか
本文では、$\mathrm{Type} : \mathrm{Type}$ を許すと体系が矛盾すると述べ、ラッセルのパラドックスを引き合いに出しました。
より正確には、型理論では Girard のパラドックスとして知られる結果につながります。
「すべての型を含む型」を、自分自身も含む形で作ってしまうと、体系のなかで非常に強力な自己言及が可能になります。そこから偽を導けてしまうため、無矛盾性を維持できません。
集合論のラッセルのパラドックスと構造が似ていますが、完全に同じものではありません。
型理論の側では、宇宙の階層（universe hierarchy）を導入することで、この問題を回避します。
$$\mathrm{Type}_0 : \mathrm{Type}_1$$
としますが、
$$\mathrm{Type}_1 : \mathrm{Type}_1$$
とはしません。「型について語る型」を、常に１つ上の宇宙に置くわけです。
Arend、Agda、Rocq／Coq、Lean 4 のいずれも、この階層構造を採用しています。
本文では、パラドックスの証明そのものには立ち入らず、「型を全部まとめて自分自身に入れると危険なので、型の世界にも階層を作る」 という直観を押さえることを目的としています。
宇宙の階層
専任講師：
宇宙を、各段階に分けます。
$$\mathrm{Type}_0 : \mathrm{Type}_1 : \mathrm{Type}_2 : \cdots$$
Arend で確かめてみましょう。
\func u0 : \Type0 => Nat
\func u1 : \Type1 => \Type0
\func u2 : \Type2 => \Type1
**＜Arend のコード＞**
型検査を通過します。
| 記述 | 意味 |
|---|---|
\func u0 : \Type0 => Nat |
Nat は $\mathrm{Type}_0$ に属する |
\func u1 : \Type1 => \Type0 |
$\mathrm{Type}_0$ は $\mathrm{Type}_1$ に属する |
\func u2 : \Type2 => \Type1 |
$\mathrm{Type}_1$ は $\mathrm{Type}_2$ に属する |
タロウくん：
・・・段が積み上がっている。
専任講師：
自分自身に属することは、許されません。
\func bad : \Type0 => \Type0
型検査で弾かれます。
＜Arend の型検査結果＞
[ERROR] Type mismatch
Expected type: \Type0
Actual type: \Type1
In: \Type0
**「$\mathrm{Type}_0$ を期待したが、実際は $\mathrm{Type}_1$ だった」**と述べられています。
タロウくん：
・・・１つ上の段にいる。
述語的とは何か
専任講師：
ここからが、MLTT と CIC の違いです。
「すべての型について、〜が成り立つ」という主張を考えてください。
タロウくん：
たとえば、「どんな型 A についても、A から A への恒等関数が存在する」。
専任講師：
まさにそういう主張です。この主張は、どこに属するでしょうか。
タロウくん：
・・・$\mathrm{Type}_0$ でしょうか。
専任講師：
MLTT では、そうなりません。
この主張は $\mathrm{Type}_0$ のすべての型を見渡しています。そのため、１つ上の $\mathrm{Type}_1$ に置かれます。
タロウくん：
・・・見渡している対象より、上に行く。
専任講師：
この性質を、述語的（predicative）といいます。
**「自分自身を含む集まりについて語ることを、階層が禁じている」**ということです。
非述語的とは何か
専任講師：
CIC には、Prop という特別な宇宙があります。
ここでは、事情が違います。
「すべての命題について、〜が成り立つ」という主張も、それ自身 Prop に属します。
タロウくん：
・・・上の段に上がらない。
専任講師：
そのとおりです。この性質を、非述語的（impredicative）といいます。
タロウくん：
先ほどの矛盾は、起きないのですか。
専任講師：
Prop の要素を、Type の要素として自由に取り出せないよう制限されています。
その制限によって、矛盾が生じないことが確かめられています。
タロウくん：
・・・制限つきで、自己言及を許している。
専任講師：
そう捉えていただければ十分です。
宇宙について、２つを並べると
| MLTT | CIC | |
|---|---|---|
| 宇宙の階層 | $\mathrm{Type}_0 : \mathrm{Type}_1 : \cdots$ | 同様の階層を持つ |
| 「すべての型について」 | １つ上の段へ上がる |
Type では同じ |
Prop という宇宙 |
持たない | 持つ |
Prop での「すべての命題について」 |
── | 上の段へ上がらない |
| 呼び名 | 述語的（predicative） |
Prop は非述語的（impredicative） |
タロウくん：
・・・階層そのものは、どちらにもある。
専任講師：
違いは、Prop という例外を設けるかどうかです。
なお、Arend にも \Prop という宇宙があります。 本記事の第８部で扱いますが、CIC の Prop とは別のものです。
Arend の \Prop は、「要素が高々１つしかない型」を集めた宇宙です。 名前は同じですが、意味が違います。
違い② ── 証明と計算の分離
専任講師：
CIC では、Prop と Set／Type を分けています。
Prop に置かれるのは、証明のための命題です。
Set／Type に置かれるのは、計算のためのデータです。
タロウくん：
分けると、何がよいのですか。
専任講師：
プログラムを取り出すときに、Prop の部分を捨てられます。
「この関数は正しい」という証明は、実行時には不要だからです。
タロウくん：
・・・証明を消して、プログラムだけを残す。
専任講師：
MLTT には、もともとこの分離がありません。
証明もデータも、同じ宇宙のなかに置かれます。
２つの系統を並べると
| CIC | MLTT | |
|---|---|---|
| 正式名称 | Calculus of Inductive Constructions | Martin-Löf Type Theory |
| 提唱年 | 1988年（Coquand・Huet ほか） | 1970年代（Martin-Löf） |
| 宇宙の扱い |
Prop は非述語的 |
述語的 |
| 証明と計算 |
Prop と Set を分ける |
分けない |
| 採用している処理系 | Rocq／Coq、Lean | Agda |
📌 中上級者向け：CIC・MLTT と、実際の処理系は一対一に対応しません
本文の表は、依存型理論の大まかな系統を把握するための見取り図です。
実際の証明支援系は、教科書上の CIC や MLTT をそのまま実装したものではありません。
Rocq／Coq、Lean 4、Agda、Arend は、それぞれ宇宙・帰納型・商・証明の消去・等式・公理・計算規則について独自の設計を持ちます。
そのため「Rocq／Coq と Lean 4 は CIC 側」「Agda と Arend は MLTT 側」という分類は、出発点や設計上の親縁関係を示す略図として読むのが適切です。
また、MLTT も CIC も、それぞれ複数のバリエーションがあります。
MLTT にも、体系によって宇宙の扱いや証明の非関係性（proof irrelevance）などの違いがあります。
Prop についても、単純化を避けるべき点があります。
本文では「CIC は Prop と Set／Type を分ける」「MLTT には分離がない」と述べました。
これは教育的な二分法としては有効ですが、次の点は区別しておく必要があります。
- 非述語性（impredicativity）と、証明の非関係性（proof irrelevance）と、消去の制限（elimination restrictions）は、それぞれ別の論点です
- Rocq／Coq の
Propと Lean 4 のPropも、完全に同一視はできません - そして、Arend の
\Propは、これらとはさらに別の設計です。本文で述べたとおり「要素が高々１つしかない型を集めた宇宙」であり、ホモトピーレベルの概念にあたります
本記事では、個々の処理系の完全な形式化を比較するのではなく、等しさ・計算・区間の扱いに関係する設計判断に焦点を絞っています。
タロウくん：
・・・どちらも構成的なのですか？
専任講師：
そうです。
そこは共通しています。
どちらも、「$P$ か $\lnot P$ のどちらかが必ず成り立つ」という排中律を、体系の基本規則としては持ちません。
必要であれば、公理として足すことになります。
タロウくん：
・・・構成的であることは、違いではないということですね？
専任講師：
そのとおりです。
違いは、いま述べた２点 です。
ここまでの流れを、図で整理する
専任講師：
カリー＝ハワード同型対応から、Arend までの流れを図にしました。
青い枠が出発点です。
カリー＝ハワード同型対応から、すべてが始まります。
金色の枠が、それぞれの体系です。
CoC、CIC、MLTT、HoTT Book。
枠のない部分が、何を付け加えたかを示しています。
緑の枠が、本連載の主題である Arend です。
タロウくん：
・・・左の流れが CIC、右の流れが MLTT ですね。
専任講師：
同じ出発点から、２つの系統に分かれています。
そして Arend は、MLTT 側の流れの先にあります。
タロウくん：
・・・HoTT Book に、さらに区間型を加えたもの。
専任講師：
そのとおりです。
nLab にも、そう記されています。
（原文引用）
Arend implements a theory that enhances Book HoTT with an interval type similar to that of cubical type theories, but without the additional structure needed to make univalence computable.
（筆者による日本語訳）
Arend は、立方体型理論のものと似た区間型によって HoTT Book の理論を拡張した体系を実装している。ただし、一価性を計算可能にするために必要な追加の構造は持たない。
出典：formalized libraries of homotopy type theory, nLab
タロウくん：
・・・HoTT Book の理論、というのは。
専任講師：
2013年に刊行された教科書 Homotopy Type Theory: Univalent Foundations of Mathematics で提示された体系です。
MLTT に、一価性公理と高次帰納的型を加えたものだとお考えください。
📌 中上級者向け：HoTT Book を「MLTT ＋ 一価性 ＋ 高次帰納的型」と書いてよいのか
本文では、HoTT Book の体系を
$$\text{HoTT} \approx \text{MLTT} + \text{一価性} + \text{高次帰納的型}$$
という形で紹介しました。
これは、HoTT を初めて学ぶ人に全体像を示すための教育的な表現です。
厳密には、HoTT にはさまざまな体系・変種があり、どの機能を「HoTT の構成要素」と呼ぶかについても文脈があります。
また、HoTT は「MLTT という完成した体系に、２つの機能を後付けしたもの」と考えるだけでは、その数学的背景を十分に表現できません。
それでも、この３つを並べる説明には意味があります。
| 構成要素 | 役割 |
|---|---|
| MLTT | 型を数学的対象として扱う基盤 |
| 一価性（univalence） | 同値な型を「同じ型」として扱う原理 |
| 高次帰納的型（HIT） | 値だけでなく、等式や高次の等式まで構成する仕組み |
この役割分担を意識すると、HoTT がなぜ「型理論でありながら、空間やホモトピーを扱える」のか が見えやすくなります。
本記事では、これを厳密な公理体系の定義としてではなく、HoTT を学ぶための見取り図として使用しています。
先ほどの図で、右側の流れにあたります。
ただし、本記事ではこの分類そのものに深入りしません。
「依存型理論にはいくつかの系統があり、処理系ごとに採用しているものが違う」という程度で、以降の議論は追えます。
タロウくん：
ここまでの議論は理解できたと思います。
では、モデル圏はなんですか？
専任講師：
こちらは、数学の側の道具です。
モデル圏（ model category ）とは、「ものとものを結ぶ道」を抽象的に扱うための枠組みです。
タロウくん：
道、ですか？
先ほどの話に出てきた。
専任講師：
発想は同じです。
もともとは、位相空間の変形 を研究する ホモトピー論 のなかで整備されました。
「２つの図形を連続的に変形して重ねられるか」を扱う分野 です。
そこから、変形そのものを対象として扱えるように抽象化したもの が モデル圏 です。
タロウくん：
・・・空間そのものではなく、変形のしかたを扱う枠組み、なんですね。
専任講師：
そう捉えていただければ十分です。
タロウくん：
先生、モデル圏は、圏論と関係ありますか？
つまり、HoTT を圏論の言葉でモデル化したものがモデル圏ですか？
専任講師：
前半はそのとおりです。
でも、 後半は順序が逆 です。
タロウくん：
・・・逆、ですか。
専任講師：
まず、前半から見ていきましょう。
モデル圏は、圏論の概念です。
タロウくん：
そもそも「圏」とは何ですか。
専任講師：
ものと、ものを結ぶ矢印。それだけです。
矢印のことを、射（ morphism ）と呼びます。
| 圏が持つもの | 説明 |
|---|---|
| 対象 | ものそのもの |
| 射 | 対象から対象への矢印 |
| 射の合成 | 矢印をつないで、新しい矢印を作れる |
| 恒等射 | どの対象にも、自分自身へ戻る矢印がある |
タロウくん：
・・・ずいぶん単純ですね。
専任講師：
単純だからこそ、いろいろなものが圏として扱えます。
- 集合と写像
- 群と準同型
- 位相空間と連続写像
どれも圏です。
モデル圏は、圏に何を加えたのか
専任講師：
モデル圏は、圏に「射の区別」と、それらが満たす条件を加えたものです。
タロウくん：
区別、ですか。
専任講師：
射のなかから、３種類を選び出して名前を付けます。
| 射の種類 | 役割 |
|---|---|
| 弱同値 | 「同じとみなしてよい」ことを表す |
| ファイブレーション | 上から下へ、うまく写せることを表す |
| コファイブレーション | 下から上へ、うまく写せることを表す |
そして、この３つが一定の条件を満たすように定められています。
表にすると、こうなります。
| 圏 | モデル圏 | |
|---|---|---|
| 対象 | ある | ある |
| 射 | ある | ある |
| 射の合成 | ある | ある |
| 恒等射 | ある | ある |
| ３種類の射の区別 | ない | ある |
| その３つが満たすべき条件 | ない | ある |
タロウくん：
・・・圏に、区別と条件を足したもの、ですか。
専任講師：
そういう構造です。
$$\text{圏} + \text{３種類の射の区別} + \text{条件} = \text{モデル圏}$$
タロウくん：
・・・ずいぶん抽象的ですね。
専任講師：
本記事では、条件の中身に踏み込みません。
「圏論の枠組みに、ホモトピー論を扱うための構造を入れたもの」 という程度のイメージを持ち帰っていただけたらと思います。
📌 中上級者向け：モデル圏では、何を区別しているのか
本文では、モデル圏を「圏に射の区別と、それらが満たす条件を加えたもの」と説明しました。
より正確には、モデル圏では射を次の３種類に分類し、それらが一定の公理を満たすことを要求します。
- 弱同値（weak equivalence）
- ファイブレーション（fibration）
- コファイブレーション（cofibration）
公理には、２-out-of-３、レトラクト、持ち上げ、分解といったものが含まれます。
本文では、これらの中身に立ち入っていません。
特に重要なのは「どの射が弱同値なのか」です。
弱同値 は、対象を完全に同一視するのではなく、ホモトピー論的には同じとみなしてよいという関係を表します。
この構造によって、位相空間などの対象について「厳密に同じではないが、ホモトピー論的には同じ」という考え方を、圏論的に扱うことができるようになります。
もう一点、本文の説明には簡略化があります。
本文では「型理論の側で $a = b$ と書かれるものが、モデル圏の側では $a$ から $b$ への射として読める」と述べました。
しかし、モデル圏の任意の射が、そのまま同一視型の経路になるわけではありません。
型理論をモデル圏で解釈するには、文脈や型をどのような対象・射として割り当てるか、依存型をどう表すか、同一視型をどの経路対象（path object）に対応させるかといった構造が必要です。
本文で伝えたい要点は、型理論の等しさが、ホモトピー論における経路や変形と深く対応すると分かった 、という歴史的な事実です。
タロウ君の指摘の後半部分 ── 順序が逆
専任講師：
モデル圏は、HoTT のために作られたものではありません。
1967年に、Daniel Quillen が導入しました。
タロウくん：
1967年・・・。
専任講師：
HoTT の着想が現れたのは2006年ごろです。
モデル圏のほうが、40年近く早いのです。
タロウくん：
・・・では、何のために作られたのですか？
専任講師：
ホモトピー論を、圏論の言葉で抽象化するためです。
位相空間の変形を扱う分野で、「空間そのものではなく、変形の構造だけを取り出したい」という動機がありました。
タロウくん：
・・・HoTT とは無関係に、先にあった。
専任講師：
そうです。
そして、あとから分かったことがあります。
マーティン＝レーフ型理論を、このモデル圏のなかで解釈できる ことが判明したのです。
タロウくん：
・・・先にあった枠組みに、型理論が収まった。こうう流れですね？
専任講師：
そのとおりです。
それを示したのが、Awodey と Warren の2009年の論文です。
経緯を時系列で並べてみる
青い枠が、別々に発展した２つの流れです。
左が幾何学の側、右が型理論の側。
金色の枠で、２つがつながります。
緑の枠が、その到達点です。
タロウくん：
・・・別々に発展したものが、途中でつながった。
専任講師：
そこが、この話の面白いところです。
型理論の側と、幾何学の側。
別々に育っていたものが、同じ構造を持っていたと分かったのです。
「モデル」という語について
タロウくん：
そもそも「モデル」とは、どういう意味ですか？
専任講師：
論理学の用語です。
ある体系の記号や規則に、具体的な意味を割り当てたもの を指します。
タロウくん：
・・・記号に、中身を与える、そういうことですね？
専任講師：
そうです。
たとえば、型理論の側 では、「$a = b$」と記号で書かれています。
モデル圏の側 では、その記号が持つ意味を、「$a$ から $b$ への射」として解釈することができます。
この意味の解釈が、モデルを与えるということ です。
タロウくん：
・・・だから「モデル圏」なのですね。
専任講師：
正確には、モデル圏という名前の由来は別のところにあります。
Quillen が導入したときの「モデル」は、ホモトピー論のモデルを与える圏、という意味 でした。
とはいえ、いま述べた 「記号に意味を割り当てる」という理解 でも、本記事を読み進めるには十分です。
型理論の側で「$a$ と $b$ が等しい」と書かれているものが、
モデル圏の側では「$a$ から $b$ への道」として読むことができる。
この対応が示されたことで、型理論と幾何学がつながりました。
タロウくん：
・・・だから、ホモトピー型理論 という名前なのですね。
専任講師：
そういう経緯です。
なお、本記事ではモデル圏の中身に踏み込みません。
「型理論を空間として読み替えるための枠組みが与えられた」という程度に捉えていただければ、以降の議論は追えます。
一方、ヴラジーミル・ヴォエヴォドスキーは、代数幾何でフィールズ賞を受賞した数学者でした。
論理学と圏論の側から進んだ２人と、代数幾何の側から進んだ１人。
専門も所属も異なる２組が、同じ時期に同じ着想へ至りました。
グルーポイド解釈とは何か
引用文の末尾にある「グルーポイド」について説明します。
行きと帰りが必ず対になっている構造 を指します。
ある点から別の点へ移る道があれば、必ず戻る道もある。
そういう性質を持つものだとお考えください。
日本語では 亜群 とも訳されますが、ホモトピー型理論の文献では片仮名のまま使われることが多いようです。
本稿もそれに倣います。
そして、1998年に Hofmann と Streicher が示したのは、次のことでした。
- 型理論における「等しさ」は、グルーポイドとして解釈できる。
- つまり、等しさの根拠は「行って戻れる道」として読める。
この解釈が、HoTT の出発点になりました。
道として読めるなら、道が複数あってもよい。
道と道のあいだの変形も考えられる。
そこから、ホモトピー論という幾何学の分野とつながっていきます。
第２部 ── 移送とは何か
本連載でこれまで名前だけ挙げてきた３つを、順に見ていきます。
Arend の記号 ── Haskell との対応
本記事では、Arend のコードを何度か示します。
先に、記号の読み方をまとめておきます。
| Arend | 意味 | Haskell でいえば |
|---|---|---|
\data |
データ型を定義する | data |
\func |
関数や値を定義する | 関数定義（f x = ...） |
=> |
定義の本体を書き始める | = |
\Type |
型が置かれる場所 | * |
\Set0 |
等しさの根拠が高々１本の型を集めた場所 | ── |
\Sigma |
組の型を作る | (,) |
\Pi (x : A) -> ... |
依存関数の型 | ── |
-> |
関数の型を作る | -> |
| |
データ型の選択肢を区切る | | |
\elim x |
引数 x について場合分けする |
case x of |
\lam x => ... |
無名関数を作る | \x -> ... |
: |
「〜の型を持つ」 | :: |
{A : \Type} |
暗黙の引数。呼び出し時に書かなくてよい | 型変数 a
|
a = b |
a と b が等しいことを表す型 |
── |
idp |
両辺が計算して同じ形になる証拠 | ── |
path |
区間からの写像を、等しさの根拠に変換する | ── |
@ |
道の指定した位置における値を取り出す | ── |
iso |
一対一の対応から、等しさの根拠を作る | ── |
coe |
等しさの根拠に沿って、値を運ぶ | ── |
I |
区間。両端は left と right
|
── |
Nat.* |
自然数の掛け算 | * |
Nat.+ |
自然数の足し算 | + |
Arend の公式マニュアルは、次のページにあります。
- 言語リファレンス：https://arend-lang.github.io/documentation/language-reference/
- 入門用のチュートリアル：https://arend-lang.github.io/documentation/tutorial/
なお、\ はキーワードの目印です。 Haskell のラムダ式とは異なります。
Haskell の \x -> ... にあたるものは、Arend では \lam x => ... と記述します。
\lam で１つのキーワードです。
等しさの根拠が「値である」とはどういうことか
Haskell で考えてみます。
3 == 3
この式が返すのは True という真偽値です。
「等しい」か「等しくないか」の二択であり、なぜ等しいのかという情報は残りません。
依存型を持つ言語では、事情が違います。
3 = 3
これは、真偽値ではなく型です。
そして、この型に属する値が、「３と３が等しいことの根拠」にあたります。
Arend では、その最も基本的な根拠に idp という名前が付いています。
identity path の略です。
移送 ── 根拠に沿って、値を運ぶ
２つの型が等しいと示せたとします。
このとき、その根拠に沿って、一方の型の値を他方へ運ぶことができます。
この操作を、移送（transport）と呼びます。
Agda では transp、Arend では coe という名前が付いています。
具体例で見ます。
自然数を表す方法は、１つではありません。
単進法 は、1 を並べた本数で数を表す方式です。
５なら 11111。
原始的ですが、証明を書くには扱いやすい形をしています。
二進法 は、101 のように0と1の並びで表す方式です。
桁数が少なくて済むぶん、計算が速くなります。
この２つを、それぞれ別の型として定義したとします。
前者は証明を書きやすく、後者は計算が速い。
両者が等しいと示せば、証明は前者で書き、実行は後者で行うことが可能になります。
根拠が違えば、運ばれる先の値が変わる
Bool の例で考えてみます。
Bool と Bool を過不足なく対応づける方法は、２通りあります。
| 何も変えずに対応させる | 論理反転して対応させる | |
|---|---|---|
| 対応づけ |
true → truefalse → false
|
true → falsefalse → true
|
| 比較するもの |
true と truefalse と false
|
false と falsetrue と true
|
| 結果 | 同じ | 同じ |
ここで比較しているのは、Bool の値どうしではありません。
宇宙の中にある型 Bool 自身どうしです。
HoTT では、型どうしの等しさは同値と対応します。
一価性により、Bool の自己同値が Bool = Bool の道を与えます。
Bool には、恒等の自己同値だけでなく、true と false を入れ替える否定の自己同値もあります。
そのため、宇宙の中では Bool から Bool への道を複数考えることができるのです。
この２つの自己同値から、それぞれ等しさの根拠を作ることができます。
Arend で書いてみます。
\data Bool | true | false
\func boolId (b : Bool) : Bool => b
\func boolIdId (b : Bool) : boolId (boolId b) = b => idp
\func boolNeg (b : Bool) : Bool \elim b
| true => false
| false => true
\func boolNegNeg (b : Bool) : boolNeg (boolNeg b) = b \elim b
| true => idp
| false => idp
\func idPath : Bool = Bool => path (iso boolId boolId boolIdId boolIdId)
\func negPath : Bool = Bool => path (iso boolNeg boolNeg boolNegNeg boolNegNeg)
iso は Arend の組み込みです。
行って戻れば元に帰る対応から、等しさの根拠を作ります。
boolIdId と boolNegNeg が、その「行って戻れば元に帰る」ことの証明にあたります。
そして、それぞれの根拠に沿って true を運びます。
\func movedId : Bool => coe (\lam i => idPath @ i) true right
\func movedNeg : Bool => coe (\lam i => negPath @ i) true right
\func c1 : movedId = true => idp
\func c2 : movedNeg = false => idp
coe が、移送を行う関数です。
型検査の結果です。
＜Arend の型検査結果＞
$ java -jar Arend.jar Q.ard
--- Typechecking \default ---
[ ] src.Q
--- Done (330ms) ---
通りました。
| 根拠 |
true を運ぶと |
|---|---|
idPath |
true |
negPath |
false |
idp は、両辺が計算して同じ形になるときにのみ使える証拠です。
それが通ったということは、処理系が実際に計算し、true と false にそれぞれ到達したということです。
誤った主張は、当然ながら弾かれます。
＜Arend の型検査結果＞
[ERROR] Expressions are not equal
Left: movedId
Right: false
＜Arend の型検査結果＞
[ERROR] Expressions are not equal
Left: movedNeg
Right: true
移送先の型は変わらない
ここで、注意が必要です。
Bool = Bool に沿って移送するのですから、行き先の型は常に Bool です。
変わるのは、運ばれた値のほうです。
根拠とは、「２つの型が等しい」という事実だけを表すものではありません。
「どう対応させて等しいと見なすか」という情報を含んでいます。
その対応が異なれば、運ばれた値も異なる。
これが、根拠を区別する意味です。
第３部 ── 商型とは何か
「これとこれは同じ」を、型に書き込む
ある型の値のうち、いくつかを同一視して作った型を、商型（ quotient type ）といいます。
有理数がその例です。
$1/2$ と $2/4$ は、書き方こそ違いますが同じ数です。
しかし、組として書けば (1,2) と (2,4) であり、別の値になります。
数学では、同一視して割ることを「商をとる」といいます。
商集合、商群、商環。
その型理論版だとお考えください。
なぜ、これが難しいのか
公式論文は、こう述べています。
（原文引用）
The concept of quotient type is well known to be hard to deal with in MLTT due to intensionality of equality.
（筆者による日本語訳）
商型の概念は、等式の内包性ゆえに MLTT では扱いが難しいことがよく知られている。
MLTT は Martin-Löf Type Theory の略です。**
第１部で扱ったマーティン＝レーフ型理論のことです。**
出典：Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"
「等式の内包性」とは、「書き方が違えば別のもの」という扱いのことです。
(1,2) と (2,4) は、値として違う。
この違いを消すには、型の側に「同じものとみなす」という情報を書き込む必要があります。
Arend では、型の定義に書き込める
実際に書いてみます。
＜Arend のコード＞
\data Q
| q Nat Nat
| same (a b k : Nat) : q a b = q (a Nat.* k) (b Nat.* k)
**＜Arend のコード＞**
１行ずつ読み解きます。
| 部分 | 意味 |
|---|---|
\data Q |
Q という型を定義する |
| q Nat Nat |
２つの自然数から Q の値を作る |
| same (a b k : Nat) : ... |
「これとこれは等しい」という主張 |
２行目までは、Haskell と同じです。
＜Haskell で書けば＞
data Q = Q Int Int
問題は、３行目です。
| same (a b k : Nat) : q a b = q (a Nat.* k) (b Nat.* k)
same は、値を作る構成子ではありません。
「q a b と q (a×k) (b×k) が等しい」という主張そのものです。
| 部分 | 意味 |
|---|---|
(a b k : Nat) |
３つの自然数を受け取る |
q a b |
分子 a、分母 b の組 |
q (a Nat.* k) (b Nat.* k) |
分子・分母を k 倍した組 |
= |
この２つが等しい |
Nat.* は、自然数の掛け算です。 Arend では、Nat という名前空間の中の * を指しています。
＜Arend の型検査結果＞
$ java -jar Arend.jar QT.ard
--- Typechecking \default ---
[ ] src.QT
--- Done (150ms) ---
通りました。
実際に使ってみます。
＜Arend のコード＞
\func half1 : Q => q 1 2
\func half2 : Q => q 2 4
\func eq : half1 = half2 => same 1 2 2
＜Arend の型検査結果＞
$ java -jar Arend.jar T3B.ard
--- Typechecking \default ---
[ ] src.T3B
--- Done (132ms) ---
same 1 2 2 が、q 1 2 = q 2 4 の証拠になっています。
$a = 1$、$b = 2$、$k = 2$ を渡した、ということです。
$1/2$ と $2/4$ が、等しいと示せました。
📌 中上級者向け：この `Q` は、有理数の完成形ではありません
本文の Q は、有理数全体を完成させた実装ではありません。
「値の構成子とともに、値どうしを同一視する経路の構成子を型の定義へ記述できる」という高次帰納的型の仕組みを示す最小例です。
実用的な有理数型を構成するなら、次の点を扱う必要があります。
- 分母が０でないことを型のレベルで保証する
- 符号の扱い（負の有理数をどう表すか）
- $a/b$ と $c/d$ が等しいことを表す一般の同値関係（$ad = bc$）
- その同値関係が生成する同一視の閉包
本文の same (a b k : Nat) は、倍率 $k$ による同一視だけを示す簡略化です。たとえば $k = 0$ を許すと、q a b = q 0 0 が作れてしまいます。
また、商型を実用に供するには、除去原理（その型からどう値を取り出すか）と、その整合性も必要になります。
「同一視した値のどちらを渡しても同じ結果になる関数」だけが定義できる、という制約です。
本記事では、こうした点を意図的に省き、商型の直感と、経路構成子の役割に焦点を絞っています。
Haskell の data に並ぶのは値の作り方だけでした。
Arend では、そこに「これとこれは同じ」という項目も並べられます。
この仕組みを、高次帰納的型といいます。
上村太一氏の教科書は、こう説明しています。
（引用）
高次帰納的型は帰納的型の一般化である。通常の帰納的型はいくつかの要素の構成で自由に生成された型で、自然数のなす型、リスト型、余積などがその例である。高次帰納的型は要素の同一視の構成も含めることができる。
出典：上村太一『ホモトピー型理論』2023年、はじめに （著者はホモトピー型理論の意味論を専門とする研究者。アムステルダム大学で博士号を取得）
高次帰納的型そのものについては、本連載の第４回で詳しく扱います。
第４部 ── 関数外延性とは何か
「同じ値を返す関数は、等しい」
２つの関数があるとします。
どんな入力を与えても、同じ値を返す。
このとき、２つの関数は等しいと言ってよいでしょうか。
数学では、等しいと言ってよいことになっています。
しかし、素のマーティン＝レーフ型理論では証明することはできません。
ここで、「素の」とは、第１部で扱ったマーティン＝レーフ型理論に、公理も追加の仕組みも足していない状態を指します。
📌 中上級者向け：関数外延性は、理論設定ごとに事情が違います
本文の「素のマーティン＝レーフ型理論では証明できない」は、内包的な （ intensional ）マーティン＝レーフ型理論を念頭に置いた説明です。
体系によって、事情は次のように異なります。
| 体系 | 関数外延性の扱い |
|---|---|
| 内包的 MLTT | 証明できない |
| 外延的（extensional）型理論 | 基本規則として持つ |
| HoTT | 一価性から導かれる |
| 立方体型理論 | 計算規則を伴う形で実現されることがある |
| Lean 4 | 商型から定理として導かれる |
HoTT では、関数外延性は一価性の帰結です。
独立した公理として足す必要がありません。
本文の論点は、「各入力での等しさ」から「関数そのものの等しさ」へ進むには、通常の反射律だけでは足りず、追加の原理または構造が必要になる、という点にあります。
どの原理を、どの形で足すかは体系ごとに違います。
関数の中身の書き方が違えば、別のものとして扱われるからです。
先ほどの「等式の内包性」と、同じ構図です。
なお、Lean 4 では証明できます
ここで、注意すべき点があります。
Lean 4 は、関数外延性を証明できます。
公理として追加しているのではなく、商型という別の仕組みから導かれる定理です。
（原文引用）
Unlike some intensional type theories, funext is a theorem in Lean. It can be proved using quotient types.
（筆者による日本語訳）
いくつかの内包的型理論とは異なり、
funextは Lean では定理である。
商型を用いて証明できる。
出典：Functions, The Lean Language Reference
ただし、Lean でも代償があります。
Lean のドキュメントは、関数外延性がカーネル内での計算を妨げる例を示しています。
カーネルとは、証明が正しいかどうかを最終的に判定する、処理系の中核部分です。
ここで計算が進まなければ、証明を走らせても具体的な値が出てきません。
関数外延性を使って型を書き換えると、数値に簡約されない Nat 型の閉じた項が生じるのです。
簡約とは、式を計算規則に従って変形し、より単純な形にすることです。
2 + 3 を 5 にする。そういう変形を指します。
（原文引用）
But that is enough to do the damage: under the computational rules of the system, we now have a closed term of ℕ that does not reduce to a numeral.
（筆者による日本語訳）
しかし、それだけで損害を与えるには十分である。体系の計算規則のもとで、我々はいま、数値へ簡約されない
ℕの閉じた項を手にしている。
出典：Axioms and Computation, Theorem Proving in Lean 4
第５部で述べる現象が、Lean でも起きているのです。
Arend では、一行で記述できる
＜Arend のコード＞
\func funExt {A : \Type} {B : A -> \Type} (f g : \Pi (x : A) -> B x)
(h : \Pi (x : A) -> f x = g x) : f = g
=> path (\lam i a => h a @ i)
**＜Arend のコード＞**
型検査は通ります。
型の部分を、順に読みます。
| 部分 | 意味 |
|---|---|
{A : \Type} |
型 A を暗黙に受け取る |
{B : A -> \Type} |
A の値を受け取って型を返す関数 |
(f g : \Pi (x : A) -> B x) |
比べたい２つの関数 |
(h : \Pi (x : A) -> f x = g x) |
どんな x についても f x = g x である、という前提 |
: f = g |
返すのは、f と g が等しいという根拠 |
\Pi は、依存関数の型を作る記号です。
\Pi (x : A) -> B x は、**「A の値 x を受け取って、B x という型の値を返す関数」**を表します。
返り値の型が、引数の値によって変わります。
本体を読み解きます。
=> path (\lam i a => h a @ i)
**＜Arend のコード＞**
| 部分 | 意味 |
|---|---|
path |
区間からの写像を、等しさの根拠に変換する |
\lam i a => ... |
区間の値 i と、A の値 a を受け取る |
h a |
a における等しさの根拠。f a = g a
|
@ i |
その根拠の、位置 i における値 |
h a @ i は、「a における等しさの根拠を、区間の位置 i で見たもの」です。
それを a について束ねると、関数どうしの等しさになります。
中身は、引数の順序を入れ替えただけです。
h は「a を受け取って、道を返す」関数でした。
それを「区間の位置 i を受け取って、関数を返す」形に組み替えているのです。
実際に使ってみます。
＜Arend のコード＞
\data Bool | true | false
\func f1 (b : Bool) : Bool => b
\func f2 (b : Bool) : Bool \elim b
| true => true
| false => false
\func pointwise (b : Bool) : f1 b = f2 b \elim b
| true => idp
| false => idp
\func same : f1 = f2 => funExt f1 f2 pointwise
＜Arend の型検査結果＞
$ java -jar Arend.jar T3C.ard
--- Typechecking \default ---
[ ] src.T3C
--- Done (145ms) ---
**＜Arend のコード＞**
f1 と f2 は、書き方が違います。
f1 は受け取った値をそのまま返し、f2 は場合分けして返しています。
しかし、どんな入力に対しても同じ値を返します。
pointwise が、そのことの証明です。
そして funExt に渡すと、f1 = f2 が得られます。
公式論文は、この点をこう述べています。
（原文引用）
Function extensionality is provable in Arend and computes well.
（筆者による日本語訳）
関数外延性は Arend で証明可能であり、計算的に良く振る舞う。
出典：Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"
第５部 ── 公理として足すと、何が起きるのか
ここまでの３つを、公理として足す方法でも実現できます。
Rocq／Coq 上で HoTT 的な数学を展開する代表的なライブラリには、Coq-HoTT や UniMath があります。
これらは、Cubical Agda のようにカーネルの定義的計算規則として一価性を実装する方式とは異なります。
なお、Coq-HoTT と UniMath は、目的・基盤・採用する公理・実践上の立場が完全に同じではありません。
本記事では、「カーネルに立方体型理論の計算規則を持たない処理系の上で HoTT 的数学を展開する」という点でまとめて扱います。
公理には、計算規則が伴わない
この点について、査読論文が述べています。
（原文引用）
This approach can, in principle, be implemented using an ITP based on MLTT, such as Coq or Agda, by merely appending univalence and higher inductive types as axioms devoid of any computational content. However, this severely impairs the computational properties of MLTT, which are crucial for practical formalization efforts.
（筆者による日本語訳）
この手法は、原理的には Coq や Agda のような MLTT に基づく対話型定理証明系を用いて実装できる。一価性と高次帰納的型を、計算内容を一切持たない公理として単に付け加えればよい。しかし、これは MLTT の計算的性質を著しく損なう。計算的性質は、実際の形式化の作業において決定的に重要である。
出典：Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"
「計算内容を一切持たない公理」という表現が使われています。
具体的に、何が止まるのか
先ほどの移送で考えます。
根拠を公理として認める場合でも、移送そのものはできます。
「Bool と Bool は等しい」と宣言し、その根拠に沿って true を運ぶ。式としては記述できます。
しかし、その式が何になるのかを、処理系が求められません。
movedNeg を計算しても、false にたどり着かない。式がそのまま残ります。
証明としては成立します。しかし、プログラムとしては動きません。
先ほどの単進法と二進法の使い分けは、この場合には成立しません。
第６部 ── 正準性とは何か
正準性の定義
すでに公開済みの記事で解説済みですが、ここで改めて解説します。
正準性とは、閉じた項が必ず正準形へ評価されるという性質です。
イメージとしては、自然数の計算で 2 + 3 が評価されれば 5 のような正準的な値に到達する、ということです。
自然数について正確に述べると、こうなります。
「自然数の型に属する閉じた項は、すべて zero と successor だけを使って構成されたものと同一である」
「閉じた」とは、自由な変数を含まないという意味です。
n + 3 は変数 n を含むので、閉じていません。
2 + 3 は閉じています。
Arend は正準性を備えていない
Arend の開発者自身が、Arendを公開した際に、以下のように発言しています。
（原文引用）
Does Arend have the canonicity property, i.e. does it evaluate closed expressions to their canonical forms? No, but it computes more terms than ordinary homotopy type theory, which makes it more convenient in many aspects.
（筆者による日本語訳）
Arend は正準性を持つか、すなわち閉じた式を正準形へ評価するか。いいえ。しかし通常のホモトピー型理論より多くの項を計算するため、多くの面でより便利になっている。
出典：
New theorem prover Arend is released, Homotopy Type Theory mailing list, 2019年8月6日
nLab の記述
型理論の事典である nLab にも、同じ趣旨の記述があります。
（原文引用）
Arend implements a theory that enhances Book HoTT with an interval type similar to that of cubical type theory, but without the extra structure necessary to make univalence computational.
（筆者による日本語訳）
Arend は、立方体型理論のものと似た区間型によって HoTT Book の理論を拡張した体系を実装している。ただし、一価性を計算可能にするために必要な追加の構造は持たない。
出典：formalized libraries of homotopy type theory, nLab
「一価性を計算可能にするために必要な追加の構造」── その中身が、次に述べる二層理論です。
では、HoTT がない言語ではどうなるのか
タロウくん：
先生、確かめさせてください。
HoTT の計算規則が定義されていない定理証明言語では、移送・商型・関数外延性の３つは、できないのですか？
また、HoTT を公理としてのみ定義した言語では、どうですか？
専任講師：
まず、言語を３つに分けて考えましょう。
| 言語の状態 | 例 | |
|---|---|---|
| ① | HoTT を一切持たない | Rocq／Coq、Agda（標準）、Lean 4 |
| ② | HoTT を公理としてのみ持つ | Rocq／Coq 上の HoTT ライブラリ |
| ③ | HoTT の計算規則を持つ | Arend、Cubical Agda |
タロウくん：
①と②が、私の質問にあたりますね。
専任講師：
そのとおりです。そして、移送・商型・関数外延性のそれぞれで事情が違います。
順に見ていきましょう。
①移送について
専任講師：
「同じ型の値どうし」の移送なら、HoTT を一切持たない言語でもできます。
$a = b$ という道があるとき、$a$ について示したことを $b$ へ運ぶ。
これは HoTT がなくても可能です。
タロウくん：
・・・普通のプログラミングでも、やっていることでは？
専任講師：
似て見えますが、違います。
＜Python で書けば＞
a = 4
b = 2 + 2
def is_even(n):
return n % 2 == 0
# a が偶数だと分かっている
assert is_even(a)
# a と b は等しいので、b も偶数のはず
assert a == b
assert is_even(b) # ← これは「実行して確かめた」だけ
タロウくん：
・・・最後の行も、実行すれば通りますね。
専任講師：
そこが違うのです。
Python では、実際に b を計算して、２で割った余りを見ています。
「a が偶数だから b も偶数」という推論を、言語がしているわけではありません。
＜Haskell で書けば＞
a :: Int
a = 4
b :: Int
b = 2 + 2
isEven :: Int -> Bool
isEven n = n `mod` 2 == 0
-- a == b は True を返す
-- しかし「a が偶数なら b も偶数」を型で述べる手段がない
タロウくん：
Haskell でも、同じですか？
専任講師：
a == b は True を返します。しかし、そこで終わります。
「a について示したことを、b へ運ぶ」という操作が、言語の側にありません。
タロウくん：
先生、待ってください。
さきほど、「$a = b$ という道があるとき、$a$ について示したことを $b$ へ運ぶ。
これは HoTT がなくても可能です」とおっしゃいました。**
しかし、Python も Haskell もできないのですよね。
あの説明は、誤りではありませんか？
専任講師：
言葉が足りませんでした。
「HoTT がなくても可能」という話には、前提があります。
タロウくん：
前提、ですか。
専任講師：
依存型を持っている、という前提です。
タロウくん：
・・・依存型がなければ、そもそも・・・。
専任講師：
a = b が型になりません。
タロウくん：
先生、待ってください。
依存型がなくても、高階型があればできるのではありませんか。
Haskell の Maybe は、型を受け取って型を返します。
型を作る関数があるなら、a = b も作れそうに思えます。
専任講師：
第１部で述べた３つの拡張を、思い出してください。
| 拡張 | 何ができるか | Haskell に |
|---|---|---|
| 第１ | 値が型に依存する | ある |
| 第２ | 型が型に依存する（高階型） | ある |
| 第３ | 型が値に依存する（依存型） | ない |
高階型は、第２の拡張です。
タロウくん：
・・・型を受け取って、型を返す。
専任講師：
a = b を作るには、何を受け取る必要がありますか。
タロウくん：
a と b を・・・あ。
専任講師：
a と b は、値です。
値を受け取って型を返す。それが第３の拡張、つまり依存型です。
タロウくん：
高階型では、値を受け取れない。
専任講師：
そこが違いです。
Maybe Int の Int は型です。3 = 3 の 3 は値です。
受け取るものが違います。
タロウくん：
・・・高階型がいくらあっても、届かない。
専任講師：
そのとおりです。
なお、Haskell にも型どうしの等しさを表す仕組みはあります。
data a :~: b where
Refl :: a :~: a
これは、a と b という「型」が等しいことを表します。
タロウくん：
値どうしではない。
専任講師：
そこが限界です。
DataKinds という拡張を使えば、値を型のレベルへ持ち上げることはできます。
しかし、持ち上げたものについての等しさであって、値そのものの等しさではありません。
そして、標準の Haskell の範囲を超えます。
タロウくん：
・・・話を戻します。依存型がないと、どうなるのでしたか。
専任講師：
a = b が型になりません。
型にならないので、「その型の値」も存在しません。
運ぶべき根拠が、はじめから無いのです。
タロウくん：
Python と Haskell は、そこで止まっている。
専任講師：
そのとおりです。
必要なものを整理すると、こうなります。
| やりたいこと | 必要なもの |
|---|---|
a = b を型として記述する |
依存型 |
値どうしの移送（3 = 3 の根拠に沿って運ぶ） |
依存型のみ。HoTT は不要 |
型どうしの移送（Bool = Bool の根拠に沿って運ぶ） |
依存型に加えて、一価性 |
タロウくん：
・・・私が挙げた Python と Haskell は、いちばん上の行から満たしていない。
専任講師：
そこが要点です。
Rocq／Coq、Agda、Lean 4 は、依存型を持っています。
だから、HoTT がなくても値どうしの移送ができるのです。
タロウくん：
最初の説明は、定理証明支援系の話だった。
専任講師：
そう述べるべきでした。
依存型を持つ言語であれば、HoTT がなくても値どうしの移送ができます。
しかし、型どうしの移送は、依存型があっても、一価性（HoTT）が定義されていないと移送できません。
タロウくん：
先生、そこを確かめさせてください。
型どうしの移送ができるようになるためには、公理として HoTT を定義するだけで事足りますか？
それとも、HoTT の計算規則まで定義しないとだめですか？
専任講師：
「移送できる」を２つに分けると、答えが出ます。
| 何をしたいか | 公理として足すだけ | 計算規則まで持つ |
|---|---|---|
| 移送する式を記述し、型検査を通す | できる | できる |
| 移送した結果を、具体的な値として得る | できない | できる |
タロウくん：
・・・記述だけなら、公理で足りる。
専任講師：
そうです。
「一価性は正しいものとする」と宣言すれば、それを使った移送の式を記述できます。型検査も通ります。
タロウくん：
では、何ができないのですか。
専任講師：
運んだ結果が、具体的な値になりません。
公理には計算規則が伴わないので、式がそのまま残ります。
タロウくん：
・・・単進法で書いた証明を二進法へ運んでも、動かない。
専任講師：
そこが第５部で扱う内容です。
証明としては成立します。しかし、プログラムとしては動きません。
📌 中上級者向け：「公理を足すと計算が止まる」とは、正確には何が止まるのか
本文でいう「計算が止まる」は、Rocq／Coq や Lean 4 のプログラム一般が実行不能になる、という意味ではありません。
問題になるのは、ある種の公理に依存する閉じた項について、自然数などの具体的な正準形まで定義的に還元できない場合が生じることです。
すなわち、証明としては利用できても、評価器がその項を 0、1、true、false のような具体値へ計算しきれないことがあります。
「Rocq／Coq や Lean 4 は計算できない」という一般化は、正確ではありません。 これらの処理系は、公理を使わない部分では通常どおり計算します。止まるのは、公理を通過する特定の項です。
また、どの性質が保たれるかは、体系・公理・評価戦略・拡張の仕方によって異なります。
本文では、HoTT に関する原理を「計算規則を伴って組み込む」設計と、「公理として仮定する」設計の違いを説明することに焦点を絞っています。
タロウくん：
計算規則まで持てば、値になる。
専任講師：
Arend や Cubical Agda が、その方式です。
ただし、Arend も完全ではありません。
区間変数を含んだままの式では、計算が途中で止まってしまうのです。
定理証明支援系では、運ぶ操作が定義できます
専任講師：
Arend で書いてみます。
＜Arend のコード＞
\func subst {A : \Type} (B : A -> \Type) {x y : A} (p : x = y) (b : B x) : B y \elim p
| idp => b
これが、値どうしの移送です。
| 部分 | 意味 |
|---|---|
(B : A -> \Type) |
A の値を受け取って、性質を返す関数 |
(p : x = y) |
x と y が等しいという根拠 |
(b : B x) |
x がその性質を持つという証拠 |
: B y |
返すのは、y がその性質を持つという証拠 |
タロウくん：
・・・「x について示したこと」を、y へ運んでいる。
専任講師：
使ってみましょう。
＜Arend のコード＞
\data IsEven (n : Nat) \elim n
| 0 => evenZero
| suc (suc m) => evenStep (IsEven m)
\func fourIsEven : IsEven 4 => evenStep (evenStep evenZero)
\func p : 4 = {Nat} 4 => idp
\func moved : IsEven 4 => subst IsEven p fourIsEven
＜Arend の型検査結果＞
$ java -jar Arend.jar SUBST.ard
--- Typechecking \default ---
[ ] src.SUBST
--- Done (191ms) ---
IsEven が「偶数である」という性質です。
fourIsEven が、「４は偶数である」という証拠 です。
そして subst が、その証拠を等しさの根拠に沿って運んでいます。
タロウくん：
Python では、運んだのではなく、計算し直していた。
専任講師：
そこが違いです。
この subst に、HoTT は要りません。
Rocq／Coq でも Agda でも Lean 4 でも、同じことができます。
②商型について
専任講師：
こちらは、HoTT の有無とは別の話です。
| 言語 | 商型の扱い |
|---|---|
| Lean 4 |
組み込みで持っている（Quot） |
| Rocq／Coq | 組み込みでない。同値関係を手で持ち回る方式が一般的 |
| Agda（標準） | 組み込みでない |
| Cubical Agda | 高次帰納的型として作れる |
| Arend | 高次帰納的型として作れる |
タロウくん：
Lean 4 は、HoTT を持たないのに商型があるのですか。
専任講師：
そうです。HoTT とは別の仕組みとして、体系に組み込まれています。
「HoTT がないと商型が作れない」というわけではありません。
「高次帰納的型として作れる」とは、どういうことか
タロウくん：
表の下の２行に「高次帰納的型として作れる」とあります。
これは、どういう意味ですか。
専任講師：
第３部で見たコードを、思い出してください。
＜Arend のコード＞
\data Q
| q Nat Nat
| same (a b k : Nat) : q a b = q (a Nat.* k) (b Nat.* k)
タロウくん：
・・・same が、「これとこれは等しい」という主張でした。
専任講師：
Haskell の data に並ぶのは、値の作り方だけです。
＜Haskell で書けば＞
data Q = Q Int Int
構成子は Q ひとつ。値をどう作るかを述べているだけです。
タロウくん：
Arend では、そこに等しさも並べられる。
専任講師：
この仕組みが、高次帰納的型です。
| データ型の種類 |
data に並べられるもの |
|---|---|
| 通常の帰納的型 | 値の作り方だけ |
| 高次帰納的型 | 値の作り方＋「これとこれは同じ」という指定 |
タロウくん：
・・・商型は、その仕組みで作れる。
専任講師：
「同じとみなしたいもの」を、型の定義に書き込むわけです。
$1/2$ と $2/4$ を同じとみなしたい。そう思ったら、same の行を並べます。
Lean 4 の方式との違い
タロウくん：
Lean 4 は、どうやって商型を作っているのですか。
専任講師：
Quot という組み込みの仕組みを使います。
「型」と「その上の同値関係」を渡すと、商型を返してくれます。
タロウくん：
・・・専用の仕組みが用意されている。
専任講師：
並べると、こうなります。
| 方式 | 商型の作り方 |
|---|---|
| Lean 4 | Quot という専用の仕組みに、型と同値関係を渡す |
| Arend／Cubical Agda | data の定義のなかに、等しさを直接書き込む |
タロウくん：
・・・どちらでも、商型は得られる。
専任講師：
そうです。
ただし、Arendは、商型以外のものも同じ仕組みで作れます。
例えば、円周や球面といった図形も、この仕組みで型として定義することができます。
「点をひとつ置き、その点から自分自身への道をひとつ置く」。
それだけで、円周を表す型になります。
タロウくん：
・・・図形を、データ型として書くのですね。
専任講師：
高次帰納的型そのものについては、本連載の第４回で詳しく扱います。
③関数外延性について
専任講師：
HoTT を一切持たない言語では、原則として証明できません。
しかし、Lean 4 は証明できます。
タロウくん：
・・・先ほど扱った話ですね。商型から導かれる定理だと。
専任講師：
そうです。ここでも、HoTT は必須ではありません。
ただし、Lean 4 でも代償があります。
関数外延性を使って型を書き換えると、数値へ簡約されない項が生じます。
３つを並べると
| ① HoTT を持たない | ② 公理としてのみ持つ | ③ 計算規則を持つ | |
|---|---|---|---|
| 値どうしの移送 | できる | できる | できる |
| 型どうしの移送 | できない | 記述はできる。計算は進まない | できる |
| 商型 | 言語による（Lean 4 は持つ） | 記述はできる | できる |
| 関数外延性 | 言語による（Lean 4 は証明できる） | 記述はできる | できる |
タロウくん：
③だけが、値まで届く。
専任講師：
ただし、Arend も完全ではありません。
区間変数を含んだままの式では、計算が途中で止まります。
ここまでを、まとめると
タロウくん：
ここまでの議論をまとめると、こういうことですね。
計算規則として HoTT を持たない定理証明言語では、型レベルまでフルスペックに、移送・商型・関数外延性の３つをできない。
専任講師：
移送については、そのとおりです。
しかし、商型と関数外延性は、少し違います。
タロウくん：
違う、といいますと。
専任講師：
Lean 4 が反例になります。
Lean 4 は HoTT を持ちません。
しかし、商型を組み込みで持っています。
そして、その商型を使って、次の定理を証明できます。
＜Lean 4 のコード＞
theorem funext {f g : (x : α) → β x}
(h : ∀ x, f x = g x) : f = g
「どんな x についても f x = g x であるならば、f と g は等しい」という主張です。
タロウくん：
・・・関数外延性そのものですね。
専任講師：
そうです。公理として足したのではありません。
すでに体系にある商型から、導き出しています。
タロウくん：
・・・HoTT がなくても、その２つは手に入る。
専任講師：
３つを分けて整理しましょう。
| 計算規則として HoTT を持たない言語で、どこまでできるか | |
|---|---|
| 値どうしの移送 | **できる。**依存型さえあればよい |
| 型どうしの移送 | **できない。**公理として足せば記述はできるが、計算が進まない |
| 商型 | **言語による。**Lean 4 は組み込みで持つ |
| 関数外延性 | **言語による。**Lean 4 は商型を使って証明できる |
タロウくん：
・・・「３つとも一律にできない」ではなかった。
専任講師：
HoTT が決定的に効いてくるのは、型どうしの移送です。
「２つの型が等しい」と言い、その根拠に沿って値を運ぶ。
これだけは、一価性なしには成り立ちません。
（より厳密に述べると、「同値から型の等しさを得て、その等しさに沿って値を移送する」という HoTT 的な仕組みには、一価性が決定的に関係します、という表現が適切です。）
タロウくん：
Lean 4 でも、できないのですか。
専任講師：
できません。
Lean 4 が反例になるのは、商型と関数外延性の２つについてだけです。
タロウくん：
なぜ、型どうしの移送だけができないのですか。
専任講師：
理由を、３つ挙げます。
理由① ── 等しさを作る手段が、ひとつしかない
専任講師：
Lean 4 の等しさは、次のように定義されています。
＜Lean 4 のコード＞
inductive Eq : α → α → Prop where
| refl (a : α) : Eq a a
構成子は refl ひとつだけです。
タロウくん：
・・・Arend の idp にあたるものですね。
専任講師：
そのとおりです。そして、それしかありません。
A = B を作るには、A と B が計算して同じ形にならなければなりません。
タロウくん：
Bool と Bool なら、同じ形ですが。
専任講師：
そのときは rfl で作れます。しかし、それは「何も変えない対応」だけです。
true と false を入れ替える対応から Bool = Bool を作る。その手段がありません。
理由② ── 同値から等しさを導く関数がない
専任講師：
Lean 4 にも、同値を表す仕組みはあります。
＜Lean 4 のコード＞
-- 2つの型のあいだの一対一対応
structure Equiv (α β : Sort u) where
toFun : α → β
invFun : β → α
left_inv : ∀ a, invFun (toFun a) = a
right_inv : ∀ b, toFun (invFun b) = b
「行って戻れば元に戻る」対応です。
タロウくん：
Arend の iso に渡していたものと、同じ形ですね。
専任講師：
中身は同じです。しかし、続きがありません。
Arend では、この対応から path (iso ...) で等しさの根拠を作れました。
Lean 4 には、それにあたる関数がないのです。
タロウくん：
・・・対応は作れるが、そこから等しさへ渡れない。
専任講師：
その橋渡しをするのが、一価性公理です。
$$\mathsf{ua} : (A \simeq B) \to (A = B)$$
Lean 4 の標準には、これがありません。
理由③ ── Lean 4 は、逆の方向を向いている
専任講師：
さらに、Lean 4 には別の事情があります。
「等しさの根拠は、高々１本である」という性質と両立するように設計されています。
タロウくん：
・・・一価性とは、逆ですね。
専任講師：
Bool = Bool の根拠が２本ある、というのが一価性でした。
Lean 4 は、そうならない方向を選んでいます。
タロウくん：
・・・一価性を足すと、矛盾するのですか。
専任講師：
Lean 4 の標準の体系に一価性をそのまま足すと、両立しない部分が生じます。
そのため、Lean 4 で HoTT を扱うには、体系の一部を制限した別の枠組みを用意することになります。
では、商型と関数外延性はなぜできるのか
タロウくん：
では、なぜ商型と関数外延性はできるのですか。
専任講師：
どちらも、値どうしの等しさだからです。
＜Lean 4 のコード＞
-- 同値な2つの値は、商型では等しくなる
theorem Quot.sound : a ≈ b → Quot.mk r a = Quot.mk r b
Quot.mk r a と Quot.mk r b は、値です。
タロウくん：
型どうしではない。
専任講師：
関数外延性も同じです。
「２つの関数が等しい」。関数も値です。
タロウくん：
・・・Lean 4 が作れるのは、値どうしの等しさ。
（より厳密に述べると、Lean 4 には、同値な型から直接 A = B を作る一価性が標準の体系にない、という表現が適切です。）
📌 中上級者向け：Lean 4 の `funext` は定理ですが、計算とは別の問題です
本文では、Lean 4 が関数外延性を商型から導いていると述べました。
「定理として証明できる」ことと、「その証明が定義的に計算され、常に具体的な正準形まで還元される」ことは、別の問題です。
Lean 4 の商型を経由して得られる等しさは、型検査や証明には利用できます。
しかし、計算規則の観点では、立方体型理論の系統における関数外延性と同じ挙動を保証するものではありません。
本文で引いた Lean 4 の公式ドキュメントが、まさにその点を述べています。
もう一点、本文の整理について補足します。
本文では、「商型と関数外延性は、どちらも値どうしの等しさだから Lean 4 でもできる」と述べました。
関数はたしかに項（term）ですが、関数外延性が成り立つ理由は「値どうしだから」という一言に還元できるものではありません。
より正確には、Lean 4 には、同値な型から直接 $A = B$ を作る一価性が、標準の体系にない、というのが型どうしの移送ができない理由です。
商型と関数外延性については、一価性とは別の仕組みが体系に用意されている、ということです。
本文では、この差を第５部・第６部の「公理と計算」「正準性」の議論へつなげるために、簡略化した整理を採っています。
専任講師：
型どうしの等しさを、同値から作ることはできません。
そこが、Lean 4 の限界です。
| Lean 4 で作れるか | |
|---|---|
| 値どうしの等しさ |
作れる（rfl、Quot.sound、funext） |
| 型どうしの等しさ（定義的に同じ場合） |
作れる（rfl） |
| 型どうしの等しさ（同値から作る場合） | 作れない。一価性が必要 |
タロウくん：
・・・いちばん下の行だけが、HoTT の領分。
専任講師：
そこが、本記事の主題につながります。
標準の Haskell では、どうなるのか
タロウくん：
最後に、もう１つ。
特別なライブラリを組み込まず、標準の Haskell を使う場合はどうですか。
公理としても、計算規則としても HoTT が定義されていません。
移送・商型・関数外延性の３つは、できないのでしょうか。
専任講師：
本記事で述べた意味では、３つとも扱えません。
理由は、HoTT の有無より手前にあります。
タロウくん：
手前、といいますと。
専任講師：
Haskell には、依存型がありません。
そのため、3 = 3 が型になりません。
＜Haskell のコード＞
3 == 3
これは True という値を返して終わります。
タロウくん：
・・・等しさが型でないなら、その中身も問えない。
専任講師：
そこが出発点です。
等しさの根拠を値として持てないので、根拠に沿って運ぶ という操作も定義できません。
タロウくん：
では、商型は。
専任講師：
Haskell では、newtype と限定された構成子で近いことができます。
分数を作るときに、必ず約分してから作る。
そういう規約を設けるわけです。
しかし、それは型が保証しているのではありません。
ライブラリが、規約として遵守することを求めているだけです。
タロウくん：
・・・型検査は、その規約を確かめてくれない。
専任講師：
そこが違いです。
Arend の \data Q では、「これとこれは同じ」が型の定義に書き込まれています。
タロウくん：
関数外延性は、どうですか。
専任講師：
Haskell では、そもそも問いとして立ちません。
「２つの関数が等しい」という主張を、型として記述できないからです。
タロウくん：
・・・等しさを型にできないと、何も始まらない。
専任講師：
そこが、本記事の主題です。
なお、Haskell にも型レベルで等しさを扱う仕組みはあります。 GADTs や TypeFamilies を使うと、限定的に依存型に近いことができます。
しかし、「等しさの根拠が複数ある」という状況は扱えません。
第７部 ── 二層理論とは何か
前回の記事で扱った内容を、振り返ります
専任講師：
本記事から読み始めた方もいらっしゃるでしょうから、前回の記事で扱った内容を、ここで振り返っておきます。
タロウくん、覚えていますか。
タロウくん：
・・・区間 I の話でしたね。
専任講師：
そのとおりです。順に確かめましょう。
おさらい① ── 区間とは何か
専任講師：
区間は、両端を持つ線分だとお考えください。Arend では I と記述します。
両端には、left と right という名前が付いています。
等しさの根拠を、この区間から型への写像として表しました。
$$p : I \to X, \qquad p(\mathsf{left}) = a, \qquad p(\mathsf{right}) = b$$
始点が一方の値、終点が他方の値に対応します。
タロウくん：
・・・先ほどのコードに出てきた \lam i => idPath @ i の i が、この区間の点ですね。
おさらい② ── 区間は、実数の閉区間ではありません
専任講師：
ここで、誤解しやすい点に触れておきます。
「線分」と聞くと、実数の数直線を思い浮かべる方がいらっしゃるでしょう。
でも、区間 I は実数の閉区間ではありません。
たとえば 3 と 5 を比べるとき、区間の両端が数 3 と数 5 になるわけではありません。
区間 I の両端は、常に left と right です。
$$\mathsf{left} : I, \qquad \mathsf{right} : I$$
一方、3 と 5 は自然数型 Nat の値です。
$$3 : \mathrm{Nat}, \qquad 5 : \mathrm{Nat}$$
この２つは、別の型に属しています。
そして、区間の中間点が 3.41 や 4.74、あるいは $3\sqrt{7}$ を表しているわけでもありません。
これらは、実数の閉区間 $[3,5]$ に属する数です。
$$I \neq [3,5] \subseteq \mathbb{R}$$
left と right は、道を記述するための抽象的な両端です。
タロウくん：
・・・比べる対象が変わっても、区間は同じ。
専任講師：
そのとおりです。整数を比べようが、文字列を比べようが、使う区間は同じ I です。
変わるのは、写像 $p$ の行き先と、両端に置かれる値のほうです。
| 何が変わるか | |
|---|---|
| 区間 $I$ | 変わらない。常に同じ区間 |
| 道 $p$ | 比べる対象ごとに変わる |
| 行き先 $X$ | 比べる対象が属する型 |
おさらい③ ── ２つの操作
専任講師：
証明を最後まで走らせるには、２つの操作が要りました。
| 操作 | 何をするか | Agda での名前 | Arend での名前 |
|---|---|---|---|
| 値を運ぶ | 道に沿って、値を別の型へ移す | transp |
coe |
| 隙間を埋める | 描きかけの道の残りを補う | hcomp |
── |
hcomp は homogeneous composition（等質合成）の略です。
道どうしを合成して、新しい道を作る操作を指します。
なお、Arend には hcomp にあたる名前の操作がありません。
対応する働きは、道についての場合分けを通じて処理系が引き受けます。
タロウくん：
Arend では coe が、値を運ぶ操作でした。
専任講師：
そして iso が、等しさの根拠を作る操作です。
先ほど第２部で見たコードを、もう一度示します。
\func negPath : Bool = Bool => path (iso boolNeg boolNeg boolNegNeg boolNegNeg)
\func movedNeg : Bool => coe (\lam i => negPath @ i) true right
\func c2 : movedNeg = false => idp
true を運んだ結果が false になりました。
処理系が実際に計算した、ということです。
おさらい④ ── Kan 条件
専任講師：
この２つの操作は、Kan 条件として現れます。
Kan は人名です。 代数トポロジーの数学者、Daniel M. Kan に由来します。
もとは、図形についての条件でした。
三角形を思い浮かべてください。
３辺のうち、２辺だけが描かれている状態があるとします。
残りの１辺を、必ず補えるか。
補えるなら、その図形は Kan 条件を満たします。
欠けた部分を、いつでも埋められるということです。
タロウくん：
その２つの操作から、何が導かれるのですか。
専任講師：
等しさについて当たり前に使っている性質が、すべてここから出てきます。
「$a = a$ である」。「$a = b$ なら $b = a$ である」。「$a = b$ かつ $b = c$ なら $a = c$ である」。
（原文引用）
Now, the common properties of equalities can all be derived: reflexivity by constant functions from I, symmetry by negating the interval variable of a path, transitivity by the hcomp operation, and substitutivity by applying transp with predicates.
（筆者による日本語訳）
これにより、等しさの通常の性質はすべて導かれる。反射性は区間からの定数関数によって、対称性は道の区間変数を反転させることによって、推移性は
hcomp操作によって、代入はtranspを述語に適用することによって得られる。
出典："Towards Computational UIP in Cubical Agda", arXiv:2511.21209
おさらい⑤ ── 区間だけが例外
専任講師：
通常の型は、この条件を満たすように設計されています。
Nat も Bool も、組の型も関数の型も、すべて対象に含まれます。
しかし、区間だけは例外でした。
タロウくん：
理由が２つありましたね。
専任講師：
１つは型検査です。
区間を通常の型として扱うと、$f : \mathbb{N} \to \mathbb{I}$ のような関数が記述できてしまう。そうした自由を許すと、型検査が有限時間で終わる保証を失いかねません。
もう１つは、区間の上に「欠けた部分を埋める」構造を定義できないことです。
（原文引用）
There are multiple reasons for this distinction. One is that the interval should not participate in any type formers, so for example we cannot have functions $f: \mathbb{N} \to \mathbb{I}$ which easily make type-checking undecidable. Another reason is the interval is not Kan, i.e. we cannot define a composition structure on it, and it cannot be interpreted semantically as a space.
（筆者による日本語訳）
この区別には、複数の理由がある。１つは、区間が型構成子に一切関与すべきでないということである。たとえば $f : \mathbb{N} \to \mathbb{I}$ のような関数を許すと、型検査の決定可能性を容易に失いうる。もう１つの理由は、区間が Kan でないことである。すなわち、区間の上に合成構造を定義することができず、区間を空間として意味論的に解釈することもできない。
合成構造とは、道と道をつなぐ操作、および欠けた部分を埋める操作をまとめたものです。先ほど述べた transp と hcomp が、これにあたります。
出典："Normal forms in cubical type theory", arXiv:2603.24923
なお、この文献はプレプリントです。 区間を特別なソートに置く理由そのものは、Agda 公式ドキュメントにも記されており、本記事はそちらを主たる根拠としています。
上の引用は、理論的背景の補足として引きました。
おさらい⑥ ── 両言語の分かれ目
専任講師：
Arend は、区間を普通の型として扱いました。
Nat や Bool と同じ場所、すなわち \Type に置いたのです。
\func t1 : \Type => Nat
\func t2 : \Type => I
**＜Arend のコード＞**
どちらも型検査を通過します。
Cubical Agda は、区間を型の外に置きました。IUniv という特別なソートです。
区間 I の置き場所 |
普通の型の置き場所 | |
|---|---|---|
| Arend | \Type |
\Type |
| Cubical Agda | IUniv |
Set |
タロウくん：
・・・その結果、Arend では計算が途中で止まる場合がある。
専任講師：
その代わり、理論は単純に保たれます。
そして Cubical Agda は、そのぶん理論が複雑になりました。
この二層に分かれた構造を、二層理論と呼びます。
タロウくん：
・・・型が置かれる場所が、２つに分かれている。
専任講師：
そのとおりです。
**なお、区間の場合分けが禁じられている点は、Arend でも Cubical Agda でも共通です。
** 両者の違いではありません。
前回の記事では論じなかった論点が、残っています
専任講師：
ここまでが、前回の振り返りです。
しかし、論じ残したことが２つあります。
タロウくん：
何でしょうか。
専任講師：
１つは、デカルト立方体型理論という別の体系での例です。
前回は、Cubical Agda が採用しているド・モルガン立方体型理論を中心に述べました。
しかし、立方体型理論には別の系統もあります。
タロウくん：
・・・体系が１つではない。
専任講師：
もう１つは、区間が pretype（前型）と呼ばれることです。
「型になりきれていないもの」という意味です。
前回は、この語に触れていませんでした。
順に見ていきましょう。
デカルト立方体型理論での例
Kan でないことの直観を、別の論文が具体例で示しています。
なお、これは デカルト立方体型理論（cartesian cubical type theory）という設定での議論です。
Cubical Agda が採用しているド・モルガン立方体型理論とは、区間に備わる演算が異なります。
（原文引用）
We suggested above that every type is Kan. In fact, the interval is the only exception to this rule, since we have been implicitly treating it as a "type", but it actually does not support any Kan operations. Consider, for example, the identity path on the interval, which goes from 0 to 1, $\lambda i.i$. If the interval were Kan, then the identity path would have an inverse. But what could that be in our cartesian setting? Given that the interval lacks some properties required by typehood in a cubical type theory, it is often referred to as a pretype.
（筆者による日本語訳）
我々は先に、すべての型が Kan であると述べた。実のところ、区間はこの規則の唯一の例外である。我々は区間を暗黙に「型」として扱ってきたが、実際には Kan 操作を一切サポートしない。たとえば、0 から 1 へ向かう区間上の恒等な道 $\lambda i.i$ を考えてみよ。もし区間が Kan であれば、この恒等な道は逆を持つはずである。しかし、我々のデカルト的な設定において、それは何でありうるだろうか。区間は、立方体型理論における型であることに要求される性質のいくつかを欠いているため、しばしば pretype（前型）と呼ばれる。
出典：Bruno Bentzen, "Naive cubical type theory", arXiv:1911.05844
タロウくん：
「もし区間が Kan であれば、この恒等な道は逆を持つはずである」・・・。
専任講師：
道には向きがあり、逆向きの道を作れました。
区間の上にも、0 から 1 へ向かう道があります。
もし区間が Kan なら、その逆の道、つまり 1 から 0 へ戻る道も作れるはずです。
タロウくん：
・・・しかし、それが何なのかを言えない。
専任講師：
デカルト立方体型理論には、区間の向きを反転させる演算がありません。
そのため、逆の道を作る手立てがないのです。
タロウくん：
Cubical Agda では、どうなりますか。
専任講師：
Cubical Agda の区間には、~ という反転演算があります。
ただし、演算があることと、区間が Kan であることは別です。
区間が Kan でない点は、両方の体系で共通します。
pretype（前型）とは何か
専任講師：
引用文の末尾に、pretype という語が出てきました。
「型になりきれていないもの」という意味です。
区間は型のように見えます。
しかし、型に要求される条件を満たしていません。
タロウくん：
Kan 条件を満たさない、ということですね？
専任講師：
そのとおりです。そのため、別の呼び名が与えられています。
| 呼び名 | 意味 |
|---|---|
| 型（type） | Kan 条件を満たす |
| 前型（pretype） | Kan 条件を満たさない |
タロウくん：
Arend では、区間は \Type に属していました。
専任講師：
Arend は、この区別を体系のなかに持ち込まなかったのです。
区間を普通の型として扱い、そのぶん理論を単純に保ちました。
Cubical Agda は、この区別を持ち込みました。
IUniv という別のソートが、それにあたります。
タロウくん：
・・・pretype という語は、その区別を持つ体系で使われる。
専任講師：
そういう位置づけの語です。
📌 中上級者向け：区間の「型の内／外」は、設計を示す略図です
本文の「区間を型の内に置く／外に置く」は、両者の設計上の差をつかむための略図です。
Cubical Agda の区間 I は、通常のデータ型と同じ意味で自由に扱える型ではありません。
型の形成や Kan 構造との関係で、特別な位置づけを持ちます。
このため文献では pretype（前型） と呼ばれることもあります。
一方、Arend は区間を通常の型として扱える設計を採っています。
ただしその選択は、一価性を完全に計算可能にするための追加構造とは別のトレードオフを伴います。本文で引用した nLab の記述が、その点を述べています。
関連する用語を、ここで整理しておきます。
| 用語 | 意味 |
|---|---|
| 区間（interval） | 道を記述するための、両端を持つ対象 |
| Kan 構造 | 欠けた部分を埋められるという条件 |
| ファイブラント（fibrant） | Kan 条件を満たしていること |
| 前型（pretype） | 型に要求される条件の一部を欠いているもの |
| 二層理論（two-level type theory） | 型が置かれる場所が２つに分かれた体系 |
本記事では、技術的な意味論の全体ではなく、「区間をどこに置くか」が、記述できるプログラム、型検査、計算性、正準性に関わる設計判断になることを伝えるために、この対比を用いています。
得たものと、失ったもの
| Arend | Cubical Agda | |
|---|---|---|
| 区間の扱い | 普通の型 | 型ではない（別の層） |
| 理論の複雑さ | 単純 | 二層理論 |
| 一価性 | 組み込みの公理（計算規則付き） | 導出可能 |
| 正準性 | 持たない | 持つ |
Cubical Agda は、HoTT の主要な構成を計算的に扱える力を得ました。
その代償として、理論が複雑になってしまいました。
Arend は、理論の単純さを保ちました。その代わり、正準性（閉じた項が必ず具体的な値へ計算される、という性質）を手放す結果となりました。
第８部 ── 対話篇
ここまでの流れを、対話の形でもう一度たどります。
１ ── 等しさの根拠が「値である」とは
タロウくん：
先生、前回「等しさの根拠を値として扱う」という話がありました。
あれが、よく分かりませんでした。
専任講師：
Haskell で 3 == 3 と書くと、何が返りますか。
タロウくん：
True です。真偽値ですね。
専任講師：
そこで話が終わります。
なぜ等しいのかという情報は、どこにも残りません。
タロウくん：
残す必要があるのですか。
専任講師：
依存型を持つ言語では、3 = 3 と書くと、これは 型 になります。
タロウくん：
真偽値ではなく、型。
専任講師：
そして、その型に属する値が、「３と３が等しいことの根拠」です。
タロウくん：
・・・根拠が、値として存在する。
専任講師：
Arend では、最も基本的な根拠に idp という名前が付いています。
２ ── 移送とは何か
タロウくん：
根拠が値として存在すると、何ができるのですか？
専任講師：
まず、移送ができます。
タロウくん：
移送。
専任講師：
２つの型が等しいと示せたとき、その根拠に沿って、一方の値を他方へ運ぶ操作です。
タロウくん：
運ぶ、というのは。
専任講師：
例を挙げましょう。
自然数を、単進法で表した型と、二進法で表した型を考えてください。
タロウくん：
単進法というのは、1 を並べて数を表すあれですか。
専任講師：
そうです。
証明は書きやすいが、計算は遅い。 二進法は逆です。
タロウくん：
・・・両方の利点を使いたいですね。
専任講師：
両者が等しいと示せば、証明は単進法で書き、実行は二進法で行えます。
３ ── なぜ、根拠が複数あることに意味があるのか
タロウくん：
先生、素朴な疑問があります。
専任講師：
どうぞ。
タロウくん：
Bool と Bool は同じ型ですよね。
どの根拠を使っても、移送先は同じ Bool ではないのですか？
専任講師：
移送先の型は、確かに同じです。
タロウくん：
では、何が変わるのですか。
専任講師：
運ばれた値です。
タロウくん：
・・・値。
専任講師：
true を運ぶとします。何も変えずに対応させる根拠を使えば、true のまま届きます。
タロウくん：
論理反転する根拠を使うと。
専任講師：
false になります。
タロウくん：
本当ですか。
専任講師：
実際に確かめました。
\func c1 : movedId = true => idp
\func c2 : movedNeg = false => idp
型検査は通ります。idp は、両辺が計算して同じ形になるときにのみ使える証拠です。
タロウくん：
・・・処理系が、実際に計算したということですね。
専任講師：
根拠とは、「２つの型が等しい」という事実だけを表すものではありません。
「どう対応させて等しいと見なすか」という情報を含んでいるのです。
３の補足 ── 値と型と、宇宙
タロウくん：
先生、この先の話に進む前に、確かめておきたいことがあります。
専任講師：
どうぞ。
タロウくん：
「値」と「型」の関係が、まだ整理できていません。
専任講師：
Haskell で考えてみましょう。
x :: Int
x = 3
3 が値で、Int が型です。
タロウくん：
そこは分かります。
専任講師：
では、Int そのものには型があるでしょうか。
タロウくん：
・・・考えたことがありませんでした。
専任講師：
Arend では、あります。
-- 3 は Nat の値
\func a : Nat => 3
-- Nat は \Set0 の値
\func b : \Set0 => Nat
-- \Set0 は \1-Type1 の値
\func c : \1-Type1 => \Set0
-- \1-Type1 は \2-Type2 の値
\func d : \2-Type2 => \1-Type1
型検査は、すべて通ります。
＜Arend の型検査結果＞
$ java -jar Arend.jar H1.ard
--- Typechecking \default ---
[ ] src.H1
--- Done (93ms) ---
タロウくん：
・・・型が、また別の型の値になっている。
専任講師：
そうです。この積み上げが、どこまでも続きます。
$$3 : \mathrm{Nat}, \qquad \mathrm{Nat} : \mathsf{Set0}, \qquad \mathsf{Set0} : \mathsf{1\text{-}Type1}, \qquad \ldots$$
タロウくん：
なぜ、こんな積み上げが必要なのですか。
専任講師：
型そのものを、値として扱いたい場面があるからです。
「型を受け取って型を返す関数」を書きたいとき。
受け取る側は、型を値として扱っています。
タロウくん：
・・・値である以上、その型が要る。
専任講師：
そのとおりです。そして、型を集めたものを宇宙と呼びます。
\Set0 も \1-Type1 も、宇宙です。
３の補足の続き ── 宇宙に付いている、２つの数
タロウくん：
\1-Type1 という書き方が、まだ読めません。
専任講師：
Arend では、宇宙を２つの数で指定します。
\1-Type1 を分解してみましょう。
| 位置 | 数 | 何を表すか |
|---|---|---|
\1-Type の 1
|
1 | 等しさの構造が、どこまで複雑になりうるか |
Type1 の 1
|
1 | 積み上げの何段目か |
タロウくん：
２つの数が、別々のことを表している。
専任講師：
そうです。まず、後ろの数から説明します。
後ろの数は、大きさを表します。
Nat や Bool を集めたものが Type0。
その Type0 自身を集めたものが Type1 です。
タロウくん：
段の番号ですね。
専任講師：
Agda や Lean にも、この数はあります。
Type 0、Type 1、Type 2。
１つの数で階層を表しています。
タロウくん：
では、前の数は。
専任講師：
Arend に固有のものです。等しさの構造の複雑さを表します。
タロウくん：
複雑さ、といいますと。
専任講師：
先ほど見たことを思い出してください。
Nat では、3 = 3 の根拠が高々１本でした。
根拠どうしの等しさを問う段階では、もう何も起きません。
一方、宇宙の中では Bool = Bool の根拠が２本ありました。
そして、その２本のあいだの等しさも問えました。
タロウくん：
・・・段階の深さが違う。
専任講師：
その深さを表すのが、前の数です。
| 前の数 | どういう型か | 例 |
|---|---|---|
| 0 | 等しさの根拠が高々１本 |
Nat、Bool、文字列 |
| 1 | 根拠が複数ありうる。根拠どうしの等しさは高々１本 | 集合を集めた宇宙 |
| 2 以上 | さらに深い構造がある | 宇宙を集めた宇宙 |
タロウくん：
\Set0 は、どう読むのですか。
専任講師：
\Set0 は、\0-Type0 の略記です。
\func x : \Set0 => Nat
\func y : \0-Type0 => Nat
どちらも型検査を通ります。同じものです。
Set という語が、**「等しさの根拠は高々１本」という情報を担っています。
** 前の数を 0 に固定した書き方です。
タロウくん：
・・・「集合」と呼ぶのは、そういう意味でしたか。
専任講師：
日常の数学でいう集合とは、少し意味が違います。
「等しさの根拠が高々１本しかない型」を、この文脈では集合と呼びます。
タロウくん：
\Prop というのも出てきましたね。
専任講師：
要素が高々１つしかない型を集めた宇宙です。
\func z : \Prop => 0 = {Nat} 0
型検査は通ります。
0 = 0 という型の要素は、「０と０が等しいことの根拠」です。 それが高々１つしかない、と述べています。
タロウくん：
根拠が高々１つ・・・先ほどの「根拠が高々１本」と同じことですか。
専任講師：
同じことを、別の角度から言っています。
Nat が \Set0 に属する、というのは型についての主張です。
x = y が \Prop に属する、というのは、 その型の中の、等しさの型についての主張です。
タロウくん：
・・・一段、下がったところの話・・・。
専任講師：
そのとおりです。
３の続き ── 型によって、根拠の本数が違います
タロウくん：
先生、Bool と Bool のあいだには根拠が２本ありました。
どんな型でも、根拠は複数あるのですか？
専任講師：
いいえ。多くの型では、根拠は高々１本です。
タロウくん：
たとえば。
専任講師：
整数で確かめてみましょう。
-- 3 = 3 の根拠は１通りしかない
\func nat-unique (p q : 3 = {Nat} 3) : p = q => idp
これは、型検査を通りません。
＜Arend の型検査結果＞
$ java -jar Arend.jar D1.ard
[ERROR] src.D1:9:43: Expressions are not equal
Left: p
Right: q
In: idp
タロウくん：
・・・通らないのですか。根拠は１本だと思っていましたが。
専任講師：
根拠が１本であることは正しいのです。
ただし idp だけでは証明できません。
idp は、両辺が計算して同じ形になるときに使えます。
p と q は変数なので、計算しても同じ形にはなりません。
タロウくん：
では、どう示すのですか。
専任講師：
型の側で宣言します。
-- Nat は集合。等しさの根拠は高々１本である
\func natIsSet : \Set0 => Nat
-- したがって、等しさの型は \Prop に属する
\func natEqIsProp (x y : Nat) : \Prop => x = y
型検査は通ります。
＜Arend の型検査結果＞
$ java -jar Arend.jar E1.ard
--- Typechecking \default ---
[ ] src.E1
--- Done (107ms) ---
タロウくん：
\Set0 と \Prop が出てきましたね。
専任講師：
\Set0 は、等しさの根拠が高々１本である型を集めた宇宙です。
そして \Prop は、要素が高々１つしかない型を集めた宇宙です。
Nat が \Set0 に属するので、x = y は \Prop に属します。
要素、つまり根拠が高々１つということです。
タロウくん：
文字列でも同じですか。
専任講師：
同じです。文字列を、自然数のリストとして表してみましょう。
\data List (A : \Type) | nil | cons A (List A)
\func Str => List Nat
\func s1 : Str => cons 104 (cons 105 nil)
\func s2 : Str => cons 104 (cons 105 nil)
-- ２つの文字列が等しいことの根拠
\func p1 : s1 = s2 => idp
-- Str も集合
\func strIsSet : \Set0 => Str
\func strEqIsProp (x y : Str) : \Prop => x = y
型検査は通ります。
タロウくん：
・・・整数も文字列も、根拠は１本。
専任講師：
では、Bool と Bool の場合はどうだったでしょうか。
タロウくん：
根拠が２本ありました。
専任講師：
そこが違うのです。
true と false は Bool の値です。
根拠は１本しかありません。
一方、Bool = Bool は型どうしの等しさ です。
こちらに根拠が２本あります。
タロウくん：
・・・値と型で、話が違う。
専任講師：
そのとおりです。実際に確かめてみましょう。
-- Nat は \Set0 に属する
\func natIsSet : \Set0 => Nat
-- では、宇宙 \Set0 自身は？
\func u : \Set0 => \Set0
最後の一行で、型検査が通りません。
＜Arend の型検査結果＞
$ java -jar Arend.jar E2.ard
[ERROR] src.E2:1:20: Type mismatch
Expected type: \Set0
Actual type: \1-Type1
In: \Set0
タロウくん：
\1-Type1 と表示されていますね。
専任講師：
エラーメッセージを、一行ずつ読み解きましょう。
Expected type: \Set0
**＜Arend のコード＞**
処理系は \Set0 を期待しました。
私が \func u : \Set0 => と書いたからです。
Actual type: \1-Type1
しかし実際には、\1-Type1 でした。
タロウくん：
２つの数が、どちらも 0 から 1 に変わっていますね。
専任講師：
その２つが、それぞれ別のことを述べています。
まず、後ろの数です。 Type0 が Type1 になりました。
\Set0 は Nat や Bool を集めたものです。
集めたものは、集められたものより一段上に置かれます。 だから 0 から 1 へ上がりました。
タロウくん：
段が上がった。それは分かります。
専任講師：
問題は、前の数です。
\0-Type が \1-Type になりました。
等しさの構造が、一段深くなったということです。
タロウくん：
・・・どういうことでしょうか。
専任講師：
Nat の中では、3 = 3 の根拠が高々１本でした。
だから Nat は \Set0、すなわち前の数が 0 の宇宙に属します。
タロウくん：
はい。
専任講師：
では、\Set0 という宇宙の中ではどうでしょうか。
宇宙の要素は、Nat や Bool といった型です。
そして Bool = Bool の根拠は、２本ありました。
タロウくん：
・・・宇宙の中では、根拠が複数ある。
専任講師：
そのため、宇宙は集合ではありません。
前の数が 0 ではなく 1 になります。
それが \1-Type1 です。
タロウくん：
\Set0 に属さない理由が、そこにある。
専任講師：
そういうことです。整理しましょう。
| 属する宇宙 | その中での等しさの根拠 | |
|---|---|---|
3（値） |
Nat |
── |
Nat（型） |
\Set0 |
3 = 3 の根拠は高々１本 |
\Set0（宇宙） |
\1-Type1 |
Bool = Bool の根拠は２本ありうる |
タロウくん：
・・・値と型で、話が違うというのは、このことでしたか。
専任講師：
そのとおりです。
先ほど、true と false を入れ替える対応と、そのまま重ねる対応の２つを見ました。
あれは、Bool という型の中の話ではありません。
Bool を要素として含む宇宙の中で、Bool = Bool の根拠が２本ある、という話でした。
タロウくん：
3 = 3 の根拠は１本なのに、Bool = Bool の根拠は２本。
専任講師：
片方は値どうしの等しさ、もう片方は型どうしの等しさです。
住んでいる階層が違うのです。
３のさらに続き ── 根拠どうしの等しさ
タロウくん：
先生、素朴な疑問があります。
専任講師：
どうぞ。
タロウくん：
根拠が２本あるとき、その２本が等しいかどうかを問えますか？
専任講師：
問えます。実際に書いてみましょう。
\data Bool | true | false
\func boolNeg (b : Bool) : Bool \elim b
| true => false
| false => true
\func boolNegNeg (b : Bool) : boolNeg (boolNeg b) = b \elim b
| true => idp
| false => idp
\func boolId (b : Bool) : Bool => b
\func boolIdId (b : Bool) : boolId (boolId b) = b => idp
-- Bool = Bool の道が２本
\func idPath : Bool = Bool => path (iso boolId boolId boolIdId boolIdId)
\func negPath : Bool = Bool => path (iso boolNeg boolNeg boolNegNeg boolNegNeg)
-- この２本が等しいと主張してみる
\func distinct : idPath = negPath => idp
最後の一行が、型検査を通りません。
＜Arend の型検査結果＞
$ java -jar Arend.jar F1.ard
[ERROR] src.F1:16:38: Expressions are not equal
Left: idPath
Right: negPath
In: idp
タロウくん：
・・・２本の道が、等しくないと判定されましたね。
専任講師：
そこは、慎重に読む必要があります。
タロウくん：
えっ。「等しくない」と出ているではありませんか。
専任講師：
では、確かめてみましょう。
idPath は、iso に恒等関数を渡して作った道でした。
「そのまま重ねる」対応です。
一方、idp という道も記述できます。
これは、反射性の証拠です。
「Bool は Bool に等しい」という、当たり前の主張にあたります。
タロウくん：
どちらも「そのまま重ねる」ということですね。
専任講師：
では、この２つが等しいと主張してみてください。
\func third : Bool = Bool => idp
\func t3 : third = idPath => idp
タロウくん：
・・・通りますよね？ どちらも同じ対応なのですから。
専任講師：
実行してみましょう。
＜Arend の型検査結果＞
$ java -jar Arend.jar V1.ard
[ERROR] src.V1:15:30: Expressions are not equal
Left: third
Right: idPath
In: idp
タロウくん：
・・・通りません。
同じ対応のはずなのに、「等しくない」と出ました。
専任講師：
ここが要点です。
タロウくん：
・・・あっ。
専任講師：
気づかれましたか。
タロウくん：
「等しくない」と出たからといって、本当に等しくないとは限らない、ということですか。
専任講師：
そのとおりです。
idp は、両辺が計算して同じ形になるときにのみ使える証拠でした。
このエラーが述べているのは、「計算しても同じ形にならなかった」ということだけです。
タロウくん：
・・・「等しくない」ことの証明ではない。
専任講師：
証明ではありません。 等しくないことを示すには、別の議論が要ります。
タロウくん：
私は、エラーメッセージを読み違えていました。
専任講師：
よくある誤りです。
処理系が「Expressions are not equal」と出すとき、それは 「いま提出された証拠 idp では示せない」 という意味です。
タロウくん：
では、idPath と negPath は、本当は等しいのですか？
専任講師：
等しくありません。ただし、その根拠は別のところにあります。
タロウくん：
どこにあるのですか。
専任講師：
第２部でお見せした移送の結果です。
\func movedId : Bool => coe (\lam i => idPath @ i) true right
\func movedNeg : Bool => coe (\lam i => negPath @ i) true right
\func c1 : movedId = true => idp
\func c2 : movedNeg = false => idp
**＜Arend のコード＞**
両方とも、型検査を通ります。
タロウくん：
idPath で運ぶと true、negPath で運ぶと false。
専任講師：
もし２本が等しければ、運んだ結果も等しくなるはずです。
タロウくん：
・・・true と false は違う。だから、２本も違う。
専任講師：
それが、２本が異なることの根拠です。
エラーメッセージではなく、運んだ結果の違いが証拠になります。
タロウくん：
・・・エラーが出たことを、根拠にしてはいけなかった。
専任講師：
そのとおりです。
📌 中上級者向け：idp が証明できる「等しさ」とは何か？
ここからは、本文で説明した「等しい」という言葉を、型理論の用語を使ってもう少し正確に整理します。
本記事では、「等しい」という言葉を、読者にとって分かりやすいように使ってきました。
しかし型理論では、「等しい」といっても、重要な区別があります。
① 計算すると同じになる ── definitional equality
まず、計算すると同じものになる、という意味での等しさがあります。
ある式を計算規則に従って変形していった結果、左右が同じ形になったとします。
このような等しさを、型理論では definitional equality（定義的等値）と呼びます。
judgmental equality（判断的等値）という名前で呼ばれることもあります。
なお、この２つの語は一般的な型理論の文脈ではほぼ同じ意味で使われますが、文献や処理系によってニュアンスが異なります。
別々の２種類の等しさとして並列に扱わないでください。
ここで重要なのは、これが通常の意味での「等しいことを証明する命題」ではないという点です。
型検査器が、「この２つの式は、計算規則に従えば同じものとして扱ってよい」 と判断する種類の等しさです。
② 型検査器は、どのように「同じ」と判断するのか
この「同じものとして扱ってよい」という判断の背後には、conversion（変換可能性）、あるいは convertibility という考え方があります。
$$t \equiv u$$
と判断できるなら、型検査器は $t$ と $u$ を、型を調べる際に同じものとして扱えます。
この $\equiv$ は、「$t$ と $u$ は、計算規則によって互いに同じものとして扱える」 という意味です。
ここでいう「計算規則」には、型理論によって次のものが関係します。
- β-reduction
- δ-reduction
- ι-reduction
- η-rule
ただし、どの規則を definitional equality に含めるかは、採用している型理論や定理証明系によって異なります。
③ 正規化 ── 計算して、最終的な形にする
この話と深く関係するのが normalization（正規化）です。
正規化とは、式を計算規則に従って変形し、これ以上計算できない形まで持っていくことです。
単純化したイメージでは、
$$(\lambda x., x), a$$
を計算すると、
$$a$$
になります。このような計算を reduction（簡約）と呼びます。
そして、これ以上その種の簡約ができない形を normal form（正規形） と呼びます。
型理論では、**「２つの式を計算していったとき、同じ正規形に到達する」**という考え方が、definitional equality を理解するうえで重要になります。
※ ここでの正規形による説明は、直観を与えるためのものです。実際の型検査器は、必ずしも式全体を正規形まで計算してから比較しているわけではありません。
型検査では、必要に応じて reduction を行いながら、２つの式が convertible かどうかを判断します。
④ では、idp は何なのか
ここで、本文に登場した idp に戻ります。
idp は、任意の２つの式が等しいことを証明してくれる魔法の証明ではありません。
idp は、HoTT およびマーティン＝レーフ型理論における identity type の基本的な導入規則に対応するものです。
直感的には、
$$\mathrm{idp} : a = a$$
という「自分自身と自分自身が等しい」という等しさを表す基本的な道です。
そして、型検査器が左右の式を definitional equality によって同じものとして扱えるなら、idp を使ってその等しさを示すことができます。
つまり $a = a$ だけでなく、$t = u$ についても、$t$ と $u$ が定義上同じものとして扱えるなら、idp が適用できる場合があります。
⑤ もう１つの「等しさ」── propositional equality
これに対して、もう１つ重要なのが propositional equality（命題的等値）です。
こちらは、
$$a = b$$
という型そのものを考えます。
そして、**「この型には値が存在する」ことによって、「$a$ と $b$ は等しい」**ことを証明します。
HoTT では、この $a = b$ 自体が identity type（同一視型）です。
つまり $a = b$ は、単なる「等しい」というコンパイラ内部の判断ではなく、等しさを表す型なのです。
そして、その型の値が、**$a$ から $b$ への path（道）**として解釈されます。
⑥ definitional equality と propositional equality は別物
ここが、このコラムで最も重要な点です。
| 意味するところ | |
|---|---|
| definitional equality | 計算すれば同じものとして扱える |
| propositional equality | $a = b$ という型の値として、等しさの証明を持っている |
definitional equality が成立することと、propositional equality の証明が存在することは、同じ意味ではありません。
２つの項 $a$ と $b$ が計算によって同じ形になるなら、型検査器はそれらを definitional equality によって同一視できます。
その場合、$a = b$ の証明には idp を利用できます。
しかし逆方向は、一般には成立しません。
$a = b$ という命題を証明できるからといって、必ずしも $a$ と $b$ が計算によって同じ形になるわけではありません。
これが、本文で説明した「『等しくない』と表示されたからといって、本当に等しくないとは限らない」という話の背景です。
型検査器が「等しくない」と判断したというのは、definitional equality によって同じものとして扱えなかったという意味であって、propositional equality の証明が絶対に存在しないという意味ではありません。
⑦ なぜ、この区別が Arend と Cubical Agda の比較につながるのか
ここで、本記事の本題に戻ります。
定理証明系では、「数学的に等しい」ことと、「型検査器が計算によって同じものとして認識できる」ことは、同じではありません。
特に HoTT では、$a = b$ という型の中に、単なる真偽ではなく、$a$ から $b$ へのさまざまな path が存在できます。
そのため、「この２つは数学的には等しい」ことを、「型検査器が計算した結果、同じ式になった」という definitional equality だけで表現することはできません。
このギャップが、HoTT の証明をどこまで計算可能なものとして扱えるかという問題につながります。
Arend と Cubical Agda の違いを理解するには、「証明として等しい」と「計算によって同じ」の違いを理解しておくことが重要なのです。
３のさらに続き ── 「２本」とは、何を数えているのか
タロウくん：
先生、いまの話で気になったことがあります。
専任講師：
どうぞ。
タロウくん：
idp と idPath は、同じ対応なのに別々の式として記述できました。
では、Bool = Bool の道は、いくらでも記述できるのではありませんか。「２本」というのは、どういう意味なのでしょうか。
専任講師：
構文の上では、いくらでも記述できます。 idp と記述しても、iso を使って記述しても、道は道です。
タロウくん：
では、なぜ２本と言えるのですか。
専任講師：
道どうしが等しい場合は、同じ１本として数えているからです。
idp と idPath は、別々に書かれた式です。
しかし、どちらも「そのまま重ねる」対応に対応します。
タロウくん：
・・・同じ１本として数える。
専任講師：
そのうえで数えると、２本になります。
そのまま重ねる対応と、入れ替える対応。
Bool から Bool への対応は、この２つしかありません。
タロウくん：
なぜ、２つしかないと言えるのですか。
専任講師：
Bool の値が true と false の２つだけだからです。
過不足なく一対一に対応させる方法は、そのまま送るか、入れ替えるかの２通りしかありません。
タロウくん：
・・・確かにそうですね。
専任講師：
そして一価性公理が、この２つを Bool = Bool の２本の道に対応させます。
タロウくん：
道の本数を数えるとき、書き方の違いは数えない。
専任講師：
そういう数え方をしています。 本記事で「根拠が２本」と述べるときは、常にこの意味です。
📌 中上級者向け：ここでいう「２本」を数学的に厳密にいうと？
ここからは、本文の「２本」という言い方を、数学の言葉で整理します。
同値類とは何か
まず、同値類という概念を説明します。
同じものとして扱えるものを、ひとつのグループにまとめたものを、同値類（equivalence class）といいます。
たとえば整数を「３で割った余り」で分類すると、余り $0$、$1$、$2$ の３つのグループに分かれます。この各グループが、同値類です。
「２本」が指しているもの
本記事でいう「２本」は、idp と idPath のような別々の書き方が２つある、という意味ではありません。
構文の上では、Bool = Bool の項はいくらでも記述できます。
ここで、道と道のあいだの等しさを考えます。
$$\mathrm{idp} = \mathrm{idPath}$$
この型の要素が存在すれば、２つの道を同じものとみなせます。
そのようにして、道どうしの等しさまで考慮して分類したときに残るグループの個数が、「２本」の意味です。
Bool = Bool の構造
一価性公理により、次の同値が成り立ちます。
$$(\mathrm{Bool} =_{\mathcal{U}} \mathrm{Bool}) ;\simeq; (\mathrm{Bool} \simeq \mathrm{Bool})$$
右辺は、Bool から Bool への同値の型です。
Bool は要素が２つの集合ですから、自己同値は恒等写像と否定写像の２つに分類されます。
$$\mathrm{id}, \qquad \mathrm{not}$$
したがって、左辺の $\mathrm{Bool} =_{\mathcal{U}} \mathrm{Bool}$ も、道どうしの等しさで分類すると２つのグループに分かれます。
構造をまとめると
Bool = Bool
↓ （一価性公理）
Bool から Bool への equivalence
↓
id と not
↓ （道どうしの等しさで分類）
２つの異なる種類
本記事でいう「２本」は、この最下段の２つを指しています。
３のさらに続き ── 道どうしの等しさ
専任講師：
さて、もう１つ注目していただきたいことがあります。
先ほどの idPath = negPath という式です。証明はできませんでしたが、式そのものは書けていました。
タロウくん：
書けている、といいますと。
専任講師：
道と道のあいだの等しさが、型として存在するのです。
$$\mathrm{idPath} = \mathrm{negPath}$$
これは、道どうしを結ぶ道の型です。
タロウくん：
一段、上がったということですか。
専任講師：
そのとおりです。そして、さらに上がれます。
\func meta : idPath = idPath => idp
\func metameta : meta = meta => idp
型検査は通ります。
タロウくん：
meta = meta ・・・道どうしを結ぶ道の、そのまた道。
専任講師：
この階層は、どこまでも続きます。
$$a = b, \quad p = q, \quad \alpha = \beta, \quad \ldots$$
タロウくん：
・・・無限に続くのですか。
専任講師：
理論としては、そうです。
ただし、どの段階から先が自明になるかは、型によって違います。その段階を表すのが、先ほどの \Set0 や \1-Type1 の数です。
タロウくん：
Nat なら \Set0 だから、１段目で止まる。
専任講師：
そうです。Nat では、3 = 3 の根拠が高々１本しかありません。 したがって、根拠どうしの等しさを問う段階では、もう何も新しいことが起きません。
宇宙は \1-Type1 なので、１段深いところまで構造があります。
３のさらに続き ── 複数の根拠を区別できると、何ができるのか
タロウくん：
先生、複数の根拠を区別できると、その後どんなことができるのですか。
専任講師：
第２部でお見せした移送が、その答えです。
どの根拠を使って運ぶかによって、運んだ先の値が変わりました。
タロウくん：
idPath なら true、negPath なら false でしたね。
専任講師：
根拠を区別できなければ、この使い分けができません。
「Bool と Bool は等しい」としか言えなければ、どちらの対応で運ぶのかを指定できないからです。
タロウくん：
・・・区別できるから、選べる。
専任講師：
そして、選んだ結果が計算で確かめられます。
先ほど確かめたとおり、idPath で運べば true、negPath で運べば false になりました。処理系が、実際に計算した結果です。
タロウくん：
・・・区別できることが、そのまま計算の結果に表れる。
専任講師：
そのとおりです。
４ ── 商型とは何か
タロウくん：
２つ目は、商型でしたね。
専任講師：
ある型の値のうち、いくつかを同一視して作った型です。
タロウくん：
同一視。
専任講師：
有理数を考えてください。$1/2$ と $2/4$ は、書き方こそ違いますが同じ数です。
タロウくん：
・・・組として書けば、(1,2) と (2,4) ですね。別の値です。
専任講師：
そこが問題です。 公式論文は、これを「等式の内包性」と呼んでいます。
タロウくん：
書き方が違えば別のもの、ということですか。
専任講師：
そうです。同じものとみなすなら、型の側に書き込む必要があります。
タロウくん：
書き込める、と。
専任講師：
Arend では、型の定義に並べられます。
\data Q
| q Nat Nat
| same (a b k : Nat) : q a b = q (a Nat.* k) (b Nat.* k)
タロウくん：
２行目が、値ではないですね。
専任講師：
「これとこれは等しい」という主張です。
タロウくん：
Haskell の data には、値の作り方しか並びませんでした。
専任講師：
この仕組みを、高次帰納的型といいます。 第４回で詳しく扱います。
５ ── 公理として足すと、どうなるのか
タロウくん：
Rocq は、これを公理として足しているのでしたね。
専任講師：
そうです。そして、そこで計算が止まります。
タロウくん：
止まる、というのは。
専任講師：
移送そのものは、公理でもできます。「Bool と Bool は等しい」と宣言し、true を運ぶ式を記述できる。
タロウくん：
記述できるなら、よいのでは。
専任講師：
しかし、その式が何になるのかを、処理系が求められません。
タロウくん：
・・・false にたどり着かない。
専任講師：
式が、そのまま残ります。 証明としては成立しますが、プログラムとしては動きません。
６ ── なぜ、区間を型の外に置くと計算しきれるのか
タロウくん：
先生、冒頭で伺った話を、もう一度確かめさせてください。
区間を型の外に置くと、計算しきれるようになる。その理屈が、まだ腑に落ちていません。
専任講師：
では、区間が普通の型だと何が起きるかを考えてみましょう。
タロウくん：
はい。
専任講師：
Nat や Bool と同じ型なのですから、他の型と同じ操作がすべて許されます。
区間を要素に持つリストを作る。区間から区間への関数を作る。
そうしたことが、いくらでも書けてしまいます。
タロウくん：
・・・記述できて、困るのですか？
専任講師：
そのすべてについて、計算規則を用意しなければなりません。
記述できる式の種類が増えれば増えるほど、取りこぼしなく規則を定めるのが難しくなります。
タロウくん：
なるほど。それで、型の外に置くと。
専任講師：
許される操作を、あらかじめ絞れます。
区間についてできることを限定してしまえば、その限られた範囲について規則を定めればよいのです。
タロウくん：
・・・自由を制限したから、規則を漏れなく用意できた。
専任講師：
そう理解して差し支えありません。
６の続き ── 区間 I 型とは、そもそも何なのか
タロウくん：
先生、そもそも区間 I という型が、まだよく分かりません。
専任講師：
では、他の型と並べてみましょう。
| 型 | 値の例 | プログラマが何に使うか |
|---|---|---|
Bool |
true、false
|
条件分岐 |
Nat |
0、1、2、… |
数を数える |
List Nat |
cons 104 (cons 105 nil) |
並びを表す |
I |
left、right |
等しさの根拠を書くとき |
タロウくん：
値が left と right の２つだけ・・・Bool と同じに見えます。
専任講師：
見た目は似ています。しかし、用途がまったく違います。
Bool は、データを表すために使います。 条件が成り立つか、成り立たないか。
I は、データを表すためには使いません。
タロウくん：
では、何のために。
専任講師：
「等しさの根拠」を書くために使います。
第２部で見た道の定義を思い出してください。
$$p : I \to \mathrm{Bool}, \qquad p(\mathsf{i0}) = \mathrm{true}, \qquad p(\mathsf{i1}) = \mathrm{false}$$
タロウくん：
・・・区間から Bool への写像でした。
専任講師：
I は、この写像の入力側です。
「左端では true、右端では false」と書くための座標にあたります。
タロウくん：
座標、ですか。
専任講師：
実際のコードで見てみましょう。
\func negPath : Bool = Bool => path (iso boolNeg boolNeg boolNegNeg boolNegNeg)
-- 道に沿って値を運ぶとき、区間変数 i が現れる
\func moved : Bool => coe (\lam i => negPath @ i) true right
**＜Arend のコード＞**
\lam i => negPath @ i の i が、区間の値です。
negPath @ i は、「道 negPath の、位置 i における値」を意味します。
i を左端から右端へ動かすと、道の上を移動していきます。
タロウくん：
・・・道の上の位置を指す変数。
専任講師：
そういう使い方をします。
プログラマが I を直接書くのは、**等しさの証明を組み立てるときだけです。
** 業務のデータ処理で I の値を扱うことは、まずありません。
６のさらに続き ── なぜ、区間には２つの操作がないのか
タロウくん：
先生、ひとつ確かめさせてください。
専任講師：
どうぞ。
タロウくん：
区間 I が２つの操作を持たないのは、I が、文字型・文字列型・整数型・論理型より抽象度の高い、一段メタレベルの型だからですか？
専任講師：
惜しいのですが、そうではありません。
タロウくん：
違うのですか。
専任講師：
「抽象度が高いから操作が定義できない」ということではないのです。
宇宙 \Set0 を思い出してください。**宇宙は、型を要素に持つ型です。
** Nat や Bool より、明らかに一段上のものです。
タロウくん：
・・・はい。
専任講師：
しかし宇宙には、２つの操作が定義されています。
型と型のあいだで値を運べますし、道の隙間も埋められます。
第２部でお見せした coe は、まさに宇宙の中の道に沿って値を運ぶ操作でした。
タロウくん：
では、抽象度の問題ではない。
専任講師：
そうです。理由は別のところにあります。
タロウくん：
どこにあるのですか。
専任講師：
区間の上には、欠けた部分を埋める構造そのものが定まらないのです。
立方体型理論の正規形を扱った論文が、こう述べています。
（原文引用）
Another reason is the interval is not Kan, i.e. we cannot define a composition structure on it, and it cannot be interpreted semantically as a space.
（筆者による日本語訳）
もう１つの理由は、区間が Kan でないことである。すなわち、区間の上に合成構造を定義することができず、区間を空間として意味論的に解釈することもできない。
出典："Normal forms in cubical type theory", arXiv:2603.24923
タロウくん：
先生、「Kan」という語が出てきました。
専任講師：
人名です。 代数トポロジーの数学者、Daniel M. Kan に由来します。
タロウくん：
どういう条件なのですか。
専任講師：
第７部で述べたとおり、もとは図形についての条件でした。
三角形の３辺のうち、２辺だけが描かれている状態を考えてください。残りの１辺を、必ず補える。 それが Kan 条件です。
タロウくん：
・・・それが、型理論とどうつながるのですか。
専任講師：
先ほどの２つの操作が、まさにそれです。
道が途中までしか引けていないとき、残りを補う。これが、欠けた部分を埋める操作にあたります。
タロウくん：
２つの操作を持つことが、Kan であるということですか。
専任講師：
そうです。そして、この２つから多くのことが導かれます。
第７部で引いたとおり、反射性、対称性、推移性、代入。 等しさについて当たり前に使っている性質が、すべてこの２つから出てきます。
タロウくん：
「$a = a$ である」「$a = b$ なら $b = a$ である」といったことですね。
専任講師：
そのとおりです。
タロウくん：
・・・逆に言えば、２つの操作がなければ、そうした性質も使えない。
専任講師：
だから、通常の型についてはこの２つが使えるように設計されているのです。
📌 中上級者向け：Kan 条件をもう少し厳密に見る
ここからは、本文で述べた Kan 条件を、もう少し正確に整理します。
もとは、単体集合についての条件でした
Kan 条件は、代数トポロジーにおける単体集合の理論から来ています。
単体集合 $X$ について、次が成り立つとき、$X$ を Kan 複体（Kan complex）と呼びます。
任意の射 $\Lambda^n_k \to X$ が、$\Delta^n \to X$ へ拡張できる。
$\Lambda^n_k$ は ホーン（horn）と呼ばれ、$n$ 次元単体の面のうち１つを欠いた図形です。$\Delta^n$ は、欠けていない $n$ 次元単体です。
つまり「欠けた面を、必ず補える」という条件です。
$n = 2$、$k = 1$ の場合を考えてください。三角形の３辺のうち２辺が与えられていて、残りの１辺を補う。 これが、本文で述べた例にあたります。
Kan 複体は、ファイブラント（fibrant）とも呼ばれます。
立方体型理論では、どう現れるのか
立方体型理論では、この性質が基本操作として実装されています。
（原文引用）
The primitive operations on paths are the so-called "Kan operations", and the only two such primitives in Cubical Agda are (i) the homogeneous composition (hcomp), which composes paths together to form a new one, and (ii) the transport operation (transp), which "transports" objects along path-equivalent types.
（筆者による日本語訳）
道に対する基本操作は、いわゆる「Kan 操作」と呼ばれる。Cubical Agda において、そうした基本操作は２つだけである。すなわち、(i) 道どうしを合成して新しい道を作る等質合成（
hcomp）と、(ii) 道でつながれた型のあいだで対象を運ぶ輸送操作（transp）である。
出典："Towards Computational UIP in Cubical Agda", arXiv:2511.21209
ここで注意すべき点があります
「Kan 条件 ＝ hcomp と transp を持つこと」と単純に等号で結ぶのは、正確ではありません。
引用文が述べているのは、Cubical Agda における primitive operations が hcomp と transp の２つであるということです。
Kan 条件そのものは、上に述べた単体集合の充填条件に由来する概念であり、それが立方体型理論において hcomp と transp という形で実現されている、という関係です。
本文では、読者に伝わりやすくするため「２つの操作」という言い方をしています。
厳密には、この対応関係を指しています。
等しさの性質は、ここから導かれます
（原文引用）
Now, the common properties of equalities can all be derived: reflexivity by constant functions from I, symmetry by negating the interval variable of a path, transitivity by the hcomp operation, and substitutivity by applying transp with predicates.
（筆者による日本語訳）
これにより、等しさの通常の性質はすべて導かれる。反射性は区間からの定数関数によって、対称性は道の区間変数を反転させることによって、推移性は
hcomp操作によって、代入はtranspを述語に適用することによって得られる。
出典：同上
なお、対称性が「区間変数を反転させること」で得られるという記述は、ド・モルガン立方体型理論を前提としています。 区間に反転演算 ~ が備わっているためです。
デカルト立方体型理論では、区間に反転演算がありません。 そのため、対称性の導き方が異なります。
区間が Kan でないこと
（原文引用）
Another reason is the interval is not Kan, i.e. we cannot define a composition structure on it, and it cannot be interpreted semantically as a space.
（筆者による日本語訳）
もう１つの理由は、区間が Kan でないことである。すなわち、区間の上に合成構造を定義することができず、区間を空間として意味論的に解釈することもできない。
出典："Normal forms in cubical type theory", arXiv:2603.24923
「合成構造を定義できない」という表現に注目してください。
先ほどの単体集合の言葉でいえば、区間の上ではホーンの充填が定まらない、ということです。
そして、そのために区間は pretype（前型）と呼ばれることがあります。
タロウくん：
「空間として解釈できない」というのは。
専任講師：
ここが要点です。
立方体型理論では、型を空間として捉えます。Nat も Bool も、宇宙も、すべて空間として読めます。
タロウくん：
区間は読めない、と。
専任講師：
区間は、空間そのものではなく、空間の中に道を描くための座標だからです。
座標を空間として扱おうとすると、話が合わなくなります。
タロウくん：
・・・役割が違う。
専任講師：
そのとおりです。抽象度の高低ではなく、役割の違いなのです。
そして、もう１つ理由があります。型検査です。
（原文引用）
One is that the interval should not participate in any type formers, so for example we cannot have functions $f: \mathbb{N} \to \mathbb{I}$ which easily make type-checking undecidable.
（筆者による日本語訳）
１つは、区間が型構成子に一切関与すべきでないということである。たとえば $f : \mathbb{N} \to \mathbb{I}$ のような関数を許すと、型検査の決定可能性を容易に失いうる。
出典：同上
タロウくん：
決定不能、というのは。
専任講師：
処理系が、有限の時間で答えを出せなくなるということです。
型検査が終わらないかもしれない。それでは、道具として使えません。
タロウくん：
・・・Arend では、その関数を記述できるのでしたね。
専任講師：
記述できます。先ほど確かめたとおりです。
\func g (n : Nat) : I => left
Cubical Agda では、記述できません。
タロウくん：
Arend は、そのぶん計算可能性について制約を抱えている。
専任講師：
理論の単純さと引き換えに、そうした側面を残しています。
６のさらに続き ── プログラマの負担について、振り返ります
タロウくん：
先生、Cubical Agda の理論が複雑になった結果、プログラマの負担が大きくなるとのことでした。
前回の記事で、３つの場面を見せていただきましたね。
専任講師：
振り返っておきましょう。
| 場面 | Arend | Cubical Agda |
|---|---|---|
| １. 区間を型構成子に渡す | 記述できる | 記述できない |
| ２. 道と道の関係を証明する | 本体は１行 | 面条件・底面・向きを指定 |
| ３. 等しさについて場合分けする | 本体は１行 |
J を組み立てる |
タロウくん：
場面１では、List I が Arend では記述できて、Cubical Agda では記述できませんでした。
専任講師：
区間が置かれている場所が違うからです。
タロウくん：
場面２では、正方形の各辺を自分で書き並べることになりました。
専任講師：
面条件です。 どの辺がどういう値で埋まっているかを、証明を書く側が指定します。
Arend では、道について場合分けすれば済みました。
\func assoc {A : \Type} {a b c d : A} (p : a = b) (q : b = c) (r : c = d)
: concat (concat p q) r = concat p (concat q r) \elim r
| idp => idp
**＜Arend のコード＞**
結合律が、\elim r | idp => idp の２行です。
タロウくん：
そして場面３では、J の引数を組み立てることになりました。
専任講師：
Arend では、J そのものも場合分けで記述できます。
\func J {A : \Type} {x : A} (P : \Pi (y : A) -> x = y -> \Type)
(d : P x idp) {y : A} (p : x = y) : P y p \elim y, p
| _, idp => d
Cubical Agda では、transport と区間の演算を使って組み立てます。
タロウくん：
・・・どの場面でも、Arend のほうが短く記述できる。
専任講師：
その代わり、Arend は正準性を持ちません。
計算が進むほど、負担も増える。 それが前回の主題でした。
なお、両言語のコードを並べた詳しい比較は、前回の記事をご覧ください。
７ ── 本記事を振り返って
タロウくん：
先生、今日はありがとうございました。
専任講師：
等しさの根拠を値として扱えると、３つのことができるようになりました。
証明を別の型へ運ぶ。同じ数だと型に書き込む。同じ値を返す関数を等しいと言う。
タロウくん：
・・・移送、商型、関数外延性。
専任講師：
しかし、この３つを公理として足すだけでは、計算が進みません。
タロウくん：
Arend は、計算規則を組み込んだ。
専任講師：
その代わり、正準性は手放しました。
正準性とは、閉じた項が必ず正準形へ評価されるという性質です。
タロウくん：
「閉じた項」というのは。
専任講師：
自由な変数を含まない式のことです。
2 + 3 は閉じています。n + 3 は、変数 n を含むので閉じていません。
そして 正準形とは、その型の値として最も基本的な形のことです。自然数でいえば、2 + 3 を計算して得られる 5 がそれにあたります。
タロウくん：
・・・計算すれば、必ず具体的な数になる。
専任講師：
Arend は、この性質を持ちません。
区間変数を含んだままの式では、計算が途中で止まる場合があるからです。
タロウくん：
・・・何を優先したかの違い。
専任講師：
設計とは、そういうものです。
次回の予告
【Arend Theorem Prover 連載（４回目）】の主題は、数学の代数構造を Arend でどう定義するか、です。
モノイド、群、環、体。数学の構造は階層をなしています。
下の構造の条件を、上の構造がすべて引き継ぐ形です。
この階層を、そのままArendのコードとして記述できるでしょうか？
ここで光があたるのが、Arend の レコード です。
レコードとは何か
レコード とは、複数の値をひとまとめにして名前を付ける仕組みです。
Haskell のレコード構文にあたります。
Arend では、レコードの定義のなかに「満たすべき法則」を一緒に書き込むことが可能です。
たとえば、「この演算は結合律を満たす」という条件 を、型の定義の中に書き込むことができる のです。
実際にコードを見てみましょう。
＜Arend のコード＞
\record Monoid (A : \Type)
| unit : A
| op : A -> A -> A
| assoc (x y z : A) : op (op x y) z = op x (op y z)
＜Arend の型検査結果＞
$ java -jar Arend.jar REC2.ard
--- Typechecking \default ---
[ ] src.REC2
--- Done (99ms) ---
１行ずつ読み解きます。
| 部分 | 意味 |
|---|---|
\record Monoid (A : \Type) |
Monoid というレコードを定義する。型 A を受け取る |
| unit : A |
単位元。A の値をひとつ持つ |
| op : A -> A -> A |
演算。A の値を２つ受け取って、A の値を返す |
| assoc (x y z : A) : ... |
結合律。この演算が満たすべき法則 |
上の３行までは、Haskell のレコード構文と同じ発想です。
値と関数を、ひとまとめにしています。
注目すべきは、４行目です。
assoc は値でも関数でもなく、「$(x \cdot y) \cdot z$ と $x \cdot (y \cdot z)$ が等しい」という主張です。
この4行目が記述されているので、Monoid を 作るときには結合律の証明を渡さなければなりません 。法則を満たさないものは、そもそも Monoid として作ることができない のです。
階層を記述するには、２つの仕組みが必要
Lean、Rocq／Coq、Agda は、言語の土台となる型理論のなかで、２つの仕組みを避けてきました。
ここでいう土台とは、型検査器が直接扱う規則の集まりのことです。
避けてきた仕組みのうち、ひとつ目は、群はモノイドの条件をすべて満たすのだから、群の値をそのままモノイドとして使ってよい。そういう扱いを、言語の側で認める仕組みを指します。
この扱いのことを、専門用語では 包摂的部分型付け と呼びます。
Lean、Rocq／Coq、Agda は、 包摂的部分型付け を避けてきたのです。
避けてきた、とはどういうことなのかは、このすぐあとで解説します。
避けてきた仕組みの２つ目は、顕在フィールド と呼ばれるものです。
これは何かというと、レコードの項目のうち、いくつかの値を定義の時点で確定させておく仕組み のことです。
レコードを定義した瞬間に確定した値は、レコード型の一部になります。
既定値のように、あとから上書きできるものではありません。
「避けてきた」とは、どういうことか
避けてきた、という言葉の意味ですが、上記の２つを、Lean、Rocq／Coq、Agda はその言語の中核となる理論には入れず、外側の仕組みで補ってきた、という意味です。
Lean、Rocq／Coq、Agda では、群の値をモノイドとして渡したいとき、変換のための関数を別に用意するか、型クラスの仕組みを使って、処理系に探させます。
言い換えると、群の値をモノイドとして渡したいとき、型検査器が変換のための関数を自動で挿入します。言語の中核が「群はモノイドの一種である」と認めているわけではありません。
Lean、Rocq／Coq、Agdaが、包摂的部分型付けと顕在フィールドを避けてきた理由については、筆者が調べた範囲では、一次資料で確認できませんでした。
結果として、Lean、Rocq／Coq、Agdaを使って数学の階層構造を書くときには、外側で手当てをすることになります。
顕在フィールドは、代数構造を定義する上でどう役立つのか
顕在フィールド は、代数構造を定義する上でどう役立つのかを理解するために、
半環 と 環 の関係を例に挙げることにします。
半環 は、足し算と掛け算を持つ構造です。
ただし、足し算の逆元は要求されません 。
ところで、半環の定義 には、$0 \times x = 0$ という等式が、公理として 含まれています。掛け算についての性質でありながら、公理として置かれている のです。
タロウくん：
なぜ、公理にする必要があるのですか？
専任講師：
半環 では、$0 \times x = 0$ という等式を導くことができないからです。
環 になると、事情が変わります。
環 は半環に足し算の逆元を加えたものですから、次のように進めることができます。
$$0 \times x = (0 + 0) \times x = 0 \times x + 0 \times x$$
両辺から $0 \times x$ を引けば、$0 = 0 \times x$ が残ります。
逆元があるので、この引き算ができるわけです。
タロウくん：
・・・環では、公理として置く必要がない。
専任講師：
ところが、ここで面倒が生じます。
環 を 半環 の拡張として定義したいのですが、半環 には、 $0 \times x = 0$ という項目が残っています。
環 では導けるのだから 公理として要求したくない。
それでも、拡張である以上、その項目を空欄のままにはできません。
ここで、顕在フィールドが、この空欄を埋める手段になります。
＜Arend のコード＞
\class Semiring \extends AbMonoid, Monoid {
| ldistr {x y z : E} : x * (y + z) = x * y + x * z
| rdistr {x y z : E} : (x + y) * z = x * z + y * z
| zro_*-left {x : E} : zro * x = zro
| zro_*-right {x : E} : x * zro = zro
}
\class Ring \extends Semiring, AbGroup {
| zro_*-left {x} => {?} -- 0 * x = 0 の証明。逆元を使って導ける
| zro_*-right {x} => {?} -- x * 0 = 0 の証明
}
出典：
Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"（Arend 公式論文に掲載されているコードです）
Semiring の zro_*-left は、公理として置かれた項目です。
そして Ring の側では、同じ名前に => を付けて値を与えています。
この => が 顕在フィールド であり、半環から受け継いだ空欄を、環の側で埋めている のです。
タロウくん：
・・・受け継いだ空欄を埋めながら、階層を積み上げていく。
専任講師：
顕在フィールドがなければ、そうはいきません。
論文が、その場合に何が起きるかを述べています。
（原文引用）
Without manifest fields, in bundled or unbundled case, typically one has to define more of the small, atomic records and combine them to define various composite records, the option of constructing composite records as specializations of other composite records becomes unavailable.
（筆者による日本語訳）
顕在フィールドがなければ、束ねた場合でも束ねない場合でも、通常はより多くの小さく原子的なレコードを定義し、それらを組み合わせてさまざまな複合レコードを定義することになる。複合レコードを、別の複合レコードの特殊化として構成するという選択肢が使えなくなるのである。
出典：同上
タロウくん：
環を半環の特殊化として書くのではなく、小さなレコードを集めて作り直す。
専任講師：
モノイド、群、環、体と階層が深くなるほど、その作り直しが積み重なります。
Arend は、包摂的部分型付けと顕在フィールドを Arend自身の中に組み込んだ
まず、包摂的部分型付けです。
＜Arend のコード＞
\data Bool | true | false
\func notB (b : Bool) : Bool \elim b
| true => false
| false => true
\func xor (x y : Bool) : Bool \elim x
| true => notB y
| false => y
-- モノイド：演算と単位元を持つ
\record Monoid (A : \Type)
| unit : A
| op : A -> A -> A
-- 群：モノイドを拡張し、逆元を加える
\record Group \extends Monoid
| inv : A -> A
-- Bool と xor は群をなす
\func BoolXor : Group \cowith
| A => Bool
| unit => false
| op => xor
| inv => \lam x => x
-- モノイドを受け取る関数
\func twice {A : \Type} (M : Monoid A) (x : A) : A => Monoid.op {M} x x
-- 群 BoolXor を、そのままモノイドとして渡せる
\func t : Bool => twice BoolXor true
\func c : t = false => idp
＜Arend の型検査結果＞
$ java -jar Arend.jar SUB3.ard
--- Typechecking \default ---
[ ] src.SUB3
--- Done (161ms) ---
\record Group \extends Monoid が、「群はモノイドを拡張したものである」 という宣言です。
そして twice は Monoid を受け取る関数です。しかし、群である BoolXor をそのまま渡すことができています。
変換のための関数は書いていません。
言語が「群はモノイドの一種である」と認めているためです。
次に、顕在フィールドです。
＜Arend のコード＞
\record Point
| x : Nat
| y : Nat
-- y を 0 に固定したレコード
\record OnAxis \extends Point
| y => 0
\func p1 : OnAxis \cowith
| x => 5
＜Arend の型検査結果＞
$ java -jar Arend.jar REC3.ard
--- Typechecking \default ---
[ ] src.REC3
--- Done (154ms) ---
| y => 0 が、顕在フィールドです。OnAxis の y は、定義の時点で 0 に確定しています。
そのため p1 を作るときには、x だけを与えれば済みます。y を渡す必要がありません。
第４回では、包摂的部分型付けと顕在フィールドを使って、モノイドから群、環、体へと階層を積み上げていきます。
そして、そもそも「型クラスに法則を書く」とはどういうことなのかという論点について、Haskell の Monoid を題材に向き合ってみることにします。
連載リンク
- 第１回：【Arend Theorem Prover 連載（初回）】「同型なものは等しい」を機械に検査させる ── 定理証明支援系 Arend がHoTTを公理としなかった理由
-
第２回：【Arend 連載②】なぜ Arend は「計算しきる力」よりも言語の使いやすさを優先したのか ── 区間
Iを「型」の中・「型」の外、どちらに置くか - 第３回：本記事
【発展篇】コラム ── 文脈について
【発展篇】コラム ── 文脈について
**対話の中で登場した `3 = 5` は、変数を含まない「空の文脈」で考えていました。** ここでは、この「文脈」という言葉が何を意味するのかを、少し丁寧に見ておきます。 ### 空の文脈で閉じた、とは何か **空の文脈で閉じたとは、簡単にいえば、外から与えられる変数を１つも使わずに書かれた式・値という意味です。** **型理論** では、変数とその型の並びを **文脈** と呼びます。 何も並んでいない状態が、**空の文脈** です。 ### 文脈とは何か たとえば、Arend に次の関数定義があるとします。 ``` \func addOne (n : Nat) : Nat => n Nat.+ 1 ``` 右辺の ``` n Nat.+ 1 ``` は、変数 `n` を使っています。 **この式は、`n : Nat` という前提のもとでしか意味を持ちません。** 型理論の記法では、概念的に次のように書きます。 $$n : \mathrm{Nat} \vdash n + 1 : \mathrm{Nat}$$ 左側の $$n : \mathrm{Nat}$$ が **文脈** です。 つまり、これは次の意味です。 **「自然数 `n` が与えられている状況で、`n + 1` は自然数である。」** ### 空の文脈とは何か 一方で、 ``` 2 Nat.+ 3 ``` には変数がありません。 **外から何かを受け取る必要もありません。** $$\vdash 2 + 3 : \mathrm{Nat}$$ **左側に何もないため、これが空の文脈です。** そして、変数をまったく含まない項を **閉じた項** と呼びます。 ``` \func five : Nat => 2 Nat.+ 3 ``` この `five` の右辺は閉じた項であり、**計算すると `5` になります。** | 式 | 文脈 | 閉じているか | |---|---|---| | `n Nat.+ 1` | `n : Nat` | 閉じていない | | `2 Nat.+ 3` | なし | **閉じている** | | `left` | なし | **閉じている** | | `i` | `i : I` | 閉じていない | | `i ∧ j` | `i : I, j : I` | 閉じていない | ### 区間 `I` での意味 Cubical Agda の説明で、 **空の文脈における閉じた `I` の値は、`i0` と `i1` の２つだけ** というのは、次の意味です。 ``` i0 : I i1 : I ``` **`i0` と `i1` は、変数を使わずに記述できます。したがって閉じた値です。** 一方、 ``` i : I ``` の `i` は、**あらかじめ `i : I` という変数を導入したときだけ使えます。** 概念的には、 $$i : I \vdash i : I$$ と書きます。**左側に `i : I` という前提があるため、`i` は閉じた値ではありません。** 同様に、 ``` i ∧ j i ∨ j ~ i ``` も `i` や `j` という変数に依存するので、**空の文脈では記述できません。** | 区間式 | 必要な文脈 | 閉じた値か | |---|---|---| | `i0` | なし | **はい** | | `i1` | なし | **はい** | | `i` | `i : I` | いいえ | | `~ i` | `i : I` | いいえ | | `i ∧ j` | `i : I, j : I` | いいえ | | `i ∨ j` | `i : I, j : I` | いいえ | **Cubical Agda の公式ドキュメントは、区間変数 `i : I` を導入した状況と、変数を何も持たない閉じた状況を区別しています。** そして、閉じた状況では `I` の値が端点 `i0` と `i1` に限られることを説明しています。 ### 日常語で言い換えると **「空の文脈」をプログラムの感覚で言えば、引数も自由変数もない状態です。** ```haskell x + 1 ``` では、`x` が何かを外から渡してもらわなければなりません。 **これは閉じていません。** ```haskell 2 + 3 ``` は、**何も渡してもらわなくてよいので閉じています。** 区間についても同じです。 ``` i0 i1 ``` は最初から記述できる **閉じた端点** です。 ``` i i ∧ j ~ i ``` は、**先に「`i` や `j` という区間変数を置く」という状況を作らなければ記述できません。**出典一覧
Arend
- Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"
https://arend-lang.github.io/assets/lang-paper.pdf - New theorem prover Arend is released, Homotopy Type Theory mailing list, 2019年8月6日
https://groups.google.com/g/homotopytypetheory/c/rf6YJB5Omj0 - Language Reference, Arend Documentation
https://arend-lang.github.io/documentation/language-reference/ - Tutorial, Arend Documentation
https://arend-lang.github.io/documentation/tutorial/
Lean
- Functions, The Lean Language Reference
https://lean-lang.org/doc/reference/latest/The-Type-System/Functions/ - Axioms and Computation, Theorem Proving in Lean 4
https://lean-lang.org/theorem_proving_in_lean4/axioms_and_computation.html
Kan 条件
- Kan fibration, Wikipedia
https://en.wikipedia.org/wiki/Kan_fibration
立方体型理論
- Bruno Bentzen, "Naive cubical type theory", arXiv:1911.05844
https://arxiv.org/abs/1911.05844 -
"Normal forms in cubical type theory", arXiv:2603.24923
https://arxiv.org/abs/2603.24923 -
"Towards Computational UIP in Cubical Agda", arXiv:2511.21209
https://arxiv.org/abs/2511.21209
ホモトピー型理論の起源
- Steve Awodey, Michael A. Warren, "Homotopy theoretic models of identity types", Mathematical Proceedings of the Cambridge Philosophical Society, vol. 146, no. 1, 2009, pp. 45–55
- Michael A. Warren, "Homotopy Theoretic Aspects of Constructive Type Theory", Ph.D. thesis, Carnegie Mellon University, 2008
- Martin Hofmann, Thomas Streicher, "The groupoid interpretation of type theory", Twenty-five years of constructive type theory, Oxford Logic Guides 36, 1998, pp. 83–111
- Daniel G. Quillen, "Homotopical Algebra", Lecture Notes in Mathematics 43, Springer, 1967
ホモトピー型理論（HoTT）
- The Univalent Foundations Program, "Homotopy Type Theory: Univalent Foundations of Mathematics", Institute for Advanced Study, 2013
https://homotopytypetheory.org/book/ - formalized libraries of homotopy type theory, nLab
https://ncatlab.org/nlab/show/formalized+libraries+of+homotopy+type+theory - 上村太一『ホモトピー型理論』2023年（著者はホモトピー型理論の意味論を専門とする研究者。アムステルダム大学で博士号を取得。本記事の訳語は、これに従いました）
https://uemurax.github.io/hott-ja/0000.html
型理論の系統
- Thierry Coquand, Gérard Huet, "The Calculus of Constructions", Information and Computation, vol. 76, no. 2–3, 1988, pp. 95–120
- Per Martin-Löf, "Intuitionistic Type Theory", Bibliopolis, 1984
検証環境
本記事に掲載した Arend のコードは、すべて実機で検証しました。
- Arend 1.10（Java 21）
型検査の結果とエラーメッセージは、実行時の出力をそのまま掲載しています。
一方、Cubical Agda については、執筆環境に処理系を用意できませんでした。
そのため、Cubical Agda のコード例は掲載していません。
同言語に関する記述は、Agda 公式ドキュメントおよび査読論文の記載に基づくものです。