open import Level

open import Data.Unit
open import Data.Product
open import Data.Sum

open import Chapter2.Logic

open import Chapter4.Desc
open import Chapter4.Desc.Fixpoint


module Chapter4.Desc.Lifting
          {ℓ k : Level}
          {X : Set ℓ} where


[_]^ : (D : Desc ℓ)(P : X → Set (ℓ ⊔ k)) (xs : ⟦ D ⟧ X) → Set (ℓ ⊔ k)
[ `1 ]^ P (lift tt) = Lift ⊤
[ `var ]^ P xs = P xs
[ T `× T' ]^ P (t , t') =  [ T ]^ P t × [ T' ]^ P t'
[ T `+ T' ]^ P (inj₁ t) =  [ T ]^ P t
[ T `+ T' ]^ P (inj₂ t') =  [ T' ]^ P t'
[ `Σ S T ]^ P (s , xs) = [ T s ]^ P xs
[ `Π S T ]^ P f = (s : S) → [ T s ]^ P (f s) 

[_]^map : (D : Desc ℓ){P : X → Set (ℓ ⊔ k)}(p : (x : X) → P x)
          (xs : ⟦ D ⟧ X) → [ D ]^ P xs
[ `1 ]^map p (lift tt) = lift tt
[ `var ]^map p xs = p xs
[ T `× T' ]^map p (t , t')= [ T ]^map p t , [ T' ]^map p t'
[ T `+ T' ]^map p (inj₁ t) = [ T ]^map p t
[ T `+ T' ]^map p (inj₂ t') =  [ T' ]^map p t'
[ `Σ S T ]^map p (s , xs) = [ T s ]^map p xs
[ `Π S T ]^map p f = λ s → [ T s ]^map p (f s)