0
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

@etale_cohomology(Etale Cohomology)

【Arend 連載⑥】証明を持ち回るか、型に書くか ── Arend の宇宙が２つの数で指定される理由

0
Last updated at Posted at 2026-09-05

thumbnail_picture.jpg

本記事は、連載記事の第６回です

Arend という定理証明支援系について、全７回にわたってお伝えしています。

これまでの流れ

回 何を扱ったか
第１回 なぜ Arend が生まれたのか。３つ目の可能性として「証明を持ち回らずに済む」を挙げた
第２回 区間を型の中に置き、仕様を単純に保った。代償は計算しきる力
第３回 等しさを型として扱うと、何ができるようになるか
第４回 代数構造の階層を、どこで支えるか
第５回 data で図形を作る。円周はどのホモトピーレベルにも収まらない
第６回 型の性質を、どこに置くか（宇宙の設計）

本記事の主題

本記事のテーマは、「証明を引数で運ぶか、型に語らせるか」ということです。

なお、本記事だけでも読めるように書きました。
第１回目から第５回目までの記事で扱った概念も、必要な範囲で改めて解説します。

本記事のExecutive Summary

本記事を読むと、何が分かるのか

Haskell で、3 の型は Int です。

では、Int の型は何でしょうか。

Haskell では * と記述します。種、あるいは kind と呼ばれます。

* の型は何でしょうか。

Haskell では、* の型を問うところで、階層が止まってしまいます。
Haskell は、* の型を問う手段がないからです。* の上に、もう階層がないのです。

Arend は、「型の型は何か」という問いに対して、 ある２つの数を導入する方法を選択しました 。

Haskell の * にあたるものを、Arend では \Type0 と記述します。

この \Type0 の型は \Type1 であり、
\Type1 の型は \Type2 です。

Haskell では止まっていた階層が、Arend では上へ続きます。

Arend には、もうひとつ別の数 があります。

\Type0 の横に、\Set0 や \Prop といった別の名前が並びます。

縦に上がる数と、横に並ぶ数。
２つの数 は、具体的に何を表しているのか。

本稿（本記事）は、その２つの数の定義を概観するのと同時に、こうした２つの数をArendが導入した理由を（記事の）テーマとして掲げます。

pic_1.jpg

注：上の図版の棚の並びは、本稿 第２部の２次元の表とは、左右が逆に描かれています。

左 → 右
第２部の２次元の表 \Prop、\Set0、\1-Type0、...
上の図版 \Type0、\Set0、\Prop

画像は「横に並ぶ」ことを示すためのものであり、並び順に意味はありません。
表では、\Prop が左端にあります。

２つの数とは、何か

縦に上がる数 と、横に並ぶ数 。

これら２つの数は、それぞれ。「大きさ」と「ホモトピーレベル」と呼ばれます。

なお、Arend では、型を分類するための型を宇宙と呼びます。
\Type0 も \Set0 も \Prop も、宇宙 です。

表記のしかた

Arend では、宇宙 を \n-Type p という形で記述 します。
n がホモトピーレベル、p が大きさです。

記法 ホモトピーレベル n 大きさ p
\Prop $-1$ なし
\Set0 $0$ $0$
\Set1 $0$ $1$
\1-Type0 $1$ $0$
\1-Type1 $1$ $1$
\2-Type3 $2$ $3$

\Set はホモトピーレベル $0$ の別名、\Prop はホモトピーレベル $-1$ の別名です。

\Set0 の 0 は大きさであり、Set という語がホモトピーレベル $0$ を表しています。

\1-Type1 のように２つの数が並ぶときは、前がホモトピーレベル、後ろが大きさです。

次に、ホモトピーレベル と 大きさ の定義を説明します。

表記順序とは逆になりますが、まず最初に 大きさ の定義を見ます。
そのあとで、ホモトピーレベル の定義を見ることにします。

大きさとは

大きさとは、その宇宙が、どれだけ多くの型を含めるかを表す数です。

\Type0 には、Nat や Bool のような普通の型が属します。

しかし、\Type0 自身は、\Type0 に属しません。

\Type0 自身を含めるには、より大きな宇宙が必要 です。
それが \Type1 です。

\Type1 には、\Type0 に属するすべての型に加えて、\Type0 自身も属します。

同様に、\Type1 自身を含めるには \Type2 が必要になります。

宇宙が自分自身を含めるために、ひとつ大きな宇宙を用意する。

この積み重ねが、階層 になります。

宇宙 何を含めるか
\Type0 Nat、Bool など
\Type1 \Type0 に属するすべての型、および \Type0 自身
\Type2 \Type1 に属するすべての型、および \Type1 自身

大きさの数が大きいほど、その宇宙はより多くの型を含めます。
これが、縦に上がる数です。

「\Type0 に属するすべての型について」と述べると、その主張は \Type1 に置かれます。 \Type0 全体を範囲として指定した時点で、\Type0 自身を扱っているからです。

ホモトピーレベルとは

ホモトピーレベルとは、その宇宙に属する型 が、等しさの構造をどこまで複雑に持ちうるかを表す数 です。

\Prop に属する型は、要素が高々１つです。

\Set0 に属する型は、要素は複数あってよいが、任意の２つの要素が 等しいことの根拠は高々１本 です。

\1-Type0 に属する型は、その型に属する２つの要素どうしの等しさの根拠が、複数あってよく、根拠どうしが等しいことの根拠が高々１本です。

「等しさ」を何段重ねたところで打ち止めになるかが、ホモトピーレベルです。

これが、横に並ぶ数 です。

なお、この２つの数の詳しい定義は、本稿の第２部と第５部で改めて扱います。
ここでは、２つの数がそれぞれ何を指すかを押さえておいてください。

宇宙とは何か

本記事の中心にある概念を、先に定義しておきます。

宇宙（universe）とは、型を分類するための型 です。

3 の型が Int であるように、Int の型が \Set0 です。

何を分類するか
型 値を分類する
宇宙 型を分類する

Arend の公式ドキュメントは、次のように述べています。

（原文引用）

A universe is a type of types.

（筆者による日本語訳）

宇宙とは、型の型である。

出典：
Universes, Arend Documentation

「型を集めた場所」という言い方は、直感としては分かりやすいのですが、正確ではありません。

その理由は、第２部で扱います。

ここで、タロウくんと専任講師の対話篇による補足説明を眺めてみましょう。

タロウくん：
先生、そうすると、宇宙は複数あるということですね？

なんだか、宇宙物理学における仮説の１つである、並行宇宙論みたいですね。

専任講師：
複数あります。しかし、並行ではありません。

タロウくん：
・・・並行ではない。

専任講師：
並行宇宙は、互いに独立して存在します。Arend の宇宙は、ひとつがもうひとつに属しています。

\Type0 は \Type1 に属し、\Type1 は \Type2 に属します。入れ子です。

タロウくん：
・・・マトリョーシカのような。

専任講師：
そのほうが近いです。

小さな人形が、ひとつ大きな人形の中に収まる。その人形が、さらに大きな人形の中に収まる。

ただし、入れ子の理由が違います。

タロウくん：
・・・理由、ですか。

専任講師：
マトリョーシカは、遊びのために入れ子になっています。

Arend の宇宙は、矛盾を避けるために入れ子になっています。

タロウくん：
・・・矛盾ですか？何か矛盾が生じてしまうのですか？

専任講師：
宇宙が、自分自身に 属すると、Arend の型理論そのものが矛盾してしまうのです。

そのために、ひとつ大きな宇宙を用意して、そこに属させるのです。

その理由は、この記事の第２部で扱います。

さて。ここまで、**「大きさ」という概念と、「ホモトピーレベル」**という概念について、入門向けの定義を紹介してみました。

以下では、Steve Awodey氏の論文から原文とその和訳文を引用する形で、ホモトピーレベル と向き合ってみます。

ホモトピーレベルとは何か

本記事の２つ目の中心概念です。

ホモトピーレベルとは、型の等しさの構造が、どこまで複雑になりうるかを表す数です。

（原文引用）

The homotopy level of a type is the height at which the tower of iterated identity types becomes degenerate.

（筆者による日本語訳）

型のホモトピーレベルとは、反復した同一視型の塔が退化する高さである。

出典：Steve Awodey, "A proposition is the (homotopy) type of its proofs", arXiv:1701.02024

この定義の意味は、第５部で対話篇を交えて解きほぐします。

本記事の結論

この記事の論旨展開と結論を先に要約してお伝えします。

第１に、Haskell の * の上には、まだ階層があります。

Haskell では問う手段がありませんが、定理証明支援系では階層が続いています。
そして、その階層には理由があります。

第２に、HoTT を扱う体系では、「この型は集合である」という証明を関数から関数へ渡し続けることになります。

Agda がそうです。関数が10個あれば、10箇所に同じ証明を書きます。

第３に、Arend では、その必要がありません。

\Set0 と書いた時点で、その情報が型に含まれているからです。

証明を引数で運ぶか、型に語らせるか。 そのために Arend は、宇宙に２つ目の軸を足しました。

ところで、標準の Lean 4 も、その証明を持ち回らずに済みます。

しかし、持ちまわらずに済む理由は、Arendとは正反対 です。

Lean 4 の 標準的な 等号では、同じ２つの値の等号証明を区別しない原理（UIP） が成り立ちます。

その結果、HoTT のように、等号そのものが豊かな高次構造を持つものとして扱う設計にはなっていません。

第５回目の記事で扱った高次帰納型としての円周は、そのままの形では中心的な対象になりません。

ひとことで言えば、Lean 4 は「等しさの根拠どうしの違い」を追いかけない設計です。

Arend は、区別を型で管理する 設計を 選択 しました。
その結果、Arendでは、宇宙の仕様が複雑に なりました。

pic_2.jpg

同じ問題に向き合う上で、正反対の設計方法による対処法を考えることができる のです。

  • Lean 4 は「等しさの根拠どうしの違い」を追いかけない設計を選択しました。

  • Arend は、「等しさの根拠どうしの違い」を型で管理する 設計を 選択 しました。

pic_3.jpg

なぜ、この２つが正反対の設計といえるのでしょうか？

順に確かめてみましょう。

まず、Lean 4 の側です。

Lean 4 の標準の等号 Eq は Prop に属し、証明無関係が成り立ちます。

「証明無関係」 とは、同じ主張についての証明は、すべて等しいとみなす という規則です。
ある命題の証明を２通り書けたとしても、その２つを区別しない、ということです。

その結果、UIP が成り立ち、等しさの証明どうしを区別しない 設計になっています 。

pic_4.jpg

UIP については、少し前の行で簡単に定義を紹介しましたが、改めてその定義を掲載します。

UIP（ uniqueness of identity proofs、等しさの証明の一意性） とは、どの型のどの２つの要素についても、それらが等しいことの証明は高々１つしかない、という原理 です。

一見異なる ２つの証明があっても、等しいものとして扱う、ということです。

pic_5.jpg

（Lean 4より過去のバージョンである）Lean 2 には証明無関係を外した HoTT モードがありましたが、Lean 3 以降では、廃止されました。

pic_6.jpg

等しさの根拠どうしの違いを追いかけない、という設計 は、Lean の開発者が、証明無関係を採るかどうかを判断した結果、明示的になされた選択です。**

次に、Arend の側です。

宇宙 に ホモトピーレベルの軸 を付け加えることで、\Prop、\Set0、\1-Type0 と、根拠の構造を型の側で分類する設計が選択されています。

等しさの根拠どうしの違いを、型が管理する設計 です。

pic_7.jpg

Lean 4とArendを比べる、同じ問題に対する（対応法の）設計思想が、互いに正反対で様子が浮かび上がります。

証明を持ち回らずに済む理由
Lean 4 等しさの根拠どうしの違いを、区別しないことにした
Arend 等しさの根拠どうしの違いを、型で管理することにした

Arendの設計方針について、Arendの開発者自身が公開直後に専門家から問われています。

「証明は、まだどこか背後に隠れているのですか」と。

その問いと回答を、本記事の第６部で扱います。

本記事には、Arend 以外の言語も登場します

本記事の主題は Arend です。

しかし、Arend の設計判断を理解するには、他の言語がどうしているかを見る必要があります。

言語・処理系 本記事で登場する理由 実機検証
Arend **本記事の主題。**宇宙が２つの数で指定される 1.10
Haskell 出発点。* から始める。Type :: Type が通る GHC 9.4.7
Agda 対比の中心。--without-K では isSet の証明を持ち回る Agda 2.6.3
Lean 4 **対比。**UIP（uniqueness of identity proofs、等しさの証明の一意性。どの２つの要素についても、等しいことの証明は高々１つしかないという原理）を認め、すべての型を集合とする 4.33.1
Rocq／Coq 対比。Set が非可述的から可述的へ変わった経緯 未検証

Rocq／Coq を除き、本記事に掲載したコードはすべて実機で検証しました。 一覧は本稿末尾の Appendix に掲載しています。

本記事の議論の流れ

青い枠が、出発点です。

Haskell の * から始めます。読者が毎日使っている道具です。

赤い枠が、問題です。

「この型は集合である」という証明を、関数から関数へ渡し続けることになります。

金色の枠が、本記事の中心です。

Arend が、その問題をどう解いたか。そして、その解き方について開発者が何を語ったか。

緑の枠が、到達点です。

Lean 4 も、証明を持ち回らずに済みます。しかし、Arend とは理由が正反対です。

本連載シリーズの第１回目の記事で予告した「証明を持ち回らずに済む」の中身が、ここで明らかになります。

対話篇 ── 本記事は何を扱うのか

タロウくん：
先生、本記事は何を扱うのですか？

専任講師：
宇宙の設計です。

タロウくん：
・・・本連載シリーズの第４回目の記事で、２つの数で指定される表を見ました。

専任講師：
そのとおりです。
あの表が、なぜ必要なのかを扱います。

タロウくん：
なぜ必要なのですか。

専任講師：
証明を持ち回らずに済ませるためです。

タロウくん：
・・・持ち回る、といいますと。

専任講師：
HoTT を扱う体系 では、「この型は集合である」という性質を使いたいとき、その証明 を引数として受け取ります。

Agda がそうです。

そして、別の関数を呼ぶときにも渡します。

タロウくん：
・・・関数が増えれば、そのすべてに付いて回る。

専任講師：
Arend では、その必要がありません。

\Set0 と書いた時点で、その情報が型に含まれているからです。

タロウくん：
・・・型が、自分の性質を語っている。

専任講師：
証明を引数で運ぶか、型に語らせるか。

そこが、本記事で扱う論点です。

タロウくん：
・・・Lean ではどうなのですか。

専任講師：
Lean 4 も、持ち回らずに済みます。

タロウくん：
・・・では、Arend と同じですか？

専任講師：
理由が正反対です。

そこは、本記事の最後で扱います。

タロウくん：
・・・では、証明はどこへ行ったのですか。

専任講師：
同じ問いを、2019年8月に発した人がいます。

Arend が公開された直後、ホモトピー型理論の研究者が開発者に対して、次のように尋ねました。

「それらはまだどこか背後に隠れているのですか」と。

タロウくん：
・・・専門家も、同じところが気になった。

専任講師：
その問いと回答が、本記事の後半にあります。

本記事の読み方

本記事は長いため、関心に応じた入口を示しておきます。

関心 どこから読むか
Haskell の * から読みたい 第１部から順に
宇宙とは何かを、正確に知りたい 第２部
「この型は集合である」という証明を、なぜ持ち回ることになるのかを知りたい 第３部
Arend の宇宙が、なぜ２つの数で指定されるのかを知りたい 第５部
宇宙という考え方が、Arend 以外の言語にもあるのかを知りたい 第５部の末尾
Arend の開発者が、公開直後に専門家から何を問われたのかを知りたい 第６部
Lean 4 と Arend が、なぜどちらも証明を持ち回らずに済むのかを知りたい 第７部

なお、本記事は入門者向けに簡略化した表現を用いています。

正確な言い換えの一覧については、本稿末尾の コラム欄 （本文の簡略化と、その正確な言い換えの一覧）をご参照ください。

第１部 ── Haskell の * は、階層が１段しかない

pic_8.jpg

型の型

Haskell で 3 の型は Int でした。

では、Int の型は何でしょうか。

タロウくん：
・・・型に、型があるのですか。

専任講師：
あります。

Haskell では * と記述します。
種、あるいは kind と呼ばれます。

＜Haskell のコード＞

Int  :: *
Bool :: *

タロウくん：
・・・* という記号が、種の名前ですか。

専任講師：
そうです。現在の GHC では Data.Kind.Type が推奨され、* は旧来の表記です。

タロウくん：
・・・関数の型は、どうなりますか。

専任講師：
Maybe のように、型を受け取って型を返すものは、* -> * という種を持ちます。

型 種
Int *
Maybe * -> *
Either * -> * -> *

タロウくん：
・・・型のレベルにも、関数がある。

そして、その上は

タロウくん：
・・・では、* の型は。

