[Agda] Polymorphism is not (always) naturality

[Andrea Vezzosi]

It is FP folklore that polymorphic functions of type

(a : Set) -> F a -> G a

correspond to natural transformations via parametricity.
(Assuming F and G are "Functor"s)

So it was a bit surprising to me that the result fails in dependent type theory.

open import Data.Product
open import Data.Unit
open import Data.Empty
open import Data.Bool
open import Relation.Binary.PropositionalEquality

S : Set → Set₁
S X = Σ Set \ R → R → X

mapS : ∀ {X Y} → (X → Y) → S X → S Y
mapS f (R , g) = (R , \ x → f (g x))

eta : ∀ {X} → S X → S X
eta (R , g) = (Σ R \ r → ∀ r' → g r ≡ g r') , (λ x → g (proj₁ x))

postulate
  eta-nat : ∀ {X Y} → (f : X → Y) → ∀ s → eta (mapS f s) ≡ mapS f (eta s)

counter : ∀ {X : Set} → eta (mapS (λ _ → tt) (X , (λ x → x)))
                      ≡ mapS (λ _ → tt) (eta (X , (λ x → x)))
counter {X} = eta-nat {X} {⊤} _ (X , (λ x → x))

empty-sigma : Σ Bool (λ r → (r' : Bool) → r ≡ r') → ⊥
empty-sigma (b , p) with p (not b)
empty-sigma (true , p) | ()
empty-sigma (false , p) | ()

impossible : ⊥
impossible = empty-sigma (subst (\ x -> x) (cong proj₁ (counter {Bool}))
                                (true , (λ _ → refl)))