Cubical Agda开发中目标导出的参数化定理是否不可证明？

结论 #

你的两个判断都是正确的，具体解释如下：

关于parametric?的可证性判断 #

你提到的parametric?确实是仅在参数化语义下成立、但标准无额外公理的Cubical Agda系统中无法证明的命题：

• 成立的依据：从参数化理论的自由定理出发，形如f : {A : Type ℓ} → List A ≃ List A的多态等价必须保持列表长度，长度是List函子上的自然变换，多态函数的参数化条件要求其与所有自然变换交换，因此该命题在参数化模型中恒真。
• 不可证的依据：Cubical Agda的基础类型论本身没有内置参数化约束，其合法模型允许存在非参数化的多态函数（例如可以按类型的内部结构分支执行不同逻辑的多态函数），无法从系统本身的规则推导出所有多态函数都满足参数化要求，因此你给出的parametric?没有办法在纯Cubical Agda中构造证明。

parametric? : ∀ ℓ →  Type (ℓ-suc ℓ)  
parametric? ℓ = (f : {A : Type ℓ} → List A ≃ List A)
                   → (A : Type ℓ) → length ∘ equivFun (f {A}) ≡ length

关于待证目标的可证性推导 #

如果你已经在纯Cubical Agda中无额外公理地证明了「你的待证目标 → parametric?」这一蕴含关系，那么完全可以直接得出你的待证目标在纯Cubical Agda中同样不可证明的结论：
逻辑上如果系统允许从P推导得到Q，且Q不可证，那么P必然也不可证，否则可以通过P的证明直接构造Q的证明，和Q的不可证性矛盾。

注：上述结论仅适用于标准无额外公理的Cubical Agda环境，如果你后续引入了参数化公理、宇宙约束等额外规则，两个命题的可证性都可能发生变化。

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