open import Level open import Data.Unit open import Data.Product open import Chapter2.Logic open import Chapter5.IDesc open import Chapter8.Ornament module Chapter8.Ornament.Examples.Lifting {ℓ : Level} {K L : Set ℓ} {X : K → Set ℓ} where private u : Σ K X → K u = proj₁ [_]^h : (D : IDesc ℓ K) → ⟦ D ⟧ X → Orn u D [ `1 ]^h (lift tt) = `1 [ `var k ]^h x = `var (inv (k , x)) [ T `× T' ]^h (t , t') = [ T ]^h t `× [ T' ]^h t' [ `σ n T ]^h (k , xs) = deleteσ k ([ T k ]^h xs) [ `Σ S T ]^h (s , xs) = deleteΣ s ([ T s ]^h xs) [ `Π S T ]^h f = `Π λ s → [ T s ]^h (f s) [_]^ : (D : func ℓ K L) → orn D proj₁ proj₁ [ D ]^ = orn.mk (λ { (k , x) → [ func.out D k ]^h x })