open import Level open import Chapter5.IDesc open import Chapter8.Ornament module Chapter9.Lift.Fold {ℓ : Level} {I I⁺ : Set ℓ} {D : func ℓ I I} {u : I⁺ → I} (o : orn D u u) where open import Data.Product open import Chapter2.Logic open import Chapter5.IDesc.InitialAlgebra open import Chapter8.Reornament o open import Chapter9.Functions open import Chapter9.FunOrnament open import Chapter9.Patch AlgLift : ∀{T} → Alg D (λ _ → ⟦ T ⟧Type) → FunctionOrn T → Set ℓ AlgLift α T⁺ = Alg reornD (λ ix → Patch (fold D α (proj₂ ix)) T⁺) liftAlg : {i : I}{i⁺ : u ⁻¹ i} {T : Type ℓ}{T⁺ : FunctionOrn T} (α : Alg D (λ _ → ⟦ T ⟧Type)) (β : AlgLift α T⁺) → Patch (fold D α) (μ⁺ o [ i⁺ ]→ T⁺) liftAlg {i⁺ = inv i⁺} α β = λ x x⁺⁺ → fold reornD (λ {ix} ih → β {ix} ih) x⁺⁺