[Agda] error in plfa exercise

[Michel Levy]

I wrote in this mail list, with the subject [Agda] error in plfa
exercise, the 15/04/2020 at 17:14,
that I saw an error in the writing of the proof of the currying function
described in https://plfa.github.io/Connectives/.

I have to apologize to everyone for my error which I had falsely
attributed to my old version 2.5.3 of agda.
I had written incorrectly
"currying: ∀ {A B C: Set} → (A → B → C) ≃ (A × B) → C"
in place of the correct
"currying: ∀ {A B C: Set} → (A → B → C) ≃ (A × B → C)
The incorrect placement of the parenthesis was fatal to me.


-- 
courriel : michel.levy.imag at free.fr
mobile : 06 59 13 42 53
web : michel.levy.imag.free.fr