高阶归纳类型

在类型论中, 高阶归纳类型指一种归纳类型的推广, 其中构造子的返回类型除了类型本身, 还可以将该类型应用到模态中.

换言之, 高阶归纳类型 $D$ 可以由如下两类构造子生成:

•	一般的归纳类型的构造子, 接受一些参数, 返回 $D$,
•	高阶的构造子, 接受一些参数, 返回 $M(D)$, 其中 $M:\mathcal{U}\to \mathcal{U}$ 是某个模态.

在用模式匹配定义函数 $f:D\to X$ 的时候, 需要给出如下信息:

•	对于一般的构造子 $c:C\to D$, 需要给出 $f(cx)=u$ 中的 $u$, 它需要满足的规则如下: $$x:C⊢u:X$$
•	对于高阶的构造子 $p:P\to D$, 需要给出 $M_f(px)=w$ 中的 $w$, 它需要满足的规则如下: $$x:P⊢w:M(X)$$

1例子

•	同伦类型论中, 高阶归纳类型 (同伦类型论) 特指使用相等类型模态的高阶归纳类型.

术语翻译

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