逻辑截断类型

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

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

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

1类型规则

构造规则

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

消去规则

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

计算规则:

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

2应用

选择公理

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

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

定义 2.1. 考虑如下数据: 其中 集合 (类型论). 在语境 下, 选择公理是说如下命题:

3性质

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

引理 3.2. 对于类型 , 类型 等价, 其中 (参见:空类型双重否定 (类型论)), 类比逻辑中命题的否定.

引理 3.3. 对于类型 , 类型 能推出 .

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

引理 3.4. 对于类型 , 类型 等价 (参见:无交并类型).

引理 3.5. 对于类型 , 可以借助 构造出 的实例.

4编码

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

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

术语翻译

逻辑截断类型英文 propositional truncation