Agda错误消息:无法消除具有可变模式的类型

Question

我被要求完成plfa推荐的一个问题：

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

我知道我需要首先证明等价的一些性质，这里是我的证明：

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 )
} 

现在，根据我的理解，我需要证明⇔≃× : ∀ {A B : Set} → A ⇔ B ≃ (A → B) × (B → A)因此，为了证明这一点，我们需要证明四个部分：；至"从"从"到"从"；

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

但当我完成"；至"；部分，我想看看它是否能通过。所以我编译了，得到了这个错误消息：

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

有人能解释一下这种错误信息吗？

提前感谢

Answer 1

λ{ x ⇔ y →绑定了三个参数：x、⇔和y，但您应该定义的函数只需要一个。