専任講師：
Haskell では、そこで止まります。

* 自身の型を問う手段が、言語に用意されていません。

タロウくん：
・・・階層が１段しかない。

専任講師：
そして、Haskell ではそれで足ります。

通常の型システムの範囲では、* のさらに上を同じように問い続ける仕組みはありません。

タロウくん：
・・・数学の議論を組み立てる言語だと、足りないのですか。

専任講師：
足りません。その理由を、第２部で見ます。

Arend では、この問いに答えがあります。

なお、種と宇宙の違いについては、本稿末尾の コラム欄 （種と宇宙の違いについて）をご参照ください。

第２部 ── 宇宙とは、型を分類するための型である

pic_9_.jpg

宇宙は、型を集めた箱ではありません

タロウくん：
・・・宇宙というのは、型を 集めた 箱のようなものですか？

専任講師：
いまのタロウくんの認識には、注意すべき論点が潜んでいます。

「集めたもの」 と考えると、あとで話が合わなくなります。

タロウくん：
・・・では、何なのですか。

専任講師：
図書館で考えてみましょう。

書棚には、本が並んでいます。

タロウくん：
はい。

専任講師：
そして、それぞれの本には 分類記号 が付いています。
「哲学」「歴史」「自然科学」といった具合です。

タロウくん：
・・・本を、種類ごとに分けるための記号ですね。

専任講師：
では、その分類記号そのものは、どこから来たのでしょうか？

タロウくん：
・・・分類 の体系 がある、ということですか？

専任講師：
日本十進分類法という分類体系 があります。

どの記号が使えるか、それぞれが何を指すかを定めたものです。

タロウくん：
・・・ 本を集めたものではない。

専任講師：
分類体系は、本の集まりではありません。

「本をどう分類するか」を定めるもの です。

pic_9.jpg

図書館 型理論
本 値
分類記号 型
分類体系 宇宙

タロウくん：
・・・　宇宙は、型を分類するためのもの 。

専任講師：
そのとおりです。

宇宙とは、型を分類するための型です。

「型を集めた場所」という言い方は、直感としては分かりやすいのですが、正確ではありません。

タロウくん：
・・・どう違うのですか。

専任講師：
「集めたもの」と考えると、集合論の話に引きずられます。

「すべての型を要素として持つ集合 が存在する」と主張しているように読めてしまうのです。

タロウくん：
・・・ラッセルのパラドックスの話につながる。

専任講師：
型理論の宇宙は、そういう主張をしていません。

A : \Type0 と書いたとき、これは「型 A が \Type0 に分類される」という型付けを表しています。

なお、宇宙が「型を集めた場所」ではないことについては、本稿末尾の コラム欄 （宇宙は「型を集めた場所」ではありません）をご参照ください。

２つの入口をつなぐ

タロウくん：
・・・Haskell の * も、分類記号の体系だったのですね。

専任講師：
そうです。
ただし、体系が１つしかありませんでした。

Arend では、その体系が２つの数で指定されます。

タロウくん：
・・・２つ。

専任講師：
これは、今回の記事で取り上げる大きなテーマのひとつです。

まず最初に、１つ目の数 から見ていきましょう。

大きさの階層

専任講師：
Arend の公式ドキュメントが、宇宙を次のように定義しています。

（原文引用）

A universe is a type of types. Since the type of all types cannot be consistently introduced to a type theory with dependent Pi types, as the type of types cannot contain itself, Arend contains a hierarchy of universes \Type n (the whitespace is optional), parameterized by a natural number n.

（筆者による日本語訳）

宇宙とは、型の型である。
すべての型の型を、依存関数型を持つ型理論へ矛盾なく導入することはできない。
型の型が自分自身を含むことはできないからである。
そのため Arend は、自然数 n で径数づけられた宇宙の階層 \Type n を持つ。

出典：
Universes, Arend Documentation

タロウくん：
・・・「型の型が自分自身を含むことはできない」というのが分かりません。

専任講師：
\Type0 という宇宙があるとします。その \Type0 自身の型は何でしょうか。

タロウくん：
・・・\Type0 ですか。

専任講師：
そう置くと、体系が壊れます。

「自分自身を要素として含む集まり」を許すと、矛盾が導けるのです。

ラッセルのパラドックスと同じ構造です。

タロウくん：
・・・では、どうするのですか？

専任講師：
ひとつ上に、\Type1 を用意します。

実機で確かめてみます。

＜Arend のコード＞

\func a : \Prop => \Type0

＜Arend の型検査結果＞

$ java -jar Arend.jar UU3.ard

[ERROR] src.UU3:1:21: Type mismatch
  Expected type: \Prop
    Actual type: \Type1
  In: \Type0

タロウくん：
・・・\Type0 の型は \Type1 ですね。

専任講師：
エラーメッセージが、そう教えてくれています。

書き方 読み方
3 : Nat 値 3 の型は Nat
Nat : \Set0 型 Nat の型は \Set0
\Type0 : \Type1 \Type0 の型は \Type1
\Type1 : \Type2 \Type1 の型は \Type2

この積み上げが、限りなく続きます。

タロウくん：
・・・\Type のあとの数字が、何段目かを表している。

専任講師：
それが、１つ目の数です。大きさと呼びます。

なお、自分自身を含めると矛盾する理由については、本稿末尾の コラム欄 （ジラールのパラドックスについて）をご参照ください。

可述性 ── なぜ、階層が要るのか

タロウくん：
先生、「可述的レベル」という言葉が公式ドキュメントに出てきました。

「可述的」というのは、何ですか。

専任講師：
本連載シリーズの第４回目の記事で論じた内容の振り返りになりますが、ここで改めて解説します。

そして、第４回目の記事より正確な形で述べます。

タロウくん：
・・・正確な形、ですか。

専任講師：
第４回目の記事では、「自分自身を含む集まりについて語ることを禁じる立場」と述べました。

その一文だけでは、定義になりません。

まず、具体例から

専任講師：
\Type0 のことを考えてください。

「\Type0 に属するすべての型について、〜が成り立つ」という主張を書きたいとします。

タロウくん：
はい。

専任講師：
その主張自身は、どこに置かれるでしょうか。

タロウくん：
・・・\Type0 ですか。

専任講師：
\Type1 に置かれます。

＜Arend のコード＞

\func allTypes : \1-Type1 => \Pi (A : \Type0) -> \Type0

＜Arend の型検査結果＞

$ java -jar Arend.jar PRED1.ard

--- Typechecking \default ---
[ ] src.PRED1
--- Done (88ms) ---

タロウくん：
・・・ ひとつ上へ上がってしまう。

専任講師：
「\Type0 のすべてについて語る」主張は、\Type0 には入りません。

この性質を、可述的といいます。

pic_10.jpg

なぜ、ひとつ上へ上がるのか

タロウくん：
・・・なぜ、ひとつ上へ上がるのですか。

専任講師：
先ほど見た、\Type0 の型が \Type1 であることを思い出してください。

「すべての型 A について」と言うとき、A が動く範囲を指定します。

タロウくん：
・・・その範囲が \Type0。

専任講師：
そして \Type0 は、\Type1 に属します。

範囲を指定した時点で、\Type1 の住人を使っているのです。

タロウくん：
・・・だから、主張も \Type1 へ行く。

専任講師：
$\Pi$ 型の大きさは、定義域と値域の大きいほうで決まります。

$$\text{大きさ}\bigl(\Pi(x : A)., B\bigr) = \max\bigl(\text{大きさ}(A),\ \text{大きさ}(B)\bigr)$$

タロウくん：
・・・返す型が小さくても、定義域が大きければ上がる。

専任講師：
確かめてみます。

＜Arend のコード＞

\func f : \Set0 => \Pi (A : \Type0) -> Nat

＜Arend の型検査結果＞

$ java -jar Arend.jar PI3.ard

[ERROR] src.PI3:1:21: Type mismatch
  Expected type: \Set0
    Actual type: \Set1
  In: \Pi (A : \Type0) -> Nat

返すのは Nat です。\Set0 に属します。それでも、全体は \Set1 になります。

タロウくん：
・・・定義域のほうが効いている。

専任講師：
「すべての型について」と言うたびに、ひとつ上の宇宙を使うことになるのです。

定義を、正確に述べます

専任講師：
可述的（predicative）とは、ある対象を定義するとき、その対象自身を含む全体について量化することを許さない、という性質です。

タロウくん：
・・・「量化する」というのは。

専任講師：
「すべての〜について」と述べることです。

\Pi (A : \Type0) -> ... の \Pi が、量化にあたります。

タロウくん：
・・・「すべての A について」。

専任講師：
そして、その A が動く範囲のなかに、いま作ろうとしている主張自身が入っていない こと。

それが、可述的ということです。

pic_12.jpg

タロウくん：
・・・だから、「可述的レベル」 と呼ぶのですね。

専任講師：
大きさの階層は、可述性を保つための仕組み です。

pic_11.jpg

非可述性 ── \Prop だけは違います

専任講師：
では、\Prop はどうでしょうか。

（原文引用）

Note that the universe \Prop is impredicative: it does not have predicative level. Practically, this means that if B : \Prop, then the type \Pi (x : \Prop) -> B is in \Prop.

（筆者による日本語訳）

宇宙 \Prop は非可述的であることに注意せよ。それは可述的レベルを持たない。実際上これは、B : \Prop なら型 \Pi (x : \Prop) -> B も \Prop に属する、ということを意味する。

出典：Universes, Arend Documentation

タロウくん：
・・・\Pi (x : \Prop) -> B という書き方が分かりません。

専任講師：
「すべての命題 x について、B が成り立つ」という主張です。

タロウくん：
・・・先ほどの \Pi (A : \Type0) -> ... と、同じ形ですね。

専任講師：
同じ形です。しかし、置かれる場所が違います。

実機で確かめます。

＜Arend のコード＞

\func f (B : \Prop) : \Prop => \Pi (x : \Prop) -> B

＜Arend の型検査結果＞

$ java -jar Arend.jar PRED2.ard

--- Typechecking \default ---
[ ] src.PRED2
--- Done (77ms) ---

通ります。

主張 どこに置かれるか
\Pi (A : \Type0) -> ... \Type1（ひとつ上へ上がる）
\Pi (x : \Prop) -> B \Prop（上がらない）

タロウくん：
・・・\Prop だけ、上がらない。

専任講師：
「すべての命題について」と述べても、\Prop から出ないのです。

タロウくん：
・・・すべての命題について、という部分が気になります。

専任講師：
「すべての命題」と言うとき、その中には、いま作ろうとしている主張も含まれます。

タロウくん：
・・・自分自身を含む全体について、量化している。

専任講師：
そこが、非可述的ということです。

非可述的（ impredicative ）とは、ある対象を定義するとき、その対象自身を含む全体について量化することを許す という性質です。

タロウくん：
先生、ひとつ確かめさせてください。

非可述的 というのは、自分自身を含む全体について量化している、ということでした。

しかし、非可述的な場合 こそ、自分自身は含まない のではありませんか？

専任講師：
タロウくんは、２つの別のことが頭の中で混同している と思います。

「自分自身を含む」 と言うとき、何が何を含むかで、答えが変わります。

何が 何を 含むか
量化範囲 \Prop 命題 \Pi (x : \Prop) -> B 含む
宇宙 \Prop 宇宙 \Prop 含まない

タロウくん：
・・・上の行が、非可述性ですね。

専任講師：
\Pi (x : \Prop) -> B は命題です。\Prop に属します。

x は \Prop 全体を動きます。

だから、この命題自身が x の範囲に入ります。

タロウくん：
・・・下の行は？

専任講師：
\Prop という宇宙が、\Prop に属するかどうか。これは成り立ちません。

タロウくん：
・・・ 命題が範囲に入ることと、宇宙が自分に属することは、別のこと 。

専任講師：
そのとおりです。非可述性は、前者です。

後者については、このあとすぐに確かめます。

pic_13.jpg

\Prop 自身は \Prop に属しません

タロウくん：
・・・では、\Prop そのものも \Prop に属するのですか？

専任講師：
そこは違います。

コードを動かして、確かめてみましょう。

＜Arend のコード＞

\func p : \Prop => \Prop

＜Arend の型検査結果＞

$ java -jar Arend.jar PRED3.ard

[ERROR] src.PRED3:1:20: Type mismatch
  Expected type: \Prop
    Actual type: \Set0
  In: \Prop

弾かれます。\Prop 自身は \Set0 に属します。

タロウくん：
・・・「すべての命題について」は \Prop に入るのに、\Prop 自身は入らない。

専任講師：
そこを混同しないことが大切です。

成り立つか
\Pi (x : \Prop) -> B が \Prop に属する 成り立つ
\Prop 自身が \Prop に属する 成り立たない

非可述的とは、「すべての命題について量化した主張が、\Prop から出ない」ということです。

\Prop そのものが \Prop に属する、という意味ではありません。

pic_14.jpg

タロウくん：
・・・もし属したら、どうなりますか。

専任講師：
先ほど見た、自分自身を含む問題が起きます。

タロウくん：
・・・論理として壊れる。

専任講師：
そうなりますね。

\Prop は \Set0 に属します。
階層のなかに、きちんと置かれています。

なお、非可述性と自己所属を混同しないための整理については、本稿末尾の コラム欄 （非可述的な \Prop は、なぜ直ちに \Prop : \Prop を意味しないのか）をご参照ください。

また、可述性と非可述性の厳密な議論については、本稿末尾の 別のコラム欄 （可述性と非可述性を、厳密にいうと）を併せてご一読いただけると、より一層理解が深まると思われます。

記号の読み方

本稿（本記事）では、Arend の記号を繰り返し掲載しします。

本連載シリーズの第４回目の記事で論じた内容の振り返りになりますが、ここで改めて解説します。

Arend の記号 読み方 意味
\Type タイプ 型が置かれる場所。宇宙
\Type0, \Type1, \Type2, ... タイプ・ゼロ、タイプ・イチ 大きさの階層
\Prop プロップ 命題として扱われる型を分類する宇宙（要素が高々１つ）
\Set セット 集合とみなせる型を受け入れる宇宙（等しさの根拠が高々１本）
\Set0, \Set1, \Set2, ... セット・ゼロ、セット・イチ \Set の大きさの階層
\n-Type p エヌ・タイプ・ピー ホモトピーレベル n、大きさ p の宇宙
\lp エル・ピー 大きさの径数
\lh エル・エイチ ホモトピーレベルの径数
\oo 無限大 ホモトピーレベルの無限大

pic_15.jpg

「高々１つ」という言い回しについて

タロウくん：
先生、「要素が高々（たかだか）１つしかない」という言い方が気になります。

「高々」というのは、「多くても」という意味ですよね。

専任講師：
そうです。
０個か１個、ということです。

タロウくん：
・・・では、\Prop の型には、要素が １個しかないのですか？

専任講師：
「高々１つ」とは、要素が文字どおり１個しかない、という意味ではありません。

タロウくん：
・・・どういう意味ですか。

専任講師：
要素が複数あるように見えても、どの２つを取っても等しい、という意味です。

タロウくん：
・・・見た目が違っても、等しい。

専任講師：
たとえば、「$3$ は奇数である」という主張を考えてください。

その証明を、２通りの書き方で書いたとします。

書き方 内容
① $3 = 2 \times 1 + 1$ だから
② $3 = 2 \times 1 + 1$ であり、$1 \leq 1$ だから

タロウくん：
・・・②のほうが、余計なことを言っていますね。

専任講師：
しかし、どちらも同じ主張の証明です。

そして、この２つは等しいとみなされます。

タロウくん：
・・・別々に書いたのに、等しい。

専任講師：
一見異なる証明であっても、同じ主張についての証明であれば、等しいものとして扱う。

それが、「要素が高々１つ」ということの意味です。

pic_16.jpg

タロウくん：
・・・「高々（たかだか）」は、数学者の言い回しなのですね。

専任講師：
型理論 では、「型 A の要素が高々１つである」 を、次のように 定義 します。

$$\text{isProp}(A) := \prod_{(x, y : A)} (x = y)$$

「どの２つの要素 x、y を取っても、x = y が成り立つ」ということです。

タロウくん：
・・・ 「１個しかない」ではなく、「どれも等しい」 。

専任講師：
そうです。
\Set の「等しさの根拠が高々１本」も、同じ意味 です。

x = y の要素、つまり等しさの根拠が複数あるように見えても、どの２つを取っても等しい、ということ です。

タロウくん：
・・・ 一見異なる 根拠であっても、 本質的には同じ１つの根拠とみなせる場合は、１つとみなす 。

専任講師：
そのとおりです。

本記事では、この言い回しを何度も使います。

なお、\Set0 と \Prop の「高々１つ」が何を数えているのかについては、本稿末尾の コラム欄 （\Set0 と \Prop の「高々１つ」は何を数えているのか）をご参照ください。

なお、\ はキーワードの目印です。
Haskell のラムダ式とは異なります。

Arend の公式マニュアル のURLは、下記のとおりです。

