Cubical Agda为何选用特定二元同伦路径合成算子？

惯例与历史传承 #

同伦类型论（HoTT）及早期Agda的同伦编程实践中，就已采用从左到右的路径合成顺序：对于路径p : a ≡ b和q : b ≡ c，p ∙ q表示先沿p从a走到b，再沿q从b走到c，最终得到a ≡ c的路径。Cubical Agda作为HoTT的实现，延续了这一行业惯例，降低了熟悉HoTT的开发者的学习成本，也保证了与现有同伦编程生态的兼容性。

计算特性的原生适配 #

Cubical Agda的核心计算模型基于立方体构造，标准算子∙的定义（固定三元合成_∙∙_∙∙_的第一个参数为refl）更贴合立方体路径的原生计算规则：

• 合成p ∙ q时，底层是将两个路径按[0, 0.5]和[0.5, 1]区间分段拼接，这种构造直接对应立方体模型中路径的连续拼接行为，计算时可直接归约，无需额外优化规则。
• 而固定第二个参数的∘算子，底层是p ∙∙ refl ∙∙ q的三段式拼接（先p、再停在中间点的refl、最后q）。即便能通过额外规则优化掉中间的refl分段，其计算复杂度仍高于标准的∙，且与立方体模型中其他构造（如路径填充hfill、递推J等）的交互不如∙顺畅。

生态与成本的考量 #

Cubical Agda的标准库围绕∙算子构建了大量定理、证明工具和构造。如果替换为∘，所有依赖路径合成的代码都需要调整，迁移成本极高。此外，∘的核心优势——sym (p1 ∘ p2)与sym p2 ∘ sym p1定义相等——可以通过引理证明来弥补（虽非定义相等，但在证明中可通过rewrite或等价推理工具轻松使用），无需改变标准算子的选择。

内容的提问来源于stack exchange，提问作者Eric Dobson