congruencia por la igualdad heterogéneo

Question

Estoy tratando de utilizar la igualdad heterogéneo para probar las declaraciones que implican este tipo de datos indexada:

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

yo era capaz de escribir mis pruebas usando Relation.Binary.HeterogenousEquality.≅-Razonamiento, pero sólo asumiendo la propiedad siguiente congruencia:

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′ = {!!} 

sin embargo, no puede coincidir con el patrón en k≅k′ siendo refl sin obtener el siguiente mensaje de error desde el comprobador de tipos:

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

y si trato de hacer un análisis de caso en k≅k′ (es decir mediante el uso de C-c C-c de la interfaz de Emacs) para asegurarse de que todos los argumentos implícitos están correctamente emparejados con respecto a sus limitaciones impuestas por el refl, consigo

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′] 

(si está interesado, aquí hay algunos no relevante antecedentes: Eliminating subst to prove equality)

Answer 1

Lo que puede hacer es tomar una prueba adicional de que los dos índices son iguales:

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 

El problema original es que el conocimiento de Counter n ≅ Counter n′ doesn Implica n ≡ n′ porque no se supone que los constructores de tipo sean inyectivos (hay una marca --injective-type-constructors para esto, que de hecho hace que la coincidencia se realice, pero se sabe que es inconsistente con el medio excluido), por lo que puede concluir que los dos tipos son iguales, no reescribirá n en n′ y entonces obtendrá ese error cuando verifique más tarde si k y k′ son unificables.

Desde Counter n tiene exactamente n elementos, en realidad es posible probar Counter es inyectiva usando algo así como el principio del palomar (e igualdad quizá decidable de productos naturales), por lo que podría hacer sin el argumento n ≅ n′, aunque eso sería sucio.

Editar: AFAICT el Het. la conducta de igualdad sigue siendo la misma.