这是在阿格达使用异质平等的正确方式吗?

另一种解决方案,基于重写。请注意,您必须设置公设参数。

open import Data.Vec
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.HeterogeneousEquality

data P : ∀ {n} → Vec ℕ n → Set where

lemma :
  (n : ℕ)
  (xs : Vec ℕ (n + 1))
  (ys : Vec ℕ (suc n))
  (eq : xs ≅ ys)
   → P xs → P ys
lemma n xs ys eq h rewrite +-comm 1 n = subst (λ i → P i) eq h

你也可以摆脱 subst 通过依赖模式匹配:

lemma n xs ys rewrite +-comm n 1 = \ { refl h -> h }

这里有一个解决你问题的方法:

open import Data.Nat using (ℕ ; zero ; suc ; _+_)
open import Data.Product using (Σ-syntax ; _,_ ; proj₁ ; proj₂)
open import Data.Vec using (Vec)
open import Relation.Binary.HeterogeneousEquality using (_≅_ ; refl)
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_ ; refl)


n+1≡Sn : ∀ n → n + 1 ≡ suc n
n+1≡Sn zero = refl
n+1≡Sn (suc n) = ≡.cong suc (n+1≡Sn n)


isubst : ∀ {la lp lq} {A : Set la} {P : A → Set lp} (Q : ∀ a → P a → Set lq)
  → ∀ {a a′}
  → a ≡ a′
  → {p : P a} {p′ : P a′}
  → p ≅ p′
  → Q a p
  → Q a′ p′
isubst Q refl refl h = h


postulate
  n : ℕ
  xs : Vec ℕ (n + 1)
  ys : Vec ℕ (suc n)
  eq : xs ≅ ys
  P : ∀ n → Vec ℕ n → Set


lemma : P (n + 1) xs → P (suc n) ys
lemma h = isubst P (n+1≡Sn n) eq h

这个把戏(憋在心里) isubst )我们正在“统一” xs 和 ys 在消除之前 eq .

一般来说:我总是发现异质平等比它的价值更麻烦。在决定之前,你可能想调查一下替代方案。