[Agda] Proving Parametricity?

[Brandon Moore]

> Funny you should mention this, I've been emailing Adam on this very  topic...

> 
> My back-of-envelope thought is that a form of naturality might  do the 
> trick, that is rather than defining exp to be:
> 
>    exp = ∀  var → Exp var
> 
> we define it as:
> 
>    exp = ∃ λ e → ∀ {V W} (φ :  V ↠ W) → (⟨Exp⟩ φ (e V) ≣ e W)
> 
> where V ↠ W  is the type of  surjections from V to W, and ⟨Exp⟩ is the 
> functorial action of Exp.   Code attached.
> 
> I don't think this is enough to prove exp_param, but  something like it 
> might go through.

Have you tried redoing any of Adam's interesting proofs with this definition?

I've written a bit of code that suggests it will be feasible to automate proofs
of the well-formedness condition using reflection, but re-establishing it
for the results of transformations could be difficult.

Brandon