Skip to content

Instantly share code, notes, and snippets.

What would you like to do?
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′ {!!}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.