This almost #haskell with #unimath
PCF type σ a
term [[t]] of type [[σ ]], by the following inductive clauses:
(1) [[zero]] :≡ η(0);
(2) [[succ]] :≡ L (s), where s : N → N is the successor function;
(3) [[pred]] :≡ L (p), where p : N → N is the predecessor function;
(4) ifz : [[ι ⇒ ι ⇒ ι ⇒ ι]] is defined using the Kleisli extension as: λx, y.(χx,y
)#, where
χx,y(n) :≡
{
x if n = 0;
y else;
(5) [[k]] :≡ λx, y.x;
(6) [[s]] :≡ λf , g, x.(f (x))(g(x));
(7) [[fix]] :≡ μ, where μ is the least fixed point operator from Theorem 16
file:///home/x/Downloads/the-scott-model-of-pcf-in-univalent-type-theory.pdf