The Scott model of PCF in univalent type theory

Let f : D \to E be a morphism of dcpos and suppose x,y : D with x \leq y. Consider the family \mathsf{1} + \mathsf{1} \to D defined as \operatorname{\mathsf{inl}}(\star) \mapsto x and \operatorname{\mathsf{inr}}(\star) \mapsto y. This family is easily seen to be directed and its least upper bound is y. Now f preserves this least upper bound, so f(x) \leq f(y).

Using monotonicity of f.

The least upper bound of a directed family of dcpo morphisms is also given pointwise. The proof only differs from the standard proof of [Streicher2006, Theorem 4.2] in that it uses directed families, rather than subsets. One may consult the formalisation for the technical details.

Since the order is pointwise, the least morphism from D to E is simply given by mapping every element in D to the least element in E. The rest is as in Theorem 13.

We have formalised the proof of [AbramskyJung1994, Theorem 2.1.19]. We sketch the main construction here. For each natural number n, define \mathsf{iter}(n) : D^D \to D as

By induction on n, one may show that every \mathsf{iter}(n) is continuous. Then, the assignment n~\mapsto~{\mathsf{iter}(n)} is a directed family in D^{\pa*{D^D}}. Finally, one defines \mu as the least upper bound of this directed family. Recall that least upper bounds in the exponential are given pointwise, so that \mu(f) = \bigsqcup_{n : \mathsf{N}} f^n(\bot).

Suppose that \mathsf{N}_{\bot} is (\mathcal{U}_0-)directed complete. Let \alpha : \mathsf{N} \to \mathsf{2} be an arbitrary binary sequence. Define the family \beta : \mathsf{N} \to \mathsf{N}_{\bot} as

Then \beta is directed, so by assumption, it has a supremum s in \mathsf{N}_{\bot}. By the induction principle of sum-types, we can decide whether s = \operatorname{\mathsf{inl}}(k) for some k : \mathsf{N} or s = \operatorname{\mathsf{inr}}(\star). The former implies \sum_{k : \mathsf{N}} \alpha(k) = 1 and we claim that the latter implies \prod_{n : \mathsf{N}} \alpha(n) = 0. For suppose that s = \operatorname{\mathsf{inr}}(\star) and let n : \mathsf{N}. Since \mathsf{2} has decidable equality, it suffices to show that \alpha(n) \neq 1. Assume for a contradiction that \alpha(n) = 1. Then \beta(n) = \operatorname{\mathsf{inl}}(k) for some natural number k \leq n. Using that s is the supremum of \beta yields: \operatorname{\mathsf{inl}}(k) = \beta(n) \leq_\bot s = \operatorname{\mathsf{inr}}(\star). By definition of the order we also have the reverse inequality \operatorname{\mathsf{inr}}(\star) \leq_\bot \operatorname{\mathsf{inl}}(k). Hence, \operatorname{\mathsf{inr}}(\star) = \operatorname{\mathsf{inl}}(k) by antisymmetry, which is a contradiction, so \alpha(n) \neq 1 as desired.

First of all, the characterisation of the identity type of \Sigma-types [HoTTbook, Theorem 2.7.2] yields:

Thus we only have to show that the right-hand side of (Proof) is logically equivalent to (?) in the lemma. Suppose first that we have e' : \operatorname{\mathsf{isdefined}}(l) = \operatorname{\mathsf{isdefined}}(m) and an equality {p : \operatorname{\mathsf{transport}}(e',\operatorname{\mathsf{value}}(l)) = \operatorname{\mathsf{value}}(m)}. Then

Using path induction on e', we can prove that \operatorname{\mathsf{value}}(l) \circ \operatorname{\mathsf{pr_2}}(e) = \operatorname{\mathsf{transport}}(e',\operatorname{\mathsf{value}}(l)). Together with p, this equality implies \operatorname{\mathsf{value}}(l) \circ \operatorname{\mathsf{pr_2}}(e) \sim \operatorname{\mathsf{value}}(m), as desired.

