Как мне конвертировать результат?

Question

У меня есть эта программа Agda:

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}

Проблема во второй последней строке: он жалуется, что one не ℕ⁺ m, однако у меня есть p, чтобы доказать, что они на самом деле.

Как я могу это сделать? Я знаю, как это сделать, если то, что я хотел доказать, на самом деле было равенством (ну, просто передайте p в этом случае), но я не знаю, как использовать p для преобразования универсального ℕ⁺ m в ℕ⁺ (suc zero).

Answer 1

Тип равенства _≡_ не имеет особого значения в Агде.Для Agda one выглядит как значение типа ℕ⁺ (suc zero), и для этого нужно ℕ⁺ m.transport должно помочь.

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⁺

(Здесь я удалил one, так как он не нужен.)

Answer 2

Если вы сопоставите паттерн с p, он уточнит m в .(suc n):

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

(отказ от ответственности: это не с точки зрения HoTT / CTT; вероятно, это не сработает без аксиомы K .)