Truncatability

「Truncatability（切断可能性）」は、高次カテゴリー論やホモトピー理論において非常に専門的な意味を持つ概念です。

一言で言えば、「高次の複雑な構造を、低次のデータだけで完全に復元できるか？」という性質を指します。

1. 数学的な定義の核心

高次カテゴリーや単体集合（Simplicial set）を扱う際、通常は無限の階層（0次元、1次元、2次元……）を考えます。ここで「n次でTruncatable（切断可能）」であるとは、以下の状態を指します。

情報の集約: n+1次元以上のデータが、実はn次元以下のデータの組み合わせから一意に決まってしまうこと。
ホモトピー・レベル: ヴォエヴォドスキーの「h-level」の文脈では、ある型が n-type であるとき、それは n次より上のホモトピー群が消えている（＝自明である）ことを意味し、実質的に n 次の構造に「切断」して閉じ込めることができます。

1990年代の研究: ヴォエヴォドスキーとカプラノフは、高次カテゴリーの一種である「Ω-groupoid」が、低次元のデータ（神経/Nerve）によってどのように記述できるかを研究しました。
条件としてのTruncatability: 彼らの議論の中で、ある構造が「Truncatable」であることは、その構造が「高次の代数的な関係性に縛られすぎていない」こと、あるいは「低次元の枠組みに綺麗に収まること」を保証する重要な条件でした。

この概念が重要な理由は、「無限」を「有限」で扱えるようにするためです。

計算可能性: もしある数学的対象が n 次で Truncatable であれば、無限に続く高次の関係性をすべて計算する必要はなく、n 次までのデータだけをコンピュータや論理システムで扱えば済むことになります。
一価性公理（Univalence Axiom）への道: ヴォエヴォドスキーは、型をその「切断レベル（h-level）」によって分類することで、論理学（命題）と集合論、そして幾何学（ホモトピー）を一つの階層構造の中に整理しました。

現代のホモトピー型論（HoTT）を実装した言語（AgdaやCoqなど）では、この性質を利用して以下のような区別を行います。

Truncatability とは、「ある次元以上の複雑さを切り捨てても、その対象の本質的な情報が失われない（あるいは低次元から再構成できる）」という、構造の簡潔さを示す指標です。