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

[Jason -Zhong Sheng- Hu]

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<mailto:capn.freako at gmail.com>
Sent: Wednesday, January 13, 2021 8:20 PM
To: Agda mailing list<mailto: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


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210114/468d3356/attachment.html>