Chapter9.Functions

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 ⊤