module Palmse.Combinators.Sem where open import Palmse.Combinators.TyTm open import Data.Nat [[_]]₀ : Ty -> Set [[ N ]]₀ = ℕ [[ a => b ]]₀ = [[ a ]]₀ -> [[ b ]]₀ [[_]]₁ : {a : Ty} -> Tm a -> [[ a ]]₀ [[ ze ]]₁ = zero [[ su ]]₁ = suc [[ k ]]₁ = \x y -> x [[ s ]]₁ = \x y z -> x z (y z) [[ e ´ e' ]]₁ = [[ e ]]₁ [[ e' ]]₁