Conversely, suppose e : \operatorname{\mathsf{isdefined}} (l) \leftrightarrow \operatorname{\mathsf{isdefined}} (m) and v : \operatorname{\mathsf{value}} (l) \circ \operatorname{\mathsf{pr_2}}(e) \sim \operatorname{\mathsf{value}}(m). By propositional extensionality, we obtain e' : \operatorname{\mathsf{isdefined}}(l) = \operatorname{\mathsf{isdefined}}(m) from e. From e' we can get an equivalence \mathsf{idtoeqv}(e') : \operatorname{\mathsf{isdefined}} (l) \simeq \operatorname{\mathsf{isdefined}}(m). Furthermore, using path induction on e', one can prove that

Hence, it suffices to show that the right-hand side of (?) is equal to \operatorname{\mathsf{value}}(m). The homotopy v yields \operatorname{\mathsf{value}}(l) \circ \operatorname{\mathsf{pr_2}}(e) = \operatorname{\mathsf{value}}(m) by function extensionality, so it suffices to prove that (\mathsf{idtoeqv}(e'))^{-1} = \operatorname{\mathsf{pr_2}}(e). But these are both functions with codomain \operatorname{\mathsf{isdefined}}(l), which is a proposition, so they are equal by function extensionality.

The proofs are straightforward thanks to Lemma 22. Item (?) is essentially the associativity of \Sigma, i.e. equivalence between \sum_{a : A} \sum_{b : B(a)} C(a,b) and \sum_{(a,b) : \sum_{a : A} B(a)} C(a,b).

As in the proof of Lemma 22, we have:

Since X is a set, the type \operatorname{\mathsf{transport}}(e,\operatorname{\mathsf{value}}(l)) = \operatorname{\mathsf{value}}(m) is a proposition. So, if we can prove that \operatorname{\mathsf{isdefined}}(l) = \operatorname{\mathsf{isdefined}}(m) is a proposition, then the right hand side is a proposition indexed sum of propositions, which is again a proposition.

So let us prove that if P and Q are propositions, then so is P = Q. At first glance, it might seem like one needs univalence (for propositions) to prove this, but in fact propositional extensionality suffices. By [Krausetal2017, Lemma 3.11] (applied to the type of propositions), it suffices to give for every proposition R, a (weakly) constant (i.e. any two of its values are equal) endomap on P = R. But the composition

is weakly constant, because P \leftrightarrow R is a proposition, so this finishes the proof.

First of all, we should prove that \operatorname{\mathcal L}(X) is a poset with the specified order. In particular, \sqsubseteq should be proposition-valued. If X is a set, then \operatorname{\mathsf{isdefined}}(l) \to l = m is a function type into a proposition and therefore a proposition itself.

Reflexivity and transitivity of \sqsubseteq are easily verified. Moreover, \sqsubseteq is seen to be antisymmetric using Lemma 22.

The \bot element of \operatorname{\mathcal L}(X) is given by \bot_X from Definition 19.

The construction of the least upper bound of a directed family is the most challenging part of the proof. Let u : I \to \operatorname{\mathcal L}(X) be a directed family in \operatorname{\mathcal L}(X). Consider the diagram (of solid arrows):

We are going to construct the dashed map \psi that makes the diagram commute and define the least upper bound of u as: \pa*{\squash*{\sum_{i : I}\operatorname{\mathsf{isdefined}}(u_i)},\psi}. Truncating the type is necessary, as \sum_{i : I}\operatorname{\mathsf{isdefined}}(u_i) may have more than one element if I is not a proposition. The difficulty lies in the fact that the universal property of the truncation only tells us how to define maps into propositions. But X is a set. We solve this problem using [Krausetal2017, Theorem 5.4], which says that every weakly constant function f : A \to B to a set B factors through \squash*{A}. That f is weakly constant means that f(a) = f(a') for every a,a' : A. So, to construct \psi, we only need to prove that the top map \varphi in the diagram is weakly constant. Let (i,d_i) , (j,d_j) be two elements of the domain of \varphi. We are to prove that \operatorname{\mathsf{value}}(u_i)(d_i) = \operatorname{\mathsf{value}}(u_j)(d_j). As X is a set, this is a proposition. Therefore, using that u is directed, we obtain k : I with u_i,u_j \sqsubseteq u_k. But d_i : \operatorname{\mathsf{isdefined}}(u_i) and d_j : \operatorname{\mathsf{isdefined}}(u_j), so u_i = u_k = u_j by definition of the order. Hence, \varphi(i,d_i) = \operatorname{\mathsf{value}}(u_i)(d_i) = \operatorname{\mathsf{value}}(u_j)(d_j) = \varphi(j,d_j), as we wished to show.

Let v be the least upper bound of a directed family u : I \to \operatorname{\mathcal L}(X) in \operatorname{\mathcal L}(X). Proving that f^\# is monotone is quite easy. By monotonicity, f^\#(v) is an upper bound for the family f^\# \circ u. We are left to prove that it is the least. Suppose that l : \operatorname{\mathcal L}(Y) is another upper bound for the family f^\#\circ u, i.e. l \sqsupseteq f^\#(u_i) for every i : I. We must show that f^\#(v) \sqsubseteq l. To this end, assume we have q : \operatorname{\mathsf{isdefined}}(f^\#(v)). We must prove that f^\#(v) = l.

From q, we obtain p : \operatorname{\mathsf{isdefined}}(v) by definition of f^\#. By our construction of suprema in \operatorname{\mathcal L}(X) and the fact that f^\#(v) = l is a proposition, we may in fact assume that we have an element i : I and d_i : \operatorname{\mathsf{isdefined}}(u_i). But l \sqsupseteq f^\#(u_i), so using d_i, we get the equality l = f^\#(u_i). Since v is an upper bound for u, the term d_i also yields u_i = v. In particular, l = f^\#(u_i) = f^\#(v), as desired.

We only prove (?) the rest is similar. Suppose r' \mathbin{\triangleright}^\ast r'. Since \operatorname{\mathsf{succ}} r' \mathbin{\triangleright}^\ast \operatorname{\mathsf{succ}} r is a proposition, we may assume that we actually have a term p of type r' \mathbin{\triangleright}_\ast r'. Now we can perform induction on p. The cases were p is formed using \mathsf{refl} or \mathsf{trans} are easy. If p is formed by \mathsf{extend}, then we get a term of type r \mathbin{\triangleright} r' \equiv \squash{r \widetilde{\mathbin{\triangleright}} r'}. Again, as we are proving a proposition, we may suppose the existence of a term of type r \widetilde{\mathbin{\triangleright}} r'. By Definition 33, we then get \operatorname{\mathsf{succ}} r'\widetilde{\mathbin{\triangleright}}\operatorname{\mathsf{succ}} r. This in turn yields, \operatorname{\mathsf{succ}} r'\mathbin{\triangleright}\operatorname{\mathsf{succ}} r and finally we use \mathsf{extend} to get the desired \operatorname{\mathsf{succ}} r'\mathbin{\triangleright}^\ast\operatorname{\mathsf{succ}} r.

We proceed by induction on n. The n\equiv 0 case is by definition of \densem{\underline 0}. Suppose \densem{\underline m} = \eta (m) for a natural number m. Then,

as desired.

Since the carriers of dcpos are defined to be sets, the type \densem{s} = \densem{t} is a proposition. Therefore, we can use induction on the derivation of s \mathbin{\triangleright}^\ast t. We use the Kleisli monad laws in proving some of the cases. For example, one step is to prove that

This may be proved by the following chain of equalities:

By induction on \sigma, making use of the last part of Lemma 36.

By the previous lemma and Lemma 36.

By induction on \sigma. For the base type, this holds vacuously. For function types, it follows by induction hypothesis and the pointwise ordering.

This proof is somewhat different from the classical proof, so we spell out the details. We prove the lemma by induction on \sigma.

The case when \sigma is a function type is easy, because least upper bounds are calculated pointwise and so it reduces to an application of the induction hypothesis. We concentrate on the case when \sigma \equiv \iota instead.

Recall that \bigsqcup_{i : I} d_i is given by \pa*{\squash*{\sum_{i : I} \operatorname{\mathsf{isdefined}}(d_i)}, \varphi}, where \varphi is the factorisation of

through \squash*{\sum_{i : I} \operatorname{\mathsf{isdefined}}(d_i)}.

We are tasked with proving that t \mathbin{\triangleright}^\ast \underline{\varphi (p)} for every p : \operatorname{\mathsf{isdefined}}\pa*{\bigsqcup_{i : I}d_i}. So assume that p : \squash*{\sum_{i : I}\operatorname{\mathsf{isdefined}}(d_i)}. Since we are trying to prove a proposition (as \mathbin{\triangleright}^\ast is proposition-valued), we may actually assume that we have (j,p_{j}) : \sum_{i : I}\operatorname{\mathsf{isdefined}}(d_i). By definition of \varphi we have: \varphi (p) = \operatorname{\mathsf{value}}(d_{j})(p_{j}) and by assumption we know that t \mathbin{\triangleright}^\ast \underline{\operatorname{\mathsf{value}} (d_{j}) (p_{j})}, so we are done.

Let t be a PCF term of type \sigma\Rightarrow\sigma and let f : \densem{\sigma\Rightarrow\sigma} such that t R_{\sigma\Rightarrow\sigma} f. We are to prove that \operatorname{\mathsf{fix}} t R_\sigma \mu(f).

By definition of \mu and the previous lemma, it suffices to prove that \operatorname{\mathsf{fix}} t R_\sigma f^n(\bot) where \bot is the least element of \densem{\sigma} for every natural number n. We do so by induction on n.

The base case is an application of Lemma 46.

Now suppose that \operatorname{\mathsf{fix}} t R_\sigma f^m(\bot). Then, using t R_{\sigma\Rightarrow\sigma} f, we find: t(\operatorname{\mathsf{fix}} t) R_\sigma f(f^m(\bot)). Hence, by Lemma 44, we obtain the desired \operatorname{\mathsf{fix}} t R_\sigma f^{m+1}(\bot), completing our proof by induction.

The proof is by induction on t. The base cases are taken care of by Lemma 45 and the previous lemma. For the inductive step, suppose t is a PCF term of type \sigma\Rightarrow\tau. By induction hypothesis, ts R_\tau \densem{ts} for every PCF term s of type \sigma, but \densem{ts} \equiv \densem{t}\densem{s}, so we are done.

We start by proving the first logical equivalence. The second then follows from the fact that \operatorname{\mathsf{isdefined}}(\densem{t}) is a proposition. Suppose p is of type \operatorname{\mathsf{isdefined}}(\densem{t}). By computational adequacy, we find that t \mathbin{\triangleright}^\ast {\underline {\operatorname{\mathsf{value}} (\densem{t}) (p)}}, so we are done.

Conversely, suppose that we are given a natural number n such that t \mathbin{\triangleright}^\ast \underline n. Soundness and Proposition 40 then yield \densem{t} = \eta(n). Now \star : \operatorname{\mathsf{isdefined}}(\eta(n)), so we may transport along the equality to get an element of \operatorname{\mathsf{isdefined}}(\densem{t}).

This follows from Lemma 51 and Lemma 57.

Define x R' y inductively by:

It is not hard to verify that R' is reflexive, transitive and that it extends R. Using this, one shows that x R' y and x R_\ast y are logically equivalent for every x,y : X. Now one easily proves \prod_{k : \mathsf{N}} (x R_k y \to x R' y) by induction on k. This yields \pa*{\sum_{k : \mathsf{N}} x R_k y} \to x R' y. The converse is also easily established. Thus, x R' y and \sum_{k : \mathsf{N}} x R_k y are logically equivalent, finishing the proof.

Let x and y be in X. By the previous lemma and functoriality of propositional truncation, we have

But the latter is equivalent to \squash*{\sum_{k : \mathsf{N}} \squash*{x R_k y}} \equiv \squash*{\sum_{k : \mathsf{N}} x R^k y} by [HoTTbook, Theorem 7.3.9]. This may also be proved directly, as done in the formalisation.

Suppose that X is decidable. Then there are two cases to consider. Either we have x : X or \lnot X. If we have x : X, then obviously we have |x| : \squash{X}.

So suppose that \lnot X. We claim that \lnot\squash{X}. Assuming \squash{X}, we must find a term of type \mathsf{0}. But \mathsf{0} is a proposition, so we may actually assume that we have x : X. Using \lnot X, we then obtain \mathsf{0}, as desired.

Suppose X and R satisfy conditions (?)–(?). By Lemma 60, it suffices to prove that the untruncated version of R^k, that is R_k, is decidable by induction on k.

For the base case, let x and y be elements of X. We need to decide x R_0 y. By definition this means deciding x = y, which we can, since X is assumed to have decidable equality.

Now suppose x and z are elements of X and that a R_k b is decidable for every a,b : X. We need to show that xR_{k+1}z is decidable. By definition this means that we must prove

to be decidable. By (?), we can decide \sum_{y : X}x R y. Obviously, if we have \lnot\sum_{y : X}x R y, then \lnot\eqref{toprovedec}. So assume that we have y : X such that x R y. By induction hypothesis, y R_k z is decidable. If we have y R_k z, then we get \eqref{toprovedec}. So suppose that \lnot y R_k z. We claim that \lnot\eqref{toprovedec}. For suppose \eqref{toprovedec}, then we obtain y' : X with x R y' and y' R_k z. But R is single-valued, so y = y' and hence, y R_k z, contradicting our assumption.

Suppose that A has decidable equality and I is a set. We are to show that the fiber of t over i has decidable equality for every i : I. Let i : I be arbitrary. Suppose we have (a,p) and (a',p') in the fiber of t over i. Since A has decidable equality, we can decide whether a and a' are equal or not. If they are not, then certainly (a,p) \neq (a',p'). If they are, then we claim that the dependent pairs (a,p) and (a',p') are also equal. If e : a = a' is the supposed equality, then it suffices to show that \operatorname{\mathsf{transport}}^{\lambda x : A.t(x) = i}(e,p) = p', but both these terms are paths in I and I is a set, so they must be equal.

Straightforward.

Let r : Y \to X and s : X \to Y be respectively the retraction and section establishing X as a retract of Y. Let a,b : X. Since Y has decidable equality, we can consider two cases: r(a) = r(b) and r(a) \neq r(b). In the first case, we find a = s(r(a)) = s(r(b)) = b. In the second case, we immediately see that a \neq b. This finishes the proof.

Let X and Y be \Pi-compact types. Suppose F is a type family over X + Y such that F(z) is decidable for every z : X + Y. We must show that \prod_{z : X + Y}F(z) is decidable.

Define F_X : X \to \mathcal U by F_X(x) \vcentcolon\mspace{-1.2mu}\equiv F(\operatorname{\mathsf{inl}}(x)) and F_Y : Y \to\mathcal U as F_Y(y) \vcentcolon\mspace{-1.2mu}\equiv F(\operatorname{\mathsf{inr}}(y)). By our assumption on F, the types F_X(x) and F_Y(y) are decidable for every x : X and y : Y. Hence, since X and Y are assumed to be \Pi-compact, the dependent products \prod_{x : X}F_X(x) and \prod_{y : Y}F_Y(y) are decidable.

Finally, \prod_{z : X + Y}F(z) is logically equivalent to \prod_{x : X}F_X(x) \times \prod_{y : Y}F_Y(y). Since the product of two decidable types is again decidable, an application of Lemma 67 now finishes the proof.

As with Example 63, we only spell out the details for the fragment \mathsf{T}. Recall that \mathsf{T} may be encoded as a \mathsf{W}-type, indexed by the PCF types. Using Example 65 and Lemma 70, we see that B(a) is \Pi-compact for every a : A. Note that A has decidable equality if I does. So it remains to prove that I, the type of PCF types, has decidable equality.

This will be another application of Theorem 66. Define A' \vcentcolon\mspace{-1.2mu}\equiv \mathsf{2} and define B' : A' \to \mathcal U by B'(\operatorname{\mathsf{inl}}(\star)) \vcentcolon\mspace{-1.2mu}\equiv \mathsf{0} and B'(\operatorname{\mathsf{inr}}(\star)) \vcentcolon\mspace{-1.2mu}\equiv \mathsf{2}. Let t' and s' be the unique functions to \mathsf{1} from A' and \sum_{x : A'}B'(x), respectively. One quickly verifies that the type of PCF types is a retract of \mathsf{W}_{s',t'}(\star). Observe that B'(x) is \Pi-compact for every x : A' because of Example 65 and Lemma 70. Finally, \mathsf{1} and A' \equiv 2 clearly have decidable equality, so by Theorem 66 the type \mathsf{W}_{s',t'}(\star) has decidable equality. Thus, by Lemma 69, so do the PCF types.

Let i : I and u,v : \mathsf{W}_{s,t}(i). Taking j \vcentcolon\mspace{-1.2mu}\equiv i and p \vcentcolon\mspace{-1.2mu}\equiv \mathsf{refl}_i in Lemma 79, we see that u = v is decidable, as desired.

Suppose X is a set, x : X and y,y' : Y(x) with e : (x,y) = (x,y'). From e, we obtain e_1 : x = x and e_2 : \operatorname{\mathsf{transport}}^{Y}(e_1,y) = y'. Since X is a set, we must have that e_1 = \mathsf{refl}_{x}, so that from e_2 we obtain a term of type y \equiv \operatorname{\mathsf{transport}}^Y(\mathsf{refl}_{x},y) = y', as desired.

Suppose \mathsf{indexesup}(a,f) = \mathsf{indexedsup}(a,g). Then

As \mathsf{fib}_t(i) is decidable, it is a set by Hedberg’s Theorem [HoTTbook, Theorem 7.2.5]. Therefore f = g by Lemma 74.

By path induction on p.

Suppose i : I and u : \mathsf{W}_{s,t}(i). We proceed by induction on u and so we assume that u \equiv \mathsf{indexedsup}(a,f). The induction hypothesis reads:

Suppose we have j : I with path p : t(a) = j and v : \mathsf{W}_{s,t}(j). By induction, we may assume that v \equiv \mathsf{indexedsup}(a',f'). We are tasked to show that

is decidable, where p : t(a) = t(a').

By assumption the fiber of t over t(a') has decidable equality. Hence, we can decide if \pa*{a',\mathsf{refl}_{t(a')}} and (a,p) are equal or not. Suppose first that the pairs are not equal. We claim that in this case \lnot \eqref{indexedsupdec}. For suppose we had e : \eqref{indexedsupdec}, then

By definition, the right hand side is (a',\mathsf{refl}_{t(a')}). By Lemma 78, the left hand side is equal to (a, \mathsf{refl}_{t(a)} \mathbin{\bullet} p) which is in turn equal to (a,p), contradicting our assumption that \pa*{a',\mathsf{refl}_{t(a')}} and (a,p) were not equal.

Now suppose that \pa*{a',\mathsf{refl}_{t(a')}} = (a,p). From this, we obtain paths e_1 : a' = a and e_2~:~\operatorname{\mathsf{transport}}^{\lambda x : A.t(x) = t(a')}\pa*{e_1,\mathsf{refl}_{t(a')}} = p. By path induction, we may assume e_1 \equiv \mathsf{refl}_{a'}, so that from e_2 we obtain a path

Using this path, we see that the left hand side of (Proof) is equal to \mathsf{indexedsup}(a',f), so we are left to show that

is decidable.

By induction hypothesis (Proof) and the fact that a \equiv a', the type f(b) = f'(b) is decidable for every b : B(a'). Since B(a') is \Pi-compact, this implies that \prod_{b : B(a')}f(b) = f'(b) is decidable.

Suppose first that \prod_{b : B(a')}f(b) = f'(b). Function extensionality then yields f = f', so that \mathsf{indexedsup}(a',f) = \mathsf{indexedsup}(a',f').

On the other hand, suppose \lnot\prod_{b : B(a')}f(b) = f'(b). We claim that then, \mathsf{indexedsup}(a',f) cannot be equal to \mathsf{indexedsup}(a',f'). For suppose that \mathsf{indexedsup}(a',f) = \mathsf{indexedsup}(a',f'). Then Lemma 76 yields f = f', contradicting our assumption that \lnot\prod_{b : B(a)}f(b) = f'(b), and finishing the proof.

If, in (?), we take \mathcal W to be \mathcal U_0 and \mathcal U,\mathcal U',\mathcal V,\mathcal V' all to be \mathcal U_1, then (?) reads:

as desired.