目标隐含的参数定理
Parametric theorem implied by goal
在使用 cubical-agda 的一些开发过程中，我注意到（后来检查了）我当前的目标，如果被证明也意味着这样的定理：
parametric? : ∀ ℓ → Type (ℓ-suc ℓ)
parametric? ℓ = (f : {A : Type ℓ} → List A ≃ List A)
→ (A : Type ℓ) → length ∘ equivFun (f {A}) ≡ length
我怀疑这是参数定理的例子，这是正确的，但在立方体 agda 中无法证明。是这样吗？
我可以安全地假设我当前的目标也无法证明吗？
是的，因为它在标准（单纯集）模型中是错误的。
如果排除中间成立，我们可以通过首先对A是否可收缩进行案例分析来定义f : {A : Type ℓ} → List A ≃ List A。如果 A 不可收缩，则 f 给出恒等等价，但如果 A 可收缩，则 List A 等价于 Nat，并且 f 可以给出一个等价关系，例如，排列赔率和偶数。
在使用 cubical-agda 的一些开发过程中，我注意到（后来检查了）我当前的目标，如果被证明也意味着这样的定理：
parametric? : ∀ ℓ → Type (ℓ-suc ℓ)
parametric? ℓ = (f : {A : Type ℓ} → List A ≃ List A)
→ (A : Type ℓ) → length ∘ equivFun (f {A}) ≡ length
我怀疑这是参数定理的例子，这是正确的，但在立方体 agda 中无法证明。是这样吗？
我可以安全地假设我当前的目标也无法证明吗？
是的，因为它在标准（单纯集）模型中是错误的。
如果排除中间成立，我们可以通过首先对A是否可收缩进行案例分析来定义f : {A : Type ℓ} → List A ≃ List A。如果 A 不可收缩，则 f 给出恒等等价，但如果 A 可收缩，则 List A 等价于 Nat，并且 f 可以给出一个等价关系，例如，排列赔率和偶数。