高阶归纳类型

普通归纳声明规定“有哪些点”；HIT 还能在生成点的同时规定“哪些点由指定路径粘在一起”，并继续规定路径之间的面或更高相干。圆周不是先生成一个点再从外部证明某条自等式，而是把基本回路列为生成结构。消去一个 HIT 时，目标不仅要接收每个点构造子，还要证明所给分支尊重所有粘合路径。

这使 quotient、截断和拓扑空间获得统一的内部描述。商类型可用点构造子注入元素，再用路径构造子识别关系中的两点；集合截断还要加入更高构造，压平任意平行路径。构造签名决定最小自由对象，归纳原理则表达从该自由对象映出时必须保存的全部结构。

用圆周递归原理定义二次绕圈映射 $d_2:{\mathbb{S}}^1\to {\mathbb{S}}^1$。点数据取 $d_2(\mathsf{base})=\mathsf{base}$，路径数据取回路连接

于是递归原理给出 $d_2$，并有

这不是把输入点复制两次；圆周只有一个生成点，映射的“次数”完全记录在它对生成路径的作用上。若只给 $d_2(\mathsf{base})$ 而漏掉回路证据，定义不完整，因为目标点可带许多不同自路径。

边界首先是 computation strength。公理式 HIT 的路径 β-law若只有 propositional equality，包含该消去子的闭项不一定按判断归约暴露预期路径；模型一致性也不自动带来严格 canonicity。立方类型论能为圆周、悬挂、pushout 等许多 HIT 提供计算规则，但需要 composition/coherence machinery，不能据此断言任意写下的高阶构造签名都被实现。边界其次是严格正性与相干：负位置递归、端点引用尚未合法生成的数据或缺失高维 coherence，可能使形成规则不良。

HIT 可内部构造圆周、球面、悬挂、pushout、quotient 与 truncation，并通过其归纳原理推导同伦群、encode–decode 证明和结构同一原则。程序层面，它为“数据加方程”提供高阶版本：计算不仅按点构造器分支，还要证明函数尊重生成等式，避免把 quotient representative 的选择泄露到结果。

HIT 与单价性经常共同出现，却没有 special-case 关系。单价性描述宇宙中等价与路径的联系；HIT 描述由点和路径自由生成新类型。可以研究带 HIT 而不公设 univalence 的理论，也可以先讨论单价宇宙而不加入一般 HIT。任何实现都应分别列出支持哪些构造签名、点/路径 computation 是判断式还是命题式，以及相应 normalization/canonicity 已证明到何种范围。