Defining decidable equality for dependent pair in Agda

Question

I am trying to define decidable equality on a sigma type, but getting stuck despite my goal matches what I have in the hole.

module SigmaEqual where

open import Function using (id)
open import Data.Nat using (ℕ) renaming (_≟_ to _≟ℕ_)
open import Data.Product using (Σ; _,_; proj₁; proj₂)
open import Relation.Nullary using (yes; no)
open import Relation.Binary using (Decidable)
open import Relation.Binary.PropositionalEquality using (_≡_; cong; refl)

data B : ℕ → Set where
  bcons : (n : ℕ) → B n

Tuple = Σ ℕ B

_≟B_ : ∀ {n} → Decidable {A = B n} _≡_
bcons n ≟B bcons .n = yes refl

_≟_ : Decidable {A = Tuple} _≡_
(n₁ , b₁) ≟ (n₂ , b₂) with n₁ ≟ℕ n₂
(n₁ , b₁) ≟ (n₂ , b₂) | no ¬p = no λ q → ¬p (cong proj₁ q)
(n₁ , b₁) ≟ (.n₁ , b₂) | yes refl with b₁ ≟B b₂
(n₁ , b₁) ≟ (.n₁ , .b₁) | yes refl | yes refl = yes refl
(n₁ , b₁) ≟ (.n₁ , b₂) | yes refl | no ¬p = no λ q → ¬p (lemm {n₁} {b₁} {b₂} q)
  where
  lemm : {a : ℕ}{b₁ b₂ : B n₁} → (a , b₁) ≡ (a , b₂) → b₁ ≡ b₂
  lemm refl = refl

When I inspect the context in the hole I have the following:

Goal: (n₁ , b₁) ≡ (n₁ , b₂)
Have: (n₁ , b₁) ≡ (n₁ , b₂)
————————————————————————————————————————————————————————————
q  : (n₁ , b₁) ≡ (n₁ , b₂)
¬p : b₁ ≡ b₂ → .Data.Empty.⊥
...

So I imagine I should be able to refine this and place q in its place, but it doesn't work and if I put q, I get the following error.

x != n₁ of type ℕ when checking that the expression q has type (n₁ , b₁) ≡ (n₁ , b₂)

This is particularly baffling as I don't know where the x in question comes from.

Answer 1

You can figure out what's going on by adding the following lines at the top of your file:

{-# OPTIONS --show-implicit #-}
open import Agda.Primitive

Then you can see what goes wrong:

Goal: _≡_ {lzero} {Σ {lzero} {lzero} ℕ (λ v → B n₁)} (n₁ , b₁)
      (n₁ , b₂)
Have: _≡_ {lzero} {Σ {lzero} {lzero} ℕ B} (n₁ , b₁) (n₁ , b₂)

You can see in the goal you have a non-dependent sigma type but your lemma has a dependent one! So you just need to change the dependency of B on n₁ in your lemma to a:

lemm : {a : ℕ}{b₁ b₂ : B a} → _≡_ {A = Tuple} (a , b₁) (a , b₂) → b₁ ≡ b₂
lemm refl = refl

With this small change to the type of lemma, your proof is accepted!