parametricity.txt

parametricity.txt

Let's say a function
    j : ∏(X : 𝒰). (S¹ → X) → (X → X)
is (binary relationally) parametric just in case we have
    ∏(X₁ : 𝒰). ∏(X₂ : 𝒰). ∏(R : X₁ → X₂ → U).
    ∏(η₁ : S¹ → X₁). ∏(η₂ : S¹ → X₂). (∏(s : S¹). R (η₁ s) (η₂ s)) →
    ∏(x₁ : X₁). ∏(x₂ : X₂). R x₁ x₂ →
    R (j X₁ η₁ x₁) (j X₂ η₂ x₂)
Then we can pick an arbitrary function x : X₁ → X₂ and let R be f's graph
    R x₁ x₂ ⇔ f x₁ ≡ x₂
and we obtain
    ∏(X₁ : 𝒰). ∏(X₂ : 𝒰). ∏(f : X₁ → X₂).
    ∏(η₁ : S¹ → X₁). ∏(η₂ : S¹ → X₂). (∏(s : S¹). f (η₁ s) ≡ (η₂ s)) →
    ∏(x₁ : X₁). ∏(x₂ : X₂). f x₁ ≡ x₂ →
    f (j X₁ η₁ x₁) ≡ (j X₂ η₂ x₂)
which is equivalent to
    ∏(X₁ : 𝒰). ∏(X₂ : 𝒰). ∏(f : X₁ → X₂).
    ∏(η₁ : S¹ → X₁).
    ∏(x₁ : X₁).
    f (j X₁ η₁ x₁) ≡ (j X₂ (f ∘ η₁) (f x₁))
and then, for any (η' : S¹ → X₂) (x' : X₂), we can instantiate
    X₁ := S¹ + 1
    η₁ s := inl s
    x₁ := inr *
    f (x : S¹ + 1) := case x of inl s ⇒ η' s | inr * ⇒ x'
and obtain
    ∏(X₂ : 𝒰). ∏(η' : S¹ → X₂). ∏(x' : X₂).
    case (j (S¹ + 1) (λs.inl s) (inr *)) of inl s ⇒ η' s | inr * ⇒ x'
         ≡ j X₂ η' x'
So alpha-varying some things around, this is the same as
    ∏(X : 𝒰). ∏(η : S¹ → X). ∏(x : X).
    j X η x ≡
       case (j (S¹ + 1) (λs.inl s) (inr *)) of inl s ⇒ η s | inr * ⇒ x

We conclude that a function
    j : ∏(X : 𝒰). (S¹ → X) → (X → X)
is, if it's parametric, completely determined by the value of
    j (S¹ + 1) (λs.inl s) (inr *)
which, since it belongs to S¹ + 1, can only be either
inl s for s : S¹, or inr *.

In the first case, we get j X η x ≡ η s.
In the second case, we get j X η x ≡ x.