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)