Parametricity-exploiting proofs in Agda

Question

Reading this answer prompted me to try to construct, and then prove, the canonical form of polymorphic container functions. The construction was straightforward, but the proof stumps me. Below is a simplified-minimized version of how I tried to write the proof.

The simplified version is proving that sufficiently polymorphic functions, due to parametricity, can't change their behaviour only based on the choice of parameter. Let's say we have functions of two arguments, one of a fixed type and one parametric:

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

the property I'd like to prove:

open import Relation.Binary.PropositionalEquality

parametricity : ∀ {A X Y} → (f : PolyFun A) → ∀ a x y → f {X} a x ≡ f {Y} a y
parametricity f a x y = {!!}

Are statements like that provable from inside Agda?

Answer 1

Nope, there's no parametricity principle accessible in Agda (yet! [1]).

However you can use these combinators to build the type of the corresponding free theorem and postulate it:

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.LightweightFreeTheorems

[1] http://www.cse.chalmers.se/~mouling/share/PresheafModelParametericTT.pdf