[Agda] How to validate eta-reduction in equational reasoning proofs?

[Jesper Cockx]

Hi Banas,

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?

-- Jesper

On Thu, Jan 14, 2021 at 2:23 AM Jason -Zhong Sheng- Hu <
fdhzs2010 at hotmail.com> wrote:

> That’s very strange. I would expect this equality to hold definitionally.
> You shouldn’t even need extensionality.
>
>
>
> Does agda complain anything if you remove the first two lines entirely?
>
>
>
> Thanks,
>
> Jason Hu
>
>
>
> *From: *David Banas <capn.freako at gmail.com>
> *Sent: *Wednesday, January 13, 2021 8:20 PM
> *To: *Agda mailing list <agda at lists.chalmers.se>
> *Subject: *[Agda] How to validate eta-reduction in equational reasoning
> proofs?
>
>
>
> Hi all,
>
>
>
> Does anyone know how I can get this to work?
>
>
>
>                              (λ { (C , A) → (C×A→D (C , A)) })
>                            ≡⟨ extensionality (λ C×A → refl) ⟩
>                              (λ { x → (C×A→D x) })
>
>
>
> Agda is telling me:
>
>
>
> (λ { (C , A) → C×A→D (C , A) }) C×A != C×A→D C×A of type D
>
> when checking that the expression refl has type
>
> (λ { (C , A) → C×A→D (C , A) }) C×A ≡ C×A→D C×A
>
>
>
> Thanks,
>
> -db
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210114/b851bfd0/attachment.html>