open import Level

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

open import Chapter2.Logic

open import Chapter4.Desc
open import Chapter4.Desc.Fixpoint

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

mutual
  fold : μ D → X 
  fold ⟨ xs ⟩ = α (hyps D xs)

  hyps : (D' : Desc ℓ) → 
         (xs : ⟦ D' ⟧ (μ D)) →
         ⟦ D' ⟧ X
  hyps `1 (lift tt) = lift tt
  hyps `var xs = fold xs
  hyps (T `× T') (t , t') = hyps T t , hyps T' t'
  hyps (T `+ T') (inj₁ t) = inj₁ (hyps T t)
  hyps (T `+ T') (inj₂ t') = inj₂ (hyps T' t')
  hyps (`Σ S T) (s , xs) = s , hyps (T s) xs
  hyps (`Π S T) f = λ s → hyps (T s) (f s)