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

[Oleg Grenrus]

See
https://agda.readthedocs.io/en/v2.6.1/language/record-types.html#example-the-pair-type-constructor,
specifically the last paragraphs about `constructor` keyword.

- Oleg

On 15.1.2021 0.21, David Banas wrote:
> Thanks, Oleg!
> Is this correct?:
>
>     55 record _×_ (A : Set) (B : Set) : Set where
>     56   field
>     57     fst : A
>     58     snd : B
>     59     
>     60 _,_ : ∀ {A B : Set} A → B → (A × B)
>     61 x , y = record {fst = x; snd = y}
>
>
> It seems to work, in general, but is giving me the following error,
> re: my Functor instance:
>
>     ###.agda:112,3-36
>     Could not parse the left-hand side
>     fmap ⦃ ProductFunctor ⦄ f (x , y)
>     Operators used in the grammar:
>       , (infix operator, level 20) [_,_ (###.agda:60,1-4)]
>     when scope checking the left-hand side
>     fmap ⦃ ProductFunctor ⦄ f (x , y) in the definition of
>     ProductFunctor
>
>
> For reference, here is that Functor instance:
>
>     110 instance
>     111   ProductFunctor : ∀ {A : Set} → Functor (_× A)
>     112   fmap {{ProductFunctor}} f (x , y) = (f x , y)
>
>
> Thanks,
> -db
>
>
>> On Jan 14, 2021, at 12:08 PM, Oleg Grenrus <oleg.grenrus at iki.fi
>> <mailto:oleg.grenrus at iki.fi>> wrote:
>>
>> 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
>