open import Level

open import Data.Unit
open import Data.Product

open import Chapter2.Logic

open import Chapter5.IDesc
open import Chapter5.IDesc.Fixpoint
open import Chapter5.IDesc.Lifting
open import Chapter5.IDesc.Induction


module Chapter6.IDesc.InitialAlgebra 
         {ℓ k : Level}
         {I : Set k}{X : I → Set ℓ}
         (D : func ℓ I I)
         (α : {i : I} → ⟦ D ⟧func X i → X i)
       where


fold : {i : I} → μ D i → X i
fold x = lower (induction D (λ {i} _ → Lift {ℓ}{k} (X i))
                   (λ {i}{xs} ih → lift (α (replace (func.out D i) xs ih)))
                   x)
  where replace : (D' : IDesc ℓ I)(xs : ⟦ D' ⟧ (μ D)) →
                  (ih : [ D' ]^h (λ {i} _ → Lift (X i)) xs) →
                  ⟦ D' ⟧ X
        replace (`var i) xs (lift 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 (`σ n T) (k , xs) ih = k , replace (T k) xs ih
        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)