module Chapter4.Desc where

open import Level

open import Data.Unit
open import Data.Nat hiding (suc)
open import Data.Fin hiding (suc ; lift)
open import Data.Product
open import Data.Sum

infixr  _`×_
infixr  _`+_

data Desc (ℓ : Level) : Set (suc ℓ) where
  `var : Desc ℓ
  `1 : Desc ℓ
  _`×_ : (A B : Desc ℓ) → Desc ℓ
  _`+_ : (A B : Desc ℓ) → Desc ℓ
  `Σ : (S : Set ℓ)(T : S → Desc ℓ) → Desc ℓ
  `Π : (S : Set ℓ)(T : S → Desc ℓ) → Desc ℓ

⟦_⟧ : ∀{ℓ} → Desc ℓ → Set ℓ → Set ℓ
⟦ `var ⟧ X = X
⟦ `1 ⟧ X = Lift ⊤
⟦ A `× B ⟧ X = ⟦ A ⟧ X × ⟦ B ⟧ X
⟦ A `+ B ⟧ X = ⟦ A ⟧ X ⊎ ⟦ B ⟧ X
⟦ `Σ S T ⟧ X = Σ[ s ∈ S ] ⟦ T s ⟧ X
⟦ `Π S T ⟧ X = (s : S) → ⟦ T s ⟧ X

⟦_⟧map : ∀{ℓ X Y}  → (D : Desc ℓ) → (f : X → Y) →
         ⟦ D ⟧ X → ⟦ D ⟧ Y
⟦ `var ⟧map f xs = f xs
⟦ `1 ⟧map f xs = lift tt
⟦ D₁ `× D₂ ⟧map f (xs₁ , xs₂) = ⟦ D₁ ⟧map f xs₁ , ⟦ D₂ ⟧map f xs₂
⟦ D₁ `+ D₂ ⟧map f (inj₁ x) = inj₁ (⟦ D₁ ⟧map f x)
⟦ D₁ `+ D₂ ⟧map f (inj₂ y) = inj₂ (⟦ D₂ ⟧map f y)
⟦ `Σ S T ⟧map f (s , xs) = s , ⟦ T s ⟧map f xs
⟦ `Π S T ⟧map f xs = λ s → ⟦ T s ⟧map f (xs s)