open import Level open import Chapter5.IDesc open import Chapter8.Ornament module Chapter9.Lift.Constructor {ℓ : 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.Fixpoint open import Chapter5.IDesc.Induction open import Chapter7.Case open import Chapter8.Reornament o open import Chapter9.Functions open import Chapter9.FunOrnament open import Chapter9.Patch Extra : {i : I}{i⁺ : u ⁻¹ i} (x : ⟦ D ⟧func (μ D) i) → Set ℓ Extra {i⁺ = inv i⁺} x = Extension (orn.out o i⁺) x Args : {i : I}{i⁺ : u ⁻¹ i} (x : ⟦ D ⟧func (μ D) i) (e : Extra {i⁺ = i⁺} x) → Set ℓ Args {i⁺ = inv i⁺} x e = ⟦ ⟦ Structure (orn.out o i⁺) x e ⟧Orn ⟧ (μ reornD) liftConstructor : {i : I}{i⁺ : u ⁻¹ i} {T : Type ℓ}{T⁺ : FunctionOrn T} {t : ⟦ T ⟧Type} → {x : ⟦ D ⟧func (μ D) i} (e : Extra {i⁺ = i⁺} x) → Args {i⁺ = i⁺} x e → Patch t T⁺ → Patch (⟨ x ⟩ , t) (μ⁺ o [ i⁺ ]× T⁺) liftConstructor {i⁺ = inv i⁺} e a p = ⟨ e , a ⟩ , p