Directed proof-relevant logical relations in simplicial HoTT

技术摘要：单纯形 HoTT 中的定向证明相关逻辑关系

问题陈述
传统的证明相关逻辑关系（通常通过范畴粘合/gluing 形式化）将类型解释为可计算项的族，其中可计算性谓词是类型的族而非仅仅是命题。在等价呈现的类型论中，判断相等（judgmental equality）由元层级相等表示，而逻辑关系依赖于一个“在扩张下封闭”（closure under expansion）的引理：如果项 $M$ 约简为 $M'$，且 $M'$ 是可计算的，那么 $M$ 也是可计算的。然而，这种方法将计算视为一种对称关系（通过相等），或者依赖于手动的后向封闭证明。它未能原生地内化定向（directed）的约简本质，即项会步进到其他项（$M \to M'$），但反之则不一定成立。本文旨在解决构建一个能够解释定向约简、且无需依赖外部约简关系或证明无关扩张引理的证明相关逻辑关系的挑战。

方法论
作者在**单纯形同伦类型论（simplicial HoTT）**框架下开发了其理论体系，这是一种包含了定向区间（directed interval）和不等式类型（$x \leq_A y$）的定向 HoTT 扩展。

1. 通过定向 QIIT 实现的定向语法：
   对象语言的语法以定向商归纳归纳类型（directed QIIT）的形式呈现。与通过判断相等（路径构造器）进行商化的标准 QIIT 不同，此处的语法包含了生成不等式类型的定向构造器。例如，乘积的 $\beta$-约简被内化为一种不等式：
   $$\times\beta_1 : \text{fst}(\text{pair } a \, b) \leq a$$
   该语法被构建为一个“薄 Segal 类型”（thin Segal type），确保约简是可复合的，且相同端点之间的不等式是唯一的（证明无关的），从而模拟了一个预序（preorder）而非一般的范畴。

2. 反变性作为证明相关的扩张：
   其核心理论洞察是，单纯形类型论中的反变族（contravariant families）提供了实现证明相关扩张所需的精确结构。在这种设定下，类型 $A$ 的可计算性谓词 $A^\bullet$ 不仅仅是一个类型族；它必须是一个反变族。

   • 定义： 一个族 $C: X \to \mathcal{U}$ 是反变的，如果对于每一个不等式 $f: x \leq_X y$ 和见证 $v: C(y)$，提升类型 $\sum_{u:C(x)} u \leq_{C(f)} v$ 是可收缩的（contractible）。
   • 含义： 这种收缩性保证了一个唯一的、函子的“后向传输”（backward transport）操作 $f^*: C(y) \to C(x)$。该操作内化了扩张引理：可计算性证据可以沿着约简进行后向传输，并自动满足恒等性和复合性。

3. 处理依赖类型与宇宙：
   将此扩展到依赖类型会引入冲突：类型转换需要对称的相等，但语法仅提供定向的不等式。

   • 离散化（Discretization）： 作者通过添加一个构造器来离散化类型宇宙（$Ty$），该构造器将类型不等式转化为相等（$A \leq Ty B \implies A = Ty B$）。这使得标准的类型转换成为可能，同时保留了项的定向约简。
   • 平坦模态（Flat Modality）： 为了在保持宇宙谓词证明相关性的同时不丢失离散性，作者采用了来自严格类型论（crisp type theory）的平坦模态 ($\flat$)。宇宙的可计算性谓词存储为平坦代码。由于 $\flat X$ 是离散的，谓词之间的不等式会坍缩为相等，从而确保了宇宙可计算性见证的唯一性。

核心贡献

1. 定向商语法： 一种形式化的类型论语法，其中判断约简通过定向 QIIT 被内化为定向不等式。
2. 反变性即扩张： 将单纯形类型论中的反变族识别为证明相关扩张的推广，提供了内置的函子性和关于后向传输的普适性质。
3. 一元逻辑关系模型： 构建了一个一元逻辑关系模型，证明了定向布尔可计算性（directed Boolean canonicity）：每个闭合布尔项 $M$ 满足 $M \leq \text{true}$ 或 $M \leq \text{false}$。
4. 机械化： 在 Cubical Agda 中对简单类型片段（乘积、函数、布尔值）进行了概念验证式的机械化实现，证明了定向方法的可行性。
5. 向依赖类型与宇宙的扩展： 使用类型离散化和平坦模态处理依赖类型与宇宙谓词的方案。
6. 二元参数性（Binary Parametricity）： 对二元逻辑关系的适配，将垂直约简（反变性）与水平参数性分离，并通过队列（queues）的表示无关性论证展示了这一点。

结果

• 定向可计算性： 在定向设定下建立了逻辑关系的基本定理。对于任何闭合布尔项 $M$，模型给出了 $M$ 约简至规范布尔值的见证。
• 表示无关性： 二元逻辑关系成功地将垂直维度（约简/反变性）与水平维度（参数性）分离，允许对表示无关性进行证明相关的描述，此时关系是一个跨距（span）而非锯齿（zig-zag）。
• 机械化： 简单类型片段（包括定向语法和逻辑关系模型的构建）已在 Cubical Agda 中完成形式化。

意义与主张
本文声称提供了一种类型论内化的方法，即即使在通过约简而非相等来呈现语法时，逻辑关系仍能验证可计算性和参数性。

• 理论统一： 通过利用单纯形类型论原生的定向结构，将计算的运算视图（定向约简）与逻辑关系的语义视图（证明相关粘合）统一起来。
• 反变性的新角色： 它将反变族从合成范畴论的工具提升为逻辑关系的基础机制，用普适性质取代了特设的扩张引理。
• 谦逊的态度： 作者指出其结论是“并不令人意外的”（逻辑关系应当对约简有效），但其意义在于实现了内化。他们承认依赖类型扩展带来了显著的传输挑战，且目前的机械化局限于简单类型情况。他们并未声称解决了所有关于定向环境下恒等类型的问题，而是提出了未来涉及相位区分（phase distinctions）或单子模态（monadic modalities）的研究方向。

这项工作表明，单纯形类型论不仅是合成 $\infty$-范畴论的工具，也是研究编程语言和类型论约简语义的可行元理论。