open import Data.Unit
open import Data.Product

open import Logic.Logic

open import IDesc.IDesc
open import IDesc.Fixpoint


module IDesc.Lifting
          {I : Set}
          {X : I  Set } where


□h : (D : IDesc  I)(P : ∀{i}  X i  Set) (xs :  D  X)  Set
□h `1 P tt = 
□h (`var i) P xs = P xs
□h (T  T') P (t , t') =  □h T P t × □h T' P t'
□h ( n T) P (k , xs) = □h (T k) P xs
□h ( S T) P (s , xs) = □h (T s) P xs
□h ( S T) P f = (s : S)  □h (T s) P (f s) 

□hmap : (D : IDesc  I){P : ∀{i}  X i  Set}(p : ∀{i}  (x : X i)  P x)
          (xs :  D  X)  □h D P xs
□hmap `1 p tt = tt
□hmap (`var i) p xs = p xs
□hmap (T  T') p (t , t')= □hmap T p t , □hmap T' p t'
□hmap ( n T) p (k , xs) = □hmap (T k) p xs
□hmap ( S T) p (s , xs) = □hmap (T s) p xs
□hmap ( S T) p f = λ s  □hmap (T s) p (f s)

 : (D : func  I I)(P : ∀{i}  X i  Set)(xs : Σ[ i  I ]  D ⟧func X i)  Set
 D P (i , xs) = □h (func.out D i) P xs

□map : (D : func  I I){P : ∀{i}  X i  Set}(p : ∀{i}  (x : X i)  P x)
          (xs : Σ[ i  I ]  D ⟧func X i)   D P xs
□map D p (i , xs) = □hmap (func.out D i) p xs