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 })