<div dir="ltr">Andras, Thank you very much for your note [1]. Your proof appears related to the wf relation of Chlipala [2,3]. One difference is that yours is unary whereas his is binary, so I would expect his is more powerful, or do you think they have equal power? Yours, -- P<div><br></div><div>[1] <span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline"><a href="http://lpaste.net/363029">http://lpaste.net/363029</a></span></div><div><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">[2] <span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline"><a href="http://adam.chlipala.net/cpdt/html/Cpdt.ProgLang.html#HigherOrder.Wf">http://adam.chlipala.net/cpdt/html/Cpdt.ProgLang.html#HigherOrder.Wf</a></span></span></div><div><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline"><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">[3] <a href="http://adam.chlipala.net/cpdt/html/Intensional.html">http://adam.chlipala.net/cpdt/html/Intensional.html</a></span></span></div></div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr">. \ Philip Wadler, Professor of Theoretical Computer Science,<br>. /\ School of Informatics, University of Edinburgh<br></div><div>. / \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div></div></div></div>
<br><div class="gmail_quote">On 1 March 2018 at 23:54, András Kovács <span dir="ltr"><<a href="mailto:kovacsahun@hotmail.com" target="_blank">kovacsahun@hotmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Alternatively, <a href="http://lpaste.net/363029" target="_blank">we can postulate parametricity</a> for PHOAS terms, and then the translation works without further cheating (that's why it's "parametric", right?).</div><div class="gmail_extra"><br><div class="gmail_quote"><div><div class="h5">2018-02-28 19:45 GMT+01:00 Philip Wadler <span dir="ltr"><<a href="mailto:wadler@inf.ed.ac.uk" target="_blank">wadler@inf.ed.ac.uk</a>></span>:<br></div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5"><div dir="ltr">That worked perfectly!!! Thank you, Ulf! Cheers, -- P</div><div class="gmail_extra"><span><br clear="all"><div><div class="m_-5216455422973969131m_-8737000814882258390gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr">. \ Philip Wadler, Professor of Theoretical Computer Science,<br>. /\ School of Informatics, University of Edinburgh<br></div><div>. / \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/<wbr>wadler/</a></span></div></div></div></div></div>
<br></span><div><div class="m_-5216455422973969131h5"><div class="gmail_quote">On 28 February 2018 at 16:10, Ulf Norell <span dir="ltr"><<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><br><div class="gmail_extra"><div class="gmail_quote"><span>On Wed, Feb 28, 2018 at 2:31 PM, Roman <span dir="ltr"><<a href="mailto:effectfully@gmail.com" target="_blank">effectfully@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">The downside is that `agda-prelude` is not compatible with the standard library.</blockquote><div><br></div></span><div>These days agda-prelude is compatible with the standard library. The only wrinkle<br></div><div>is that the deriving Eq functionality gives you an implementation of the agda-prelude<br></div><div>Eq record, but converting it to the standard library equivalent should be straight-forward.<br><br></div><div>In fact here's the code:<br><br></div><div>\begin{code}<br></div><div>-- These two imports are from agda-prelude (<a href="https://github.com/UlfNorell/agda-prelude" target="_blank">https://github.com/UlfNorell/<wbr>agda-prelude</a>)<br></div><div>open import Tactic.Deriving.Eq using (deriveEq)<br>import Prelude<br><br>instance<br> unquoteDecl EqType = deriveEq EqType (quote Type)<br> unquoteDecl EqEnv = deriveEq EqEnv (quote Env)<br><br>⊥To⊥ : Prelude.⊥ → ⊥<br>⊥To⊥ ()<br><br>decToDec : ∀ {a} {A : Set a} → Prelude.Dec A → Dec A<br>decToDec (Prelude.yes x) = yes x<br>decToDec (Prelude.no nx) = no (⊥To⊥ ∘ nx)<span><br><br>_≟T_ : ∀ (A B : Type) → Dec (A ≡ B)<br></span>A ≟T B = decToDec (A Prelude.== B)<span><br><br>_≟_ : ∀ (Γ Δ : Env) → Dec (Γ ≡ Δ)<br></span>Γ ≟ Δ = decToDec (Γ Prelude.== Δ)<br></div><div>\end{code}<span class="m_-5216455422973969131m_-8737000814882258390HOEnZb"><font color="#888888"><br></font></span></div><span class="m_-5216455422973969131m_-8737000814882258390HOEnZb"><font color="#888888"><div><br></div><div>/ Ulf<br></div></font></span></div></div></div>
</blockquote></div><br></div></div></div>
<br></div></div>The University of Edinburgh is a charitable body, registered in<br>
Scotland, with registration number SC005336.<br>
<br>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
<br></blockquote></div><br></div>
</blockquote></div><br></div>