I've been trying to translate the paper "Continuation-Passing Style, Defunctionalization, Accumulations, and Associativity" available here: https://arxiv.org/ftp/arxiv/papers/2111/2111.10413.pdf from Idris to Agda.
The final example discusses generalized composition, which appears to be equivalent to the mapₙ function in Function.Nary.NonDependent.Base, and proves that it is pseudo-associative. I have been struggling to get this to typecheck in Agda. What I would like is a type like below:
mapₙ-assoc : ∀ {n m : ℕ} {ls ls′ r s t} {x : Set r} {y : Set s} {z : Set t} {as : Sets n ls} {bs : Sets m ls′}
→ (h : y → z) → (g : Arrows (suc m) (x , bs) y) → (f : Arrows n as x)
→ mapₙ n (mapₙ (suc m) h g) f ≡ mapₙ (n + m) h (mapₙ n g f)
But this does not type check with the error:
n != n + m of type ℕ
when checking that the expression mapₙ n g f has type _as_1119 ⇉ y
I have tried making the below version, but I can't figure out how to make the induction step work or even if it could work like this.
mapₙ-assoc : ∀ {n m : ℕ} {ls ls′ r s t} {x : Set r} {y : Set s} {z : Set t} {as : Sets n ls} {bs : Sets m ls′}
→ (h : y → z) → (g : Arrows (suc m) (x , bs) y) → (f : Arrows n as x) → Set _
mapₙ-assoc {zero} {m} h g f = mapₙ zero (mapₙ (suc m) h g) f ≡ mapₙ (zero + m) h (mapₙ zero g f)
mapₙ-assoc {suc n} {m} h g f = {!!}
This version works for any specific n that I've tried, not just zero, so I assume Agda can expand to see the types are equal, but I can't convince it that they are with a general n.
The problem is that mapₙ n g f has type Arrows n as (Arrows m bs y), not Arrows (n + m) (as ++ bs) y. You can prove these equivalent and convert between them (you'll have to define _++_ for Levels and Sets first), or you could just use mapₙ n (mapₙ m h) instead of mapₙ (n + m) h.
mapₙ-assoc : ∀ {n m : ℕ} {ls ls′ r s t} {x : Set r} {y : Set s} {z : Set t} {as : Sets n ls} {bs : Sets m ls′}
→ (h : y → z) → (g : Arrows (suc m) (x , bs) y) → (f : Arrows n as x)
→ mapₙ n (mapₙ (suc m) h g) f ≡ mapₙ n (mapₙ m h) (mapₙ n g f)