open import Cat.Functor.Subcategory
open import Cat.Displayed.Total
open import Cat.Prelude

open import Data.Bool

open import Order.Diagram.Lub
open import Order.Base

import Cat.Reasoning

import Order.Reasoning as Poset

module Order.DCPO where

private variable
o ℓ ℓ' : Level
Ix A B : Type o


# Directed-Complete Partial Orders🔗

Let $(P, \le)$ be a partial order. A family of elements $f : I \to P$ is a semi-directed family if for every $i, j$, there merely exists some $k$ such $f i \le f k$ and $f j \le f k$. A semidirected family $f : I \to P$ is a directed family when $I$ is merely inhabited.

module _ {o ℓ} (P : Poset o ℓ) where
open Poset P

is-semidirected-family : ∀ {Ix : Type o} → (Ix → Ob) → Type _
is-semidirected-family {Ix = Ix} f = ∀ i j → ∃[ k ∈ Ix ] (f i ≤ f k × f j ≤ f k)

record is-directed-family {Ix : Type o} (f : Ix → Ob) : Type (o ⊔ ℓ) where
no-eta-equality
field
elt : ∥ Ix ∥
semidirected : is-semidirected-family f


Note that any family whose indexing type is a proposition is automatically semi-directed:

  prop-indexed→semidirected
: ∀ {Ix : Type o} → (s : Ix → Ob) → is-prop Ix
→ is-semidirected-family s
prop-indexed→semidirected s prop i j =
inc (i , ≤-refl , path→≤ (ap s (prop j i)))


The poset $(P, \le)$ is a directed-complete partial order, or DCPO, if it has least upper bounds of all directed families.

  record is-dcpo : Type (lsuc o ⊔ ℓ) where
no-eta-equality
field
directed-lubs
: ∀ {Ix : Type o} (f : Ix → Ob) → is-directed-family f → Lub P f

module ⋃ {Ix : Type o} (f : Ix → Ob) (dir : is-directed-family f) =
Lub (directed-lubs f dir)

open ⋃ using () renaming (lub to ⋃; fam≤lub to fam≤⋃; least to ⋃-least) public


Since least upper bounds are unique when they exist, being a DCPO is a property of a poset, and not structure on that poset.

module _ {o ℓ} {P : Poset o ℓ} where
open Poset P
open is-dcpo

  is-dcpo-is-prop : is-prop (is-dcpo P)
