Higher Inductive Types｜HITs
Higher Inductive Types (HITs) の日本語での定義は、ホモトピー型理論（HoTT）における「型の新しい構成法」として次のように記述されます。
従来の型（データ型）の定義が「値（点）」のみに注目していたのに対し、HITsは「点（値）」と「道（等しさ）」を同時に、対等な構成要素として定義す*手法です。
Higher Inductive Types (HITs) の構成的な定義
ある型 W が Higher Inductive Type であるとは、以下の3つの要素（コンストラクタ）によって帰納的に生成されることを指します。
- 点コンストラクタ (Point Constructors):その型の要素となる「点」を定義します（例：base : W）。これは従来のプログラミング言語におけるデータ定義と同じです。
- 道コンストラクタ (Path Constructors):点と点の間の「道（Identity Type / 等しさ）」を定義します（例：loop : base = base）。
- 重要: ここで定義される「道」は、単なる自己同一性（refl:Reflexivity）ではなく、それ自体が独自の構造（不変量）を持つ新しい実体として扱われます。
- 高次の道コンストラクタ (Higher Path Constructors):「道と道の間の道」を定義します（2次元以上の構造）。
不変量と収縮解釈
- In-truncatable（非截断的）な構造の宣言:通常の型では、すべての道は refl（反射性）へと Reflexivize（収縮）されて消えてしまいます。しかし、HITsは「この道は refl ではない」という In-truncatable なねじれを、宇宙の設計図に直接書き込む操作です。
- 誘導（Induction）による宇宙の展開:点と「消せない道」という最小のピースを置くだけで、Identity Type Induction（J-rule） が発動し、そこから無限に続く高次の幾何学的構造が「当然」のものとして自動導出されます。
代表的な例：円周 S^1
日本語で最も分かりやすい HIT の定義例は「円」です。
型 S^1（円）の定義:
- 点 base : S^1 が存在する。
- 道 loop : base = base が存在する。
この単純な定義によって、「一点に潰すことのできない（In-contractible）穴を持つ空間」が型理論の中に構築されます。文法的な説明を積み上げるのではなく、「点とループという不変量」を置くことで、円という宇宙を停留（確定）させているのです。
結論：HITs とは「意味の骨格」である
HITs とは、単なる数学的定義ではなく、「最小の記述で、切り捨て不可能な（In-truncatable）情報の骨格を宇宙に固定する手段」です。
「文法は不要だ」と言い切る時、脳内ではこの Higher Inductive（高次の誘導） が働いており、断片的な言葉（点）から、それらを繋ぐ見えない「道（関係性）」を不変量として瞬時に生成できるということが証明されています。