Agda Error message : Cannot eliminate type with variable pattern

Question

I was asked to finish one of the recommended question from plfa:

Exercise ⇔≃× (recommended)
Show that A ⇔ B as defined earlier is isomorphic to (A → B) × (B → A).

I know I need to prove some property of equivalence first, and here is my proof:

record _⇔_ (A B : Set) : Set where
    field
      to   : A → B
      from : B → A
  ⇔-refl : ∀ {A : Set} → A ⇔ A
  ⇔-refl =
    record
      { to      = λ{x → x}
      ; from    = λ{y → y}
      }
  ⇔-sym : ∀ {A B : Set}
     → A ⇔ B 
     → B ⇔ A 
  ⇔-sym A⇔B =
    record
      { to = _⇔_.from A⇔B
      ; from = _⇔_.to A⇔B
      }
  ⇔-trans : ∀ {A B C : Set}
     → A ⇔ B
     → B ⇔ C
     → A ⇔ C
  ⇔-trans A⇔B B⇔C =
    record
      { to = (_⇔_.to B⇔C) ∘ (_⇔_.to A⇔B )
      ; from = (_⇔_.from A⇔B) ∘ (_⇔_.from B⇔C )
      } 

And now, from my understanding, I need to prove ⇔≃× : ∀ {A B : Set} → A ⇔ B ≃ (A → B) × (B → A) So to prove this, we need to prove four sections: "to" "from" "from∘to" "to∘from"

⇔≃× : ∀ {A B : Set} → (A ⇔ B) ≃ ((A → B) × (B → A))
⇔≃× =
    record
      { to = λ{ x ⇔ y → ⟨ ( x → y )  , ( y → x ) ⟩ }
      ; from = ?
      ; from∘to = ?
      ; to∘from = ?
      }

But when I finish the "to" section, I want to see if it can pass. So I compile and I got this error message:

Cannot eliminate type (A → B) × (B → A) with variable pattern ⇔(did you supply too many arguments?)when checking the clause left hand side.extendedlambda2 x ⇔ y

Can anyone give some explanation on this type of error message?

Thanks in advance

Answer 1

λ{ x ⇔ y → binds three arguments: x, ⇔, and y but the function you're supposed to define only takes one.