foldr-zip

FoldZipFusion.agda

module FoldZipFusion {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} (_⊕_ : A → B → B) (_⊗_ : C → D → A)where

open import Function
open import Data.List
open import Relation.Binary.PropositionalEquality

_⊛_ : {z : B} → C → (List D → B) → List D → B
_⊛_ {z} x k [] = z
_⊛_ {z} x k (y ∷ ys) = (x ⊗ y) ⊕ k ys

foldr-zip-fusion : ∀ (z : B) (cs : List C) (ds : List D) → ((_∘_ (foldr _⊕_ z)) ∘ zipWith _⊗_) cs ds ≡ (foldr (_⊛_ {z}) (const z)) cs ds
foldr-zip-fusion z [] [] = refl
foldr-zip-fusion z [] (x ∷ ds) = refl
foldr-zip-fusion z (x ∷ cs) [] = refl
foldr-zip-fusion z (x ∷ cs) (x₁ ∷ ds)
  rewrite foldr-zip-fusion z cs ds
        = refl