open import Chapter2.Logic

open import Level

open import Data.Unit
open import Data.Sum
open import Data.Product

open import Chapter4.Desc
open import Chapter4.Desc.Fixpoint
open import Chapter4.Desc.Lifting
open import Chapter4.Desc.Induction


module Chapter6.Desc.InitialAlgebra 
         {ℓ : Level}
         {X : Set ℓ}
         (D : Desc ℓ)
         (α : ⟦ D ⟧ X → X)
       where


fold : μ D → X
fold x = induction D (λ _ -> X) 
                  (λ {xs} ih → α (replace D xs ih))
                  x
  where replace : (D' : Desc ℓ)(xs : ⟦ D' ⟧  (μ D))
                  (ih : [_]^ {k = zero} D' (λ _ → X) xs) → ⟦ D' ⟧ X
        replace `var xs x = x
        replace `1 (lift tt) (lift tt) = lift tt
        replace (D `× D') (xs , xs') (x , x') = replace D xs x , replace D' xs' x'
        replace (D `+ D') (inj₁ xs) x = inj₁ (replace D xs x)
        replace (D `+ D') (inj₂ xs') x' = inj₂ (replace D' xs' x')
        replace (`Σ S T) (s , xs) ih = s , replace (T s) xs ih
        replace (`Π S T) xs ih = λ s → replace (T s) (xs s) (ih s)