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

[Oleg Grenrus]

You need to define the type as a record.

See
https://agda.readthedocs.io/en/v2.6.1/language/record-types.html#eta-expansion

- Oleg

On 14.1.2021 21.46, David Banas wrote:
> Thanks, Ulf!
> After changing my product type definition to match yours, I am unstuck. :)
>
> Originally, I’d written:
>
>     data _×_ (A : Set) (B : Set) : Set where
>       _,_ : A → B → (A × B)
>
>
> I guess there was something more I needed to do, in order to have this
> type play nicely with the rest of the system?
>
> Now (using your product type), I’m able to complete the proof in a
> single step and without invoking extensionality:
>
>     117 begin
>     118   (λ { C→A⇒D (C , A) → C→A⇒D C · A })
>     119   (λ C₁ → ƛ (λ A₁ → C×A→D (C₁ , A₁)))
>     120 ≡⟨⟩
>     121   C×A→D
>     122 ∎
>
>
> However, I’m getting the following warning, related to the highlighted
> code above (line 118):
> (Note that /column/ numbers below are inaccurate.)
>
>     Sort _78  [ at ###.agda:118,31-64 ]
>     _79 : _78  [ at ###.agda:118,31-64 ]
>     _81 : _79  [ at ###.agda:118,31-64 ]
>
>
> Do you know why?
>
> Thanks,
> -db
>
>
>> On Jan 14, 2021, at 6:02 AM, Ulf Norell <ulf.norell at gmail.com
>> <mailto:ulf.norell at gmail.com>> wrote:
>>
>> 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 <mailto: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
>>     <mailto:capn.freako at gmail.com>>
>>     > *Sent: *Wednesday, January 13, 2021 8:20 PM
>>     > *To: *Agda mailing list <mailto:agda at lists.chalmers.se
>>     <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 <mailto:Agda at lists.chalmers.se>
>>     > https://lists.chalmers.se/mailman/listinfo/agda
>>     >
>>
>>     _______________________________________________
>>     Agda mailing list
>>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>>     https://lists.chalmers.se/mailman/listinfo/agda
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se <mailto: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