目标隐含的参数定理

Question

在使用cubical-agda进行一些开发期间，我注意到（后来检查）我当前的目标如果被证明也意味着这样的定理：

\n

parametric? : \xe2\x88\x80 \xe2\x84\x93 \xe2\x86\x92  Type (\xe2\x84\x93-suc \xe2\x84\x93)  \nparametric? \xe2\x84\x93 = (f : {A : Type \xe2\x84\x93} \xe2\x86\x92 List A \xe2\x89\x83 List A)\n                   \xe2\x86\x92 (A : Type \xe2\x84\x93) \xe2\x86\x92 length \xe2\x88\x98 equivFun (f {A}) \xe2\x89\xa1 length\n

\n

我怀疑这是参数定理的例子，这是正确的，但在三次 agda 中无法证明。是这样吗？

\n

我可以放心地假设我当前的目标也是无法证明的吗？

\n

Answer 1

是的，因为它在标准（单纯集）模型中是错误的。

\n

如果排除中间成立，我们可以f : {A : Type \xe2\x84\x93} \xe2\x86\x92 List A \xe2\x89\x83 List A先通过案例分析确定是否A可收缩。如果A不可收缩，f则给出恒等等价，但如果A可收缩，则List A等价于Nat，且f可以给出等价，例如排列奇数和偶数。

\n