open import Level open import Chapter5.IDesc open import Chapter8.Ornament module Chapter9.Lift.Induction {ℓ : 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.Induction open import Chapter8.Reornament o open import Chapter9.Functions open import Chapter9.FunOrnament open import Chapter9.Patch DAlgLift : {T : Type ℓ} → DAlg D (λ _ → ⟦ T ⟧Type) → FunctionOrn T → Set ℓ DAlgLift α T⁺ = DAlg reornD ((λ {ix} _ → Patch (induction D _ α (proj₂ ix)) T⁺)) liftInd : {i : I}{i⁺ : u ⁻¹ i} {T : Type ℓ}{T⁺ : FunctionOrn T} (α : DAlg D (λ _ → ⟦ T ⟧Type)) (β : DAlgLift α T⁺) → Patch (induction D (λ _ → ⟦ T ⟧Type) α) (μ⁺ o [ i⁺ ]→ T⁺) liftInd {i⁺ = inv i⁺} α β = λ x x⁺⁺ → induction reornD _ (λ {ix} → β {ix}) x⁺⁺