module Chapter6.Desc where

open import Level

open import Data.Unit
open import Data.Product

open import Chapter4.Desc
open import Chapter4.Desc.Fixpoint


data DescC {ℓ : Level} : Set (suc ℓ) where
  `var` `1` `×` `+` `Σ` `Π` : DescC

DescD : (ℓ : Level) → Desc (suc ℓ)
DescD ℓ = `Σ DescC λ { `var` → `1 
                   ; `1` → `1 
                   ; `×` → `var `× `var `× `1 
                   ; `+` → `var `× `var `× `1 
                   ; `Σ` → `Σ (Set ℓ) λ S → (`Π (Lift {ℓ = suc ℓ} S) λ _ → `var) `× `1  
                   ; `Π` → `Σ (Set ℓ) λ S → (`Π (Lift {ℓ = suc ℓ} S) λ _ → `var) `× `1 } 


Desc' : (ℓ : Level) → Set (suc ℓ)
Desc' ℓ = μ (DescD ℓ)

`var' : ∀{ℓ} → Desc' ℓ
`var' = ⟨ `var` , lift tt ⟩

`1' : ∀{ℓ} → Desc' ℓ
`1' = ⟨ `1` , lift tt ⟩

_`×'_ : ∀{ℓ} → (D D' : Desc' ℓ) → Desc' ℓ
D `×' D' = ⟨ `×` , D , D' , lift tt ⟩

_`+'_ : ∀{ℓ} → (D D' : Desc' ℓ) → Desc' ℓ
D `+' D' = ⟨ `+` , D , D' , lift tt ⟩

`Σ' : ∀{ℓ} → (S : Set ℓ)(T : S → Desc' ℓ) → Desc' ℓ
`Σ' S T = ⟨ `Σ` , S , (λ { (lift s) → T s }) , lift tt ⟩

`Π' : ∀{ℓ} → (S : Set ℓ)(T : S → Desc' ℓ) → Desc' ℓ
`Π' S T = ⟨ `Π` , S , (λ { (lift s) → T s }) , lift tt ⟩