Agda报错‘Cannot eliminate type...’：⇔≃×同构证明求助

你的代码中to字段的lambda表达式使用了λ{ x ⇔ y → ... }的写法，这是导致报错的核心原因，具体解析如下：

• _⇔_是你定义的record类型，而非带数据构造器的归纳类型，不能用x ⇔ y这种中缀形式做模式匹配。Agda错误地将⇔识别为试图消除(A → B) × (B → A)类型的变量模式，而⇔根本不是该乘积类型的构造器，因此抛出了匹配错误。
• 对于record类型，你需要通过字段访问器或者record { ... }的结构语法来提取内部值。

修正后的代码示例 #

⇔≃× : ∀ {A B : Set} → (A ⇔ B) ≃ ((A → B) × (B → A))
⇔≃× =
    record
      { to = λ{ record { to = t; from = f } → ⟨ t , f ⟩ }
      ; from = λ{ ⟨ t , f ⟩ → record { to = t; from = f } }
      ; from∘to = λ{ record { to = t; from = f } → refl }
      ; to∘from = λ{ ⟨ t , f ⟩ → refl }
      }

或者用字段访问器的简化写法：

⇔≃× : ∀ {A B : Set} → (A ⇔ B) ≃ ((A → B) × (B → A))
⇔≃× =
    record
      { to = λ ab⇔ → ⟨ _⇔_.to ab⇔ , _⇔_.from ab⇔ ⟩
      ; from = λ ab×ba → record { to = proj₁ ab×ba; from = proj₂ ab×ba }
      ; from∘to = λ ab⇔ → refl
      ; to∘from = λ ab×ba → refl
      }

关键错误总结 #

你混淆了record类型与归纳数据类型的模式匹配规则：归纳类型可通过构造器做中缀匹配，但record类型必须通过字段或结构语法提取内部内容，不能自定义中缀匹配形式。

内容的提问来源于stack exchange，提问作者Jackson