前回、「Haskell から始める型理論の家系図 — 単純型付きラムダから HoTT まで」という記事を公開しました。
序：ここから先の問い
前回までの記事で、私たちは次のところまで来ました。
- 数学のホモトピー理論には、対象を空間の中の点、等しさを2点をつなぐ道として捉える世界観がある（初回の記事）
- Haskell の
Intや[Char]は、点と道の集まりとしての空間と見なせる（2 本目の記事） - 型理論には家系図があり、Martin-Löf 型理論から HoTT に至る系譜がある（3 本目の記事）
- HoTT の Univalence Axiom を「実際に計算できる形」で実装するために、立方体型理論（Cubical Type Theory）が生まれた（3 本目の記事の第 7.5 節）
前回の記事の中で、私は次のように書きました。
立方体型理論には、実は複数の派生形があります。BCH cubical、CCHM cubical、ABCFHL cubical、cartesian cubical などがあります。それぞれ、区間の扱い方や、貼り合わせの仕組みが微妙に違います。
この記事は、この一文をまるごと展開したものです。
「Cubical Type Theory」と一口に言っても、その心臓部にある 区間 $I$ にどのような数学的構造を与えるか について、複数の理論的な選択肢があります。
この記事では、その選択肢を 2 つの主要な流派 に整理し、それぞれの計算規則の違いを見ていきます。
そして、この分類軸を使うことで、Cubical Agda 、 redtt 、 cooltt 、RedPRL 、Arend 、NuPRL といった 複数の証明支援系 が、きれいに整理できることも見ていきます。
1. 出発点の問いを再考する
前回の記事の第 7.5 節（立方体型理論）で、私たちは次のように述べました。
HoTT では恒等型を数学的な「道」として解釈できる。しかし、Univalence Axiom を公理として置くと、道を実際に構成しても計算が詰まって進まないことがある。
ここから、次のような疑問を持たれた方もおられたのではないでしょうか。
道を「計算可能なもの」として型理論の中で扱うには、何を用意すればよいのか？
立方体型理論が取った対応は、区間 $I$ を容易することでした。
これは、前回の記事で述べたとおりです。
型理論の中に、形式的な区間 $I$ を持ち込む。そして、道を「$I$ から型 $A$ への関数」として定義する。
この答え自体は、立方体型理論の全ての流派に共通しています。
立法体型理論の中でも、対応が分かれるのは、「区間 $I$ にどのような数学的構造を持たせるか」 を決める局面です。
なぜ、判断が分かれうるのでしょうか？
それは、区間 $I$ は数学の区間 $[0,1]$ の「形式的な模倣」であって、実物ではないから です。
前回の記事の補足で私は次のように書きました。
立方体型理論の I は、位相幾何の区間 [0,1] そのものではなく、その形式的な模倣です。I は自由に和集合や交わりを取れる操作（min, max, 否定）を持ち、これによって n 次元立方体を組み立てられるように設計されています。
上記の補足文を手掛かりに、何が論点となるのか、さらに議論を続けていきましょう。
2. なぜ「形式的な模倣」でなければならないのか
数学の区間 $[0,1]$ は、実数の集合の中の閉区間です。
無限個の実数が入っていて、大小関係があり、加減乗除などの計算が全部できます。
しかし、型理論 の中に 区間 を持ち込むとき、実数全体をそのまま持ち込むことはできません 。
理由は 2 つ あります。
第1に、型理論は「計算できるもの」しか扱わないからです。
実数 は一般には計算できません。
円周率 $\pi$ を最後の桁まで書き出すことは有限のステップではできません。
型理論 の道具として使うなら、有限のステップで答えが出る操作しか許されません 。
📌 中上級者向け補足：「型理論は計算できるものしか扱わない」は、型理論一般の性質ではない
「型理論は『計算できるもの』しか扱わない」という言い回しは、型理論一般 の性質として読むと強すぎます。
実数 を 形式化した型理論 ・ライブラリは実在します。
Rocq にも、LeanのMathlib にも、実数の理論 は整備されており、円周率 $\pi$ も 型理論の中の立派な住人 です。
「計算できる」の意味自体も、理論と計算規則の与え方によって変わります。
本文で言いたかったことは、文脈を限定した 次のような主張です
── 立方体型理論の区間 $I$ は、実数の区間 $[0,1]$ をそのまま持ち込むのではなく、型検査の計算規則が直接扱える形式的な対象として設計される、ということ。
区間 が理論の心臓部で毎回の型検査に関わる以上、そこに乗せる構造はシンボリックに簡約できるものでなければならない、という設計上の要請の話であって、型理論が実数を扱えないという主張ではありません 。
第2に、型理論の中で「区間 $I$ の要素」を書き出せなければならないから です。
前回の記事で PathP (λ i → A) x y という書き方を紹介しました。
ここに出てくる $i$ は、区間 $I$ の要素を表す変数です。
プログラムの中で $i = 0.31415...$ などと書きたいわけではありません。
書きたいのは、$i = 0$、$i = 1$、あるいは「$i$ と $j$ の小さいほう」のような、シンボリックに扱える式 です。
以上の理由（背景、前提）から、型理論の区間 $I$ は次のように設計されることが要求されます。
- 0 と 1 という 2 つの特別な要素を持つ
- 他の要素は、変数 $i, j, k, ...$ として扱う（ 何の値かは決めない、抽象的な区間の点 ）
- 変数どうしを組み合わせて新しい要素を作る 演算 を持つ
- 演算の結果には、いくつかの 等式規則（計算規則） が付いている
ここが設計判断の分かれ目 です。
- 「どんな演算を持たせるか」
- 「その演算がどんな等式規則に従うか」
を決めるところで、複数の選択肢が生じてくるのです。
3. n 次元立方体を組み立てる、とはどういうことか
まず最初に、なぜ 区間 $I$ に 演算 を持たせる必要があるのか、その理由を先に考えたいと思います。
前回の記事の第 7.5 節で、次のように述べました。
0 次元の立方体 = 点、1 次元の立方体 = 線分、2 次元の立方体 = 正方形、3 次元の立方体 = 立方体、以下 n 次元立方体まで続く。この階層で、型の中の「道の階層」を表現する。
$n$ 次元立方体を「区間の $n$ 個の直積」として作る、という発想です。
- 1 次元の立方体（辺）は $I$ そのもの
- 2 次元の立方体（正方形）は $I \times I$
- 3 次元の立方体は $I \times I \times I$
具体的に 2 次元の場合を絵にすると以下のようになります。
(0,1) ───────── (1,1)
│ │
│ │
│ I × I │
│ │
│ │
(0,0) ───────── (1,0)
この正方形の 4 つの頂点は、$I \times I$ の中で $(0,0), (1,0), (0,1), (1,1)$ と書けます。
4 つの辺のうち、
- 下辺は $i$ を動かして $(i, 0)$
- 上辺は $(i, 1)$
- 左辺は $(0, j)$
- 右辺は $(1, j)$
と書けます。
正方形の内部は $(i, j)$ で $i, j$ が両方動きます。
さて、この 2 次元の正方形の 対角線 を書きたいとします。
左下 $(0,0)$ から右上 $(1,1)$ へ結ぶ線。この対角線を書くには、どのように記述したらよいでしょうか？
答えを述べてしまうと、
$i = j$
という条件で書けます。
他にも、$i$ を受け取って $(i, i)$ を返す、という書き方も考えられます。
もう少し複雑な図形も欲しくなります。
たとえば、正方形の左下の三角形（$i \le j$ の部分）だけ取り出したい。
あるいは、「$i$ と $j$ の小さいほう」を返す操作、つまり $\min(i, j)$ が欲しい。
これが、区間 $I$ に $\wedge$（min、最小値） の演算を持たせる動機です。
同じ理由で、
- $\vee$（max、最大値）
- 「区間の向きを反転する」$\sim i$（否定、$1 - i$ に相当）
も欲しくなる方もおられるかもしれません。
これらの 演算 を、 「区間の要素の間の操作」 として持たせておくと、正方形や立方体の中の複雑な図形（辺、面、対角線、部分立方体）を、$i, j, k$ と $\wedge, \vee, \sim$ の式で記述できるようになります。
整理しましょう。
「区間 $I$ に、どこまで演算を持たせるか」
「持たせた演算にどんな等式規則を要求するか」
上記の判断ポイント を通過するとき、立方体型理論 は 複数の流派に枝分かれする のです。
なお、そもそも何を基準に立方体型理論の「流派」を分類するのかも、厳密に考えると見解は一意に定まりません。
本稿は、このあたりの議論には深入りしません。
📌 中上級者向け補足：研究文献では、どんな分類基準が議論されているか
「流派の分類基準は一意に定まらない」と述べました。
では、研究の現場では何が分類のパラメータとして扱われているのでしょうか。
立方体型理論とそのモデルを比較する研究では、次に示す分類軸が議論されています。
１つ目は、土台の立方体圏にどの構造演算を入れるか、という分類軸です。
面（端点への代入）・退化・対称・対角・connection（$\wedge$、$\vee$）・反転（$\sim$）のうち、どれを立方体圏に持たせるか。
Buchholtz と Morehouse の Varieties of Cubical Sets（2017）は、この選択肢を 代数的な理論 として 体系的にカタログ化 した研究です。
https://arxiv.org/abs/1701.08189
２つ目は、Kan 合成（fibration）をどう定めるか、という分類軸です。
Cavallo・Mörtberg・Swan の Unifying Cubical Models of Univalent Type Theory（CSL 2020）は、立方体圏にどの構造演算を入れるかという観点だけではなく、Kan 合成をどう定式化するか、どのクラスの fibration を採用するかという観点も、考慮に入れねばならないという見解を示しています。
同論文は CCHM 型と AFH 型の合成構造を比較し、両方を含む、より緩やかな定め方を与えました。
https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.14
３つ目は、cofibration をどこまで認めるか、という分類軸です。
「部分的に決まった図形」は、区間の変数についての条件式で切り出されます。
どの形の条件式まで認めるか ── たとえば対角（$i = j$）という条件式を認めるかどうか ── は、理論ごとに異なります。
前掲の CSL 2020 の論文は、対角の条件式にも connection にも頼らずにモデルを構成できることを示しました。
Orton と Pitts による公理的な枠組み（Axioms for Modelling Cubical Type Theory in a Topos）も、この「どこまで認めるか」を取り替え可能な前提として切り出す土台になっています。
「部分的に決まった図形」をどの条件式で切り出せるか、たとえば対角（$i = j$）を cofibration として認めるかどうかは、それ自体がひとつの設計判断です。
４つ目は、意味論の与え方による分類軸です。
前層による圏論的モデルで意味を与えるか、
NuPRL の伝統に連なる計算的意味論で与えるか。
本文の第5節で、AFHとABCFHLの違いに着目して解説する分類軸です。
５つ目は、古典的なホモトピー論をどこまで正しく再現できるか、という分類軸です。
立方体圏の上の前層が、古典的なホモトピー論（空間のホモトピー論）を正しく再現するかどうか。
前掲の Buchholtz と Morehouse の論文は、どの立方体圏が test category（この再現が成り立つ圏）であり、どれがさらに強い strict test category であるかを判定しています。
以上、見てきた 5 つの分類軸は、どれか 1 つを決めれば残りも決まる、という関係にはありません。
それぞれの軸で、理論ごとに別々の答えがありえます。
したがって、どの軸を物差しに選ぶかによって、「流派」の切り分け方も変わってきます。
また、本稿は、研究者や実務家によって議論されているすべての流派を取り上げることもできません。
本稿が取り上げるのは、 De Morgan Cubical Type Theory（CCHM） と Cartesian Cubical Type Theory（CCTT） の 2 つの流派です。
| 略称 | 正式名称 | 略称の由来 | 区間 $I$ に入れる構造 |
|---|---|---|---|
| CCHM | De Morgan Cubical Type Theory | 提案者 4 人の頭文字（Cohen・Coquand・Huber・Mörtberg、2015 年発表の論文の著者） | De Morgan 代数（$\wedge$、$\vee$、$\sim$ と、その等式規則） |
| CCTT | Cartesian Cubical Type Theory | Cartesian Cubical Type Theory の頭文字（Cartesian は「デカルトの」の意） | Cartesian 立方体圏の構造のみ（対角・対称・退化。追加の演算は入れない） |
なお、本稿は、CCHM と CCTT を、文脈に応じて次の呼び方でも書きます。
以下の表のとおりです。
| 本文での呼び方 | 意味するもの |
|---|---|
| De Morgan 版、CCHM 版 | CCHM（De Morgan Cubical Type Theory）そのもの |
| Cartesian 版、CCTT 版 | CCTT（Cartesian Cubical Type Theory）そのもの |
| De Morgan 系 | CCHM を代表とする系統。実装の Cubical Agda・cubicaltt を含む |
| Cartesian 系 | Cartesian の設計を共有する系統。CCTT の派生形（AFH・ABCFHL）と、実装の redtt・cooltt・RedPRL を含む |
「版」は特定の理論を、「系」はその理論と派生形・実装をまとめた系統を指します。
さて。
続いて、本稿がなぜ、 数ある立方体型理論のうち、De Morgan Cubical Type Theory（CCHM） と Cartesian Cubical Type Theory（CCTT） の 2つに着目するのか、その動機をご説明致します。
CCHM と CCTT は、型理論や HoTT の研究コミュニティが採用している立方体型理論の流派の名称です。
本稿を一つの出発点として、型理論や HoTT に関する学習や研究にご関心を寄せられた読者の方々がおられた場合、専門文献や論文、有識者が集まる和文や英文のオンラインコミュニティでの議論を読む際に、そこで使われている流派名に慣れておいていただいた方がよいのではないかと考えました。
そこで、型理論や HoTT の研究コミュニティによって採用されている De Morgan Cubical Type Theory（CCHM） と Cartesian Cubical Type Theory（CCTT） の２分類を取り上げることに致しました。
なお、立方体型理論を CCHMと CCTTの 2 つに分類する（分類）基準は、中上級者向け補足コラム「研究文献では、どんな分類基準が議論されているか」 で取り上げる 5 つの軸のうち、第 1 の軸 （「土台の立方体圏にどの構造演算を入れるか」、「区間 $I$ が $\wedge$、$\vee$、$\sim$ の演算を持つかどうか」）になります。
特定の分類基準を支持する立場は取らない、と述べたばかりです。それでも本稿が、数ある軸の中から第 1 の軸を説明の主役に据えたのには、入門記事としての実務的な理由が 2 つあります。
ちなみに、CCHM が「De Morgan cubical」と呼ばれるのは、区間 $I$ に De Morgan 代数の構造を入れたからです。
また、CCTT が「Cartesian cubical」と呼ばれるのは、区間を Cartesian 立方体圏の素朴な構造にとどめたからです。
なお、Cartesian という英語は、「デカルトの」という意味の形容詞です。
哲学者にして数学者、「我思う、ゆえに我あり」の René Descartes（ルネ・デカルト）のことです。デカルトのラテン語名 Cartesius に由来します。
座標平面（$xy$ 座標）を英語で Cartesian coordinates と呼ぶのと同じ用法で、直積 $A \times B$ を Cartesian product（デカルト積）と呼ぶ習わしから、この流派の名前にも Cartesian の語が使われています。
4. De Morgan Cubical Type Theory（CCHM）
CCHM 版 の立方体型理論（Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg, 2017）は、区間 $I$ に De Morgan 代数 という構造を持たせます（Cohen-Coquand-Huber-Mörtberg 2018）。
De Morgan 代数とは、この文脈で何を意味するか
「De Morgan 代数」 という言葉自体は、論理学 や 束論 の用語です。
ここでは、次の 3 つの演算とそれらの等式規則を持つ構造 として理解してください。
区間 $I$ に、次の演算を持たせます。
- $i \wedge j$ — 最小値（min）
- $i \vee j$ — 最大値（max）
- $\sim i$ — 反転（$1 - i$ に相当）
そして、これらの演算は次の等式規則に従います。
- 交換律：$i \wedge j = j \wedge i$、$i \vee j = j \vee i$
- 結合律：$(i \wedge j) \wedge k = i \wedge (j \wedge k)$、$(i \vee j) \vee k = i \vee (j \vee k)$
- 分配律：$i \wedge (j \vee k) = (i \wedge j) \vee (i \wedge k)$、$i \vee (j \wedge k) = (i \vee j) \wedge (i \vee k)$
- 吸収律：$i \wedge (i \vee j) = i$、$i \vee (i \wedge j) = i$
- 端点の規則：$i \wedge 0 = 0$、$i \vee 1 = 1$、$i \wedge 1 = i$、$i \vee 0 = i$
- De Morgan の法則：$\sim(i \wedge j) = \sim i \vee \sim j$、$\sim(i \vee j) = \sim i \wedge \sim j$
- 二重否定：$\sim\sim i = i$
- 端点の反転：$\sim 0 = 1$、$\sim 1 = 0$
ただし、通常の論理の Boole 代数と違って、$i \wedge \sim i = 0$ や $i \vee \sim i = 1$ は成り立ちません（$i$ は抽象的な区間の点なので、$i = 0$ でも $i = 1$ でもない中間にいる可能性があります）。
これが「De Morgan」であって「Boole」ではないゆえん です。
📌 中上級者向け補足：区間 $I$ は、束論におけるDe Morgan 代数である
本文で、区間 $I$ に持たせる構造を「De Morgan 代数」と呼びました。
De Morgan 代数は、数学の 束論（そくろん、lattice theory）という分野で厳密に定義されている構造です。
このコラムでは、束論という数学の分野で、De Morgan代数がどう定義されているのかを見た上で、区間 $I$ がその定義を満たしていることを確認します。
束論は、順序のついた集合を代数の言葉で研究する分野です。
集合のどの 2 要素 $a$、$b$ についても、「$a$ 以下でも $b$ 以下でもある要素のうち、最大のもの」（$a \wedge b$ と書きます）と、「$a$ 以上でも $b$ 以上でもある要素のうち、最小のもの」（$a \vee b$ と書きます）が必ず存在するとき、その集合を 束（そく、lattice）と呼びます。
束論では、$a \wedge b$ を 交わり（meet）と呼びます。
「$a$ 以下でも $b$ 以下でもある要素」を $a$ と $b$ の 下界（かかい、lower bound）と呼ぶので、交わりは $a$ と $b$ の 最大下界（greatest lower bound）です。
同じく、$a \vee b$ を 結び（join）と呼びます。「$a$ 以上でも $b$ 以上でもある要素」が 上界（じょうかい、upper bound）で、結びは $a$ と $b$ の 最小上界（least upper bound）です。
束 の実例は身近にあります。
整数の大小順序 では、$a \wedge b$ は min、$a \vee b$ は *max です。
集合の包含関係 では、$\wedge$ は共通部分 $\cap$、$\vee$ は 和集合 $\cup$ です。
自然数の「割り切る」という順序 では、$\wedge$ は 最大公約数 、 $\vee$ は 最小公倍数 です。
これらの構造は、見た目は違いますが、どれも交換律・結合律・吸収律という同じ等式を満たします。
だから、束 というひとつの概念でまとめて扱うことができます。
プログラミング領域では、 コンパイラの静的解析（抽象解釈） や 部分型付けの理論 が、束 の言葉で組み立てられています。
なお、束 に 条件を追加 すると、より特殊な構造 になります。
分配律 を満たす束は 分配束 と呼ばれます。
最小元 0 と最大元 1 を持つ束は 有界束 と呼ばれます。
そして、有界な分配束に、De Morganの法則 と 二重否定の消去を満たす反転 $\sim$ を追加した構造が、De Morgan 代数 です。
De Morgan 代数 は、Boole 代数を一般化した構造 です。
真と偽の 2 値だけを扱う 古典論理の代数 が Boole代数 であるのに対し、
De Morgan 代数 は、真理値が 0 と 1 のあいだにも並ぶ論理 ── 多値論理やファジィ論理 ── の 代数的な土台 として使われてきました。
たとえば、++ファジィ論理で使う実数区間 $[0,1]$ に min・max・$1-x$ の演算を入れた構造は、De Morgan 代数の代表的な実例** です。
ここで、本文に列挙した区間 $I$ の等式規則を見返してください。
- 交換律
- 結合律
- 分配律
- 吸収律
- 端点 0 と 1 の規則
- De Morgan の法則
- 二重否定
いま述べた De Morgan代数 の要件と、一対一で対応しています。
つまり、区間 $I$ は、束論の定義をそのまま満たす De Morgan 代数です。
（正確には、変数 $i, j, k, \ldots$ から自由に生成される De Morgan 代数です）。
Boole代数 との違いは、補元の法則（$i \wedge \sim i = 0$、$i \vee \sim i = 1$）を 要求しない点 にあります。
$i$ は 0 でも 1 でもない中間の点でありえます。
だから、補元の法則を要求しない De Morgan 代数が、区間 $I$ に合う のです。
もうひとつ、留意すべき点があります。
本稿で述べた「$\wedge$ ＝ 最小値（min）、$\vee$ ＝ 最大値（max）、$\sim i$ ＝ $1 - i$ に相当」という解説は、直感をつかむため の対応関係です。
区間 $I$ は 形式的な対象 です。
実数の区間 $[0,1]$ 上の関数 min、max、$1 - x$ を、そのまま演算として持っているわけではありません。
演算の意味を定めているのは、実数の計算ではなく、上に列挙した等式規則（公理）そのものです。
「min のように振る舞う形式的な 演算」と読むのが正確です。
この構造から何が得られるか
De Morgan構造 があると、区間の要素どうしを比較的自由に組み合わせられます 。
道の反転
型 $A$ の中で、$x$ から $y$ への道 p : PathP (λ i → A) x y があるとき、その反転（$y$ から $x$ への道）は λ i → p (~ i) と書けます。
$\sim$ があるおかげで、道の反転は「自明な操作」として書けます。
道の合成の一部
「道と道をつなぐ」という操作を組み立てるとき、$i \wedge j$ や $i \vee j$ が使えると、その合成の途中の面を書きやすくなります。
HIT のコンストラクタとの相性
前回までの記事で見た円周 $S^1$ の loop : base ≡ base のように、道をコンストラクタとして直接持つ HIT を扱うとき、De Morgan 構造 は組み立てを楽にします。
実装：Cubical Agda と cubicaltt
CCHM の理論を実装した処理系は2つあります。
cubicaltt — Anders Mörtberg らによる、CCHM の初期プロトタイプ実装。
Haskell で書かれた小さな処理系で、Path、comp（合成）、Glue（貼り合わせ）などの立方体型理論の中核機能を持ちます。研究用。
Cubical Agda — Agda に CCHM ベースの拡張機能を組み込んだもの。cubicaltt よりも実用に耐える処理系 で、標準ライブラリ agda/cubical が整備されています。
現時点で HoTT の実用的な形式化に最もよく使われている のが、この CCHM 系の Cubical Agda です。
5. Cartesian Cubical Type Theory（CCTT、ABCFHL）
もう一つの流派が、Cartesian Cubical Type Theory（CCTT） です。
カーネギーメロン大学の Carlo Angiuli、Guillaume Brunerie、Thierry Coquand、Kuen-Bang Hou (Favonia)、Robert Harper、Daniel R. Licata らが 2017 年頃から発展させました（頭文字を取って ABCFHL 版 とも呼ばれます）。
Cartesian とは、何を意味するか
「Cartesian」 という語は、数学では デカルト積（直積） を意味します。
この文脈では、次の姿勢を表します。
区間 $I$ には、0, 1, 変数 $i, j, k, ...$ だけあれば十分。$\wedge, \vee, \sim$ のような追加の演算は入れない。
これが、CCHM（De Morgan 版）との最大の対比 です。
CCHM は、区間に豊かな代数構造を入れる。
CCTT は、区間を極力シンプルに保つ。
CCTT の区間 で使える 操作 は、次のようなものです。
- 端点への代入：変数 $i$ に 0 や 1 を代入する（
i := 0、i := 1） - 変数の同一視：別々の変数 $i$ と $j$ を同じものと見なす（
i := j。これを「対角写像 diagonal」と呼ぶ） - 変数の入れ替え：$i$ と $j$ の役割を入れ替える（対称性、symmetry）
- 変数を落とす：使わない変数を式から取り除く（degeneracy、退化）
$\sim i$ はありません。$i \wedge j$ や $i \vee j$ もありません。
📌 中上級者向け補足：「Cartesian」は「区間が直積を成す」という素朴な意味ではない
本文では「Cartesian ＝ デカルト積（直積）」と入口の説明をしましたが、区間の直積 $I \times I$ を取れること自体は、De Morgan 系を含むどの流派にも共通です。
それだけでは流派の名前になりません。
この名前の由来は、Cartesian cube category（デカルト立方体圏） の上に理論を組み立てることにあります。
おおまかに言えば、対象が「有限個の区間変数の組」で、射が 変数の置換・対角（変数の同一視）・対称（変数の入れ替え）・退化（変数を落とす） から生成される圏 です。
本文で列挙した「Cartesian の区間で使える操作」は、まさに この圏の射に対応 しています。
つまり「Cartesian」とは、$\wedge$、$\vee$、$\sim$ のような追加の代数演算を持たない、この最も基本的な立方体圏だけを土台に採用する、という設計宣言 なのです。
圏論 を学ばれた方なら、 「有限直積だけで生成される圏＝ Cartesian な構造」という語感 で捉えると、命名者の心のうちが透けて見えるかもしれません。
なぜ、あえて演算を絞るのか
De Morgan 版 のほうが機能豊富に見えます。
なぜ CCTT はあえて構造を減らすのでしょうか。
理由は 3 つ あります。
ひとつ目は、数学的な自然さ の追求です。
圏論 では、Cartesian cube category（対角、対称、退化だけを持つ立方体圏） は、非常に自然で扱いやすい対象です。
De Morgan 版 のように 追加の代数構造を入れる と、圏論的な扱いが少し複雑 になります。
「シンプルな圏の上でモデルを構成したい」という数学的な動機 があります。
２つ目は、正準性（canonicity）の証明のしやすさです。
前回の記事で「Univalence が計算できる」ことの背景には、canonicity という性質があると述べました。
CCHM 版 でも Huber がこれを証明しましたが、CCTT のシンプルな構造のほうが、canonicity の証明が見通しやすい と考える研究者もいます。
実際、Angiuli の博士論文（CMU, 2019）は、Cartesian版で canonicity を計算的意味論（computational semantics）の観点から与えています。
３つ目は、ある研究の伝統との相性のよさを好感するものです。
少し回り道になりますが、この理由を理解するには、Cartesian 版を発展させた研究者たちの背景を知る必要があります。
ここは初学者にとって新しい話題なので、丁寧に説明します。
CMU（カーネギーメロン大学）と NuPRL の伝統
Cartesian 版の主要な発案者たち — Robert Harper、Kuen-Bang Hou (Favonia)、Carlo Angiuli、Daniel Licata — は、いずれも カーネギーメロン大学（Carnegie Mellon University、以下 CMU）の研究者、あるいはそこで学位を取った研究者です。ペンシルベニア州ピッツバーグにある、コンピュータ科学で世界的に知られた大学です。
CMU の型理論グループには、198年代から続く独特の伝統があります。
それは、 NuPRL という証明支援系を軸とする伝統です。
NuPRL は、コーネル大学の Robert L. Constable らが 1980 年代に開発した証明支援系です。
名前は「Nu(=new) Proof Refinement Logic」の略で、当時としては先進的な、依存型を持つ証明支援系 でした。
この NuPRL が採用した型理論の考え方が、後に CMU の Robert Harper 一派に受け継がれ、独特の系譜として今日まで続いています。
前回の記事で詳述した型理論の家系図では、この流派を明示的には書きませんでした。
位置づけを補うと、次のようになります。
1972年 Martin-Löf 型理論 開始
│
├──────────────┬──────────────┐
│ │ │
│ │ 1984年 Constable ら: NuPRL
│ │ │ ─── 計算による意味付けの流派
│ CoC/CIC │
│ (Rocqへ) │ Harper (CMU) ── AFH cubical へ
│ │
HoTT の流れへ │
現在も CMU で継続
「計算による意味付け」とは、どういう立場か
この NuPRL の伝統が持つ独特の姿勢を、分かりやすく説明します。
型理論 には、大きく分けて 2つの意味付けの流儀 があります。
流儀 A：型を「集まり」として先に決めておく立場
Haskell を書くとき、多くの方は、おそらく次のように考えておられるのではないでしょうか。
-
Intという型は、... -2, -1, 0, 1, 2, ... という整数の集まりである。 -
Boolという型は、TrueとFalseの 2 つからなる集まりである。 -
Int -> Boolは、Intの要素を受け取ってBoolを返す関数の集まりである。
先に「型 = 何かの集まり」があり、あとから「その中の要素として、この関数はこう動く」と関数を書く。これが自然な考え方に思えます。ほとんどの型理論の教科書もこの立場を取ります。この立場を、専門用語では、「denotational（外延的、集合的）な意味付け」 と呼びます。
流儀 B：型を「計算の振る舞い方」として決める立場
これに対し、NuPRL の伝統 は 逆の順序 を取ります。
先に「計算がどう動くか」を決めておき、あとから「こういう動き方をするものを、この型に住むと呼ぶ」と型を規定する のです。
たとえば、Int という型を先に集合として定めるのではなく、こう考えます。
ある計算 M が「Int 型を持つ」とは、M を実行すると必ず、有限のステップで具体的な整数値（0 や -3 や 42 のような）に停止することである。
型は、計算の振る舞い方の一種の「合格基準」として定義されます。
「合格基準を満たす計算」が集まって、事後的に型を成す。
集まりが先で計算が後、ではなく、計算が先で型が後、という順序です。
この立場を、専門用語では、「computational（計算的）な意味付け」 と呼びます。NuPRL とその後継の証明支援系が採用してきた立場 です。
なぜこの立場が Cartesian 版と相性がいいか
この 計算的な立場 から見ると、立方体型理論 の 設計目標 は次のように読めます。
区間 $I$ に、道の反転や合成といった「幾何学的な意味」を代数構造として付与しておくのではなく、「道はこう動く」「道と道はこう組み合わさる」という 計算の規則そのもの を、区間の側にはなるべく持ち込まず、Kan操作の側に集約したい。
De Morgan 版（CCHM） は、区間 $I$ に $\wedge$、$\vee$、$\sim$ といった代数構造を 先に 与えます。
これは、「区間はこういう代数の対象である」という「型を集まりとして先に決める」流儀に近い姿勢 です。
Cartesian 版 は、区間 $I$ からそうした代数構造を 意図的に取り除きます。
区間はほぼ何も持たない素朴な対象にしておいて、道の反転や合成の意味は、Kan 操作の計算規則として与える。
（補足説明）
本文の流れを損なうことを防ぐために、引用文の体裁にしました。
「Kan 操作の計算規則として与える」を、もう少し具体的に説明します。
CCHM では、道の反転を
λ i → p (~ i)と書けました。
$\sim$ という区間の演算に「向きを反転する」という意味が担わされているからです。Cartesian 版の区間には $\sim$ がありません。では、道の反転はどう作るのでしょうか。
Cartesian 版には、coe という操作（第 5 節の後半で紹介する Kan 操作の一種）
が備わっています。coe は「型の族に沿って値を運ぶ」操作で、「どの位置からどの位置へ運ぶか」を引数で受け取ります。この coe に、運ぶ向きを逆向きに指定して道を作り直すと、反転した道が得られます。道の合成も同様で、coe や hcom という操作に、合成したい道たちを部分的な図形として渡し、残りを埋めさせることで作ります。
つまり、こういう分担です。
CCHM では、「反転」や「合成」の意味の一部を、区間の演算（$\sim$、$\wedge$、$\vee$）が最初から知っています。
Cartesian 版では、区間は何も知りません。
その代わり、coe や hcom という操作の側に、「向きを指定して運ぶ」「部分図形から残りを埋める」という規則が備わっていて、反転も合成も、その規則を使った組み立てとして表現されます。
計算の振る舞い方で意味を決める という NuPRL の伝統的な流儀 と、この設計は響き合います。
そのため、Robert Harper や Favonia や Angiuli のように、NuPRLの伝統で育った研究者たちにとって、Cartesian 版は自然な選択 なのです。
実際、彼らが AFH 版を最初に提示した論文 Cartesian Cubical Computational Type Theory のタイトルには 「Computational」 の語がはっきり入っています。
これは装飾ではなく、「NuPRL 系の計算的な意味付けの流儀で立方体型理論をやります」という宣言 と受け取ることができるのではないでしょうか。
証明支援系 RedPRL の名前も、この文脈で読み解くことができます。
「Red」は、RedPRL や redtt の開発グループが看板として掲げる赤い立方体から、「PRL」は NuPRL の「PRL（Proof Refinement Logic）」から取られています。
（なお、なぜ「赤い」立方体を看板に掲げたのかについては、筆者が調べた限りでは判然としませんでした）
いずれにせよ、NuPRL の伝統を Cartesian 立方体型理論に接続する処理系 という自己規定が、名前に埋め込まれているわけです。
貼り合わせ（composition）の仕組みの違い
区間の構造が違うと、道と道を組み立てる仕掛けにも違いが出てきます。
「道と道を組み立てる」 とは、たとえば 次のような操作のこと です。
- 型 $A$ の中に、$x$ から $y$ への道 $p$ と、$y$ から $z$ への道 $q$ があるとき、これを組み合わせて $x$ から $z$ への道を作りたい。
- あるいは、$x$ から $y$ への道 $p$ があるとき、その反転として $y$ から $x$ への道を作りたい。
- あるいは、正方形の 3 辺（下辺・左辺・右辺）が既に決まっているとき、それらに整合するように上辺を「補完」したい。
これらは全て、部分的に決まっている図形を、整合するように残りまで埋める という同じ性格の操作としてまとめられます。
この「部分的に決まっている図形を、整合するように埋めきる」という操作を、専門用語で Kan 操作（Kan operation、あるいは Kan filling）と呼びます。
名前の由来は、20 世紀半ばに Daniel M. Kan（オランダ出身、後に MIT）という数学者が 代数トポロジーの分野 で「単体的集合において、部分的な図形を全体に伸ばせる」という条件（Kan condition）を定式化したことにあります。
📌 中上級者向け補足：圏論の「Kan 拡張」の Kan と、同じ人物か
Haskell を入り口に圏論を学ばれた方は、Kan 拡張（Kan extension）という言葉をご存知かもしれません。
圏論の中心概念のひとつで、Mac Lane の教科書には「すべての概念は Kan 拡張である」という有名な節題があるほどです。
この Kan と、本稿の Kan 操作の Kan は、同じ人物なのでしょうか。
答えは、人物は同一、概念は別物 です。
どちらも Daniel M. Kan というひとりの数学者 に由来します。
ただし、名前が付いた 概念は別のもの です。
Kan 条件・Kan 操作 は、ホモトピー論 の概念です。
単体的集合（や立方体）において「部分的な図形を全体に伸ばせる」という条件から来ています。
本稿の Kan 操作は、こちらの系譜 に連なるものです。
これに対して、Kan 拡張 は、圏論 の概念です。
関手を別の圏に沿って「最良の形で延長する」普遍的な構成のことで、本稿の Kan 操作とは別の概念 です。
ふたつの概念に同じ名前が残っているのは偶然ではありません。
Kan は組合せ的なホモトピー論の研究のなかで 随伴関手（adjoint functor）の概念そのものを導入した人物でもあり、Kan 拡張もその研究の流れから生まれました。
ホモトピー論と圏論の結び目に立っていた数学者 の名前が、両方の分野に残った。それが歴史的な事実です。
したがって、「図形を整合するように埋める」という本稿の Kan 操作の説明を、圏論の Kan拡張の知識で読み替える必要はありません。
名前の一致に気づいた方は、同一人物の別の仕事だ、と整理しておいてください。
立方体型理論 では、この Kan の発想 を立方体の側に持ち込んで、「立方体の面が部分的に決まっているとき、残りを整合するように埋める操作」として計算規則の中核に据えています。
Kan 操作という語を憶えておいてください。
今後、立方体型理論や HoTT の論文を読むと、頻繁に出てきます。
この記事の残りでも、この語を使います。
立方体型理論 では、Kan 操作 を具体的に、comp（composition）、coe（coercion、道に沿って値を運ぶ操作）、hcomp（homogeneous composition、同じ型の中での貼り合わせ）などの名前で提供します。
名前は複数ありますが、いずれも **「部分的に決まっている図形を、整合するように埋めきる」**という Kan 操作 の一種です。
📌 中上級者向け補足：comp・hcomp・coe・filling は、厳密には同一概念ではない
本文では comp、coe、hcomp などを「いずれも Kan 操作の一種」とひとまとめにしました。
共通の性格を掴むための要約としては正しいのですが、厳密には、これらは切り分けて理解すべき別々の操作です。
-
hcomp（homogeneous composition）は、同じ型の中 での合成です。
型 $A$ を固定したまま、部分的に決まった面から残りの面を作ります。
-
coe / transp（coercion、transport）は、型の族に沿って値を運ぶ 操作です。$i$ に依存して変わる型の列 $A(i)$ があるとき、$A(0)$ の値を $A(1)$ の値へ運びます。
-
comp（composition）は、この 2 つを合わせた一般形です。
CCHM の原論文では comp がプリミティブですが、Cubical Agda の実装では hcomp と transp がプリミティブで、comp はそこから導出されます。
Cartesian 系（AFH）では coe と hcom という、また別の切り分けのプリミティブを採用します。
- composition と filling の区別もあります。composition が「欠けていた面」だけを返すのに対し、filling は「埋めた内部全体」まで返します。
どの操作をプリミティブに選び、どう定式化するかは、理論と実装ごとに異なります。
「埋める」という本文の説明は、この一群の操作に共通する性格を述べたものとお読みください。
CCHM 版（De Morgan） では、Kan 操作 の代表として comp を持ち、これを区間の $\wedge$、$\vee$、$\sim$ を使って組み立てます。
区間の演算が豊かなおかげ で、たとえば「道の反転」は λ i → p (~ i) と一言で書けます し、「道の合成」も $\wedge$ と $\vee$ を組み合わせて 比較的コンパクトに 書けます。
CCTT 版（Cartesian） では、区間に $\wedge$、$\vee$、$\sim$ の演算がありません。
そのぶん、Kan 操作の側により多くの仕掛けを持たせます。
「道の反転」や「道の合成」は、区間の演算では書けず、coe や com といったプリミティブな Kan 操作の計算規則の中に組み込まれます。
区間はシンプル、Kan 操作は複雑、というトレードオフです。
どちらの流派も、最終的には「Univalence が計算できる」「HIT が扱える」という同じゴールに到達します。到達の仕方が違うだけです。
- De Morgan 版 ：「区間に道具を積んで、Kan 操作をシンプルに保つ」道
- Cartesian 版 ：「区間を素朴にして、Kan 操作に道具を積む」道
と対比することができます。
📌 中上級者向け補足：「区間に積むか、Kan 操作に積むか」は教育的な見取り図
「区間に道具を積むか、Kan 操作に道具を積むか」という本文の対比は、2 つの流派の設計思想を掴むための、この記事の中心的な見取り図です。
ただし、CCHM と CCTT の違いのすべてが、この「複雑さの置き場所」という一軸に収まるわけではありません。
実際には、両者は複数の設計要素で異なります。
土台に選ぶ立方体圏が違い、cofibration（部分的な図形を「どの条件式で切り出せるか」を定める仕組み）の設計が違い、composition の定式化が違い、意味論の与え方（圏論的モデルか、計算的意味論か）が違い、正準性の証明手法も違います。
本文の対比は、これら複数の差異のうち、初学者にとって最も見えやすい「区間の演算の有無」に光を当て、他の差異をその一軸に投影した要約です。
原論文を読み進める際は、この見取り図を入口にしつつ、各設計要素を個別に確かめていくことをお勧め します。
実装：redtt と cooltt
*CCTTの系譜 には、以下の実装 があります。
redtt — Cartesian Cubical Type Theory の証明支援系。RedPRL プロジェクトが開発。「Between the darkness and the dawn, a red cube rises!」のキャッチフレーズで知られます。研究用の処理系。
cooltt — redtt の後継として開発が進む処理系。Normalization by Evaluation（NbE）という技法を使い、より効率的な実装を目指しています。cofibrations の除去を含む、より一般的な立方体型理論をサポートします。
cart-cube — Daniel Licata らによる Cartesian 版の論文リポジトリと関連コード。
これらはいずれも研究用で、Cubical Agda ほどの規模の標準ライブラリはまだありません。しかし、Cartesian版 の理論を実際に触れるのはこれらの処理系です。
6. 「Cartesian ＝ De Morgan と別物」なのか
ここまでの議論を整理してみましょう。
「De Morgan Cubical Type Theory」 と呼ばれるのは CCHM の方で、Cartesian の方は De Morgan の演算を「持たない」 ことで区別されます。
したがって、以下のようになります。
- De Morgan 系 ＝ CCHM → Cubical Agda、cubicaltt
- Cartesian 系 ＝ CCTT / ABCFHL → redtt、cooltt、RedPRL
7. その他の派生形：BCH と AFH
前回の記事で名前だけ挙げた 2 つの流派を、もう少し丁寧に説明します。
BCH cubical（Bezem-Coquand-Huber, 2014）
最初期の立方体型理論 です。
Marc Bezem、Thierry Coquand、Simon Huber の 3 人が "A Model of Type Theory in Cubical Sets" で発表しました。
区間の構造 は、*CCHM とも CCTT とも異なる構造で、非常にシンプル です。
単に 0 と 1 を持つだけで、$\wedge$、$\vee$、$\sim$ も、対角や対称のような Cartesian 構造もありません。
この 最小限の構造 で、HoTT のモデル を cubical sets（立方体集合） で作ることができることを示した、歴史的な出発点 の論文です。
しかし、この BCH 版 は Univalence の計算的な扱いに難点 があり、そのままでは処理系として 実用化できませんでした 。
独立した実装処理系はありません（研究論文の中の理論として存在）。
CCHM や CCTT は、この BCH の後継として、「区間にもう少し構造を入れれば Univalence が計算できる」という方向で発展したもの です。
ABCFHL cubical / AFH cubical
「Cartesian Cubical Type Theory」 の中には、実は 複数の派生形 があります。
- AFH cubical（Angiuli-Favonia-Harper, 2017-2018）— Cartesian Cubical Computational Type Theory で提示された、計算的意味論 に基づく Cartesian 版。NuPRL系の伝統 に連なる。RedPRLの理論的な土台 。
- ABCFHL cubical（Angiuli-Brunerie-Coquand-Favonia-Harper-Licata）— Syntax and Models of Cartesian Cubical Type Theory で提示された、より 統語論（syntax）と圏論的モデル に力点を置いた Cartesian 版。redtt の理論的土台。
両者はどちらも Cartesian 系ですが、意味論の与え方（計算的意味論 vs 圏論的モデル）が違います。
上で挙げた「区間には $\wedge$、$\vee$、$\sim$ を入れず、対角・対称・退化だけ」という設計思想は共通しています。
8. 分類軸の抽出 — 区間の構造と計算規則
ここまでの整理を、「区間 $I$ に何を入れるか」「区間の要素の間にどんな計算規則を持たせるか」 という 2つの軸 で表にします。
| 流派 | 区間 $I$ の演算 | 区間の等式規則 | Kan 操作の性格 | 代表的な実装 |
|---|---|---|---|---|
| BCH（2014） | なし（0 と 1 と変数のみ） | 最小限 | Univalence の計算的な扱いに難点が残る | なし（理論のみ） |
| De Morgan 系（CCHM、2017） | $\wedge$、$\vee$、$\sim$ | De Morgan 代数の等式一式 | 区間の演算を活用でき、比較的シンプル | Cubical Agda、cubicaltt |
| Cartesian 系（CCTT / AFH / ABCFHL、2017〜） | なし（対角・対称・退化のみ） | 最小限 | 反転・合成まで Kan 操作側に集約され、仕掛けが厚い | redtt、cooltt、RedPRL |
9. 複数の証明支援系を、この分類軸で並べる
ここまでの分類軸を使うと、序で挙げた複数の処理系がきれいに整理できます。
「区間の構造」と「その系譜」という 2 軸で並べます。
| 処理系 | 背後の理論（区間の構造） | 系譜・性格 |
|---|---|---|
| Cubical Agda | CCHM（De Morgan 代数） | Agda の拡張。HoTT の実用的形式化の現在の主力。標準ライブラリ agda/cubical |
| cubicaltt | CCHM（De Morgan 代数） | CCHM の初期プロトタイプ。Haskell 製の研究用処理系 |
| redtt | ABCFHL（Cartesian） | RedPRL プロジェクト。研究用 |
| cooltt | Cartesian 系（redtt の後継） | NbE による効率的な実装を目指す。研究用 |
| RedPRL | AFH（Cartesian、計算的意味論） | NuPRL の伝統を立方体型理論に接続する処理系 |
| NuPRL | 立方体型理論以前（計算的意味付けの源流） | 1980 年代からの、計算による意味付けの流派の原点 |
| Arend | 独自（区間型はあるが、Univalence を計算可能にする追加構造は持たない） | JetBrains 製。HoTT を土台にした独自の折衷案 |
ここで Arend の位置づけは注目に値します。
nLab の記述によれば、Arend は HoTT を土台にしつつ、立方体型理論 に似た 区間 型 を持ちます。
この 区間型 のおかげで、Arend では Univalence（一価性公理。「型 A と型 B のあいだに同値があるなら、A と B は等しい」という HoTT の中心原理）を、公理として仮定するのではなく、定理として証明できます 。
📌 振り返り：Univalence とは何だったか
Univalence については、3 本目の記事の第 7 節で導入したきりでした。
ここで手短に振り返っておきます。
型理論には、 宇宙（型そのものを点として並べた特別な型）があります。
宇宙の中では、型 $A$ と型 $B$ のあいだの「等しさ」$A ≡ B$ を問うことができます。
一方、型どうしには 同値（$A \simeq B$。$A$ の値と $B$ の値を、情報を失わずに行き来できる対応）という関係もあります。
Univalence は、この 2 つを結びつける原理です ── 宇宙における等しさ $A ≡ B$ と、同値 $A \simeq B$ とは、それ自体が同値である、と主張します。
これは、数学者が昔から使ってきた作法 ── 「同型な構造は、区別せずに同じものとして扱ってよい」 ── を、型理論の規則として正面から認めたもの です。
集合論の上では技術的に成り立たないこの作法が、HoTT では原理として成立します。型を空間として読む世界観の、要の位置にある原理 です。
2 本目の記事の例で言えば、Bool から Bool への同値は 2 つありました（そのままの対応と、True と False の入れ替え）。Univalence は、この 2 つの同値を、宇宙の中の Bool から Bool への 2 本の道として空間に登録します。
ただし、CCHM や CCTT のように、Univalence を含む 項の計算（canonicity の意味での簡約）を保証する Kan 操作一式までは備えていません 。
CCHM でも CCTT でもない、独自の折衷案です。
なお、これは「第３の流派」という積極的な分類ではなく、本記事が採用した「区間の構造と Univalence の計算」という分類軸の上では独立した位置にある、という整理です。
なお、本稿の執筆者は、最近、Arend の入門者向け解説連載シリーズ(全 7 回＋補足記事)を公開済みです。
Arend にご関心をお持ちの方は、本稿と併せてご一読ください。
📚 Arend 入門連載(全 7 回＋補足記事)の一覧
https://qiita.com/etale_cohomology/items/0abc51fe5e2a3eb02f08
https://qiita.com/etale_cohomology/items/8126e8eae37eefdf86f6
https://qiita.com/etale_cohomology/items/61193814df628ace0bf7
https://qiita.com/etale_cohomology/items/679faed081b6cd8be97c
https://qiita.com/etale_cohomology/items/865503fbcfc68b23d759
https://qiita.com/etale_cohomology/items/e80c18c3c35460f316b7
https://qiita.com/etale_cohomology/items/543ba6180aef46a21cbe
https://qiita.com/etale_cohomology/items/3b332aa9c22ebe838c5c
なお、この地図に Lean と Rocq が登場しない ことを不思議に思われた方もおられるかもしれません。
前回の記事で見たとおり、両者は CIC（Calculus of Inductive Constructions、帰納的構成計算。Rocq や Lean の土台となっている型理論）の枝の、UIP（Uniqueness of Identity Proofs、恒等証明の一意性。「等しさの証明はどの 2 つも等しい」という性質）が成り立つ側にいる処理系です。
すべての型が h-set に見える世界では、そもそも Univalence を計算させるという動機自体が生じない ため、区間の設計を競うこの地図の外側にいるのです。
（Rocq の上には HoTT ライブラリや UniMath がありますが、これらは Univalence を計算しない公理として仮定する、立方体以前のスタイルです）。
📌 中上級者向け補足：「地図の外」は「HoTT と無関係」という意味ではない
Lean と Rocq を「地図の外」と書きましたが、この表現は「両者が HoTT や Univalence と無関係だ」という意味ではありません。
3 つのレイヤーを区別してください。
第 1 のレイヤーは、カーネル（型検査の核）の標準的な性質 です。
Lean と Rocq のカーネルは UIP が成り立つ側にいます。本文で述べたのはこの層の話です。
第 2 のレイヤーは、その上で公理を仮定して展開する研究 です。
Rocq の上には Coq-HoTT ライブラリや UniMath という大規模な HoTT の形式化があり、Univalence を公理として仮定して豊かな数学を展開しています。
歴史的には Lean 2 にも HoTT モードがありました（3 本目の記事の第 6 節参照）。この層では、Lean・Rocq は HoTT 研究の現役の舞台です。
第 3 のレイヤーは、カーネル自体に Univalence の計算規則を組み込む設計 です。区間 $I$ を持ち、Glue や V 型に計算規則を与える ── 本記事の主題である立方体型理論 の層です。
本記事の「地図」は、この第 3 のレイヤーだけ を ── 区間にどの構造を入れるかという一点 を ── 軸にした分類です。
Lean と Rocq が「地図の外」にいるのは、この分類軸の上に乗らないという意味であって、HoTT の研究対象として無縁だという意味ではありません 。
10. どの流派を選ぶかは、目的次第
ここまで見てきた 2 つ（正確には 4 つ以上ある）の流派は、どれが「正しい」というものではありません。
目的によって使い分けが生じます。
-
HoTT の実用的な形式化をしたいなら、Cubical Agda（De Morgan 系）が現時点で最も成熟しています。標準ライブラリが豊富で、球面、トーラス、コホモロジー、Blakers-Massey の定理などの現代的な結果が実際に形式化されています。
-
理論的な研究、特に計算的意味論の側からアプローチしたいなら、redtt や cooltt（Cartesian 系）が向いています。区間の構造がシンプルなぶん、理論的な性質を証明しやすい。NuPRL の伝統に連なる研究者にとって、Cartesian 版は思想的に近い。
-
HoTT を教育目的で触ってみたいなら、Agda + agda/cubical ライブラリが最も入りやすいでしょう。2 本目の記事の第 6 節で見た $S^1$ の定義は、そのままこの環境で走ります。
- JetBrains の IDE 環境で HoTT を触ってみたいなら、Arend という選択もあります。ただし Univalence の計算については独自の設計です。
ここでひとつ、注意点があります。
実装の成熟度に差がある（Cubical Agda は実用水準、redtt や cooltt は研究用）ことから、「Cartesian 系は De Morgan 系の未完成な簡易版」と整理したくなるかもしれませんが、それは誤った理解の仕方です。
成熟度の差は、流派の理論的な優劣ではなく、投入された開発資源と、各プロジェクトが掲げる目的の差 に起因する差異です。
理論としては、両者は同じゴールに別の道で到達した、対等な設計 です。
11. 前回の記事の家系図を、Cubical の下だけ拡張する
前回の記事の家系図の、2013 年以降の部分だけを拡大すると、次のようになります。
2013年 HoTT Book 刊行
│
│ (Univalence を計算できる形にする問題)
│
2014年 BCH cubical (Bezem-Coquand-Huber)
│ ── 区間は最小限、実装処理系なし
│
├──────────────────────────────┐
│ │
2017年 CCHM cubical AFH / ABCFHL cubical
(Cohen-Coquand-Huber-Mörtberg) (Angiuli-Favonia-Harper ほか)
│ De Morgan 代数 │ Cartesian 構造
│ ∧, ∨, ~ を持つ │ ∧, ∨, ~ は持たない
│ │
│ 実装: │ 実装:
│ ├ cubicaltt (Haskell製) │ ├ redtt
2019年 │ └ Cubical Agda │ ├ cooltt
│ │ └ RedPRL (AFH 系)
│ │
└───── どちらも: ─┘
「Univalence が計算できる」
「HIT が扱える」
に到達
なお、この図は歴史的・概念的な 見取り図 です。
BCH・CCHM・Cartesian 系のあいだには、区間の構造だけでなく、統語論、土台の立方体圏、composition の定式化、意味論の与え方にも違いがあり、各理論の数学的な発展関係を 一本の線で完全に表したものではありません 。
12. まとめ — 区間の構造という一点に光を当てる意味
長い散歩でしたが、要点を3つに絞ります。
第 1 に、Cubical Type Theory は 1 つではありません。
区間 $I$ にどんな数学的構造を持たせるかによって、少なくとも De Morgan 系と Cartesian 系という 2 つの主要な流派に分かれます。
これは技術的な瑣末な違いではなく、理論全体の見通しと、実装の性格を分ける根本的な選択です。
第 2 に、この区間の構造という1点が、複数の処理系を分類する軸になります。 Cubical Agda と redtt が別々の処理系として存在するのは、単なる開発者の趣味の違いではなく、背後にある立方体型理論の流派が違うからです。
この軸を持っていると、なぜ処理系が複数あるのか、それぞれがどんな性格を持つのか を見通すことができるようになります。
第 3 に、前回までの記事で見た「Univalence を計算できる形にする」という目標は、複数の解答を持ちます。
CCHM は「区間に De Morgan 構造を入れる」という方法で、CCTT は「区間はシンプルに保ち、貼り合わせ操作の側で工夫する」という方法で、それぞれ同じゴールに到達 しました。
数学の目標に対して、複数の技術的解決があり、それぞれに実装が対応する。
これが 型理論 の面白いところです。
ここまで来ると、前回の記事で見た 「Cubical Agda」 という 1 語の背後に、CCHM という具体的な流派の選択があり、その選択によって cubicaltt や Cubical Agda が実装され、その一方で、redtt や cooltt という 別系統の処理系が並行して発展している、という景色 が見えると思います。
「型を空間として計算可能に扱う」というひとつの目標 を、複数の異なる区間の設計 で追いかけている。これが、2013 年から 2020 年代までの立方体型理論の風景 です。
13. 旅の終わりに — 4 本の記事で登ってきた視座
この記事は、数珠つなぎでお届けしてきた 4 本の単独記事の、最終回でした。
最後に、4 本ぶんの旅を振り返って締めくくります。
初回の記事で、私たちは 数学の世界 から出発しました。
対象を空間の中の点として置き、「等しい」を 2 点をつなぐ道として描く ── 池のある広場では取り替えのきかない道が何本も並び立ち、等しさの上に等しさの階層が積み上がる、という ホモトピー理論の世界観 です。
2 本目の記事で、その眼差しを プログラミング に向けました。
皆様がふだん書いておられる Haskell の Int や [Char] が、点と道の集まりとしての空間に見えること。そして円周 $S^1$ のような「退屈じゃない空間」を、データ型として書ける言語があることを見ました。
3 本目の記事で、その「書ける・書けない」の分かれ目が、型理論の家系図 のどこに立っているかの違いだと突き止めました。単純型付きラムダ計算 から Martin-Löf 型理論 を経て HoTT へ ── そして、Univalence を計算できる形にするために 立方体型理論 が生まれるところまで。
そして本記事で、その 立方体型理論 の心臓部 ── 区間 $I$ に どの数学的構造を入れるか ── という、現在も設計・研究が競われている最前線 に立ちました。
振り返ると、4 本を貫いていたのは、「等しさ」をどう扱うかという一つの問いを、世界観・データ型・言語設計・計算規則という 4 つの解像度で見直していく、という一本の道でした。
この視座は、鑑賞用ではありません。
たとえば、皆様が今後 Cubical Agda に触れられるとき、その背後に CCHM という区間設計の選択があると知っていれば、~ i や hcomp がなぜその形をしているのかが見通せます。
redtt のドキュメントで区間の演算が見つからなくても、欠陥ではなく Cartesian という思想だと分かります。
道具の設計思想まで読める目は、道具を選ぶ目に変わります。
それが、この4本の記事が皆様にお渡ししたかったものです。
この先へ進みたい方への道しるべを、順序つきで置いておきます。
- まず手を動かすなら、Agda に
--cubicalオプションを付けて、agda/cubical ライブラリのCubical.Foundations.Preludeから触るのが最短です。2 本目の記事の $S^1$ が、そのまま走ります。
- 理論を固めるなら、HoTT Book（無料公開）の第 1・2・6 章、続いて Rijke の教科書（arXiv:2212.11082）へ。
- 流派の原典に触れるなら、本文に挙げた CCHM の論文（De Morgan 系）と ABCFHL の論文（Cartesian 系）を読み比べるのが、本記事の内容の最良の復習になります。
長い散歩にお付き合いいただき、ありがとうございました。
池のある広場から歩き始めた道は、区間の設計図が並ぶ工房まで続いていました。
この先の道は、皆様のお手元の処理系の中に続いています。
補足：本文で立ち入らなかった技術的な点
- CCHM の Glue 型と、Cartesian 系の V 型（V type、Universe 型ではなく Voevodsky に因む名前ではあるが別物）の違いは、Univalence の計算的な扱いにおいて実質的に重要ですが、初学者向けの記事の範囲を超えるため省略しました。詳しくは Angiuli らの論文の第 5 節をご参照ください。
- 立方体型理論には他にも XTT（Sterling-Angiuli, 2019）や cartesian cubical with connections など、複数の派生形があります。この記事では 2 つの主要な流派に集中しました。
- RedPRL は厳密には「立方体型理論を実装した処理系」というより、「計算的立方体型意味論を持つ証明支援系」で、伝統的な NuPRL の後継としての性格が強いことも付記しておきます。
- 「Univalence が計算できる」の技術的意味である canonicity は、CCHM 版については Huber、Cartesian 版については Angiuli らによって別々に証明されました。両者の証明手法は違いますが、結論は共通です。
📌 中上級者向け補足：「計算的立方体型意味論を持つ証明支援系」とは何か
本文のこの一文を、もう一段くわしく説明します。
鍵は、第 5 節で紹介した「流儀 B ── 型を計算の振る舞い方として決める立場」です。
ふつうの証明支援系（Agda、Rocq、Lean など）は、次の順序で作られています。
まず、型理論を規則の一覧（構文と推論規則）として定めます。
次に、その規則どおりに項を検査するプログラムとして、処理系を実装します。
この順序では、理論が先、計算は後 です。
「立方体型理論を実装した処理系」という言い方は、この順序を前提にしています。
NuPRL の伝統は、順序が逆です。
まず、プログラムがどう動くか（簡約の規則）だけを決めます。
型は、その上で「こういう振る舞いをするプログラムの集まり」として、後から定義されます。
たとえば「$x$ から $y$ への道」という型は、「区間の変数を受け取って動き、端で $x$ と $y$ に簡約されるプログラムの集まり」です。
この、計算が先、型は後 という意味の与え方が、計算的意味論 です。
Angiuli・Favonia・Harper は、この流儀で立方体（Cartesian cubical）の意味論を作りました。
これが本文で AFH と呼んできた仕事で、論文の題名 Cartesian Cubical Computational Type Theory の Computational は、この流儀の宣言です。
RedPRL は、この意味論の上に建てられた証明支援系です。
RedPRL が 検査しているのは、「この項は規則の一覧に従っているか」ではなく、「この項は、計算的意味論の意味で、この型の住人として振る舞うか」 です。
それゆえに、本稿本文では、RedPRL を 「立方体型理論を実装した処理系」と呼ぶより、「計算的立方体型意味論を持つ証明支援系」と呼ぶ方が正確だ、と述べているのです。
NuPRL が 1980 年代からやってきたことを、立方体の世界で続けている ── これが 「伝統的な NuPRL の後継」という位置づけの意味 です。
なお、この流儀には実務上の帰結もあります。
型が「規則の一覧」ではなく「振る舞いの集まり」で定義される ため、後から新しい型を意味論の側に付け足すことが、規則一覧の作り直しなしにできます 。
正準性に相当する性質が理論の組み立てに最初から織り込まれることは、前のコラム（「Univalence が計算できる」の意味）で述べたとおりです。
📌 中上級者向け補足：「Univalence が計算できる」の意味と、「証明が見通しやすい」の意味
2 つの言い回しについて、誤読を防ぐ注意を添えます。
第 1 に、「Univalence が計算できる」の意味です。
これは「Univalence という定理を、普通のプログラムのように評価できる」という単純な意味ではありません。
正確には、Univalence に対応する構成（CCHM の Glue 型、Cartesian 系の V 型）に 計算規則が与えられており、それを含む閉じた項が標準形へ還元されること ── すなわち canonicity（正準性） が成り立つこと、を指します。
3本目の記事の第 7.5 節の補足で触れた話の、流派をまたいだ再確認です。normalization（開いた項の正規化）まで含めた性質は、canonicity とはまた別の定理として研究されています。
第 2 に、本文§5 の「CCTT のほうが canonicity の証明が見通しやすいと考える研究者もいる」の読み方です。
これは「構造が単純だから証明が簡単」という一般論ではありません。
証明の見通しは、どの定式化・どの意味論・どの証明技法を比べるかで変わります。
たとえば Angiuli らの 計算的意味論 のアプローチでは、型の意味が「計算の振る舞い」で最初から与えられる ため、正準性に相当する性質が理論の組み立てそのものに織り込まれる ── という、証明の難易度以前に 問いの立て方が異なる 側面があります。
本文の一文は、そうした研究上の傾向・相性の話としてお読みください。
📌 中上級者向け補足：本文の水準を超える 3 つの論点への入口
本文で名前だけ挙げた（または挙げなかった）論点のうち、中上級の読者に向けて、もう一歩だけ踏み込んだ入口を 3 つ置いておきます。
第 1 に、XTT と、connections 付き Cartesian ── 流派の地図はもっと細かい。
本文は De Morgan 系と Cartesian 系の 2 大流派に集中しましたが、区間の設計の選択肢は実際には格子状に広がっています。
Cartesian の土台（対角・対称・退化）に、反転 $\sim$ は入れずに $\wedge$ と $\vee$（connections）だけを足す、という中間的な設計も研究されています。
また XTT（Sterling-Angiuli-Gratzer, 2019）は、立方体の機構を逆向きに使う興味深い例です。
区間と境界分離の仕組みを使って、Univalence のためではなく、UIP が成り立つ「退屈な」等しさを、公理なしの計算規則として実現する 型理論で、「立方体の道具立て ＝ HoTT のためのもの」という思い込みを壊してくれます。
つまり、区間に何を入れるかという本文の分類軸は、2 択ではなく、目的に応じて部品を選ぶ設計空間なのです。
第 2 に、Kan 操作の計算規則の具体形 ── comp の型はどんな顔をしているか。
本文では Kan 操作を「部分的に決まった図形を整合するように埋める操作」とだけ述べました。
その型の形だけ、雰囲気を示しておきます。Cubical Agda の中核的なプリミティブ hcomp は、おおよそ次の形をしています。
hcomp : {φ : I} (u : I → Partial φ A) (u0 : A [ φ ↦ u i0 ]) → A
ポイントは 2 つあります。
ひとつは Partial φ A ── 「区間の条件 φ が成り立つ面の上でだけ定義された、部分的な要素」を表す型で、「3 辺だけ決まった正方形」のような部分図形を型として書くための仕掛けです。
もうひとつは A [ φ ↦ u i0 ] ── 「境界条件つきの型」で、埋めた結果が、決まっていた面と食い違わないことを型のレベルで強制します。
整合するように埋める」という日本語が、境界条件つきの型として厳密に定式化されているわけです。この 2 つの構文（partial elements と cofibration）が、立方体型理論の論文を読むときの最初の関門であり、鍵でもあります。
第 3 に、有向型理論との関係 ── 区間に「向き」を入れたらどうなるか。
本文の分類軸を一段押し広げると、こういう問いが立ちます。
「区間 $I$ に、De Morgan 代数でも Cartesian 構造でもなく、順序（0 から 1 への向き）を入れたらどうなるか」。
これが 有向型理論（directed type theory）の入口です。
向きのある区間 から作られる道は逆にたどれないので、可逆な等しさではなく、圏の射 のような 向きのある関係 を型理論の中で直接扱えるようになります。
Riehl と Shulman の simplicial HoTT がこの方向の代表で、筆者の別の記事で正面から扱っています。
「区間の構造の選択が理論の性格を決める」という本記事の主題の、最も劇的な実例と言えます。
（関連記事）
https://qiita.com/etale_cohomology/items/e7c5778802b40f15b277
今後のロードマップ
数珠つなぎの単独記事の全体像は、次のとおりです。本記事が最終回です。