is-dcpo-is-prop = Iso→is-hlevel 1 eqv $Π-is-hlevel′ 1 λ _ → Π-is-hlevel² 1 λ _ _ → Lub-is-prop P where unquoteDecl eqv = declare-record-iso eqv (quote is-dcpo)  # Scott-continuous functions🔗 Let $(P, \le)$ and $(Q, \sqsubseteq)$ be a pair of posets. A monotone map $f : P \to Q$ is called Scott-continuous when it preserves all directed lubs. module _ {P Q : Poset o ℓ} where private module P = Poset P module Q = Poset Q open is-directed-family open Total-hom   is-scott-continuous : (f : Posets.Hom P Q) → Type _ is-scott-continuous f = ∀ {Ix} (s : Ix → P.Ob) (fam : is-directed-family P s) → ∀ x → is-lub P s x → is-lub Q (f .hom ⊙ s) (f .hom x) is-scott-continuous-is-prop : ∀ (f : Posets.Hom P Q) → is-prop (is-scott-continuous f) is-scott-continuous-is-prop _ = Π-is-hlevel′ 1 λ _ → Π-is-hlevel³ 1 λ _ _ _ → Π-is-hlevel 1 λ _ → is-lub-is-prop Q  If $(P, \le)$ is a DCPO, then any function $f : P \to Q$ which preserves directed lubs is automatically a monotone map, and, consequently, Scott-continuous. To see this, suppose we’re given $x, y : P$ with $x \le y$. The family $s : \mathrm{Bool} \to P$ that sends $\mathrm{true}$ to $x$ and $\mathrm{false}$ to $y$ is directed: $\mathrm{Bool}$ is inhabited, and $\mathrm{false}$ is a least upper bound for arbitrary values of the family. Since $f$ preserves lubs, we have $f(x) \le (\sqcup f(s)) = f(\sqcup s) = f(y)$  opaque dcpo+scott→monotone : is-dcpo P → (f : P.Ob → Q.Ob) → (∀ {Ix} (s : Ix → Poset.Ob P) (fam : is-directed-family P s) → ∀ x → is-lub P s x → is-lub Q (f ⊙ s) (f x)) → is-monotone f (P .snd) (Q .snd) dcpo+scott→monotone is-dcpo f scott x y p = is-lub.fam≤lub fs-lub (lift true) where s : Lift _ Bool → P.Ob s (lift b) = if b then x else y sx≤sfalse : ∀ b → s b P.≤ s (lift false) sx≤sfalse (lift true) = p sx≤sfalse (lift false) = P.≤-refl s-directed : is-directed-family P s s-directed .elt = inc (lift true) s-directed .semidirected i j = inc (lift false , sx≤sfalse _ , sx≤sfalse _) s-lub : is-lub P s y s-lub .is-lub.fam≤lub = sx≤sfalse s-lub .is-lub.least z lt = lt (lift false) fs-lub : is-lub Q (f ⊙ s) (f y) fs-lub = scott s s-directed y s-lub  Moreover, if $f : P \to Q$ is an arbitrary monotone map, and $s : I \to P$ is a directed family, then $fs : I \to Q$ is still a directed family.  monotone∘directed : ∀ {Ix : Type o} → {s : Ix → P.Ob} → (f : Posets.Hom P Q) → is-directed-family P s → is-directed-family Q (f .hom ⊙ s) monotone∘directed f dir .elt = dir .elt monotone∘directed f dir .is-directed-family.semidirected i j = ∥-∥-map (Σ-map₂ (×-map (f .preserves _ _) (f .preserves _ _))) (dir .semidirected i j)  module _ where open Total-hom  The identity function is Scott-continuous.  scott-id : ∀ {P : Poset o ℓ} → is-scott-continuous (Posets.id {x = P}) scott-id s fam x lub = lub  Scott-continuous functions are closed under composition.  scott-∘ : ∀ {P Q R : Poset o ℓ} → (f : Posets.Hom Q R) (g : Posets.Hom P Q) → is-scott-continuous f → is-scott-continuous g → is-scott-continuous (f Posets.∘ g) scott-∘ f g f-scott g-scott s dir x lub = f-scott (g .hom ⊙ s) (monotone∘directed g dir) (g .hom x) (g-scott s dir x lub)  # The category of DCPOs🔗 DCPOs form a subcategory of the category of posets. Furthermore, since being a DCPO is a property, identity of DCPOs is determined by identity of their underlying posets: thus, the category of DCPOs is univalent. DCPOs-subcat : ∀ (o ℓ : Level) → Subcat (Posets o ℓ) (lsuc o ⊔ ℓ) (lsuc o ⊔ ℓ) DCPOs-subcat o ℓ .Subcat.is-ob = is-dcpo DCPOs-subcat o ℓ .Subcat.is-hom f _ _ = is-scott-continuous f DCPOs-subcat o ℓ .Subcat.is-hom-prop f _ _ = is-scott-continuous-is-prop f DCPOs-subcat o ℓ .Subcat.is-hom-id _ = scott-id DCPOs-subcat o ℓ .Subcat.is-hom-∘ {f = f} {g = g} = scott-∘ f g DCPOs : ∀ (o ℓ : Level) → Precategory (lsuc (o ⊔ ℓ)) (lsuc o ⊔ ℓ) DCPOs o ℓ = Subcategory (DCPOs-subcat o ℓ) DCPOs-is-category : ∀ {o ℓ} → is-category (DCPOs o ℓ) DCPOs-is-category = subcat-is-category Posets-is-category (λ _ → is-dcpo-is-prop)  module DCPOs {o ℓ : Level} = Cat.Reasoning (DCPOs o ℓ) DCPO : (o ℓ : Level) → Type _ DCPO o ℓ = DCPOs.Ob {o} {ℓ} Forget-DCPO : ∀ {o ℓ} → Functor (DCPOs o ℓ) (Sets o) Forget-DCPO = πᶠ _ F∘ Forget-subcat  # Reasoning with DCPOs🔗 The following pair of modules re-exports facts about the underlying posets (resp. monotone maps) of DCPOs (resp. Scott-continuous functions). They also prove a plethora of small lemmas that are useful in formalisation but not for informal reading. These proofs are all quite straightforward, so we omit them. module DCPO {o ℓ} (D : DCPO o ℓ) where poset : Poset o ℓ poset = D .fst set : Set o set = D .fst .fst open Poset poset public poset-on : Poset-on ℓ Ob poset-on = D .fst .snd has-dcpo : is-dcpo poset has-dcpo = D .snd open is-dcpo has-dcpo public ⋃-pointwise : ∀ {Ix} {s s' : Ix → Ob} → {fam : is-directed-family poset s} {fam' : is-directed-family poset s'} → (∀ ix → s ix ≤ s' ix) → ⋃ s fam ≤ ⋃ s' fam' ⋃-pointwise p = ⋃.least _ _ (⋃ _ _) λ ix → ≤-trans (p ix) (⋃.fam≤lub _ _ ix) module Scott {o ℓ} {D E : DCPO o ℓ} (f : DCPOs.Hom D E) where private module D = DCPO D module E = DCPO E mono : Posets.Hom D.poset E.poset mono = Subcat-hom.hom f hom : D.Ob → E.Ob hom x = Total-hom.hom mono x monotone : ∀ x y → x D.≤ y → hom x E.≤ hom y monotone = Total-hom.preserves mono opaque pres-directed-lub : ∀ {Ix} (s : Ix → D.Ob) → is-directed-family D.poset s → ∀ x → is-lub D.poset s x → is-lub E.poset (hom ⊙ s) (hom x) pres-directed-lub = Subcat-hom.witness f directed : ∀ {Ix} {s : Ix → D.Ob} → is-directed-family D.poset s → is-directed-family E.poset (hom ⊙ s) directed dir = monotone∘directed (Subcat-hom.hom f) dir pres-⋃ : ∀ {Ix} (s : Ix → D.Ob) → (dir : is-directed-family D.poset s) → hom (D.⋃ s dir) ≡ E.⋃ (hom ⊙ s) (directed dir) pres-⋃ s dir = E.≤-antisym (is-lub.least (pres-directed-lub s dir (D.⋃ s dir) (D.⋃.has-lub s dir)) (E.⋃ (hom ⊙ s) (directed dir)) (E.⋃.fam≤lub (hom ⊙ s) (directed dir))) (E.⋃.least (hom ⊙ s) (directed dir) (hom (D.⋃ s dir)) λ i → monotone (s i) (D.⋃ s dir) (D.⋃.fam≤lub s dir i))  module _ {o ℓ} {D E : DCPO o ℓ} where private module D = DCPO D module E = DCPO E open is-directed-family open Total-hom scott-path : ∀ {f g : DCPOs.Hom D E} → (∀ x → Scott.hom f x ≡ Scott.hom g x) → f ≡ g scott-path p = Subcat-hom-path$
total-hom-path _ (funext p) \$
is-prop→pathp (λ i → is-monotone-is-prop (λ x → p x i) D.poset-on E.poset-on) _ _


