open import Cat.Displayed.Univalence.Thin
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.Univalent
open import Order.Base

import Cat.Reasoning

import Order.Reasoning

module Order.DCPO where

private variable
  o β„“ β„“' : Level
  Ix A B : Type o

Directed-complete partial ordersπŸ”—

Let be a partial order. A family of elements is a semi-directed family if for every there merely exists some such and A semidirected family is a directed family when is merely inhabited.

module _ {o β„“} (P : Poset o β„“) where
  open Order.Reasoning 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 , ≀-refl' (ap s (prop j i)))

The poset 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.

unquoteDecl H-Level-is-dcpo = declare-record-hlevel 1 H-Level-is-dcpo (quote is-dcpo)

Scott-continuous functionsπŸ”—

Let and be a pair of posets. A monotone map 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 _ = hlevel 1

If is a DCPO, then any function which preserves directed lubs is automatically a monotone map, and, consequently, Scott-continuous.

To see this, suppose we’re given with The family that sends to and to is directed: is inhabited, and is a least upper bound for arbitrary values of the family. Since preserves lubs, we have

  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))
      β†’ βˆ€ {x y} β†’ x P.≀ y β†’ f x Q.≀ f y
    dcpo+scott→monotone is-dcpo f scott {x} {y} p =
      fs-lub .is-lub.fam≀lub (lift true) where
        s : Lift o 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 is an arbitrary monotone map, and is a directed family, then 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 .pres-≀) (f .pres-≀)))
      (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 (Ξ» _ β†’ hlevel 1)

module DCPOs {o β„“ : Level} = Cat.Reasoning (DCPOs o β„“)

DCPO : (o β„“ : Level) β†’ Type _
DCPO o β„“ = DCPOs.Ob {o} {β„“}

DCPOsβ†ͺPosets : βˆ€ {o β„“} β†’ Functor (DCPOs o β„“) (Posets o β„“)
DCPOsβ†ͺPosets = Forget-subcat

DCPOsβ†ͺSets : βˆ€ {o β„“} β†’ Functor (DCPOs o β„“) (Sets o)
DCPOsβ†ͺSets = Posetsβ†ͺSets F∘ DCPOsβ†ͺPosets

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

  open Order.Reasoning (D .fst) public

  set : Set o
  set = el ⌞ D ⌟ Ob-is-set

  has-dcpo : is-dcpo poset
  has-dcpo = D .snd

  open is-dcpo (D .snd) 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

  monotone : βˆ€ {x y} β†’ x D.≀ y β†’ f # x E.≀ f # y
  monotone = mono .pres-≀

  opaque
    pres-directed-lub
      : βˆ€ {Ix} (s : Ix β†’ D.Ob) β†’ is-directed-family D.poset s
      β†’ βˆ€ x β†’ is-lub (D .fst) s x β†’ is-lub (E .fst) (apply f βŠ™ s) (f # 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 (apply f βŠ™ s)
    directed dir = monotone∘directed (Subcat-hom.hom f) dir

    pres-⋃
      : βˆ€ {Ix} (s : Ix β†’ D.Ob) β†’ (dir : is-directed-family D.poset s)
      β†’ f # (D.⋃ s dir) ≑ E.⋃ (apply f βŠ™ 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.⋃ (apply f βŠ™ s) (directed dir))
          (E.⋃.fam≀lub (apply f βŠ™ s) (directed dir)))
        (E.⋃.least (apply f βŠ™ s) (directed dir) (apply f (D.⋃ s dir)) Ξ» i β†’
          monotone (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

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 fᡐ pres-lub where
      fᡐ : Monotone D.poset E.poset
      fᡐ .hom = f
      fᡐ .pres-≀ = monotone

      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 (pres-⋃ s dir) (E.⋃.has-lub (f βŠ™ s) (monotone∘directed fᡐ dir)) ⟩E.=
        E.⋃ (f βŠ™ s) _    E.β‰€βŸ¨ E.⋃.least _ _ y le ⟩E.≀
        y                E.β‰€βˆŽ

Furthermore, if 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 .Subcat-hom.hom .hom = f
  to-scott-directed f pres .Subcat-hom.hom .pres-≀ =
    dcpo+scott→monotone D.has-dcpo f pres
  to-scott-directed f pres .Subcat-hom.witness = pres