agda - 目标隐含的参数定理

Question

在使用 cubical-agda 的一些开发过程中，我注意到(后来检查了)我当前的目标，如果被证明也意味着这样的定理:

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

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

我可以安全地假设我当前的目标也无法证明吗？

Answer 1

是的，因为它在标准(简单集)模型中是错误的。

如果排除中间成立，我们可以通过首先对 A 是否可收缩进行案例分析来定义 f : {A : Type ℓ} → List A ≃ List A或不。如果 A 不可收缩，则 f 给出恒等等价，但如果 A 可收缩，则 List A 是等同于 Nat，并且 f 可以给出一个等价关系，例如，排列奇数和偶数。