この回答を読んで、ポリモーフィック コンテナー関数の標準的な形式を構築し、証明しようとしました。構造は簡単でしたが、証明は私を困惑させました。以下は、私がどのように証明を書こうとしたかを簡略化して最小化したものです。
単純化されたバージョンは、パラメトリック性のために、十分に多様な関数がパラメーターの選択のみに基づいて動作を変更できないことを証明しています。1 つは固定型、もう 1 つはパラメトリックの 2 つの引数を持つ関数があるとします。
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 = {!!}
そのような発言はアグダ内部から証明可能ですか?