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 ⟩