module Chapter6.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.Vec
open import Data.Product

open import Chapter5.IDesc
open import Chapter5.IDesc.Tagged
open import Chapter5.IDesc.Fixpoint

data IDescC {ℓ : Level} : Set ℓ where
  `var` `1` `×` `σ` `Σ` `Π` : IDescC

IDescD : ∀(ℓ : Level){k} → Set k → func ((sucL ℓ) ⊔ k) ⊤ ⊤
IDescD ℓ {k} I = func.mk λ _ →
             `Σ IDescC
                λ { `var` → `Σ (Lift {k}{sucL ℓ} I) λ _ → `1 
                  ; `1` → `1 
                  ; `×` → `var tt `× `var tt `× `1 
                  ; `σ` → `Σ (Lift ℕ) λ { (lift n) → (`Π (Lift (Fin n)) λ _ → `var tt) `× `1 }
                  ; `Σ` → `Σ (Lift {sucL ℓ}{k} (Set ℓ)) λ { (lift S) → (`Π (Lift {sucL ℓ}{k}  (Lift {ℓ}{sucL ℓ} S)) λ _ → `var tt) `× `1 }
                  ; `Π` → `Σ (Lift {sucL ℓ}{k} (Set ℓ)) λ { (lift S) → (`Π (Lift {sucL ℓ}{k}  (Lift {ℓ}{sucL ℓ} S)) λ _ → `var tt) `× `1 } }

IDesc' : ∀(ℓ : Level){k} → Set k → Set (k ⊔ (sucL ℓ))
IDesc' ℓ I = μ (IDescD ℓ I) tt

`var' : ∀{ℓ k}{I : Set k} → I → IDesc' ℓ I
`var' i = ⟨ `var` , lift i , lift tt ⟩

`1' : ∀{ℓ k}{I : Set k} → IDesc' ℓ I
`1' = ⟨ `1` , lift tt ⟩

_`×'_ : ∀{ℓ k}{I : Set k} (A B : IDesc' ℓ I) → IDesc' ℓ I
A `×' B = ⟨ `×` , A , B , lift tt ⟩

`σ' : ∀{ℓ k}{I : Set k} (n : ℕ)(T : Fin n → IDesc' ℓ I) → IDesc' ℓ I
`σ' n T = ⟨ `σ` , lift n , (λ { (lift k) → T k }) , lift tt ⟩

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

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