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

[David Banas]

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/20210113/79963788/attachment.html>