截断类型

$\mathbf{n}$-截断类型是一种高阶归纳类型. 在$n$-类型的视角下, 截断类型即是在 $n$ 层截断某个类型. 它是逻辑截断类型的推广.

1类型规则

$$\frac{\Gamma ⊢A}{\Gamma ⊢|A{|}_n}$$

构造规则

需要用到 $\mathrm{isHLvl}$, 在$n$-类型里有定义.

$$\frac{\Gamma ⊢a:A}{\Gamma ⊢\Vert a{\Vert }_n:|A{|}_n}\Gamma ⊢\mathrm{trunc}:\mathrm{isHLvl}(|A{|}_n,n)$$

消去规则

$n$-截断类型只能被映射到其它的 $n$-类型, 这和逻辑截断类型是一致的.

$$\frac{\Gamma ⊢f:A\to B\Gamma ⊢p:\mathrm{isHLvl}(B,n)}{\Gamma ⊢{\mathrm{rec}}_{|A{|}_n}(f,p):A\to B}$$

计算规则:

$$\begin{array}{rl}{\mathrm{rec}}_{|A{|}_n}(f,p)(\Vert a{\Vert }_n)& =f(a):B\\ \underset{一共n+2次\mathrm{ap}}{\underbrace{{\mathrm{ap}}_{{\mathrm{ap}}_{\cdots {\mathrm{ap}}_{{\mathrm{rec}}_{|A{|}_n}(f,p)}}}}}(\mathrm{trunc}(\cdots ))& =p(\cdots ):\cdots \end{array}$$

第二条规则由于 $n$-类型本身的定义复杂导致参数很多、很难写出, 推荐借助更容易理解 (但有类型错误) 的写法来理解直觉:

$${\mathrm{rec}}_{|A{|}_n}(f,p)(\mathrm{trunc})=p:\mathrm{isHLvl}(B,n)$$

术语翻译

$n$-截断类型 • 英文 $n$-truncation