Tom de Jong, 31 May 2019

\begin{code}

{-# OPTIONS --without-K --exact-split --safe #-}

open import SpartanMLTT
open import UF-PropTrunc
open import UF-FunExt
open import UF-Subsingletons

module ScottModelOfPCF
        (pt : propositional-truncations-exist)
        (fe : Fun-Ext)
        (pe : propext 𝓀₀)
       where

open PropositionalTruncation pt

open import NaturalNumbers-Properties
open import UF-Miscelanea

open import PCF pt

open import Dcpo pt fe 𝓀₀
open import DcpoConstructions pt fe
open DcpoConstructionsGeneral 𝓀₀
open LiftingDcpo 𝓀₀ pe

open import Lifting 𝓀₀
open import LiftingMonad 𝓀₀ hiding (ΞΌ)

⟦_⟧ : type β†’ DCPOβŠ₯ {𝓀₁} {𝓀₁}
⟦ ΞΉ ⟧     = 𝓛-DCPOβŠ₯ β„•-is-set
⟦ Οƒ β‡’ Ο„ ⟧ = ⟦ Οƒ ⟧ βŸΉα΅ˆαΆœα΅–α΅’βŠ₯ ⟦ Ο„ ⟧

⟦_βŸ§β‚‘ : {Οƒ : type} (t : PCF Οƒ) β†’ ⟨ βŸͺ ⟦ Οƒ ⟧ ⟫ ⟩
⟦ Zero βŸ§β‚‘            = Ξ· zero
⟦ Succ βŸ§β‚‘            = 𝓛̇ succ , 𝓛̇-continuous β„•-is-set β„•-is-set succ
⟦ Pred βŸ§β‚‘            = 𝓛̇ pred , 𝓛̇-continuous β„•-is-set β„•-is-set pred
⟦ ifZero βŸ§β‚‘          = β¦…ifZero⦆
⟦ Fix {Οƒ} βŸ§β‚‘         = ΞΌ ⟦ Οƒ ⟧
⟦ K {Οƒ} {Ο„} βŸ§β‚‘       = Kα΅ˆαΆœα΅–α΅’βŠ₯ ⟦ Οƒ ⟧ ⟦ Ο„ ⟧
⟦ S {ρ} {Οƒ} {Ο„} βŸ§β‚‘   = Sα΅ˆαΆœα΅–α΅’βŠ₯ ⟦ ρ ⟧ ⟦ Οƒ ⟧ ⟦ Ο„ ⟧
⟦ _Β·_ {Οƒ} {Ο„} s t βŸ§β‚‘ = (underlying-function βŸͺ ⟦ Οƒ ⟧ ⟫ βŸͺ ⟦ Ο„ ⟧ ⟫ ⟦ s βŸ§β‚‘) ⟦ t βŸ§β‚‘

\end{code}