How do I convert the result?

Question

I have this Agda program:

data ℕ⁺ : ℕ → Set where
  one : ℕ⁺ (suc zero)
  suc⁺ : {n : ℕ} → ℕ⁺ (suc n)

lemma : ∀ (m n : ℕ) → m ≡ suc n → ℕ⁺ m
lemma m zero p = one
lemma m (suc n) p  = suc⁺ {suc n}

The problem is in the second-last line: it complains one is not ℕ⁺ m, however I have p there to prove that they actually are.

How can I do this? I know how do it if what I wanted to prove were in fact an equality (well, just pass p in this case), but I don't know how to use p to convert a generic ℕ⁺ m to ℕ⁺ (suc zero).

user_1935631 · Answer

Equality type _≡_ has no special meaning in Agda. To Agda one looks like a value of type ℕ⁺ (suc zero), and it needs ℕ⁺ m. transport should help.

transport : forall {A : Set} {B : A → Set} {x y : A} → x ≡ y → B x → B y
transport refl bx = bx

comm : forall {A : Set} {x y : A} → x ≡ y → y ≡ x
comm {x = x} p = transport {B = _≡ x} p refl

lemma : ∀ (m n : ℕ) → m ≡ suc n → ℕ⁺ m
lemma _ _ p  = transport {B = \k → ℕ⁺ k} (comm p) suc⁺

(Here I removed one, since it is not needed.)

user_477476 · Answer

If you pattern match on p, it will refine m into .(suc n):

lemma : ∀ (m n : ℕ) → m ≡ suc n → ℕ⁺ m
lemma .(suc n) zero    refl = one
lemma .(suc n) (suc n) refl = suc⁺

(disclaimer: this is from a non-HoTT/CTT perspective; this probably wouldn't work without axiom K.)

How do I convert the result?

2 Answers