agda - 涉及 nat 添加的依赖类型

我需要定义一个操作的两个版本，但定义略有不同。它是一系列涉及 Nat 指数的组合。

open import Data.Nat

data Hom : ℕ → ℕ → Set where
  id    : (m : ℕ) → Hom m m
  _∘_   : ∀ {m n k} → Hom n k → Hom m n → Hom m k
  p     : (n : ℕ) → Hom (suc n) n

p1 : (m n : ℕ) → Hom (m + n) n
p1 zero n    = id n
p1 (suc m) n = p1 m n ∘ p (m + n)

p2 : (m n : ℕ) → Hom (m + n) n
p2 zero n    = id n
p2 (suc m) n = {!!} -- p n ∘ p2 m (1 + n)

-- Goal: Hom (suc (m + n)) n
-- Have: Hom (m + suc n) n

我想同时定义 p1 和 p2 并且能够互换使用它们。这是可行的吗？

最佳答案

您可以使用 here 描述的技巧通过 p2 上的直接递归(无 subst 或重写)来定义 _+_。看起来像这样:

record Homable (H : ℕ → ℕ → Set) : Set where
  field
    id-able  : (m : ℕ) → H m m
    _∘-able_ : ∀ {m n k} → H n k → H m n → H m k
    p-able   : (n : ℕ) → H (suc n) n

suc-homable : ∀ {H} → Homable H → Homable (λ m n -> H (suc m) (suc n))
suc-homable homable = record
  { id-able  = λ m → id-able (suc m)
  ; _∘-able_ = _∘-able_
  ; p-able   = λ m → p-able (suc m)
  } where open Homable homable

p2-go : ∀ {H} → Homable H → (m : ℕ) → H m 0
p2-go homable  zero   = id-able 0 where
  open Homable homable
p2-go homable (suc m) = p-able 0 ∘-able p2-go (suc-homable homable) m where
  open Homable homable

plus-homable-hom : ∀ k → Homable (λ m n → Hom (m + k) (n + k))
plus-homable-hom k = record
  { id-able  = λ n → id (n + k)
  ; _∘-able_ = _∘_
  ; p-able   = λ n → p (n + k)
  }

p2 : (m n : ℕ) → Hom (m + n) n
p2 m n = p2-go (plus-homable-hom n) m

代价是你需要维护那些有点乏味的 Homable 记录，但根据我的经验，证明以这种方式定义的函数比用 subst 或 _+′_ 定义的函数更简单(除非你永远不想将 _+′_ 强制转换为 _+_ ， 当然)。

关于agda - 涉及 nat 添加的依赖类型，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/47114214/