なお、本記事に掲載したコードの検証環境については、本稿末尾の Appendix および 本稿末尾のコラム欄 （本記事のコードの検証環境について）をご参照ください。

また、訳語の選定については、本稿末尾の別のコラム欄 （訳語について）をご参照ください。

２つの数の読み分け

タロウくん：
・・・\Set0 の 0 は、大きさですか、ホモトピーレベルですか？

専任講師：
大きさです。

Set という語が、ホモトピーレベル $0$ を表しています。

タロウくん：
・・・\1-Type1 は、どちらも 1 ですね。

専任講師：
前のほうがホモトピーレベル、後ろのほうが大きさです。

\n-Type p という形で、n がホモトピーレベル、p が大きさです。

記法 ホモトピーレベル 大きさ
\Prop $-1$ なし（非可述的）
\Set0 $0$ $0$
\Set1 $0$ $1$
\1-Type0 $1$ $0$
\1-Type1 $1$ $1$
\2-Type3 $2$ $3$

タロウくん：
・・・\Set0 は、\0-Type0 と書いても同じですか。

専任講師：
同じものを指します。

Set は、ホモトピーレベル $0$ の別名です。

２次元の表

専任講師：
本連載シリーズの第４回目の記事で示した表を、再掲します。

レベル $-1$ レベル $0$ レベル $1$ レベル $2$ レベル $3$
大きさ 0 \Prop \Set0 \1-Type0 \2-Type0 \3-Type0
大きさ 1 ── \Set1 \1-Type1 \2-Type1 \3-Type1
大きさ 2 ── \Set2 \1-Type2 \2-Type2 \3-Type2
大きさ 3 ── \Set3 \1-Type3 \2-Type3 \3-Type3

表は、上にも右にも続きます。

表の見方

# 説明
① 縦軸が大きさ、横軸がホモトピーレベルです
② \n-Type p の n が横軸、p が縦軸です
③ \Set はレベル $0$ の別名、\Prop はレベル $-1$ の別名です
④ **\Prop の列だけ、大きさの欄が空いています。**非可述的だからです
⑤ 実際に使うのは、表の左のほうです

タロウくん：
・・・⑤について、どこをよく使うのですか。

専任講師：

よく使う場所 何に使うか
\Prop 「正しい」という主張。真偽値のかわり
\Set0 自然数、整数、文字列など、通常の離散的なデータ型を置く場所
\Set1 「集合をすべて集めたもの」。圏を定義するときなど
\1-Type1 圏そのもの

タロウくん：
・・・横軸のホモトピーレベルが、まだ分かりません。

専任講師：
そこは第５部で扱います。

その前に、なぜ横軸が要るのかを、第３部と第４部で見ておきます。

第３部 ── 証明を、関数から関数へ渡し続ける

pic_17.jpg

「この型は集合である」という性質

専任講師：
本連載シリーズの第３回目の記事で、等しさの根拠が複数ある場合を見ました。

過去の記事で論じた内容の振り返りになりますが、ここで改めて解説します。

3 = 3 の根拠は、実質１本でした。Bool = Bool の根拠は２本ありました。
何も変えない対応と、true と false を入れ替える対応です。

タロウくん：
・・・型によって、根拠の数が違う。

専任講師：
「この型については、根拠が高々１本しかない」という性質 には、名前が与えられて います。

isSetについて

専任講師：
「この型は集合である」という性質を、型として書いたもの が、isSet です。

＜Agda のコード＞

isSet : Set → Set
isSet A = (x y : A) (p q : x ≡ y) → p ≡ q

「どの２つの要素 x、y についても、x ≡ y の証明が２つあれば、その２つは等しい」という主張 です。

タロウくん：
・・・等しさの根拠が、高々１本ということですね。

専任講師：
isSet A は、「A の要素どうしについては、根拠が１本しかない」と述べています。

add_pic_1.jpg

タロウくん：
・・・Agda の Set は、Arend の \Set と同じですか？

専任講師：
違います。

Agda の Set は、Arend の \Type にあたります。

紛らわしいので、注意してください。

Agda Arend 意味
Set \Type0 型が置かれる場所
Set₁ \Type1 ひとつ上
isSet A ── 「A は集合である」という主張

pic_18.jpg

UIP ── isSet を、すべての型について認めると

タロウくん：
先生、isSet を「すべての型について認める」と、どうなりますか。

専任講師：
それが UIP です。

UIP（ uniqueness of identity proofs ）とは、どの型のどの２つの要素についても、それらが等しいことの証明は高々１つしかない、という原理です。

日本語では「等しさの証明の一意性」と訳します。

$$\text{UIP} := \prod_{(A : \mathcal{U})} \prod_{(x, y : A)} \prod_{(p, q : x = y)} (p = q)$$

タロウくん：
・・・「すべての型 A について、isSet A が成り立つ」と読めますね。

専任講師：
そのとおりです。

何を主張しているのか

専任講師：
本連載シリーズの第３回目の記事で、Bool = Bool の 根拠が２本あること を見ました。

根拠 対応
① true → true、false → false
② true → false、false → true

UIP は、「この２本は、実は同じものである」と主張します。

タロウくん：
・・・第２部で見た「高々１つ」の意味ですね。
一見異なる根拠でも、等しいとみなす。

専任講師：
等しさの根拠を、いつでも１本に潰します。

UIP を認めると、何が起きるか

# 起きること
① すべての型が、集合になる
② 直感的には、円周が１点に潰れるようなことが起こる
③ 一価性と両立しなくなる

タロウくん：
・・・②は、本連載シリーズの第５回目の記事で見ました。

専任講師：
base = base の根拠が idp と loop の２本ありました。
UIP は、その２本を同じにしてしまいます。

厳密には、HoTT で考えていたような高次構造を持つ円周が、そのままでは成立しなくなる、ということです。

タロウくん：
・・・③は。

専任講師：
一価性は、「同値な型は等しい」と述べます。その結果、Bool = Bool の根拠が２本になります。

UIP は、その２本を１本に潰します。両方を認めると、矛盾します。

タロウくん：
・・・どちらかを選ぶことになる。

なお、UIP と一価性が両立しない理由については、本稿末尾の コラム欄 （UIP と一価性が両立しない理由を、厳密にいうと）をご参照ください。

どの処理系が、UIP を認めているか

処理系 UIP 理由
Lean 4 認める Prop の証明無関係から導かれる
標準の Agda 認める パターンマッチの K 規則が、UIP を導く
Agda --without-K 認めない K 規則を無効にする
Arend 認めない HoTT を扱うため

タロウくん：
・・・「--without-K」の K というのは。

専任講師：
K は、UIP と同じ内容を別の形で述べた公理の名前です。

Agda は既定でこの規則を使い、--without-K で無効にします。

タロウくん：
・・・だから、HoTT を扱うときは --without-K を付ける。

専任講師：
そして、これから見る Agda のコードは、すべて --without-K を付けています。

UIP を認めない設定で、isSet の証明をどう扱うかを見るためです。

なお、K 公理と UIP の関係については、本稿末尾のコラム欄（K 公理と UIP の同値性について）をご参照ください。Rocq／Coq と UIP の関係については、本稿末尾の コラム欄 （Rocq／Coq と UIP の関係）をご参照ください。

証明を、引数として受け取る

専任講師：
isSet を使う関数を書いてみます。

＜Agda のコード＞

