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)