open import Level 

open import Data.Unit
open import Data.Product

open import Chapter2.Logic

open import Chapter5.IDesc
open import Chapter5.IDesc.Fixpoint


module Chapter5.IDesc.Lifting
          {ℓ k : Level}
          {I : Set k}
          {X : I → Set ℓ} where


[_]^h : (D : IDesc ℓ I)(P : ∀{i} → X i → Set (k ⊔ ℓ)) (xs : ⟦ D ⟧ X) → Set (k ⊔ ℓ)
[ `1 ]^h P (lift tt) = Lift ⊤
[ `var i ]^h P xs = P xs
[ T `× T' ]^h P (t , t') =  [ T ]^h P t × [ T' ]^h P t'
[ `σ n T ]^h P (k , xs) = [ T k ]^h P xs
[ `Σ S T ]^h P (s , xs) = [ T s ]^h P xs
[ `Π S T ]^h P f = (s : S) → [ T s ]^h P (f s) 

[_]^hmap : (D : IDesc ℓ I){P : ∀{i} → X i → Set (k ⊔ ℓ)}(p : ∀{i} → (x : X i) → P x)
          (xs : ⟦ D ⟧ X) → [ D ]^h P xs
[ `1 ]^hmap p (lift tt) = lift tt
[ `var i ]^hmap p xs = p xs
[ T `× T' ]^hmap p (t , t')= [ T ]^hmap p t , [ T' ]^hmap p t'
[ `σ n T ]^hmap p (k , xs) = [ T k ]^hmap p xs
[ `Σ S T ]^hmap p (s , xs) = [ T s ]^hmap p xs
[ `Π S T ]^hmap p f = λ s → [ T s ]^hmap p (f s)

[_]^ : (D : func ℓ I I)(P : ∀{i} → X i → Set (k ⊔ ℓ))(xs : Σ[ i ∈ I ] ⟦ D ⟧func X i) → Set (k ⊔ ℓ)
[ D ]^ P (i , xs) = [ func.out D i ]^h P xs

[_]^map : (D : func ℓ I I){P : ∀{i} → X i → Set (k ⊔ ℓ)}(p : ∀{i} → (x : X i) → P x)
          (xs : Σ[ i ∈ I ] ⟦ D ⟧func X i) → [ D ]^ P xs
[ D ]^map p (i , xs) = [ func.out D i ]^hmap p xs 


-- Intellectual curiosity:

[_]^hD : (D : IDesc ℓ I)(xs : ⟦ D ⟧ X) → IDesc (k ⊔ ℓ) (Σ I X)
[ `1 ]^hD (lift tt) = `1
[ `var i ]^hD xs = `var (i , xs)
[ T `× T' ]^hD (t , t') =  [ T ]^hD t `× [ T' ]^hD t'
[ `σ n T ]^hD (k , xs) = [ T k ]^hD xs
[ `Σ S T ]^hD (s , xs) = [ T s ]^hD xs
[ `Π S T ]^hD f = `Π (Lift {ℓ}{k} S) λ { (lift s) → [ T s ]^hD (f s) }

[_]^hmapD : (D : IDesc ℓ I){P : Σ I X → Set (k ⊔ ℓ)}(p : ∀{i} → (x : X i) → P (i , x)) →
           (xs : ⟦ D ⟧ X) → ⟦ ([ D ]^hD xs) ⟧ (λ _ → Lift ⊤) → ⟦ [ D ]^hD xs ⟧ P
[ D ]^hmapD p xs = ⟦ [ D ]^hD xs ⟧map (λ {ix} tt → p (proj₂ ix))