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