[ re #10 ] n-ary functions manipulating lists

[gallais]

No description provided.

[jamesmckinna]

I don't know what the library conventions are about pointfree vs. pointwise function composition, but how about

zipWith (suc n@(suc _)) f (v , vs) (w , ws) =
  f zero v w , zipWith n (f ∘ suc) vs ws

versus your

zipWith (suc n@(suc _)) f (v , vs) (w , ws) =
  f zero v w , zipWith n (λ k → f (suc k)) vs ws

[gallais]

I had started with that alternative but it does not typecheck.

[jamesmckinna]

Hmmm. I begin to see why: the type of _∘_ would need to be generalised so that its Level arguments b,c were made dependent (resp. on (x : A), {x : A} (y : B y)... and even then the typechecker really gets confused, trying to unify Levelₙ lsas k ⊔ Levelₙ lsbs k ⊔ Levelₙ lscs k with Levelₙ lsas k ⊔ Levelₙ lsbs k ⊔ Levelₙ lscs k... so consider my query withdrawn... ;-)

... but I can't help wondering what would value dependent levels look like, and how should we expect them to behave?