高阶归纳类型 (同伦类型论)

关于其它含义, 请参见 “高阶归纳类型”.

在同伦类型论中, 高阶归纳类型特指允许构造子的返回类型是归纳类型上的相等类型、这些相等类型上的相等类型、等等的归纳类型. 此处 “$X$ 上的相等类型” 指对于某些 $x,y:X$ 而言的 ${\mathrm{Id}}_X(x,y)$.

例如, 考虑如下类型:

•	类型定义为 $S^1$.
•	构造子 $\mathrm{base}:S^1$,
•	构造子 $\mathrm{loop}:\mathrm{Id}(\mathrm{base},\mathrm{base})$.

它的消去规则或者说模式匹配需要确保: $\mathrm{base}$ 被映射到某个值 $x:X$、$\mathrm{loop}$ 被映射到某个相等证明 ${\mathrm{Id}}_X(x,x)$.

以上类型便是圆周 (同伦类型论), 是典型的高阶归纳类型.

1定义

高阶归纳类型目前没有非常精准的定义, 只有一些具体的例子. 这是因为严格正性的条件还没有被很好地推广到高阶归纳类型的情况.

2例子

•	圆周 (同伦类型论)
•	区间 (同伦类型论)
•	纬悬 (同伦类型论)
•	整数 (同伦类型论) 的部分构造
•	逻辑截断类型、截断类型

3相关概念

•

立方归纳类型

术语翻译

高阶归纳类型 • 英文 higher inductive type • 法文 type inductif supérieur • 拉丁文 typus inductivus superior