逻辑截断类型

逻辑截断类型 (又叫命题截断类型) 是一种高阶归纳类型, 它也有一种巧妙的 $\lambda$ 编码. 它通过商掉平凡的关系的方式给出类型的命题形式.

在$n$-类型的视角下, 逻辑截断类型即是在 $-1$ 层截断某个类型. 它的推广是截断类型.

对于高阶归纳类型的实现策略来说, 实现逻辑截断类型是一种强有力的测试手段, 因为它不仅有类型参数、而且是递归的 (它的构造器用到了逻辑截断自己).

1类型规则

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

构造规则

需要用到 $\mathrm{isProp}$, 该辅助定义要求类型要么存在唯一实例、要么没有实例, 对应了同伦类型论中同伦层级为 $-1$ 的情况. 其详细动机及定义参见命题宇宙.

$$\mathrm{isProp}A:=\prod _{a,b:A}{\mathrm{Id}}_A(a,b)$$

$$\frac{\Gamma ⊢a:A}{\Gamma ⊢\Vert a\Vert :|A|}\frac{}{\Gamma ⊢\mathrm{trunc}:\mathrm{isProp}|A|}$$

消去规则

逻辑截断类型只能被映射到其它的命题, 否则会出现命题宇宙中提到的一致性问题.

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

计算规则:

$$\begin{array}{rl}{\mathrm{rec}}_{|A|}(f,p)(\Vert a\Vert )& =f(a):B\\ {\mathrm{ap}}_{{\mathrm{rec}}_{|A|}(f,p)}(\mathrm{trunc}(a,b))& =p(a,b):\mathrm{Id}(f(a),f(b))\end{array}$$

第二条规则更容易理解 (但有类型错误) 的写法如下:

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

2应用

选择公理

参见: 选择公理 (类型论)

逻辑截断类型可以用于定义同伦类型论中的选择公理.

定义 2.1. 考虑如下数据: $$\Gamma ⊢A:\mathcal{U}\Gamma ⊢B:A\to \mathrm{Set}$$其中 $\mathrm{Set}$ 指集合 (类型论). 在语境 $\Gamma$ 下, 选择公理是说如下命题: $${\Pi }_{a:A}|B(a)|\to |{\Pi }_{a:A}B(a)|$$

3性质

引理 3.1. 对于类型 $A$, 类型 $||A||$ (即逻辑截断的逻辑截断) 和 $|A|$ 等价.

引理 3.2. 对于类型 $A$, 类型 $\neg \neg A$ 和 $\neg \neg |A|$ 等价, 其中 $\neg A:=A\to \varnothing$ (参见:空类型、双重否定 (类型论)), 类比逻辑中命题的否定.

引理 3.3. 对于类型 $A$, 类型 $|A|$ 能推出 $\neg \neg A$.

这个引理的直觉可以从下面的 $\lambda$ 编码看出.

引理 3.4. 对于类型 $A$, 类型 $|A+\neg A|$ 和 $|A|+\neg |A|$ 等价 (参见:无交并类型).

引理 3.5. 对于类型 $A$, 可以借助 $A+\neg A$ 和 $|A|$ 构造出 $A$ 的实例.

4编码

另一种定义逻辑截断类型的方式是使用$\lambda$ 编码:

$$\begin{array}{rl}|A|& :={\Pi }_{P:\mathrm{Prop}}(A\to P)\to P\\ \Vert a\Vert & :=\lambda P.\lambda f.{\mathrm{ap}}_f(a)\end{array}$$

其余规则可以从这两条轻易地得出. 借助这种方式定义, 可以在没有高阶归纳类型、只有命题宇宙的时候定义类型论中的选择公理 2.1.

术语翻译

逻辑截断类型 • 英文 propositional truncation