------------------------------------------------------------------------
-- 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 χ = μ σ  τ