\begin{code}
{-# OPTIONS --rewriting --confluence-check #-}

module PCF.Types where

open import Data.Bool.Base 
  using (Bool)
open import Agda.Builtin.Nat
  using (Nat)

open import PCF.Domain-Notation
  using (Domain; ⟪_⟫; _→ᶜ_; _+⊥)

-- Syntax

data Types : Set where
  ι    : Types                  -- natural numbers
  o    : Types                  -- Boolean truthvalues
  _⇒_  : Types → Types → Types  -- functions

variable σ τ : Types

infixr  _⇒_

-- Semantics 𝒟

𝒟 : Types → Domain

𝒟 ι        = Nat  +⊥
𝒟 o        = Bool +⊥
𝒟 (σ ⇒ τ)  = 𝒟 σ →ᶜ 𝒟 τ

variable x y z : ⟪ 𝒟 σ ⟫
\end{code}