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

[James Wood]

It might not hold definitionally as written because extended λs are 
generative. The first thing I'd try, assuming sufficiently new Agda, is 
to remove all the curly braces.

James

On 14/01/2021 01:22, Jason -Zhong Sheng- Hu wrote:
> CAUTION: This email originated outside the University. Check before 
> clicking links or attachments.
> 
> 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
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>