[Agda] Proving Parametricity?

[Alan Jeffrey]

On 01/23/2011 09:52 PM, Brandon Moore wrote:
>> 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.

Well I tried proving exp_param as a theorem, which from a mile-high view 
is pretty easy, but the details are bogging me down.

The mile-high version is that an equivalence e1 ~ e2 between e1 : Exp V1 
and e2 : Exp V2 can be coded as a span, that is an expression e : Exp 
(V1 x V2) such that e1 ≣ <Exp> proj1 e and e2 ≣ <Exp> proj2 e.

The main bogged-down detail is that for proj1 : V1 x V2 → V1 to form a 
surjection, we need V2 to be nonempty, but then we need a proof 
irrelevance result to say that proj1 doesn't depend on the witness for 
V2, which in turn seemed to need everything to be redone in terms of 
pointed sets and morphisms rather than just sets and functions.  At this 
point I gave up, but I may come back to this later.

A.