ParametrictyViaLFT.agda

-- https://stackoverflow.com/questions/34388484/parametricity-exploiting-proofs-in-agda

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

open import Relation.Binary.PropositionalEquality

Parametricity : {A : Set} → Set _
Parametricity {A} = ∀ {X Y} → (f : PolyFun A) → ∀ a x y → f {X} a x ≡ f {Y} a y

open import LFT hiding (check)

PolyFun′ : Set → Set1
PolyFun′ A = Π Set λ X → A → X → A

[PolyFun] : ∀ {A} ([A] : [Set] A A) → [Set1] (PolyFun′ A) (PolyFun′ A)
[PolyFun] [A] = [Π] [Set] λ [X] → [A] [→] [X] [→] [A]

Free-Theorem : ∀ {A} → [Set] A A → Set₁
Free-Theorem {A} [A] = ∀ (f : PolyFun A) -> [PolyFun] [A] (λ X → f {X}) (λ X → f {X})

module _ where
  check : ∀ {A} {[A] : [Set] A A} →
          Free-Theorem [A] ≡ (
          ∀ (f : PolyFun A) →
          {X₁ X₂ : Set} ([X] : X₁ → X₂ → Set)
          {a₁ a₂ : A} (aR : [A] a₁ a₂)
          {x₁ : X₁} {x₂ : X₂} (xR : [X] x₁ x₂) →
          [A] (f a₁ x₁) (f a₂ x₂))
  check = refl

postulate free-theorem : {A : Set} → ([A] : [Set] A A) → Free-Theorem [A]

parametricity′ : ∀ {A} → ([A] : [Set] A A) → Parametricity {A}
parametricity′ {A} [A] {X} {Y} f a x y = {!free-theorem [A] f {X} {Y} ? {a} {a} ? {x} {y} ?!}

parametricity : ∀ {A} → Parametricity {A}
parametricity {A} = parametricity′ {!!}