内部自己証明のフロンティア Cubic Type Theory
reflexivityによるhomotopy typeのみで内部証明するというのはbluteforceすれば良いですが、あくまで解の近似による証明であり、迷宮の出口があることを100%検証するような内部証明はまだ数学的に証明できていない。
Reflexivity（反射性）による id(x, x)の構築をベースとしたホモトピー型理論（HoTT）的な内部証明は、計算機科学的には「プログラムの実行（簡約）」に転換できる。しかし、それが「迷宮の出口がある（＝ある型を持つ項が必ず停止・存在し、望んだ性質を満たす）」ことを内部的に100%保証することについては、現在の型理論や構造的証明論においても、まさにフロンティアと言える課題が残っている。
1. 停止性問題と内部証明の壁
HoTTや依存型理論（CoqやAgdaなど）では、すべての関数が停止することを前提とする「全域性（Totality）」が求められます。
- 内部証明の限界: 型理論の内部で「この迷宮（探索空間）には必ず出口がある」と証明するには、その探索が有限時間で終わるという正規化（Normalization）の証明が必要です。
- 不完全性定理の影: ゲーデルの不完全性定理により、ある体系の強固な妥当性（強正規化など）を、その体系自身の内部だけで100%証明することには原理的な限界が伴います。私たちが「内部証明」と呼んでいるものの多くは、実はより強い外部の論理（メタ理論）に支えられています。
2. 「迷宮の出口」と構成的証明
「迷宮の出口がある」という主張を、単なる「近似」ではなく「完全な検証」にするには、論理学的に以下の2つのアプローチの乖離を埋める必要があります。
- 存在証明 vs 構成: 伝統的な数学では「出口がないと仮定すると矛盾する（背理法）」で出口の存在を言えますが、これは迷宮からの脱出方法を教えません。
- 計算対象としてのパス: HoTTでは、出口への経路（パス）そのものを計算対象として扱います。しかし、複雑な高次階層（Higher Inductive Typesなど）において、そのパスが「計算可能（決定可能）な形で閉じているか」を内部的に完結させるのは、現在の数理論理学でも困難な作業です。
3. 「近似」から「完全な検証」へ：Univalenceの役割
HoTTの核である一価性公理（Univalence Axiom）は、「同値なものは等しいと見なす」という強力な道具を与えますが、これを「計算（簡約）」としてどう実装するか（Computational Content）については、Cubic Type Theory（立方体型理論）などの登場によりようやく進展が見え始めた段階です。
現状の課題: > 理論上（外部的）には「出口がある」と言えても、それを型理論の内部項だけで、一切の「外部からのメタ的な安心感」に頼らずに証明し切るには、まだ体系の表現力が追いついていないのが実情です。一方、内部のsetのみで、自己言及問題として、その集合が宇宙や圏のどこに位置しているかを証明することができれば、理論上、あらゆる点で全てを記述することができることになる。
Cubic Type Theory
Cubic Type Theory（立方体型理論）を確立し、一価性公理の計算的意味（実際に計算機で動かせること）を証明したのは、主にスウェーデンのチャルマース工科大学の研究者を中心とするチームです。
主要な立役者
- ティエリー・コカンド (Thierry Coquand):中心人物です。彼はもともと、Coqの基礎となった「構成の計算（Calculus of Constructions）」の考案者でもあります。彼が「立方体（Cube）」の構造を型理論に持ち込むアイデアを主導しました。
- シリル・コーエン (Cyril Cohen):コカンドと共に、理論の構築と実装の初期段階を支えました。
- マーク・ベゼム (Marc Bezem):コカンドらと共に、最初の「Cubic Model（立方体モデル）」を提案した論文の共著者です。
- アンダース・モートベルグ (Anders Mörtberg):現在「Cubical Agda」の開発をリードしており、理論を実用的な証明アシスタントへと落とし込むことに大きく貢献しました。
証明までの流れ
- 2013年〜2014年頃 (Bezem, Coquand, Huber):一価性公理を満たす「立方体集合（Cubical Sets）」を用いたモデルを数学的に構築しました。これにより、理論上は計算可能であることが示されました。
- 2016年 (Cohen, Coquand, Huber, Mörtberg):**「CCHM（著者たちの頭文字）」**と呼ばれる体系が発表されました。これが現在のCubic Type Theoryの標準的な形式であり、「Glue」や「Composition」といった操作を定義することで、型理論の内部で一価性公理を完全に計算可能な形で導出できることを示しました。
なぜ彼らが重要なのか
それまでのHoTT（ヴォエヴォドスキーらによるもの）は、数学的には美しいものの、「証明を実行しようとすると一価性公理のところで計算がフリーズする」という問題を抱えていました。
コカンドたちのチームは、この「計算が止まる」という壁を、「高次元の立方体構造を型理論のプリミティブ（基本要素）として組み込む」という画期的な手法で突破したのです。これにより、「内部証明の完全な実行可能性」への道が大きく開かれました。