agda - 立方体 agda 中针对特定计算行为的路径与等价关系

Question

我在 Cubical agda 工作，并试图为以后的证明建立一些通用的实用程序。其中之一是，对于任何类型 A，它与 Σ A (\_ -> Top) 类型“相同”，其中 Top是具有一个元素的类型。问题是如何从实用程序库中最好地揭示这种“相同性”。我可以将其公开为等价、路径或同构，也可能是多个。

我最初只是将它公开为一条路径:top-path : Path A (Σ A (\_ -> Top)) 这是使用来自底层 top 的胶水类型构建的-equiv : A ≃ Σ A (\_ -> Top)。但是当试图在以后的证明中使用它时，我发现沿着这条路径的传输并没有像我预期的那样计算。我的期望是它由 fst 组成，但在实践中我发现它有时会留在 transp 和 prim^unglue 术语中。如果我为 A 使用特定的具体类型，或者如果我使用等价的类似构造，情况就不是这样了。

例子:

-- Working
compute-top-path-Bool : (a : Bool) -> fst (transport (top-path Bool) a) == a
compute-top-path-Bool a = refl

compute-top-equiv-Any : (a : Bool) -> fst (transport-equiv (top-equiv Bool) a) == a
compute-top-equiv-Any a = refl

-- Broken
compute-top-path-Any : (a : A) -> fst (transport (top-path A) a) == a
compute-top-path-Any a = refl

--
-- Checking test (/Users/endobson/tmp/agda/test.agda).
-- /Users/endobson/tmp/agda/test.agda:104,26-30
-- transp (λ i → A) i0 (fst (prim^unglue a)) != a of type A
-- when checking that the expression refl has type
-- fst (transport (top-path A) a) == a 
--

独立复制:https://gist.github.com/endobson/62605cfc15a92b9111391b459d03b548 ，我使用的是 Agda 版本 2.6.1.3。

因此我的问题是这个问题的最佳解决方案是什么？我是否以某种方式以过于复杂的方式构建我的路径，如果我以不同的方式构建它们，那么计算行为会更好吗？还是直接从我的实用程序库中公开等效项？我发现暴露等价性“不雅”，因为它似乎路径应该能够做到这一点，但如果已知它们是该特定用例的更好工具，我并不反对这样做。

Answer 1

在 agda/cubical 库中，我们确实倾向于将等效项(或 iso)与路径一起导出，因为您提到的问题。

那些额外的 transp 调用的原因是 Glue 的传输必须在可能实际需要它们的一般情况下工作。

fst (prim^unglue a) 如果您要求正常形式，则应该减少。