{-# OPTIONS --without-K #-}
module CARRY where
open import Agda.Builtin.Equality

isSet : Set → Set
isSet A = (x y : A) (p q : x ≡ y) → p ≡ q

useIsSet : (A : Set) → isSet A → (x y : A) (p q : x ≡ y) → p ≡ q
useIsSet A h x y p q = h x y p q

＜Agda の型検査結果＞

$ agda CARRY.agda

Checking CARRY (/tmp/ag/CARRY.agda).

通ります。

タロウくん：
・・・h が、isSet A の証明ですね。

専任講師：
useIsSet は、h を引数として受け取っています。

タロウくん：
・・・--without-K が付いていますね。

専任講師：
先ほど述べたとおり、UIP を認めない設定です。

別の関数でも、また渡すことになる

専任講師：
useIsSet を使う、別の関数を書いてみます。

＜Agda のコード＞

useIsSet2 : (A : Set) → isSet A → (x y : A) (p q : x ≡ y) → p ≡ q
useIsSet2 A h x y p q = useIsSet A h x y p q

useIsSet3 : (A : Set) → isSet A → (x y : A) (p q : x ≡ y) → p ≡ q
useIsSet3 A h x y p q = useIsSet2 A h x y p q

＜Agda の型検査結果＞

$ agda CARRY.agda

Checking CARRY (/tmp/ag/CARRY.agda).

タロウくん：
・・・useIsSet2 も useIsSet3 も、h を受け取っています。

専任講師：
そして、次の関数を呼ぶたびに h を渡しています。

関数 h を受け取るか h を渡すか
useIsSet 受け取る ──
useIsSet2 受け取る useIsSet へ渡す
useIsSet3 受け取る useIsSet2 へ渡す

タロウくん：
・・・関数が増えれば、そのすべてに h が付いて回る。

専任講師：
関数が10個あれば、10箇所に書くことになります。

中上級者向けに補うと、implicit argument や record などで書く量を減らす方法はあります。
それでも、性質を利用側へ渡すという構図自体は残ります。

これが、「証明を持ち回る」ということ です。

渡さないと、どうなるか

タロウくん：
・・・h を渡さずに書くと、どうなりますか。

専任講師：
試してみます。

＜Agda のコード＞

{-# OPTIONS --without-K #-}
module CARRY2 where
open import Agda.Builtin.Equality

useIsSet : (A : Set) → (x y : A) (p q : x ≡ y) → p ≡ q
useIsSet A x y p q = refl

＜Agda の型検査結果＞

$ agda CARRY2.agda

/tmp/ag/CARRY2.agda:6,22-26
p != q of type x ≡ y
when checking that the expression refl has type p ≡ q

弾かれます。

タロウくん：
・・・「p と q は、x ≡ y の要素として等しくない」。

専任講師：
Agda は、p と q が等しいかどうかを知りません。

それを教えるのが h でした。

タロウくん：
・・・だから、渡し続けるしかない。

専任講師：
HoTT を扱う体系では、これが標準の書き方です。

なお、本記事で実機検証したコードの一覧は、本稿末尾の Appendix に掲載しています。

なお、標準の Lean 4 では、この持ち回りをせずに済みます。

その理由は、Arend とは正反対です。
第７部で扱います。

第４部 ── Arend では、型を書いた時点で決まっている

pic_19.jpg

\Set0 と書くだけで済む

専任講師：
同じことを、Arend で書いてみます。

＜Arend のコード＞

\func eqIsProp (A : \Set0) (x y : A) : \Prop => x = y

＜Arend の型検査結果＞

$ java -jar Arend.jar SETP.ard

--- Typechecking \default ---
[ ] src.SETP
--- Done (89ms) ---

通ります。

タロウくん：
・・・何を示しているのですか？

専任講師：
A が \Set0 の型であるとき、x = y という等しさの型が \Prop に属する、ということです。

タロウくん：
・・・\Prop は、命題として扱われる型を分類する宇宙でした。
要素が高々１つの型 です。

専任講師：
つまり、x = y の根拠が高々１本である、ということ です。

タロウくん：
・・・それを、証明せずに主張できている。

専任講師：
\Set0 と書いた時点で、その情報が型に含まれているから です。

pic_20.jpg

\Type0 では、通らない

タロウくん：
・・・\Set0 を \Type0 に変えると、どうなりますか。

専任講師：
試してみます。

＜Arend のコード＞

\func eqIsProp (A : \Type0) (x y : A) : \Prop => x = y

＜Arend の型検査結果＞

$ java -jar Arend.jar SETP2.ard

[ERROR] src.SETP2:1:52: Cannot solve equation \lh <= constant
  In: (=)

弾かれます。

タロウくん：
・・・「\lh <= constant という方程式を解けない」。

専任講師：
\lh は、ホモトピーレベルの径数（パラメータ） です。

A が \Type0 の型だと、そのホモトピーレベルが分かりません。

タロウくん：
・・・だから、x = y が \Prop に入るとは言えない。

専任講師：
そのとおりです。

A の宇宙 x = y は \Prop に属するか
\Set0 属する（型が保証する）
\Type0 分からない（ホモトピーレベルが不明）

pic_21.jpg

Agda と並べてみる

専任講師：
第３部の Agda と比較するために、下表に並べてみます。

Agda（--without-K） Arend
型の宣言 (A : Set) (A : \Set0)
証明の引数 (h : isSet A) なし
次の関数への受け渡し useIsSet A h x y p q なし

タロウくん：
・・・Arendは、Agdaよりも引数がひとつ減っている。

pic_22.jpg

Arend の公式ドキュメントが、この点を述べています。

（原文引用）

This way the universes of h-types behave just like the ordinary ones, but you do not need to carry proofs that a type belongs to a certain homotopy level.

（筆者による日本語訳）

これにより、h-型の宇宙は通常のものと同じように振る舞うが、ある型があるホモトピーレベルに属することの証明を持ち回る必要がない。

出典：Arend features, Arend Documentation

タロウくん：
・・・「h-型の宇宙」というのは。

専任講師：
\Set0 や \1-Type0 のように、ホモトピーレベルを指定した宇宙のことです。

h は homotopy の頭文字です。

タロウくん：
・・・「通常のものと同じように振る舞う」というのは。

専任講師：
\Type0 と同じように使える、ということです。
特別な扱いは要りません。

そのうえで、証明を持ち回らずに済みます。

タロウくん：
・・・では、証明はどこへ行ったのですか。

専任講師：
同じ問いを、2019年8月に発した人がいます。

その問いは、第６部で扱います。その前に、ホモトピーレベルとは何かを見ておきましょう。

注意 ── 証明が不要になったのではありません

専任講師：
ひとつ、正確に述べておくべきことがあります。

「証明を引数として渡さずに済む」のであって、「証明が不要になった」のではありません。

タロウくん：
・・・どう違うのですか。

専任講師：
\Set0 と書いたとき、「A の等しさの根拠は高々１本」という主張は、まだ体系のどこかで支えられています。

それを引数として運ぶ代わりに、宇宙の側が支えている のです。

タロウくん：
・・・消えたのではなく、場所が変わった。

専任講師：
Kraus という研究者が、まさにそこを問いました。第６部で扱います。

なお、\Set0 の等しさの型が \Prop に入る規則については、本稿末尾の コラム欄 （\Set0 の等しさの型が \Prop に入る、という規則について）をご参照ください。

第５部 ── ２つ目の軸 ── ホモトピーレベル

pic_23.jpg

\Set0 の 0 は、何を表しているのか

タロウくん：
先生、\Set0 の Set がホモトピーレベル $0$ を表す、と第２部で伺いました。

そのホモトピーレベルというのが、まだ分かりません。

専任講師：
本連載シリーズの第４回目の記事で論じた内容の振り返りになりますが、ここで改めて解説します。

改めて解説するにあたり、第４回目の記事より正確な説明を目指しますね。

第４回目の記事で述べたこと

専任講師：
第４回目の記事では、「等しさの根拠が何本ありうるか」と説明しました。

その説明は直感的ですが、正確ではありません。

タロウくん：
・・・どこが正確でないのですか。

専任講師：
根拠の本数を数えているのではなく、根拠どうしの等しさが、どこで打ち止めになるか を見ているのです。

正確な定義

専任講師：
Awodey の定義を、もう一度引きます。

（原文引用）

The homotopy level of a type is the height at which the tower of iterated identity types becomes degenerate.

（筆者による日本語訳）

型のホモトピーレベルとは、反復した同一視型の塔が退化する高さである。

出典：Steve Awodey, "A proposition is the (homotopy) type of its proofs", arXiv:1701.02024

タロウくん：
・・・「塔」というのが分かりません。

専任講師：
型 A があるとします。

その要素 x、y について、等しさの型 x = y があります。

タロウくん：
はい。

専任講師：
そして x = y の要素 p、q について、さらに等しさの型 p = q があります。

タロウくん：
・・・等しさの、等しさ。

専任講師：
その上に、p = q の要素どうしの等しさもあります。

どこまでも続きます。この積み上がりを、塔と呼んでいます。

階 型
0 A
1 x = y
2 p = q（p q : x = y）
3 r = s（r s : p = q）
... ...

タロウくん：
・・・「退化する」というのは。

専任講師：
ある階から上で、型の要素が高々１つになることです。

それ以上、新しい構造が出てこなくなります。

タロウくん：
・・・その階が、ホモトピーレベル。

専任講師：
そのとおりです。

各レベルの意味

レベル 名前 どの階で退化するか 例
$-2$ 可縮 0階（A 自身の要素が高々１つ。しかも１つは必ずある） 単位型
$-1$ 命題 0階（A の要素が高々１つ） 「$3$ は奇数である」
$0$ 集合 1階（x = y の要素が高々１つ） Nat、Bool
$1$ 1-型 2階（p = q の要素が高々１つ） 群を集めた型
$\infty$ ── 退化しない 円周

タロウくん：
・・・$-2$ から始まるのですね。

専任講師：
歴史的な事情です。

集合が $0$ になるように番号を振ったため、その下が $-1$ と $-2$ になりました。

Arend では \Prop が $-1$ にあたり、\Set が $0$ にあたります。

タロウくん：
・・・円周は $\infty$ ですか。

専任講師：
本連載シリーズの第５回目の記事で見たとおりです。

円周には loop : base = base という 非自明な ループがあります。

そこから繰り返し合成したループを考えられるため、等しさの構造は集合の場合より豊かになります。

円周がどの有限ホモトピーレベルにも収まらないことは、単に「根拠が２本ある」だけより強い主張です。

ここでは第５回目の記事の結論を使い、詳細は本稿末尾の コラム欄 （「等しさの根拠が高々１本」という比喩は、どこまで正しいか）に譲ります。

なお、ホモトピーレベルの帰納的な定義については、本稿末尾の コラム欄 （ホモトピーレベルの定義を、厳密にいうと）をご参照ください。

また、可縮型と「退化する」の厳密な定義については、本稿末尾の コラム欄 （可縮型と、ホモトピーレベル $-2$ について）をご覧いただけますと幸いです。

２つの軸は、独立している

専任講師：
Awodey は、２つの軸について次のように述べています。

（原文引用）

The stratification of types by homotopy levels gives us a new view of the mathematical universe, which is now seen to be arranged not only into the familiar, one-dimensional hierarchy of size, determined by a system of universes U_0, U_1, U_2, ..., but also into a hierarchy of homotopy levels, which form a second dimension independent of the first.

（筆者による日本語訳）

型をホモトピーレベルで階層化することは、数学的宇宙の新しい見方を与える。それは、宇宙 $U_0, U_1, U_2, \ldots$ の体系によって定まる、おなじみの一次元の大きさの階層だけでなく、ホモトピーレベルの階層にも配置される。それは第一の階層とは独立した第二の次元をなす。

出典：同上

タロウくん：
・・・「第一の次元と独立した第二の次元」。

専任講師：
第２部で見た大きさの階層が、第一の次元です。

それとは別に、もうひとつの並べ方がある、ということ です。

タロウくん：
・・・独立している、というのは？

専任講師：
一方を決めても、もう片方がどうなるのか、影響が及ばないということです。

表にすると、縦と横になります。

第２部で見た表がそれです。

累積性 ── 下の階層は、上にも属する

専任講師：
もうひとつ、確かめておくべき性質があります。

＜Arend のコード＞

\func a : \Set0 => Nat
\func b : \1-Type0 => Nat
\func c : \2-Type0 => Nat
\func d : \Set1 => Nat
\func e : \Type1 => Nat

＜Arend の型検査結果＞

$ java -jar Arend.jar CUM.ard

--- Typechecking \default ---
[ ] src.CUM
--- Done (87ms) ---

タロウくん：
・・・Nat が、５つの宇宙すべてに属している。

専任講師：
累積的（cumulative）とは、下の階層に属する型が、上の階層にも属するという性質です。

大きさについても、ホモトピーレベルについても、Arend は累積的です。

タロウくん：
・・・集合は、1-型でもある。

専任講師：
等しさの根拠が高々１本なら、等しさどうしの等しさも高々１本です。

数学的にも自然な事実です。

タロウくん：
・・・逆は成り立ちませんね。

専任講師：
試してみます。

＜Arend のコード＞

\data S1 | base | loop : base = base
\func f : \Set0 => S1

＜Arend の型検査結果＞

$ java -jar Arend.jar CUM2.ard

[ERROR] src.CUM2:2:20: Type mismatch
  Expected type: \Set0
    Actual type: \hType0
  In: S1

円周は \Set0 に属しません。

タロウくん：
・・・\hType0 というのは。

専任講師：
ホモトピーレベルが定まらない型を表す表記です。 円周がそれにあたります。

なお、累積性と宇宙多相の関係については、本稿末尾のコラム欄（累積性と、宇宙多相の関係）をご参照ください。

宇宙は、Arend 固有の議論なのか

タロウくん：
先生、確かめさせてください。

この宇宙をめぐる議論は、Arend 固有の議論ですか。

宇宙という概念、２つの径数の設定は、Arend 以外の定理証明支援系や関数型言語でもみられるのでしょうか。

また、宇宙という枠組みを使わずに、同じことを別の仕組みで実現している Arend 以外の言語もありますか。

専任講師：
３つに分けて答えます。

# 問い 答え
① 宇宙という概念は Arend 固有か 違います。広く使われています
② ２つの径数は Arend 固有か そこが、Arend の特徴です
③ 宇宙を使わない実現方法はあるか あります。標準の HoTT がそうです

①宇宙という概念は、Arend 固有ではありません

専任講師：
Rocq／Coq、Agda、Lean。いずれも宇宙の階層を持ちます。

（原文引用）

Agda's type system includes an infinite hierarchy of universes Setᵢ : Setᵢ₊₁. This hierarchy enables quantification over arbitrary types without running into the inconsistency that follows from Set : Set.

（筆者による日本語訳）

Agda の型体系は、無限の宇宙の階層 $\mathrm{Set}i : \mathrm{Set}{i+1}$ を含む。この階層により、Set : Set から生じる矛盾に陥ることなく、任意の型について量化できる。

出典：Universe Levels, Agda Documentation

タロウくん：
・・・「Set : Set から生じる矛盾」。第２部で見た話ですね。

専任講師：
どの言語も、同じ問題に同じ形で答えています。

Haskell はどうか

タロウくん：
Haskell には、この階層がないのですか。

専任講師：
本記事の第１部で、* の型を問う手段がないと述べました。

しかし正確には、Haskell には階層がないのではありません。

＜Haskell のコード＞

{-# LANGUAGE PolyKinds #-}
import Data.Kind (Type)

type T = (Type :: Type)

main :: IO ()
main = putStrLn "Type :: Type"

＜Haskell の実行結果＞

$ runghc K2.hs

Type :: Type

タロウくん：
・・・通りました。Type の型が Type である。

専任講師：
自分自身を、自分自身に入れています。

タロウくん：
・・・第２部で、それをすると体系が壊れると伺いました。

専任講師：
これをそのまま無矛盾な論理体系として読むことはできません。
Haskell は、論理として使う言語ではありません 。

プログラムを書く言語という位置づけである限り、プログラムを記述するという目的を達成する限りは、それで困らない のです。

Haskell の型体系は、依存型を用いて数学の証明そのものを内部化し、無矛盾な論理体系として使うことを主目的にはしていないから です。

ただ、 Haskell でも、型レベル計算や型安全な設計を幅広く行うことは可能 です。

なお、Type :: Type がプログラミング言語では使えて論理体系では問題になる理由については、本稿末尾の コラム欄 （Type :: Type は、なぜプログラム言語では使えて、論理体系では問題になるのか）をご参照ください。

目的 階層
Haskell プログラムを書く 不要（Type :: Type を許す）
定理証明支援系 数学の証明を検証する 必要（矛盾を避けるため）

なお、Type :: Type が矛盾する理由については、本稿末尾の コラム欄 （Type :: Type が矛盾する理由を、厳密にいうと）をご参照ください。

②２つの径数は、Arend の特徴です

専任講師：
宇宙の階層は、どの言語も持っています。

しかし、その階層に何を径数として持たせるかは、言語によって違います。

処理系 宇宙の径数
Rocq／Coq 大きさ（Type0, Type1, ...）。加えて Prop
Agda 大きさ（Set0, Set1, ...）。加えて Setω
Lean 4 大きさ（Type 0, Type 1, ...）。加えて Prop
Arend 大きさとホモトピーレベルの２つ

なお、Agda の Setω については、本稿末尾のコラム欄（Agda の Setω について）をご参照ください。Lean の Sort については、本稿末尾のコラム欄（Lean の Sort について）をご参照ください。

タロウくん：
・・・他の言語にも Prop はあるのですね。

専任講師：
あります。

ただし、その目的は、論理と計算を分けるためです。
ホモトピーレベルの階層ではない のです。

\Prop の位置づけ
Rocq／Coq、Lean 4 単独の宇宙。論理を計算から分けるため
Arend ホモトピーレベル $-1$ の宇宙。階層の一員

タロウくん：
・・・宇宙の機能は、処理系ごとに大きく違うのですね。

専任講師：
研究者が、次のように述べています。

（原文引用）

At this point, there is a veritable zoo of universe features in existing implementations.

（筆者による日本語訳）

現時点で、既存の実装における宇宙の機能は、まさに動物園の様相を呈している。

出典："Generalized Universe Hierarchies and First-Class Universe Levels", arXiv:2103.00223

タロウくん：
・・・動物園。

専任講師：
Arend は、そこにホモトピーレベルという軸を足しました。

③宇宙を使わない実現方法があります

専任講師：
３つ目の問いに答えます。

標準のホモトピー型理論では、宇宙にホモトピーレベルの軸を足しません。

タロウくん：
・・・では、どうするのですか。

専任講師：
型と、その性質の証明を、組にします。

$$\mathrm{hProp} := \sum_{X : \mathcal{U}} \mathrm{isProp}(X)$$

タロウくん：
・・・$\Sigma$ 型ですね。本連載シリーズの第４回目の記事で扱いました。

専任講師：
過去の記事で論じた内容の振り返りになりますが、ここで改めて解説します。

$\Sigma$ 型とは、組の型です。
第１成分の値によって、第２成分の型が変わります。

ここでは「型 $X$ と、$X$ が命題であることの証明」を、ひとつにまとめています。

タロウくん：
・・・証明を、型と一緒に持ち歩いている。

専任講師：
本記事の第３部で見た「証明を持ち回る」の、別の形 です。

Arend でも、この形は作ることができます。

＜Arend のコード＞

\func Set-to-SetInType (A : \Set0) : \Sigma (A : \Type0) (isSet A)
  => (A, \lam x y => prop-isProp)

＜Arend の型検査結果＞

$ java -Xmx4g -jar Arend.jar -L libs -l arend-lib src/SETSIGMA.ard

--- Done (163ms) ---

\Set0 の型から、「型と isSet の証明の組」を作れます。

タロウくん：
・・・証明を書いていませんね。

専任講師：
prop-isProp は、arend-lib の補題です。\Set0 なら、それで済みます。

この方法の代償

専任講師：
$\Sigma$ 型の方法には、代償があります。

（原文引用）

However, Prop_{U_0} is not 'small', since it is not a type in U_0, but it lives in a higher universe. This is compulsory to keep HoTT predicative.

（筆者による日本語訳）

しかし $\mathrm{Prop}_{\mathcal{U}_0}$ は「小さく」ない。それは $\mathcal{U}_0$ の型ではなく、より高い宇宙に住むからである。これは HoTT を可述的に保つために必要である。

出典："The Compatibility of the Minimalist Foundation with Homotopy Type Theory", arXiv:2207.03802

タロウくん：
・・・組にすると、ひとつ上の宇宙へ行ってしまう。

専任講師：
ここでの $\Sigma (A : \mathcal{U}_0)., \mathrm{isSet}(A)$ は、量化範囲に $\mathcal{U}_0$ 自身が現れるため、$\mathcal{U}_0$ より上に置かれます。

「$\mathcal{U}_0$ の命題を集めたもの」が、$\mathcal{U}_0$ に入らないのです。

タロウくん：
・・・Arend の \Prop は、どうでしたか。

専任講師：
非可述的でした。上の階層へ上がりません。

タロウくん：
・・・そこが違う。

pic_24.jpg

３つの方式を比較する

方式 「この型は集合である」という証明を、どこに置くか 代償
Agda で証明を引数に取る 関数の引数 関数から関数へ渡し続ける
標準の HoTT で $\Sigma$ 型にする 型と組にする ひとつ上の宇宙へ上がる
Arend で宇宙に軸を足す 宇宙そのもの 宇宙の仕様が複雑になる

タロウくん：
・・・どれも、同じ問題に答えている。

専任講師：
「この型は集合である」という証明の置き場所が違うだけ です。

pic_25.jpg

本連載シリーズの第４回目の記事で、代数構造の階層を「どこで支えるか」という論点 を扱いました。

それと同じ構図 です。

なお、\Set n と $\Sigma$ 型の関係については、本稿末尾の コラム欄 （\Set n と $\Sigma$ 型は、同値だが同型ではありません）をご参照ください。

第６部 ── では、証明はどこへ行ったのか

pic_26.jpg

開発者への問い

タロウくん：
先生、第４部で「証明はどこへ行ったのか」という問いが残っていました。

専任講師：
同じ問いを、2019年8月に発した人がいます。

Arend が公開された直後、ホモトピー型理論の研究者である Nicolai Kraus氏 が、Arendを開発したValery Isaev氏 に対して、ある質問をぶつけています。

（原文引用）

Exciting and impressive! Many of Arend's features sound very useful! I find the universes most interesting, but I don't understand how exactly they work. From your site, I learned: * A universe in Arend has two parameters, for size and for homotopy level. * Universes are cumulative in both parameters. Is type-checking still decidable?

（筆者による日本語訳）

胸が躍りますし、感銘を受けました。Arend の機能の多くは、たいへん有用に思えます。
私は宇宙が最も興味深いと思いますが、それがどう働くのか正確には理解できていません。

あなたのサイトから、次のことを学びました。

Arend の宇宙は、大きさとホモトピーレベルという２つの径数を持つこと。宇宙は、その両方の径数について累積的であること。

型検査は、まだ決定可能なのでしょうか。

出典：
Nicolai Kraus, "Re: [HoTT] New theorem prover Arend is released", Homotopy Type Theory メーリングリスト, 2019年8月7日

タロウくん：
・・・「型検査は、まだ決定可能なのでしょうか」というのが分かりません。

専任講師：
「決定可能」とは、必ず有限時間で答えが返ってくる、ということです。

型検査器が、答えを返さないまま動き続けることがあれば、道具として使えません。

タロウくん：
・・・止まらなくなる恐れがある、と問うている。

専任講師：
Kraus は、具体的な例を挙げています。

（原文引用）

Say, we have this judgment: (1) A : \3-Type 1 We have (2) A : \4-Type 1 by cumulativity, but it shouldn't be decidable whether we also have (3) A : \2-Type 1. In book-HoTT, only (1) would type-check, since A would be a pair of a type and a proof of its homotopy level (i.e. you can only get (2,3) by changing the proof).

（筆者による日本語訳）

たとえば、次の型付けがあるとします。(1) A : \3-Type 1。累積性により (2) A : \4-Type 1 も成り立ちます。しかし (3) A : \2-Type 1 も成り立つかどうかは、決定可能であるべきではありません。HoTT Book の体系では、(1) だけが型検査を通ります。そこでは A が「型と、そのホモトピーレベルの証明の組」だからです。つまり、(2) や (3) を得るには、証明のほうを変えるしかありません。

出典：同上

タロウくん：
・・・「型と証明の組」。第５部で見た $\Sigma$ 型ですね。

専任講師：
そのとおりです。

HoTT Book の体系では、A が3-型であることは、証明を組にして持ち歩くことで表されます。

タロウくん：
・・・だから、(2) や (3) を得るには証明を変えるしかない。

専任講師：
Arend では、A : \3-Type 1 と宣言するだけです。証明を組にしていません。

Kraus は、そこを問うています。

タロウくん：
・・・「では、A が実は2-型かどうかを、どうやって判定するのか」と。

専任講師：
判定しようとすると、A と同値な型を探し回ることになります。候補は無限にあります。

探し終わる保証がありません。

開発者の回答

専任講師：
Isaev は、翌日に答えています。

（原文引用）

You can say that they are hidden in the background, but I prefer to think about this in a different way. I think about \Set0 as a strict subtype of \Type0. In comparison, the type \Sigma (A : \Type0) (isSet A) is only homotopically embeds into \Type0.

（筆者による日本語訳）

背後に隠れていると言うこともできますが、私は別の見方を好みます。私は \Set0 を \Type0 の厳密な部分型として考えています。それに比べて、型 \Sigma (A : \Type0) (isSet A) は、\Type0 へホモトピー的に埋め込まれるだけです。

出典：Valery Isaev, "Re: [HoTT] New theorem prover Arend is released", Homotopy Type Theory メーリングリスト, 2019年8月8日

タロウくん：
・・・「厳密な部分型」というのが分かりません。

専任講師：
本連載シリーズの第４回目の記事で、包摂的部分型付けを扱いました。

過去の記事で論じた内容の振り返りになりますが、ここで改めて解説します。

群はモノイドの条件をすべて満たすので、群の値をそのままモノイドとして渡せる、という話でした。

タロウくん：
・・・それと同じ形ですか。

専任講師：
Isaev氏 は、\Set0 と \Type0 の関係をそう捉えている、と述べています。

\Set0 の型は、そのまま \Type0 の型として使える。変換は要らない。

タロウくん：
・・・なるほど。たしかに、そのように述べていますね。

専任講師：
ここは、正確に読む必要があります。
Isaev は、「私はそう考えることを好む」と言っています。

定理として証明されたことを述べているのではありません。

タロウくん：
・・・「ホモトピー的に埋め込まれるだけ」というのは？

専任講師：
$\Sigma$ 型のほうは、\Type0 の一部ではありません。別の型です。

\Type0 へ写す対応はありますが、\Type0 の中に入っているわけではないのです。

\Type0 との関係
\Set0 **厳密な部分型。**そのまま使える
\Sigma (A : \Type0) (isSet A) **別の型。**写す対応があるだけ

決定可能性への答え

専任講師：
そして Isaev は、Kraus の決定可能性の問いに、直接答えています。

（原文引用）

It is equivalent to \Set0, but not isomorphic to it. In particular, this means that every type in \Set0 satisfies isSet and every type in \Type0 which satisfies isSet is equivalent to some type in \Set0, but not necessarily belongs to \Set0 itself. So, if we have (1), we also have (2) and we do not have (3). It may be true that A is a 2-type, which means that there is a type A' : \2-Type 1 equivalent to A, but A itself does not belong to \2-Type 1.

（筆者による日本語訳）

それは \Set0 と同値ですが、同型ではありません。とくにこれは、次のことを意味します。\Set0 のすべての型は isSet を満たします。そして \Type0 のうち isSet を満たすすべての型は、\Set0 のある型と同値です。しかし、それ自身が \Set0 に属するとは限りません。したがって、(1) が成り立つなら (2) も成り立ち、(3) は成り立ちません。A が2-型であることは真かもしれません。それは A と同値な型 A' : \2-Type 1 が存在するという意味です。しかし A 自身は \2-Type 1 に属しません。

出典：同上

タロウくん：
・・・(1) があれば (2) はあるが、(3) はない。

専任講師：
A を \3-Type 1 として宣言したなら、A は \4-Type 1 にも属します。
累積的だからです。

しかし、\2-Type 1 には属しません。

タロウくん：
・・・実は2-型なのに、ですか？

専任講師：
A と同値な型 A' が \2-Type 1 にあるかもしれません。

けれど A 自身は、そこに属していません。

タロウくん：
・・・「属する」と「同値な型がある」は、別のこと。

専任講師：
そこが、型検査を決定可能に保つ仕組みです。

意味 判定
A : \Set0 A が \Set0 に属する 宣言を見れば分かる
A は isSet を満たす A と同値な型が \Set0 にある 別の問い

**「A が \Set0 に属するかどうか」は、A の宣言を見れば分かります。

A と同値な型が \Set0 にあるかどうかを、無限にある候補のなかから探し回る必要がありません。**

なお、\Set0 と $\Sigma$ 型が「同値だが同型ではない」ことの厳密な整理については、本稿末尾の コラム欄 （\Set0 と \Sigma (A : \Type0) (isSet A) は、なぜ「同値だが同型ではない」のか）をご参照ください。

タロウくん：
・・・だから、決定可能なまま保たれる。

専任講師：
証明は、消えたのではありません。

「属する」という形で、宣言のなかに固定されたのです。

pic_27.jpg

証明を、一度だけ渡す ── \use \level

タロウくん：
・・・では、isSet を満たす型を \Set0 に入れたいときは、どうするのですか。

専任講師：
Isaev が、その方法を述べています。

（原文引用）

In the actual implementation, you can do this using \use \level construction. If you can prove that some \data or \record satisfies isSet (or, more generally, that it is an n-type), then you can put this proof in \use \level function corresponding to this definition and it will be put in the corresponding universe.

（筆者による日本語訳）

実際の実装では、\use \level という構文でこれを行えます。ある \data や \record が isSet を満たすことを（より一般には、それが n-型であることを）証明できるなら、その証明を、その定義に対応する \use \level 関数に置くことができます。すると、その定義は対応する宇宙に置かれます。

出典：
同上

タロウくん：
・・・証明を、一度だけ 渡すのですね。

専任講師：
「証明を渡さずに済む」のではありません。

一度だけ渡して、型をその宇宙へ置く。そうすると、それ以降は、もう証明を渡さずに使うことができるようになります。

タロウくん：
・・・Agda では、使うたびに渡していました。

専任講師：
証明を渡す回数が、両言語では違うのです。

pic_28.jpg

実機で確かめてみましょう。

＜Arend のコード＞

\import Paths
\import Logic

\data Dec (A : \Prop)
  | yes A
  | no (Not A)

\data DecP (A : \Prop)
  | yesP A
  | noP (Not A)
  \where {
    \use \level levelProp {A : \Prop} (d1 d2 : DecP A) : d1 = d2 \elim d1, d2
      | yesP a1, yesP a2 => pmap yesP (prop-isProp a1 a2)
      | yesP a, noP na => absurd (na a)
      | noP na, yesP a => absurd (na a)
      | noP na1, noP na2 => pmap noP (prop-isProp na1 na2)
  }

\func checkSet (A : \Prop) : \Set0 => Dec A
\func checkProp (A : \Prop) : \Prop => DecP A

＜Arend の型検査結果＞

$ java -Xmx4g -jar Arend.jar -L libs -l arend-lib src/USELEVEL.ard

[ ] src.USELEVEL
--- Done (121ms) ---

タロウくん：
・・・Dec と DecP は、中身が同じですね。

専任講師：
違うのは、\where の中です。

DecP には \use \level levelProp があります。
Dec にはありません。

タロウくん：
・・・\use \level levelProp の行が分かりません。

専任講師：
「DecP A のどの２つの要素も等しい」ことの証明です。

タロウくん：
・・・４つの場合に分けています。

専任講師：
DecP A の要素は yesP a か noP na のどちらかです。
２つの要素の組み合わせは、４通りあります。

組み合わせ 証明
yesP a1 と yesP a2 a1 と a2 は A : \Prop の要素なので等しい
yesP a と noP na na a で矛盾を導く
noP na と yesP a 同上
noP na1 と noP na2 Not A は命題なので等しい

タロウくん：
・・・prop-isProp というのは？

専任講師：
「\Prop に属する型の要素は、どの２つも等しい」という補題です。
arend-lib に用意されています。

タロウくん：
・・・証明を \where に置くと、DecP が \Prop に置かれる。

専任講師：
checkProp が通っていることが、その証拠です。

そして、\use \level を付けずに \Prop へ置こうとすると、弾かれます。

＜Arend のコード＞

\func checkProp (A : \Prop) : \Prop => Dec A

＜Arend の型検査結果＞

[ERROR] src.USELEVEL2:5:40: Type mismatch
  Expected type: \Prop
    Actual type: \Set0
  In: Dec A

タロウくん：
・・・Dec は \Set0 に置かれたままだから。

専任講師：
証明を一度だけ渡して、型を \Prop へ移す。それが \use \level です。

なお、\use \level が自動証明ではなく分類情報の登録であることについては、本稿末尾のコラム欄（\use \level がしているのは、自動証明ではなく「分類情報の登録」である）をご参照ください。

なお、\use \level の使い方については、本稿末尾のコラム欄（\use \level の使い方）をご参照ください。

命題のリサイジング

タロウくん：
先生、Kraus はもうひとつ問いを重ねていました。

専任講師：
\Prop が非可述的であることから、命題のリサイジングが成り立つのではないか、と。

タロウくん：
・・・「命題のリサイジング」というのが分かりません。

専任講師：
第２部で、「すべての型について」と量化すると、ひとつ上へ上がることを見ました。

命題についても、同じことが起きえます。

「\Type1 のすべての命題について〜」という主張は、\Type2 へ上がります。

タロウくん：
・・・命題なのに、大きさが増える。

専任講師：
リサイジングは、それを下へ戻す原理です。

「命題であるなら、大きさに関係なく、最下層の宇宙に置いてよい」と述べます。

タロウくん：
・・・Arend では。

専任講師：
成り立ちます。開発者が、メーリングリストで明言しています。

（原文引用）

Yes, propositional resizing holds. \Prop classifies all subobjects.

（筆者による日本語訳）

はい、命題のリサイジングは成り立ちます。\Prop は、すべての部分対象を分類します。

出典：
Valery Isaev, "Re: [HoTT] New theorem prover Arend is released", Homotopy Type Theory メーリングリスト, 2019年8月

タロウくん：
・・・非可述的だから、上がらない。

専任講師：
そのとおりです。
\Prop が非可述的であることの、ひとつの帰結です。

なお、「部分対象を分類する」の意味については、本稿末尾の コラム欄 （命題のリサイジングと、部分対象分類子）をご参照ください。

HoTT Book での扱いについては、本稿末尾の コラム欄 （リサイジングは、HoTT Book では公理である）をお読みいただけますと幸いです。

pic_29.jpg

\Set0 自身は、集合ではありません

タロウくん：
先生、ひとつ気になることがあります。

\Set0 は集合とみなせる型を受け入れる宇宙でした。
では、\Set0 自身は集合なのですか？

専任講師：
集合ではありません。

実機で確かめてみましょう。

＜Arend のコード＞

\import Paths
\import Equiv
\import Equiv.Univalence
\import HLevel
\import Logic

\data Bool | true | false

\func not (b : Bool) : Bool | true => false | false => true
\func not-not (b : Bool) : not (not b) = b | true => idp | false => idp
\func true/=false (p : true = false) : Empty => absurd (transport T p ())
  \where \func T (b : Bool) : \Type | true => \Sigma | false => Empty

\func notQEquiv : QEquiv {Bool} {Bool}
  => \new QEquiv { | f => not | ret => not | ret_f => not-not | f_sec => not-not }

\func Set-isNotSet (p : isProp (Bool = {\Set0} Bool)) : Empty =>
  \let | idp=not => p idp (QEquiv-to-= notQEquiv)
       | id=not : (\lam x => x) = not => pmap (transport (\lam X => X)) idp=not
  \in true/=false (path (\lam i => (id=not @ i) true))

＜Arend の型検査結果＞

$ java -Xmx4g -jar Arend.jar -L libs -l arend-lib src/SETNOTSET.ard

[ ] src.SETNOTSET
--- Done (123ms) ---

タロウくん：
・・・何を示しているのですか。

専任講師：
「Bool = Bool の根拠が１本しかない」と仮定して、矛盾を導いています。

タロウくん：
・・・本連載シリーズの第１回目の記事で、根拠が２本あると見ました。

専任講師：
idp と、not による対応です。

この２つが等しいと仮定すると、恒等写像と not が等しくなります。

タロウくん：
・・・すると true と false が等しくなってしまう。

専任講師：
矛盾です。

したがって、Bool = Bool は命題ではありません。

タロウくん：
・・・\Set0 の中に、等しさの根拠が２本ある型がある。

専任講師：
\Set0 そのものが、集合ではないということです。

本連載シリーズの第４回目の記事で扱えなかった「宇宙自身はどのレベルに入るのか」という問いを受けて、実機で確認できた結果です。

なお、宇宙自身のホモトピーレベル については、本稿末尾の コラム欄 （宇宙自身は、どのホモトピーレベルに入るのか）をご参照ください。

第７部 ── Lean 4 も持ち回らない。しかし理由が正反対

pic_30.jpg

Arend の \Prop は、証明無関係ではありません

専任講師：
本連載シリーズの第５回目の記事で、Lean 4 の証明無関係を扱いました。

過去の記事で論じた内容の振り返りになりますが、改めて解説します。

証明無関係 とは、同じ主張についての証明は、すべて等しいとみなす という規則です。

タロウくん：
・・・Lean では rfl だけで、２つの証明が等しいと示せました。

専任講師：
Arend の \Prop も同じか、と思われるかもしれませんが、同じではありません。

（原文引用）

The universe \Prop is not proof irrelevant, but some elements of propositions are computationally equal.

（筆者による日本語訳）

宇宙 \Prop は証明無関係ではない。ただし、命題の要素のいくつかは計算的に等しい。

出典：Universes, Arend Documentation

タロウくん：
・・・「証明無関係ではない」。

専任講師：
実機で確かめます。

＜Arend のコード＞

\func try (A : \Prop) (x y : A) : x = y => idp

＜Arend の型検査結果＞

$ java -jar Arend.jar PROPIR.ard

[ERROR] src.PROPIR:10:44: Expressions are not equal
  Left:  x
  Right: y
  In: idp

弾かれます。

タロウくん：
・・・Lean では rfl で通り、Arend では通らない。

専任講師：
Arend では、\Prop の要素どうしが等しいことを、idp だけでは示すことができないのです。

示すためには、prop-isProp のような補題を使うことになります。

タロウくん：
・・・引用文には、「いくつかは計算的に等しい」 とありますが。

専任講師：
すべてではない、ということ です。

構成子へ評価されない要素については、計算的に等しいとみなされます 。

それ以外は、証明が要ります。

なお、Arend の \Prop が証明無関係でない理由については、本稿末尾の コラム欄 （Arend の \Prop は、なぜ証明無関係でないのか）をご参照ください。

UIP を認めると、持ち回らずに済みます

専任講師：
第３部で、UIP を定義しました。

すべての型について isSet を認める原理 です。

UIP を認める処理系では、isSet の証明を持ち回る必要がありません。
はじめから、すべての型が集合だから です。

タロウくん：
・・・Lean 4 が、そうでしたね。

Lean 4 では、持ち回らずに済む

専任講師：
・・・ところで、筆者は当初、Lean でも証明を持ち回ると考えていました。

タロウくん：
え？　違うのですか。

専任講師：
実機で確かめたところ、違いました。

＜Lean 4 のコード＞

theorem allTypesAreSets (α : Type) (x y : α) (p q : x = y) : p = q := rfl

＜Lean 4 の型検査結果＞

$ lean UIP.lean

何も出力されず、通ります。

タロウくん：
・・・すべての型が、集合になっている。

専任講師：
UIP が成り立つからです。

したがって、isSet の証明を持ち回る必要がありません。はじめから、すべての型が集合です。

タロウくん：
・・・Agda では弾かれたのに。

専任講師：
同じコードを Agda で書くと、弾かれました。

＜Agda のコード＞

{-# OPTIONS --without-K #-}
allTypesAreSets : (A : Set) (x y : A) (p q : x ≡ y) → p ≡ q
allTypesAreSets A x y p q = refl

＜Agda の型検査結果＞

$ agda UIP.agda

/tmp/ag/UIP.agda:7,29-33
p != q of type x ≡ y
when checking that the expression refl has type p ≡ q

タロウくん：
・・・同じコードなのに、結果が正反対になった。

専任講師：
UIP を認めるかどうかの違い です。

正しい対比

専任講師：
本連載シリーズの第５回目の記事の末尾で、「Agda や Lean では証明を持ち回る」と予告しました。

Lean については、正確ではありませんでした。訂正します。

処理系 isSet の証明を持ち回るか 理由
標準の Lean 4 不要 UIP が成り立つ。すべての型が集合
Agda --without-K 必要 UIP が成り立たない
Rocq／Coq の HoTT ライブラリ 必要 同上
Arend 不要（\Set0 と書く） 宇宙が支える

タロウくん：
・・・Lean 4 も Arend も、持ち回らない。

専任講師：
しかし、理由が正反対です。

持ち回らずに済む理由
Lean 4 UIP を認めて、すべての型を集合にした
Arend 宇宙にホモトピーレベルの軸を足した

タロウくん：
・・・Lean 4 は「区別しないことにした」。

専任講師：
Arend は「区別を型で管理する」。

なお、Lean 4 の「等号の証明を区別しない」が何を意味するかについては、本稿末尾の コラム欄 （Lean 4 の「等号の証明を区別しない」とは、何を意味するのか）をご参照ください。

第５回目の記事とつながる

タロウくん：
・・・Lean 4 が円周を扱えない理由と、同じ性質ですね。

専任講師：
そのとおりです。

回 Lean 4 の証明無関係が、どう働くか
第５回 制約になる。円周を定義できない
第６回 利点になる。isSet を持ち回らずに済む

同じ性質が、片方では制約になり、片方では利点になります。

タロウくん：
・・・ 何を扱いたいかで、評価が変わる。

専任講師：
古典数学を形式化するなら、UIP を認めて困ることはありません。

HoTT を扱うなら、UIP を認められません。そこで、別の仕組みが必要になります。

タロウくん：
・・・それが、Arend の宇宙 だった、ということですね。

なお、Lean 4 の証明無関係と UIP の関係については、本稿末尾の コラム欄 （Lean 4 の証明無関係と UIP の関係）をご参照ください。

上がる・上がらないは、言語によって変わるのか

タロウくん：
先生、ここまで３つのことを見ました。

# 内容
① 型の量化は、ひとつ上へ上がる
② \Prop の量化は、上がらない
③ \Prop : \Prop は成り立たない

これらは、言語によって変わるのですか？

専任講師：
①と③は共通です。②だけが分かれます。

実機で確かめました。

現象 Arend Lean 4 Agda Haskell
①型の量化は上がる 上がる 上がる 上がる 上がらない
②Prop の量化は上がらない 上がらない 上がらない 上がる ──
③Prop : Prop は成り立たない 成り立たない 成り立たない 成り立たない Type :: Type は成り立つ

タロウくん：
・・・Agda だけ、②が違う。

専任講師：
＜Agda のコード＞

{-# OPTIONS --prop #-}
test : (B : Prop) → Prop
test B = (x : Prop) → B

＜Agda の型検査結果＞

$ agda PROPA.agda

Prop₁ != Prop
when checking that the expression (x : Prop) → B has type Prop

Prop₁ へ上がっています。Agda の Prop は可述的です。

タロウくん：
・・・Lean 4 では？

専任講師：
＜Lean 4 のコード＞

def test (B : Prop) : Prop := ∀ (x : Prop), B
#check Prop

＜Lean 4 の出力＞

$ lean PR.lean

Prop : Type

通ります。

Lean 4 の Prop は 非可述的 です。
Prop の型は Type です。

裁量か、理論か

タロウくん：
先生、もうひとつ伺いたいのですが。

言語によって異なるのは、言語設計者が上がる・上がらないを状況別に自由に決められる裁量があるからですか？

それとも、各言語が依拠する型システム理論が異なっていて、どの型システム理論を採用するかによって、各状況で上がる・上がらないが異なるからですか？

専任講師：
後者 です。

どの型システム理論を採用するかによって、各状況で上がる・上がらないかが決まります。

タロウくん：
・・・設計者の裁量ではない、と。

専任講師：
そうです。

上がるか上がらないかは、その言語が採用した型理論の規則によって決まります。

タロウくん：
・・・では、設計者は何も決めていないのですか？

専任講師：
設計者は、どの型理論を採用するか、という場面で、この決定に大きく関与しています。

設計者の裁量は、規則そのものではなく、理論の選択にあります。

処理系 採用する型理論 Prop の量化
Rocq／Coq CIC（帰納的構成の計算） 上がらない
Lean 4 CIC 上がらない
Agda MLTT（マーティン＝レーフ型理論） 上がる

タロウくん：
・・・ CIC を採る言語は上がらず、MLTT を採る言語は上がる。

専任講師：
CIC には、非可述的 な Prop が最初から含まれています。
MLTT には、含まれていません。

タロウくん：
・・・Arend はどちらですか？

専任講師：
MLTT の系譜です。でも、非可述的な \Prop を持ちます。

タロウくん：
・・・組み合わせている。

専任講師：
そこが、Arendの設計者の判断です。

pic_31.jpg

なぜ CIC は上がらず、MLTT は上がるのか

タロウくん：
先生、そもそもの疑問なのですが。

なぜ CIC では上がらず、MLTT では上がるのですか。理論が違うから、というだけでは腑に落ちません。

専任講師：
２つの理論の出発点が違うからです。歴史をたどると、はっきりします。

意外に思われるかもしれませんが、MLTT も最初は上がりませんでした。

タロウくん：
・・・上がらなかった。

専任講師：
1971年、ペール・マーティン＝レーフが最初の型理論を発表しました。

（原文引用）

Martin-Löf's original 1971 theory of types was a very elegant formal system postulating that the type of all types (let us call it Type) was itself an object of type Type, that is the judgement Type : Type was given as an axiom.

（筆者による日本語訳）

マーティン＝レーフの当初の1971年の型の理論は、たいへん優美な形式体系であった。それは、すべての型の型（これを Type と呼ぼう）が、それ自身 Type という型の対象であること、すなわち判断 Type : Type を公理として置いていた。

出典：Gérard Huet, "Extending the Calculus of Constructions with Type:Type", INRIA

タロウくん：
・・・Haskell と同じ形ですね。

専任講師：
翌1972年、ジャン＝イヴ・ジラールが、この体系の矛盾を示しました 。

（原文引用）

Girard showed that Burali-Forti's paradox could be encoded in the system, leading to logical inconsistency.

（筆者による日本語訳）

ジラールは、ブラリ＝フォルティのパラドックスがこの体系に符号化できることを示し、論理的な矛盾へ至ることを明らかにした。

出典：同上

タロウくん：
・・・体系が壊れた。

専任講師：
マーティン＝レーフは、体系を修正しました。

（原文引用）

After Girard showed that the system was inconsistent, Martin-Löf modified the system so that the universe became predicative.

（筆者による日本語訳）

ジラールが体系の矛盾を示したのち、マーティン＝レーフは宇宙が可述的になるよう体系を修正した。

出典："Weyl's Predicative Classical Mathematics as a Logic-Enriched Type Theory", arXiv:0809.2061

タロウくん：
・・・ 矛盾を避けるために、可述的にした。

専任講師：
MLTT の可述性は、この経緯から来ています。

pic_32.jpg

タロウくん：
・・・では、CIC はどこから来たのですか。

専任講師：
別の系譜です。System F という体系が出発点になっています。

ジラール自身が作った体系です。

タロウくん：
・・・同じ人が。

専任講師：
System F では、「すべての型について」という量化そのものが、型を作ります。

そして、その量化した型自身も、 量化の範囲 に含まれます。

タロウくん：
・・・ 自分自身を含んでいる。

専任講師：
非可述的です。
しかも、System F は矛盾しません。

pic_33.jpg

何を許したか 矛盾するか
MLTT 1971年版 Type : Type（型の型が自分自身） する
System F 型についての量化（宇宙は自分自身に入らない） しない

タロウくん：
・・・似ているが、違う。

専任講師：
「すべての型について量化する」ことと、「型の型を自分自身に入れる」ことは、別のこと です。

前者だけなら、矛盾しません。

pic34_rev.jpg

1988年、Thierry Coquand と Gérard Huet により、**System F の考え方を依存型へ拡張した体系が登場しました。

構成の計算 といいます。

そこに 帰納型などを加えた 体系が、CIC につながります。!

タロウくん：
・・・System F の非可述性が、Prop に残った。

MLTT CIC
出発点 構成的数学の基礎づけ System F（型についての量化）
当初の版 Type : Type を許した 型についての量化を許した
矛盾したか した（ジラール、1972年） していない
その後 可述的に修正 非可述性を Prop に残した
いまの Prop 可述的 非可述的

タロウくん：
・・・出発点が違うと、行き着く先も違う。

専任講師：
System F が矛盾しない理由は、本記事では扱いません。証明論の議論になります。

なお、System F と非可述性については、本稿末尾の コラム欄 （System F と非可述性について）をご参照ください。

選択には代償がと伴う

タロウくん：
・・・好きなように組み合わせられるのですか？

専任講師：
組み合わせには制約があります。Rocq／Coq にその実例があります。

Coq には Set という宇宙があります。
古い版では、これが非可述的でした。

（原文引用）

In old versions of Coq, Set was impredicative by default. Later versions make Set predicative to avoid inconsistency with some classical axioms.

（筆者による日本語訳）

Coq の古い版では、Set は既定で非可述的だった。後の版では、いくつかの古典的な公理との矛盾を避けるため、Set を可述的にしている。

出典：Adam Chlipala, "Certified Programming with Dependent Types", Universes and Axioms

タロウくん：
・・・途中で変えたのですか。

専任講師：
変えざるをえませんでした。

（原文引用）

the conjunction of excluded middle and description conflicts with the impredicativity of Set. As a result, nowadays Set is predicative and behaves in CIC as the first level of the hierarchy of universes.

（筆者による日本語訳）

排中律と記述の公理の組み合わせが、Set の非可述性と衝突する。その結果、いまでは Set は可述的であり、CIC において宇宙の階層の最初の段階として振る舞う。

出典：
"Parametricity in an Impredicative Sort", arXiv:1209.6336

タロウくん：
・・・非可述性と古典論理の、どちらかを選ぶことになった。

専任講師：
結果として、Coq では現在、古典的な公理を利用しながら Set を可述的に扱う設計になっています。

設計判断ですが、自由な判断ではありません。「両方は取れない」という制約のなかでの判断です。

層 内容 裁量 例
理論が禁じている Type : Type は矛盾する ない ③はどの処理系も共通
理論の選択で決まる Prop を非可述的にするか 理論を選ぶという形である CIC は非可述的、MLTT は可述的
選択には代償がある 非可述性と古典論理は両立しにくい 制約のなかでの判断 Coq は Set を可述的に変えた

タロウくん：
・・・設計者に裁量はあるが、何を諦めるかを決めることでもある。

専任講師：
本連載シリーズを通じて、その形が繰り返し現れます。

第１回目の記事の予告が、ここで果たされます

タロウくん：
先生、本連載シリーズの第１回目の記事で、「証明を持ち回らずに済むこと」が Arend の３つ目の可能性として挙げられていました。

専任講師：
その中身が、本記事です。

タロウくん：
・・・宇宙にホモトピーレベルの軸を足すことで、\Set0 と書けば済むようになった。

専任講師：
そして、その代わりに宇宙の仕様が複雑になりました。

Kraus が「型検査は決定可能か」と問うたのは、その複雑さゆえです。

連載の背骨 ── 何を手放して、何を得たか

専任講師：
本連載シリーズは、最終回を残すのみになりました。

ここまでの「何を手放して、何を得たか」を、並べます。

回 手放したもの 得たもの
第２回 計算しきる力 仕様の単純さ
第４回 土台の小ささ 階層を組み上げる自由
第５回 ── 高次帰納型の定義の単純さ（第２回の見返り）
第６回 宇宙の仕様の単純さ 証明を持ち回らずに済むこと

タロウくん：
・・・どの判断も、何かを取れば何かを手放している。

専任講師：
そして、その判断の基準は、いつも「形式化の実践」でした。

【本記事執筆者の見解】

以下は、筆者が調べた範囲での判断です。出典のある事実ではありません。

「証明を持ち回らずに済む」ことは、Arend だけの利点ではありません。

標準の Lean 4 も、持ち回らずに済むからです。

ただし、ArendとLean 4とでは、その理由は異なります。

Lean 4 は UIP を認め、すべての型を集合としました。
HoTT で考えていたような高次構造を持つ円周は、そのままでは成立しません。

Arend が力を発揮する状況 は、HoTT を扱いながらも、証明を持ち回らずに済ませたい場面 です。

そのような場面【状況）は、Agda --without-K や Coq の HoTT ライブラリと比べたときに現れます。

そうした場面が、2026年9月現在で、どれだけ広いかは、確認できませんでした。

2026年9月現在、arend-lib の規模は、Lean 4のMathlib よりも小さいです。

本連載シリーズの第４回目の記事で述べた判断を、変える材料は見つかりませんでした。

読者の皆様が、数学の形式化 にご関心をお持ちでしたら、Lean 4 と Mathlib を選ぶのが現実的です。（2026年9月現在の状況を前提とした判断です。今後、状況の変化によって、この判断を修正すべきときが訪れる可能性は否定できません）

次回の予告

【Arend Theorem Prover 連載（７回目・最終回）】では、AI による数学証明の機械検証を扱います。

ここまで、初回記事から６回の記事にわたり、Arendの型理論について、多少掘り下げて見てきました。

では、Arendの型理論は、数学研究や産業界の実務領域において、どのように利活用されているのでしょうか。

近年、数学の証明を、大規模簿言語モデル（LLM）を搭載したAI Agentの力を借りて検証する動きが加速しています。

こうした取り組みの多くは、定理証明支援系として、Lean 4を採用しています。

（ 関連記事 ）

こうした文脈で、AI Agentによる数学定理の証明・反証を行う数々の国際プロジェクトにおける Aren の立ち位置　に関心を持たれる方もおられるのではないでしょうか。

論点となるのは、例えば以下のようなものです。

  • Arend の CLI と、AI（LLM、AI Agent） との連携のあり方と実践事例。
  • Arend と Lean 4 との目的・文脈別の役割分担。

本連載シリーズの最終回となる次回の記事では、こうしたテーマを主題として取り上げます。

連載リンク

関連記事

Appendix ── 本記事で実機検証したコード

本記事の本文には、論旨に必要なコードだけを載せました。

ここには、筆者が実機で動かして確認したコードをすべて載せ、再現できるようにします。

A-1. 検証環境

処理系 バージョン 導入方法
Arend 1.10（Java 21） 公式サイトから Arend.jar を取得
arend-lib 1.10 GitHub から arend-lib.zip を取得
GHC 9.4.7 apt-get install ghc
Agda 2.6.3 apt-get install agda
Lean 4.33.1 GitHub から lean-4.33.1-linux.tar.zst を取得

OS：Ubuntu 24.04

注意：Agda の実行には LC_ALL=C.UTF-8 の設定が必要でした。

注意：arend-lib の読み込みには、test ディレクトリを作成し、java -Xmx4g でメモリを増やす必要がありました。

A-2. Arend で確認したこと

# ファイル 確認したこと 出力
① PRED1.ard \Pi (A : \Type0) -> \Type0 が \1-Type1 に属する Done (88ms)
② PRED2.ard \Pi (x : \Prop) -> B が \Prop に属する Done (77ms)
③ PRED3.ard \Prop : \Prop が弾かれる。\Prop の型は \Set0 Actual type: \Set0
④ UU3.ard \Type0 の型は \Type1 Actual type: \Type1
⑤ PI3.ard \Pi (A : \Type0) -> Nat が \Set1 に属する Actual type: \Set1
⑥ SETP.ard \Set0 の等しさの型が \Prop に属する Done (89ms)
⑦ SETP2.ard \Type0 では、それが成り立たない Cannot solve equation \lh <= constant
⑧ CUM.ard Nat が \Set0、\1-Type0、\2-Type0、\Set1、\Type1 に属する Done (87ms)
⑨ CUM2.ard 円周が \Set0 に属さない Actual type: \hType0
⑩ PROPIR.ard \Prop の要素が idp で等しいとは示せない Expressions are not equal
⑪ USELEVEL.ard \use \level で DecP を \Prop に置く Done (121ms)
⑫ USELEVEL2.ard \use \level なしでは \Prop に置けない Actual type: \Set0
⑬ SETNOTSET.ard \Set0 自身は集合でない Done (123ms)
⑭ SETSIGMA.ard \Set0 から $\Sigma$ 型を作れる Done (163ms)

⑪〜⑭は arend-lib を必要とします。

A-3. Lean 4 で確認したこと

# ファイル 確認したこと 出力
① UIP.lean UIP が成り立つ。p q : x = y から p = q を rfl で示せる 通る
② PR.lean ∀ (x : Prop), B が Prop に属する 通る
③ PR.lean Prop の型は Type Prop : Type

A-4. Agda で確認したこと

# ファイル 確認したこと 出力
① UIP.agda --without-K で UIP が成り立たない p != q of type x ≡ y
② CARRY.agda isSet の証明を引数として持ち回るコードが通る Checking CARRY
③ CARRY2.agda 証明を渡さないと弾かれる p != q of type x ≡ y
④ PROPA.agda --prop で Prop の量化が Prop₁ へ上がる Prop₁ != Prop

A-5. Haskell で確認したこと

# ファイル 確認したこと 出力
① K2.hs Type :: Type が通る Type :: Type

A-6. 検証できなかったこと

# 内容 理由 代わりに何に基づいたか
① Coq の -impredicative-set Coq を導入していない Rocq 公式マニュアルの記載
② Idris 2 の QTT Idris を導入していない 論文の記載

A-7. 再現の手順

Arend

1. https://arend-lang.github.io/download から Arend.jar を取得する
2. 作業ディレクトリに arend.yaml を置く（sourcesDir: src）
3. src/ に .ard ファイルを置く
4. java -jar Arend.jar src/ファイル名.ard

arend-lib を使う場合

1. https://github.com/JetBrains/arend-lib/releases から arend-lib.zip を取得する
2. libs/arend-lib/ に展開する
3. libs/arend-lib/test/ を空ディレクトリとして作成する
4. arend.yaml に dependencies: [arend-lib] を追加する
5. java -Xmx4g -jar Arend.jar -L libs -l arend-lib src/ファイル名.ard

Lean 4

1. https://github.com/leanprover/lean4/releases から取得する
2. lean ファイル名.lean

Agda

1. apt-get install agda
2. LC_ALL=C.UTF-8 agda ファイル名.agda

Haskell

1. apt-get install ghc
2. runghc ファイル名.hs

【発展篇】中上級者向けのコラム

この記事は分かりやすい入門者向けの記事を心がけましたので、厳密な議論を犠牲にした部分があります。

以下、中上級者向けに補足説明すべき箇所を、本文の部ごとに分けて述べます。

第１部・第２部について

📌 中上級者向けコラム：厳密にいうと ── `Type :: Type` は、なぜプログラム言語では使えて、論理体系では問題になるのか

ここからは本文の説明を否定するためではなく、その説明がどの範囲で有効かを中上級者向けに補うための注記です。初読では読み飛ばして構いません。

本文では、Haskell で Type :: Type が通ることを示し、「論理としては壊れる」と述べました。

この説明の射程を限定します。

Haskell でも、型レベル計算、型レベル DSL、型安全な埋め込み言語などは幅広く記述できます。 したがって、「Haskell は型のレベルで数学を扱えない」という意味ではありません。

ここでいう違いは、Haskell の通常の型体系が、一貫した依存型論として数学の証明を内部化することを目的としていない、という点です。

また、Type :: Type を許すことは、Haskell のプログラムとしての実用性を損なうという意味でもありません。問題は、それを Curry–Howard 対応により、そのまま無矛盾な論理体系として読むことができない点にあります。

Curry–Howard 対応とは、 「型を命題、プログラムを証明とみなす」対応 のことです。

この対応を通じて型体系を論理体系として読むとき、Type :: Type があると、あらゆる命題が証明できてしまいます。

さらに、Haskell を単純な依存型理論と同一視できない理由は、複数あります。

# 理由
① 非停止計算や undefined が、あらゆる型の要素として存在する
② 型族・型クラス・GHC 拡張を含む型体系は、純粋な依存型理論とは異なる
③ 評価戦略が遅延であり、証明論的な正規化とは対応しない

したがって、「Haskell が劣る」ということを指摘しているのではありません。

*プログラミング言語としての型体系と、証明検証を目的とした型理論とは、設計目標が違う ことを指摘しようとした、というのが、本記事執筆者の意図です。

本文中の「論理としては壊れます。Haskell は、論理として使う言語ではありません」という記述は、この意味で書かれたものとして、お読みください。

📌 中上級者向けコラム：厳密にいうと ── 非可述的な `\Prop` は、なぜ直ちに `\Prop : \Prop` を意味しないのか

ここからは本文の説明を否定するためではなく、その説明がどの範囲で有効かを中上級者向けに補うための注記です。初読では読み飛ばして構いません。

\Prop が非可述的であるとは、命題を量化範囲に取る $\Pi$ 型が、一定の条件のもとで再び \Prop に置かれる、という宇宙規則のことです。

これは \Prop : \Prop、すなわち \Prop 自身が \Prop の要素であることを意味しません。 実際、本文の型検査結果が示すように、Arend では \Prop : \Set0 です。

主張 成り立つか
\Pi (x : \Prop) -> B が \Prop に属する 成り立つ（非可述性）
\Prop 自身が \Prop に属する 成り立たない（\Prop : \Set0）

「命題全体について量化できること」と、「命題全体を表す宇宙が自分自身に属すること」は別の主張です。

前者は、非可述的な Prop を持つ体系（CIC、Arend）で許されています。

後者は、ジラールのパラドックスにより矛盾を導くため、どの体系でも許されていません。

非可述性を、ラッセル型の自己所属と混同しないことが要点です。

📌 中上級者向け：種と宇宙の違いについて

本文では、Haskell の種 * と Arend の宇宙 \Type0 を、どちらも「型の型」として並べました。

両者は似ていますが、役割が違います。

Haskell の種は、型のレベルでの関数（* -> * など）を分類するためのものです。
種が値に依存することはありません。

Arend の宇宙は、依存型理論における「型を分類するための型」です。
宇宙の階層は、可述性を保つための仕組みでもあります。

Haskell に GHC 拡張を加えると、Type :: Type が通ります。

これは、Haskell が種の階層を持たないことを意味します。

論理として使わない言語では、その階層が不要 だからです。

本文の第１部で「* の型を問う手段がない」と述べたのは、標準の Haskell について述べたものです。

Haskellでも、拡張を有効にすれば問えますが、答えは Type 自身になります。

📌 中上級者向け：宇宙は「型を集めた場所」ではありません

本文では、宇宙を「型を分類するための型」と説明し、「型を集めた場所」という言い方を避けました。

この区別は、型理論と集合論の違いに関わります。

集合論では、「すべての集合の集合」を考えると矛盾が生じます。
型理論の宇宙は、「すべての型の集合」ではありません。

A : \Type0 という判断は、「A は \Type0 に分類される型である」という型付けです。
これは、集合論の帰属関係 $A \in U$ とは別のものです。

そして、\Type0 : \Type1 という判断も、「\Type0 は \Type1 に分類される」という型付けです。

型理論の宇宙が、集合論のグロタンディーク宇宙と似た役割を果たすことは事実です。

しかし、両者は同じ数学的対象ではありません。

本連載シリーズの第５回目の記事のコラムで、この点を扱いました。

📌 中上級者向け：可述性と非可述性を、厳密にいうと

本文では、可述性を「ある対象を定義するとき、その対象自身を含む全体について量化することを許さない」と説明しました。

この語は、一文で定義できる概念ではありません。

歴史的には、ラッセルとポアンカレによる悪循環原理の議論 に由来します。

「全体を前提としてはじめて定義できる対象は、その全体の一員であってはならない」という原理です。

型理論では、この原理が型の形成規則と量化規則の性質として現れます。
$\Pi$ 型の宇宙レベルが定義域と値域の最大値で決まる、という規則が、可述性を保っています。

非可述的な体系が、必ず矛盾するわけではありません。
System F と CIC は非可述的ですが、無矛盾です。

矛盾するのは、Type : Type のように宇宙を自分自身に入れる場合です。
これは、ジラールのパラドックス として知られています。

「型についての量化を許す」ことと「宇宙を自分自身に入れる」ことは、別のことです。
本文の第７部で扱ったとおりです。

📌 中上級者向け：ジラールのパラドックスについて

本文では、Type : Type を許すと体系が壊れると述べました。

その根拠が、ジラールのパラドックスです。

1972年、ジャン＝イヴ・ジラールは、Type : Type を持つ体系においてブラリ＝フォルティのパラドックスが符号化できることを示しました。

ブラリ＝フォルティのパラドックスとは、「すべての順序数の集合」を考えると矛盾が生じる、という集合論の逆理です。

ジラールは、System U という体系の矛盾を示し、その手法がマーティン＝レーフの1971年版にも適用できることを明らかにしました。

この結果を受けて、マーティン＝レーフは体系を可述的に修正しました。

のちに、Coquand と Hurkens がこの逆理を簡略化しました。
Hurkens の逆理は、Coq で機械検査されています。

本文では、この逆理の中身には立ち入りませんでした。

📌 中上級者向け：`Type :: Type` が矛盾する理由を、厳密にいうと

本文では、Haskell で Type :: Type が通ることを示し、「論理としては壊れる」と述べました。

この「壊れる」の意味を補います。

Type :: Type を許す体系では、任意の型に要素を作れてしまいます。
具体的には、停止しない項を構成でき、それがあらゆる型の要素として振る舞います。

論理として読むと、「あらゆる命題が証明できる」ことになります。
これは矛盾です。

Haskell では、停止しない項は最初から存在します。
** undefined や無限ループがそれです。

そのため、Type :: Type を許しても、新たに困ることはありません。

定理証明支援系では、停止しない項を排除することが体系の一貫性を支えています。
そのため、Type : Type を許すことができません。

📌 中上級者向け：`\Set0` と `\Prop` の「高々１つ」は何を数えているのか

本文の記号一覧表では、\Prop を「命題として扱われる型を分類する宇宙（要素が高々１つ）」、\Set を「集合とみなせる型を受け入れる宇宙（等しさの根拠が高々１本）」と説明しました。

同じ「高々１つ」でも、数えているものが違います。

\Prop では、型の要素そのものが高々１つです。

\Set0 では、型の要素は複数あってよく、任意の２つの要素のあいだの等しさの根拠が高々１つです。

何が高々１つか 例
\Prop 要素そのもの 「この数は偶数である」という主張
\Set0 等しさの根拠 自然数、文字列、真偽値

本文の第５部で扱ったホモトピーレベルの言葉でいえば、\Prop はレベル $-1$、\Set0 はレベル $0$ です。塔が退化する階が、ひとつ違います。

第３部・第４部について

📌 中上級者向けコラム：厳密にいうと ── 「等しさの根拠が高々１本」という比喩は、どこまで正しいか

ここからは本文の説明を否定するためではなく、その説明がどの範囲で有効かを中上級者向けに補うための注記です。初読では読み飛ばして構いません。

本文では、isSet A を「等しさの根拠が高々１本である」と説明しました。
これは入門用の比喩です。

正確には、任意の $x, y : A$ と任意の２つの経路 $p, q : x = y$ に対して、さらに $p = q$ が成り立つ、という意味です。

$$\text{isSet}(A) := \prod_{(x, y : A)} \prod_{(p, q : x = y)} (p = q)$$

したがって、「根拠が高々１本」とは、証明項が字面どおり１個しか存在しない、という意味ではありません。

異なる表現の証明があったとしても、それらを区別する高次の構造が残らない、という意味です。

ホモトピー型理論では、型を集合と呼ぶのは、各同一視型 $x = y$ が命題になるからです。

そして、命題、集合、1-型の区別は、単なる根拠の数でなく、反復同一視の階層で決まります。
本文の第５部で扱った「塔が退化する高さ」がその定義です。

円周について。 本文では「等しさの構造は集合の場合より豊かになる」と述べました。

円周がどの有限ホモトピーレベルにも収まらないことは、単に「根拠が２本ある」だけより強い主張です。

loop を合成したループが、どの階でも自明にならないことを示す必要があります。

これは円周の基本群が $\mathbb{Z}$ であるという定理と関わります。
本連載シリーズの第５回目の記事で、この定理に触れました。

本記事はこの点を第５部で自ら修正しています。

第４回目の記事の「根拠が何本ありうるか」という単純化を、「塔が退化する高さ」へ更新しました。

📌 中上級者向け：UIP と一価性が両立しない理由を、厳密にいうと

本文では、UIP と一価性を両方認めると矛盾する、と述べました。

その理由を補います。

一価性は、型の同値 $A \simeq B$ と型の等しさ $A = B$ が対応する、と述べます。

とくに、Bool の自己同値が２つあることから、Bool = Bool の要素が２つ存在することが導かれます。

UIP は、任意の型の任意の２要素について、等しさの証明が高々１つであると述べます。
Bool = Bool にこれを適用すると、その２つの要素は等しいことになります。

しかし、一価性によって、その２つの要素は Bool の異なる自己同値に対応します。
恒等写像と否定写像です。

この２つが等しいなら、true = false が導かれます。
これは矛盾です。

したがって、UIP と一価性は両立しません。

本文の第６部で示した Set-isNotSet は、まさにこの議論を Arend で形式化したものです。

📌 中上級者向け：K 公理と UIP の同値性について

本文では、K を「UIP と同じ内容を別の形で述べた公理」と説明しました。

その内容を補います。

K公理 は、Thomas Streicher によって導入されました。

「等しさの証明 $p : a = a$ についての性質を示すには、$p$ が refl である場合だけを示せばよい」と述べます。

$$K : \prod_{(a : A)} \prod_{(P : (a = a) \to \mathcal{U})} P(\mathrm{refl}a) \to \prod{(p : a = a)} P(p)$$

この公理から UIP が導かれ、UIP から K が導かれます。
つまり、両者は同値です。

Agda のパターンマッチは、既定で K に対応する規則を使います。

--without-K は、その規則を無効にします。

Coq の標準では、K も UIP も導出できません。
ただし、公理として追加することができます。

Lean 4 では、Prop の証明無関係から UIP が導かれます。
Eq が Prop に属するためです。

📌 中上級者向け：Rocq／Coq と UIP の関係

本文では、UIP を認める処理系として Lean 4 と標準の Agda を挙げ、Rocq／Coq には触れませんでした。

Rocq／Coq の状況を補います。

Rocq／Coq の標準では、UIP は公理としても定理としても含まれていません。

したがって、UIP を認めない形で HoTT を扱うことができます。

ただし、標準ライブラリには Eqdep というモジュールがあり、そこで UIP に相当する公理を追加できます。古典数学の形式化では、これを使うことがあります。

また、パターンマッチの方式によっては UIP が導出されてしまう場合があり、HoTT ライブラリはそれを避ける工夫をしています。

本文で「Rocq／Coq の HoTT ライブラリでは持ち回りが必要」と述べたのは、UIP を追加しない設定についてです。

📌 中上級者向け：`\Set0` の等しさの型が `\Prop` に入る、という規則について

本文の第４部で、A : \Set0 のとき x = y が \Prop に属することを実機で示しました。

この規則の理論的な裏づけを補います。

Arend 公式論文には、次の趣旨の記述があります。型 A が宇宙 \(h+1)-Type p に属するとき、道の型 a = {A} a' は宇宙 \h-Type p に属する。

\Set0 は \0-Type0 であり、$h + 1 = 0$ なので $h = -1$ です。**
\(-1)-Type0 が \Prop です。**

この規則により、ホモトピーレベルが１つ下がります。

集合の等しさの型は命題になり、1-型の等しさの型は集合になります。

本文で「型に書かれている」と述べたのは、この規則が型検査器に組み込まれていることを指しています。

第５部・第６部について

📌 中上級者向けコラム：厳密にいうと ── `\Set0` と `\Sigma (A : \Type0) (isSet A)` は、なぜ「同値だが同型ではない」のか

ここからは本文の説明を否定するためではなく、その説明がどの範囲で有効かを中上級者向けに補うための注記です。初読では読み飛ばして構いません。

これは本記事で最も重要な論点です。

\Set0 は、Arend の型検査器が扱う h-type universe です。

ある型が \Set0 に属するかどうかは、型に付された宇宙情報と、その累積性の規則を通じて判定されます。

これに対して \Sigma (A : \Type0) (isSet A) は、型 A と、「A が集合である」という証明を明示的に組にした型です。

両者は同じ数学的内容を表現できますが、型理論の内部では同一の型ではありません。

そのため、ある型 A が数学的には isSet A を満たすとしても、Arend の型検査器が自動的に A : \Set0 と再分類するわけではありません。

必要であれば、\use \level で h-level の証明を定義側に登録します。

この区別により、Arend は「ある型がもっと低いホモトピーレベルを満たすか」を、同値な型を無限に探して判定する必要がありません。

本文では「A : \Set0 は宣言を見れば分かる」と説明しました。 より正確には、A が変数・式・推論された宇宙レベルを伴う場合もあるため、型検査器は、型に付いた宇宙情報と累積性の規則から所属を判定します。

\Set0 \Sigma (A : \Type0) (isSet A)
何であるか 宇宙。型検査上の分類 型と証明の組
所属の判定 宇宙情報と累積性の規則から 証明を構成できるかどうか
両者の関係 同値である 同値である
同型か 同型ではない 同型ではない

「同値」とは、両方向の対応があり、往復すれば元に戻ることです。
「同型」とは、それに加えて、往復が判定的に恒等になることです。

📌 中上級者向けコラム：厳密にいうと ── `\use \level` がしているのは、自動証明ではなく「分類情報の登録」である

ここからは本文の説明を否定するためではなく、その説明がどの範囲で有効かを中上級者向けに補うための注記です。初読では読み飛ばして構いません。

\use \level は、任意の型のホモトピーレベルを型検査器が自動的に発見する仕組みではありません。

定義者が、その \data や \record が isSet、あるいはより一般に $n$-型であることを証明し、その証明を定義に対応付ける仕組みです。

誤解 正確な理解
Arend は h-level を自動推論する 定義者が証明を書き、\use \level で登録する
\use \level で証明が消える 証明は定義側に置かれ、利用側で持ち回らずに済む

したがって Arend で証明が消えるわけではありません。

証明を各利用箇所の関数引数として持ち回る代わりに、定義の側に一度だけ置き、以後は宇宙への所属として使えるようにしています。

本文の「型に語らせる」は、この設計判断を表した比喩です。

「証明を持ち回るか、型に語らせるか」という本記事の主題は、より正確には次のように述べられます。

証明を各利用箇所の関数引数として持ち回るか、
定義側に一度だけ登録して h-type universe への所属として扱うか

Isaev がメーリングリストで示した規則が、この登録の型理論的な形です。

A : \Type0    p : isSet A
--------------------------
    F(A,p) : \Set0
📌 中上級者向け：ホモトピーレベルの定義を、厳密にいうと

本文では、Awodey の「反復した同一視型の塔が退化する高さ」という定義を引きました。

帰納的な定義を補います。

$$\text{is-}(-2)\text{-type}(A) := \text{isContr}(A)$$

$$\text{is-}(n+1)\text{-type}(A) := \prod_{(x, y : A)} \text{is-}n\text{-type}(x = y)$$

可縮（contractible）とは、要素がちょうど１つあり、他のどの要素もそれと等しいことです。

この定義から、$(-1)$-型は命題、$0$-型は集合、$1$-型はグルーポイドになります。

「退化する」とは、この帰納的定義において、ある段階で可縮になることです。

本文の表では $-2$ を「可縮」として載せましたが、深入りしませんでした。

📌 中上級者向け：可縮型と、ホモトピーレベル $-2$ について

本文の表で、レベル $-2$ を「可縮」とし、例として単位型を挙げました。

可縮型について補います。

可縮な型とは、要素がちょうど１つあり、他のどの要素もそれと等しい 型です。
単位型 \Sigma（空の $\Sigma$ 型）がその例です。

なぜ $-2$ が必要かというと、帰納的定義の出発点にするためです。
命題を「任意の２要素が等しい」と定義すると、その等しさの型が可縮になります。

可縮型は、ホモトピー論では「一点と同じ」空間にあたります。

本文では、\Prop が $-1$ に対応することを述べましたが、Arend には $-2$ に対応する専用の宇宙はありません。

📌 中上級者向け：宇宙自身は、どのホモトピーレベルに入るのか

本文の第６部で、\Set0 自身が集合でないことを実機で示しました。

この結果は、一般化されています。

Nicolai Kraus と Christian Sattler が、次を示しました。

（原文引用）

For Martin-Löf type theory with a hierarchy U_0 : U_1 : U_2 : ... of univalent universes, we show that U_n is not an n-type.

（筆者による日本語訳）

一価的な宇宙の階層 $\mathcal{U}_0 : \mathcal{U}_1 : \mathcal{U}_2 : \ldots$ を持つマーティン＝レーフ型理論について、我々は $\mathcal{U}_n$ が $n$-型でないことを示す。

出典：Nicolai Kraus, Christian Sattler, "Higher Homotopies in a Hierarchy of Univalent Universes", arXiv:1311.4002

つまり、$\mathcal{U}_0$ は集合でなく、$\mathcal{U}_1$ はグルーポイドでなく、一般に $\mathcal{U}_n$ は $n$-型ではありません。

本文で示した Set-isNotSet は、$n = 0$ の場合にあたります。

本連載シリーズの第４回目の記事で扱えなかった論点が、ここで扱えました。

📌 中上級者向け：累積性と、宇宙多相の関係

本文では、Arend の宇宙が大きさとホモトピーレベルの両方について累積的であることを示しました。

累積性と宇宙多相の関係を補います。

累積的な体系では、下の宇宙の型がそのまま上の宇宙の型として使えます。
明示的な持ち上げが不要です。

累積的でない体系（Agda がそうです）では、Lift のような持ち上げ関数を使うことになります。

宇宙多相は、これとは別の仕組みです。定義を宇宙レベルで径数づけ、任意のレベルで使えるようにします。

Arend では、\lp と \lh がその径数です。
すべての定義が、暗黙にこの２つの径数を持ちます。

本文では、\lp と \lh を記号一覧表に載せましたが、宇宙多相そのものには立ち入りませんでした。

📌 中上級者向け：`\Set n` と $\Sigma$ 型は、同値だが同型ではありません

本文の第６部で、Isaev の「同値だが同型ではない」という発言を引きました。

この区別を補います。

Arend 公式チュートリアルは、次のように述べています。

（原文引用）

The universe \Set n is equivalent to the subuniverse \Sigma (A : \Type n) (isSet A) of \Type n.

（筆者による日本語訳）

宇宙 \Set n は、\Type n の部分宇宙 \Sigma (A : \Type n) (isSet A) と同値である。

出典：Stratified Universes and Univalence, Arend Documentation

同値とは、両方向の対応があり、往復すれば元に戻ることです。
同型とは、それに加えて、往復が判定的に恒等になることです。

\Set0 から $\Sigma$ 型へは、本文で示した Set-to-SetInType で対応できます。

逆方向は、\use \level を使って型を \Set0 へ置き直すことで対応します。
ただし、置き直した型は元の型と同値ではあっても、判定的に同じではありません。

Isaev が「同型ではない」と述べたのは、この点です。

📌 中上級者向け：`\use \level` の使い方

本文の第６部で、\use \level を使って DecP を \Prop に置く例を示しました。

構文を補います。

\use \level は、データ型やレコードの \where ブロックに置きます。
関数の型は、その型が命題（または $n$-型）であることを示すものでなければなりません。

命題として置く場合は、(x y : D) : x = y という型の関数を書きます。
集合として置く場合は、(x y : D) (p q : x = y) : p = q という型になります。

arend-lib の HLevel.ard に、実例があります。

\func isProp (A : \Type) => \Pi (a a' : A) -> a = a'
  \where
    \use \level levelProp (A : \Type) (e e' : isProp A) : e = e'
      => path (\lam i a a' => isProp=>isSet A e a a' (e a a') (e' a a') @ i)

isProp A という型自身が命題であることを、\use \level で示しています。

第７部について

📌 中上級者向けコラム：厳密にいうと ── Lean 4 の「等号の証明を区別しない」とは、何を意味するのか

ここからは本文の説明を否定するためではなく、その説明がどの範囲で有効かを中上級者向けに補うための注記です。初読では読み飛ばして構いません。

本文の「Lean 4 は、すべての型を集合とみなす」という表現は、等号 Eq の証明に関する設計を短く言い表したものです。

より正確には、Lean 4 の標準的な等号 Eq は UIP を満たすため、同じ２つの値について得られた等号証明どうしを区別しない設計として扱えます。

これは「Lean 4 に等号の証明がない」という意味ではありません。
また、「Lean 4 では円周という数学対象を一切扱えない」という意味でもありません。

誤解 正確な理解
Lean 4 には高次等式が一切ない Eq の証明は存在する。ただし、証明どうしを区別しない
Lean 4 では円周を扱えない 位相空間としての円周は形式化できる。HoTT 的な高次帰納型としての円周が、そのままの形では扱えない

ここで対比しているのは、HoTT や Cubical Type Theory のように、等号そのものを高次の幾何学的構造として扱い、高次帰納型として円周を導入する設計です。 Lean 4 の標準 Eq は、その目的のための等号ではありません。

Mathlib には、位相空間としての円周や、その基本群についての形式化があります。
それらは 古典的な位相幾何の方法 によるもので、本記事で扱った 高次帰納型による方法 とは異なる方法によるものです。

本文中の「円周を扱えません」という記述は、「高次帰納型としての円周を、その非自明な高次等式構造とともに同じ形では扱わない」という意味で読んでください。

📌 中上級者向け：Arend の `\Prop` は、なぜ証明無関係でないのか

本文では、Arend の \Prop が証明無関係でないことを実機で示しました。

その理由を補います。

Arend の公式ドキュメントには、次の続きがあります。

（原文引用）

If A : \Prop and a, a' : A are such that they never evaluate to a constructor, then they are computationally equal.

（筆者による日本語訳）

A : \Prop で a, a' : A が構成子へ評価されないなら、それらは計算的に等しい。

出典：Universes, Arend Documentation

つまり、条件付きで計算的に等しいとみなされます。
構成子へ評価される場合は、証明が要ります。

Lean 4 の Prop は、無条件で証明無関係です。

なぜ Arend がこの設計を採ったのかという点については、少なくとも筆者が調べた限りでは、公式資料に明示的な理由を見出すことはできませんでした。

推測にとどまりますが、Arend が HoTT を扱うため、\Prop を無条件に証明無関係にすると、一価性との整合を保つのが難しくなることが考えられます。

📌 中上級者向け：Lean 4 の証明無関係と UIP の関係

本文では、Lean 4 が UIP を認める理由を「Prop の証明無関係から導かれる」と述べました。

その導出を補います。

Lean 4 では、等しさの型 Eq a b は Prop に属します。

Prop は証明無関係なので、Eq a b の任意の２つの要素 p q について、p = q が判定的に成り立ちます。

これが UIP そのものです。

したがって、Lean 4 では UIP を公理として追加する必要がありません。
Prop の設計から、自動的に導かれるからです。

本連載シリーズの第５回目の記事で、Lean 2 に HoTT モードがあったことに触れました。
Lean 2のHoTTモードでは、Prop の証明無関係を外していました。

UIP が導かれないようにするためです。

Lean 3 以降でそのモードが廃止された結果、Lean 4 では UIP が常に成り立ちます。

📌 中上級者向け：命題のリサイジングと、部分対象分類子

本文の第６部で、Isaev の「\Prop は、すべての部分対象を分類します」という発言を引きました。

この「部分対象を分類する」という言葉を補います。

圏論では、部分対象分類子という概念があります。任意の対象の部分対象（部分集合にあたるもの）が、ある固定の対象への射と一対一に対応するとき、その固定の対象を 部分対象分類子 と呼びます。

集合論では、真偽値の集合 ${0, 1}$ がこれにあたります。
部分集合は、特性関数と対応するからです。

Arend の \Prop が部分対象を分類するとは、任意の型の部分型が \Prop への関数と対応する、ということです。

そして、これが命題のリサイジングと同値であることが知られています。

本文では、圏論の言葉を避けたため、この点に立ち入りませんでした。

📌 中上級者向け：リサイジングは、HoTT Book では公理である

本文では、Arend で命題のリサイジングが成り立つことを述べました。

HoTT Book との違いを補います。

HoTT Book では、命題のリサイジングは公理として扱われます。
可述的な体系では導出できないため、必要に応じて仮定するものです。

Arend では、\Prop が非可述的であるため、リサイジングが体系に組み込まれています。
公理として仮定する必要がありません。

この違いは、本文の第５部で扱った「$\Sigma$ 型の方法では、ひとつ上の宇宙へ上がる」という代償と対応しています。

HoTT Book の方法では、hProp がひとつ上の宇宙へ行くため、それを下へ戻すには公理が要ります。Arend では、はじめから上がりません。

📌 中上級者向け：System F と非可述性について

本文の第７部で、System F が非可述的でありながら矛盾しないことを述べました。

その内容を補います。

System F は、1972年にジャン＝イヴ・ジラールが、1974年にジョン・レイノルズが、独立に発見しました。

System F の特徴は、型についての全称量化 $\forall X., T$ を型として持つことです。
$X$ の動く範囲には $\forall X., T$ 自身も含まれます。

この意味で非可述的です。

しかし、System F は強正規化性を持ちます。
任意の項が有限回の簡約で正規形に達します。

これが無矛盾性を保証します。

他方で、System U は矛盾します。
System F に、種のレベルでの量化を加えたものです。
ジラールが1972年に矛盾を示しました。

System F と System U の違いは、量化を許す層の数にあります。
System F は型についてのみ量化を許し、System U は種についても許します。

「型についての量化を許す」ことと「宇宙を自分自身に入れる」ことの区別は、この違いに対応しています。

構成の計算（Calculus of Constructions）は、System F を依存型へ拡張したものです。
帰納型を加えたものが CIC です。

📌 中上級者向け：Agda の `Setω` について

本文の第５部で、Agda の宇宙の径数として Setω を挙げました。

Setω について補います。

Agda の宇宙は Set₀ : Set₁ : Set₂ : ... と続きます。しかし、宇宙多相な定義の型は、どの Setᵢ にも入りません。

たとえば (ℓ : Level) → Set ℓ という型は、すべてのレベルを動くため、特定のレベルに置けません。そこで、階層の外に Setω を置きます。

本連載シリーズの第５回目の記事で、Cubical Agda の区間 I が Setω に住むことに触れました。非ファイブラント型を通常の階層に置けないため、便宜的にここへ置いています。

Setω 自身は Setω₁ に属し、その上も続きますが、この階層は宇宙多相をサポートしません。

📌 中上級者向け：Lean の `Sort` について

本文の第５部で、Lean 4 の宇宙の径数として Prop を挙げました。

Lean の宇宙の記法を補います。

Lean 4 では、宇宙を Sort u と書きます。
Sort 0 が Prop、Sort 1 が Type 0、Sort 2 が Type 1 です。

つまり、Prop は宇宙階層の最下層にあります。
Prop だけが非可述的です。

本文で Prop : Type を実機で確認しました。
これは Sort 0 : Sort 1 ということです。

Type u は Sort (u+1) の略記です。

記事全体について

📌 中上級者向けコラム：厳密にいうと ── 本文の簡略化と、その正確な言い換えの一覧

ここからは本文の説明を否定するためではなく、その説明がどの範囲で有効かを中上級者向けに補うための注記です。初読では読み飛ばして構いません。

本文では入門者向けに簡略化した表現を用いました。
中上級者向けに、その正確な言い換えを一覧にします。

優先度 本文の趣旨 気になる点 正確な言い換え
高 Haskell は「型のレベルで数学の議論を組み立てないから」宇宙階層を要しない Haskell でも型レベル計算・型レベル DSL・型安全な埋め込み言語などは記述できるため、やや広すぎる Haskell の通常の型体系は、一貫した依存型論として数学の証明を内部化することを目的としていないため
高 Type :: Type を許すので、Haskell は論理として壊れる 「壊れる」が強く、Haskell の実用上の正当性まで否定しているように読める このままでは、Curry–Howard 対応を通じて無矛盾な論理体系として読むことはできない
高 Lean 4 は「すべての型を集合とみなす」 読者が「Lean には高次等式が一切ない」と誤解しやすい Lean 4 の標準的な等号 Eq は UIP を満たすため、等号の証明どうしを区別しない設計として扱える
高 円周は $\infty$、塔が退化しない 「loop と idp が二本あるから」だけでは無限 h-level の理由として不足しやすい 円周が $\infty$-型であるという主張は、単に経路が二本あることより強い。ここでは第５回の直観を再利用する
中 \Set0 の型なら等しさの根拠が「高々１本」 「根拠の本数」という比喩は、同一視の要素数の字義どおりの有限性と混同されうる 正確には、任意の二つの根拠をさらに同一視できる、という意味
中 「関数が10個あれば、10箇所に同じ証明を書く」 implicit argument、record、instance search、抽象化などで負担を軽減できるので、Agda 一般の断定に見える 単純に引数として書く設計では、10個の関数のシグネチャと呼び出しで繰り返し現れやすい
中 $\Sigma$ 型は「材料の型より大きくなる」 常に「材料より大きくなる」と読めると不正確。宇宙レベルは構成要素の最大値で決まるのが基本 ここでの $\Sigma(A : \mathcal{U}_0)., \mathrm{isSet}(A)$ は、量化範囲に $\mathcal{U}_0$ 自身が現れるため、$\mathcal{U}_0$ より上に置かれる
中 \Prop は「要素が高々１つしかない型を集めた宇宙」 記事自身が「宇宙を型を集めた箱と考えない」と注意しているため、「集めた宇宙」が比喩として揺れる 要素が高々一つである型を分類する宇宙
中 「A : \Set0 は宣言を見れば分かる」 A が変数・式・推論された宇宙レベルを伴う場合もあり、「宣言を見れば」は単純化しすぎ 型検査器は、型に付いた宇宙情報と累積性の規則から判定できる
低 「最近の Haskell では Type とも書きます」 * は現在では旧来表記というニュアンスを添えたほうが親切 現在の GHC では Data.Kind.Type が推奨され、* は旧来の表記
低 「自然数、整数、文字列など、普通のデータ」は \Set0 Arend の具体的な標準ライブラリ上の配置として読まれる可能性がある 通常の離散的データ型を置く場所として考えるとよい

本文の一部については、この言い換えを既に反映しました。
反映していない箇所は、入門者向けの読みやすさを優先したものです。

📌 中上級者向け：本記事のコードの検証環境について

本記事に掲載したコードは、Arend、Haskell、Agda、Lean 4 のすべてを実機で検証しました。

処理系 バージョン
Arend 1.10（Java 21）＋ arend-lib 1.10
GHC 9.4.7
Agda 2.6.3
Lean 4.33.1

型検査の結果とエラーメッセージは、実行時の出力をそのまま掲載しています。

詳細は、本稿の Appendix に掲載しています。

Rocq／Coq については、執筆環境に処理系を用意できませんでした。 Set の非可述性についての記述は、Rocq 公式マニュアルと査読論文の記載に基づくものです。

📌 中上級者向け：訳語について

本記事で用いた訳語のうち、日本語として定着していないものがあります。原語を併記しておきます。

訳語 原語 備考
宇宙 universe ──
ホモトピーレベル homotopy level h-レベルとも
可述的・非可述的 predicative / impredicative ──
累積的 cumulative ──
等しさの証明の一意性 uniqueness of identity proofs（UIP） ──
証明無関係 proof irrelevance 「証明無関与」とも
命題のリサイジング propositional resizing 定訳がないため、原語を片仮名にした
種 kind ──
可縮 contractible ──
部分対象分類子 subobject classifier ──

訳語の選定にあたっては、上村太一氏『ホモトピー型理論』を参考にしました。

出典一覧

Arend

メーリングリスト

型理論における宇宙とホモトピーレベル

型理論の歴史

他の処理系

ホモトピー型理論

検証環境

本記事に掲載したコードは、次の処理系で実機検証しました。

処理系 バージョン
Arend 1.10（Java 21）＋ arend-lib 1.10
GHC 9.4.7
Agda 2.6.3
Lean 4.33.1

型検査の結果とエラーメッセージは、実行時の出力をそのまま掲載しています。

Rocq／Coq については、執筆環境に処理系を用意できませんでした。 詳細は本稿の Appendix に掲載しています。

0
0
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
Sign upLogin
0
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?