------------------------------------------------------------------------
-- Semantics
------------------------------------------------------------------------

module RecursiveTypes.Semantics where

open import Coinduction

open import RecursiveTypes.Syntax
open import RecursiveTypes.Substitution

-- The semantics of a recursive type, i.e. its possibly infinite
-- unfolding.

⟦_⟧ : ∀ {n} → Ty n → Tree n
⟦ ⊥ ⟧       = ⊥
⟦ ⊤ ⟧       = ⊤
⟦ var x ⟧   = var x
⟦ σ ⟶ τ ⟧   = ♯ ⟦ σ ⟧         ⟶ ♯ ⟦ τ ⟧
⟦ μ σ ⟶ τ ⟧ = ♯ ⟦ σ [0≔ χ ] ⟧ ⟶ ♯ ⟦ τ [0≔ χ ] ⟧
              where χ = μ σ ⟶ τ