<div dir="ltr"><div>Hi Banas,</div><div><br></div><div>That looks like a bug to me, but it's hard to make sure without the full code. Also, what version of Agda and the standard library are you using?</div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Jan 14, 2021 at 2:23 AM Jason -Zhong Sheng- Hu <<a href="mailto:fdhzs2010@hotmail.com">fdhzs2010@hotmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">





<div style="overflow-wrap: break-word;" lang="EN-US">
<div class="gmail-m_-628340258469505771WordSection1">
<p class="MsoNormal">That’s very strange. I would expect this equality to hold definitionally. You shouldn’t even need extensionality.</p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">Does agda complain anything if you remove the first two lines entirely?</p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">Thanks,<u></u><u></u></p>
<p class="MsoNormal">Jason Hu<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<div style="border-color:rgb(225,225,225) currentcolor currentcolor;border-style:solid none none;border-width:1pt medium medium;padding:3pt 0in 0in">
<p class="MsoNormal" style="border:medium none;padding:0in"><b>From: </b><a href="mailto:capn.freako@gmail.com" target="_blank">David Banas</a><br>
<b>Sent: </b>Wednesday, January 13, 2021 8:20 PM<br>
<b>To: </b><a href="mailto:agda@lists.chalmers.se" target="_blank">Agda mailing list</a><br>
<b>Subject: </b>[Agda] How to validate eta-reduction in equational reasoning proofs?</p>
</div>
<p class="MsoNormal"><u></u> <u></u></p>
<div>
<p class="MsoNormal">Hi all,<u></u><u></u></p>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">Does anyone know how I can get this to work?<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">                             (λ { (C , A) → (C×A→D (C , A)) })<br>
                           ≡</span><span style="font-family:"Cambria Math",serif">⟨</span><span style="font-family:"Courier New""> extensionality (λ C×A → refl)
</span><span style="font-family:"Cambria Math",serif">⟩</span><span style="font-family:"Courier New""><br>
                             (λ { x → (C×A→D x) })</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">Agda is telling me:<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<blockquote style="margin-left:30pt;margin-right:0in">
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">(λ { (C , A) → C×A→D (C , A) }) C×A != C×A→D C×A of type D</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">when checking that the expression refl has type</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">(λ { (C , A) → C×A→D (C , A) }) C×A ≡ C×A→D C×A</span><u></u><u></u></p>
</div>
</blockquote>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">Thanks,<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">-db<u></u><u></u></p>
</div>
</div>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
</div>

_______________________________________________<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/mailman/listinfo/agda</a><br>
</blockquote></div>