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

[Ulf Norell]

FWIW this works:

open import Agda.Builtin.Sigma
open import Agda.Builtin.Equality

_×_ : Set → Set → Set
A × B = Σ A λ _ → B

postulate
  A B C : Set
  f     : A × B → C
  ext   : ∀ {A B : Set} {f g : A → B} → (∀ x → f x ≡ g x) → f ≡ g

prf : (λ { (x , y) → f (x , y) }) ≡ (λ { p → f p })
prf = ext λ _ → refl

Have you made sure that the pair type you are using has eta equality?

/ Ulf

On Thu, Jan 14, 2021 at 2:09 PM James Wood <james.wood.100 at strath.ac.uk>
wrote:

> 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
> >
>
> _______________________________________________
> 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/2fcbed80/attachment.html>