异质平等的一致性

我正在尝试使用异构相等来证明涉及此索引数据类型的语句：

data Counter : ℕ → Set where
  cut : (i j : ℕ) → Counter (suc i + j)

我能够使用以下方式编写我的证明Relation.Binary.HeterogenousEquality.≅-Reasoning，但仅通过假设以下同余性质：

Counter-cong : ∀ {n n′} {k : Counter n} {k′ : Counter n′} →
               {A : ℕ → Set} → (f : ∀{n} → Counter n → A n) →
               k ≅ k′ → f k ≅ f k′
Counter-cong f k≅k′ = {!!}

但是，我无法进行模式匹配k≅k′ being refl没有从类型检查器收到以下错误消息：

Refuse to solve heterogeneous constraint 
    k : Counter n =?= k′ : Counter n′

如果我尝试做一个案例分析k≅k′（即通过使用C-c C-c来自 Emacs 前端），以确保所有隐式参数都与其施加的约束正确匹配refl, I get

Cannot decide whether there should be a case for the constructor
refl, since the unification gets stuck on unifying the 
inferred indices 
    [{.Level.zero}, {Counter n}, k] 
with the expected indices 
    [{.Level.zero}, {Counter n′}, k′]

（如果您有兴趣，这里有一些不相关的背景：消除subst来证明平等 https://stackoverflow.com/questions/9246705)

您可以做的是额外证明两个索引相等：

Counter-cong : ∀ {n n′} {k : Counter n} {k′ : Counter n′} →
               {A : ℕ → Set} → (f : ∀{n} → Counter n → A n) →
               n ≅ n′ → k ≅ k′ → f k ≅ f k′
Counter-cong f refl refl = refl

原来的问题是知道Counter n ≅ Counter n′并不意味着n ≡ n′因为类型构造函数不被假定为单射的（有一个标志--injective-type-constructors为此，这实际上使匹配成功，但众所周知与排除的中间不一致），因此虽然它可以得出两种类型相等的结论，但它不会重写n to n′所以当它稍后检查是否时你会得到这个错误k and k′是可以统一的。

Since Counter n正好有n元素，实际上可以证明Counter是单射的，使用类似鸽巢原理的东西（也许自然数的可判定相等），所以你可以不用n ≅ n′争论，尽管那会很混乱。

编辑：AFAICT Het。平等行为仍然是一样的。