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)