parametricity.txt

parametricity.txt

If I have

𝔹 : ∀X. X → X → X

then parametricity tells me

(b : 𝔹)(f : X → Y)(x₁ x₂ : X) → f (b x₁ x₂) = b (f x₁) (f x₂).

From this I want to prove

bool-rec : (C: 𝔹 → Set) (ct : C true) (cf : C false) (b : 𝔹) → C b

Let's do a Grothendieck move and think of C instead as a (π : X → 𝔹):

bool-rec : (X : Set) (π: X → 𝔹) (ct : π⁻¹ true) (cf : π⁻¹ false) (b : 𝔹) → π⁻¹ b

I have ct in the π-preimage of true, and cf in the π-preimage of
false. I have an arbitrary b, and I must come up with something in the
π-preimage of b. Let x, y : 𝔹 be given. Let f : X → 𝔹 be

f z = (π z) [𝔹] x y

Note this is impredicative. By free theorem, I know

f (b [X] ct cf) = b [𝔹] (f ct) (f cf)
π (b [X] ct cf) [𝔹] x y = b [𝔹] (π ct [𝔹] x y) (π cf [𝔹] x y)
                        = b [𝔹] (true [𝔹] x y) (false [𝔹] x y)
                        = b [𝔹] x y

by extensionality,

π (b [X] ct cf) = b

and so we have found the desired preimage.