Dependent type involving nat addition

Question

I need to define two versions of an operation with a slightly different definition. It is a series of compositions with Nat indices involved.

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

I would like to define both p1 and p2 and be able to use them interchangeably. Is this doable?

Answer 1

You can define p2 by direct recursion (no subst or rewriting) over _+_ using the trick described here. Looks like this:

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

The cost is that you need to maintain those Homable records which is somewhat tedious, but to my experience proving things about functions defined this way is simpler than about functions defined in terms of subst or over _+′_ (unless you never want to coerce _+′_ to _+_, of course).