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  _`×_

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