module Chapter5.IDesc where

open import Level 
  renaming ( zero to zeroL 
           ; suc to sucL )

open import Data.Unit 
open import Data.Nat hiding (_⊔_)
open import Data.Fin hiding (lift)
open import Data.Product 

open import Chapter2.Logic

infixr 30 _`×_

data IDesc {k : Level}( : Level)(I : Set k) : Set (k  (sucL )) where
  `var : (i : I)  IDesc  I
  `1 : IDesc  I
  _`×_ : (A B : IDesc  I)  IDesc  I
   : (n : )(T : Fin n  IDesc  I)  IDesc  I
   : (S : Set )(T : S  IDesc  I)  IDesc  I
   : (S : Set )(T : S  IDesc  I)  IDesc  I

⟦_⟧ : ∀{k }{I : Set k}  IDesc  I  (I  Set )  Set 
 `var i  X = X i
 `1  X = Lift 
 A  B  X =  A  X ×  B  X
  n T  X = Σ[ k  Fin n ]  T k  X
  S T  X = Σ[ s  S ]  T s  X
  S T  X = (s : S)   T s  X

⟦_⟧map : ∀{ I X Y}  (D : IDesc  I)  (f : X  Y)    D  X   D  Y
⟦_⟧map (`var i) f xs = f xs
⟦_⟧map `1 f (lift tt) = lift tt
⟦_⟧map (A  B) f (a , b) =  A ⟧map f a ,  B ⟧map f b
⟦_⟧map ( n T) f (k , xs) = k ,  T k ⟧map f xs
⟦_⟧map ( S T) f (s , xs) = s ,  T s ⟧map f xs
⟦_⟧map ( S T) f xs = λ s   T s ⟧map f (xs s)

{-
func : (I J : Set) → Set₁
func I J = J → IDesc I
-}

record func {k : Level}( : Level)(I J : Set k) : Set (k  (sucL )) where
  constructor mk
  field
    out : J  IDesc  I

⟦_⟧func : ∀{k }{I J : Set k}  func  I J  (I  Set )  (J  Set )
 D ⟧func X j =  func.out D j  X 

⟦_⟧fmap : ∀{ I J X Y}  (D : func  I J)  (f : X  Y)    D ⟧func X   D ⟧func Y
 D ⟧fmap f {j} xs =  func.out D j ⟧map f xs