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