阅读这个答案促使我尝试构建并证明多态容器函数的规范形式。结构很简单，但证明让我难过。下面是我尝试编写证明的简化版本。
简化版本证明，由于参数性，足够多态的函数不能仅根据参数的选择来改变它们的行为。假设我们有两个参数的函数，一个是固定类型，一个是参数：
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 内部可以证明这样的陈述吗？