module Chapter9.Functions where open import Level renaming ( suc to sucL ) open import Data.Unit open import Data.Product open import Chapter5.IDesc open import Chapter5.IDesc.Fixpoint infixr 20 μ_[_]→_ infixr 20 μ_[_]×_ data Type {k}(ℓ : Level) : Set (sucL (k ⊔ ℓ)) where μ_[_]→_ : {I : Set k}(D : func ℓ I I)(i : I)(T : Type {k} ℓ) → Type ℓ μ_[_]×_ : {I : Set k}(D : func ℓ I I)(i : I)(T : Type {k} ℓ) → Type ℓ `⊤ : Type ℓ ⟦_⟧Type : ∀{k ℓ} → Type {k} ℓ → Set ℓ ⟦ μ D [ i ]→ T ⟧Type = μ D i → ⟦ T ⟧Type ⟦ μ D [ i ]× T ⟧Type = μ D i × ⟦ T ⟧Type ⟦ `⊤ ⟧Type = Lift ⊤