open import Level

open import Data.Unit
open import Data.Product

open import Chapter2.Logic

open import Chapter5.IDesc
open import Chapter5.IDesc.Fixpoint

module Chapter5.IDesc.InitialAlgebra
          {ℓ k : Level}
          {I : Set k}
          (D : func ℓ I I) where

Alg : (I → Set ℓ) → Set (ℓ ⊔ k)
Alg X = {i : I} → ⟦ D ⟧func X i → X i

module Fold  {X : I → Set ℓ}(α : Alg X)
       where

  mutual
    fold : {i : I} → μ D i → X i
    fold ⟨ xs ⟩ = α (hyps (func.out D _) xs)

    hyps : (D' : IDesc ℓ I) → 
           (xs : ⟦ D' ⟧ (μ D)) →
           ⟦ D' ⟧ X
    hyps `1 (lift tt) = (lift tt)
    hyps (`var i) xs = fold xs
    hyps (T `× T') (t , t') = hyps T t , hyps T' t'
    hyps (`σ n T) (k , xs) = k , hyps (T k) xs
    hyps (`Σ S T) (s , xs) = s , hyps (T s) xs
    hyps (`Π S T) f = λ s → hyps (T s) (f s)

fold : {X : I → Set ℓ}(α : Alg X) →
       {i : I} → μ D i → X i
fold = Fold.fold