equality - Agda 中的平等 - 不相关的论点

Question

我有一个依赖类型，它由一个值加上一些关于它的属性的证明组成。自然，我希望我对这种类型的平等概念等同于值组件的平等。这一切都很好，除了我在证明这种平等的提升概念的属性时遇到问题（例如这种类型的列表上的平等）。

例如：

open import Data.Nat
open import Data.Product
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.List.Pointwise renaming (Rel to ListRel) hiding (refl)

module Test where

    _≈_ : Rel (ℕ × ℕ) _
    (a₁ , _) ≈ (a₂ , _) = a₁ ≡ a₂

    ≈-sym : Symmetric _≈_
    ≈-sym refl = refl

    ≋-sym : Symmetric (ListRel _≈_)
    ≋-sym = symmetric ≈-sym

在最后一行中，Agda 抱怨它无法解决对中的第二个投影。有趣的是，将最后一行更改为以下等价的 eta 表达式意味着它可以解决它们：

    ≋-sym = symmetric (λ {x} {y} → ≈-sym {x} {y})

现在我很自然地知道，有时 Agda 无法解决所有隐含的论点，需要一些额外的帮助，但我不明白我通过这样做提供了哪些新信息......

我做了很多提升平等的工作，我宁愿避免在我的代码中到处添加这些丑陋的 eta 扩展。我想知道是否有人有任何建议允许类似于原始代码的内容通过？

我研究了不相关性，但第二个投影在其他地方使用，即使它在计算上与相等性无关。

Answer 1