agda - Agda 中的参数化利用证明

Question

阅读 this answer促使我尝试构造并证明多态容器函数的规范形式。构造很简单，但证明让我很困惑。以下是我尝试编写证明的简化版本。

简化版本证明了足够多态的函数，由于参数性，不能仅根据参数的选择来改变它们的行为。假设我们有两个参数的函数，一个是固定类型，一个是参数:

PolyFun : Set → Set _
PolyFun A = ∀ {X : Set} → A → X → A

我想证明的性质:

open import Relation.Binary.PropositionalEquality

parametricity : ∀ {A X Y} → (f : PolyFun A) → ∀ a x y → f {X} a x ≡ f {Y} a y
parametricity f a x y = {!!}

是否可以从 Agda 内部证明这样的陈述？

Answer 1

不，在 Agda 中没有可用的参数原则(还没有![1])。

但是您可以使用这些组合子来构建相应的自由定理的类型并假设它:

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.LightweightFreeTheorems

[1] http://www.cse.chalmers.se/~mouling/share/PresheafModelParametericTT.pdf