<html><body bgcolor="#FFFFFF"><div><br><br>On Jan 19, 2011, at 11:43 AM, Alan Jeffrey <<a href="mailto:ajeffrey@bell-labs.com">ajeffrey@bell-labs.com</a>> wrote:<br><br></div><div></div><blockquote type="cite"><div><span>Funny you should mention this, I've been emailing Adam on this very topic...</span><br><span></span><br><span>My back-of-envelope thought is that a form of naturality might do the trick, that is rather than defining exp to be:</span><br><span></span><br><span> exp = ∀ var → Exp var</span><br><span></span><br><span>we define it as:</span><br><span></span><br><span> exp = ∃ λ e → ∀ {V W} (φ : V ↠ W) → (⟨Exp⟩ φ (e V) ≣ e W)</span><br><span></span><br><span>where V ↠ W is the type of surjections from V to W, and ⟨Exp⟩ is the functorial action of Exp. Code attached.</span><br><span></span><br><span>I don't think this is enough to prove exp_param, but something like it might go
through.</span><br><font class="Apple-style-span" color="#000000"><font class="Apple-style-span" color="#0023A3"><br></font></font></div></blockquote><div><br></div><div>You could certainly write a similar exp where the property in the sigma is based on a relation rather than a surjection. I don't know how to go about constructing values in this type.</div><div><br></div><div>One thing I tried was making another expression type using DeBruijn indices, parameterized by the number of free variables. Given a vector of variables for context this can be converted to an Exp over the same variable type, and it's clearly provable that any polymorphic Exp constructed that way has your naturally property. Unfortunately, in Agda it seems you have to provide the corresponding DeBruijn term manually, and in Coq that can be automated but it's such a huge pain inverting a (v : vec A (S n)) into a cons that I haven't finished the
lemma.</div><div><br></div><div>Brandon. </div><br>
</body></html>