We also provide a couple methods for constructing Scott-continuous maps. First, we note that if a function is monotonic and commutes with some chosen assignment of least upper bounds, then it is Scott-continuous.

  to-scott
: (f : D.Ob → E.Ob)
→ (∀ x y → x D.≤ y → f x E.≤ f y)
→ (∀ {Ix} (s : Ix → D.Ob) → (dir : is-directed-family D.poset s)
→ is-lub E.poset (f ⊙ s) (f (D.⋃ s dir)))
→ DCPOs.Hom D E
to-scott f monotone pres-⋃ =
sub-hom (total-hom f monotone) pres-lub where
pres-lub
: ∀ {Ix} (s : Ix → D.Ob) → (dir : is-directed-family D.poset s)
→ ∀ x → is-lub D.poset s x → is-lub E.poset (f ⊙ s) (f x)
pres-lub s dir x x-lub .is-lub.fam≤lub i =
monotone _ _ (is-lub.fam≤lub x-lub i)
pres-lub s dir x x-lub .is-lub.least y le =
f x              E.≤⟨ monotone _ _ (is-lub.least x-lub _ (D.⋃.fam≤lub s dir)) ⟩E.≤
f (D.⋃ s dir)    E.=⟨ lub-unique E.poset (pres-⋃ s dir) (E.⋃.has-lub (f ⊙ s) (monotone∘directed (total-hom f monotone) dir)) ⟩E.=
E.⋃ (f ⊙ s) _    E.≤⟨ E.⋃.least _ _ y le ⟩E.≤
y                E.≤∎


Furthermore, if $f$ preserves arbitrary least upper bounds, then it is monotone, and thus Scott-continuous.

  to-scott-directed
: (f : D.Ob → E.Ob)
→ (∀ {Ix} (s : Ix → D.Ob) → (dir : is-directed-family D.poset s)
→ ∀ x → is-lub D.poset s x → is-lub E.poset (f ⊙ s) (f x))
→ DCPOs.Hom D E
to-scott-directed f pres =
sub-hom (total-hom f (dcpo+scott→monotone D.has-dcpo f pres)) pres