Tom de Jong & Martin Escardo, 20 May 2019.
Refactored January 2020, December 2021 by Tom de Jong.

Definitions of:
 * Directed complete posets (dcpos).
 * Scott continuous maps.

See DomainTheory.lagda for an overview of the formalization of the theory of
dcpos.

\begin{code}

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

open import MLTT.Spartan

open import UF.FunExt
open import UF.PropTrunc
open import UF.Sets
open import UF.SubtypeClassifier

module DomainTheory.Basics.Dcpo
        (pt : propositional-truncations-exist)
        (fe : Fun-Ext)
        (π“₯ : Universe) -- where the index types for directed completeness live
       where

open PropositionalTruncation pt

open import UF.Subsingletons
open import UF.Subsingletons-FunExt

open import Naturals.Addition renaming (_+_ to _+'_)
open import Naturals.Order
open import Notation.Order

open import OrderedTypes.Poset fe

module _ {𝓀 𝓣 : Universe}
         {D : 𝓀 Μ‡ }
         (_βŠ‘_ : D β†’ D β†’ 𝓣 Μ‡ )
       where

 open PosetAxioms

 is-upperbound : {I : 𝓦 Μ‡ } (u : D) (Ξ± : I β†’ D) β†’ 𝓦 βŠ” 𝓣 Μ‡
 is-upperbound u Ξ± = (i : domain Ξ±) β†’ Ξ± i βŠ‘ u

 is-lowerbound-of-upperbounds : {I : 𝓦 Μ‡ } (u : D) (Ξ± : I β†’ D) β†’ 𝓦 βŠ” 𝓀 βŠ” 𝓣 Μ‡
 is-lowerbound-of-upperbounds u Ξ± = (v : D) β†’ is-upperbound v Ξ± β†’ u βŠ‘ v

 is-sup : {I : 𝓦 Μ‡ } β†’ D β†’ (I β†’ D) β†’ 𝓀 βŠ” 𝓦 βŠ” 𝓣 Μ‡
 is-sup s Ξ± = (is-upperbound s Ξ±) Γ— (is-lowerbound-of-upperbounds s Ξ±)

 sup-is-upperbound : {I : 𝓦 Μ‡ } {s : D} {Ξ± : I β†’ D}
                   β†’ is-sup s Ξ±
                   β†’ is-upperbound s Ξ±
 sup-is-upperbound i = pr₁ i

 sup-is-lowerbound-of-upperbounds : {I : 𝓦 Μ‡ } {s : D} {Ξ± : I β†’ D}
                                  β†’ is-sup s Ξ±
                                  β†’ (u : D)
                                  β†’ is-upperbound u Ξ± β†’ s βŠ‘ u
 sup-is-lowerbound-of-upperbounds i = prβ‚‚ i

 has-sup : {I : 𝓦 Μ‡ } β†’ (I β†’ D) β†’ 𝓀 βŠ” 𝓦 βŠ” 𝓣 Μ‡
 has-sup Ξ± = Ξ£ s κž‰ D , is-sup s Ξ±

 the-sup : {I : 𝓦 Μ‡ } {Ξ± : I β†’ D} β†’ has-sup Ξ± β†’ D
 the-sup (s , i) = s

 sup-property : {I : 𝓦 Μ‡ } {Ξ± : I β†’ D} (h : has-sup Ξ±) β†’ is-sup (the-sup h) Ξ±
 sup-property (s , i) = i

 is-inhabited : (X : 𝓦 Μ‡ ) β†’ 𝓦 Μ‡
 is-inhabited = βˆ₯_βˆ₯

 is-semidirected : {I : 𝓦 Μ‡ } β†’ (I β†’ D) β†’ 𝓦 βŠ” 𝓣 Μ‡
 is-semidirected {𝓦} {I} Ξ± = (i j : I) β†’ βˆƒ k κž‰ I , (Ξ± i βŠ‘ Ξ± k) Γ— (Ξ± j βŠ‘ Ξ± k)

 is-directed : {I : 𝓦 Μ‡ } β†’ (I β†’ D) β†’ 𝓦 βŠ” 𝓣 Μ‡
 is-directed {𝓦} {I} Ξ± = is-inhabited I Γ— is-semidirected Ξ±

 inhabited-if-directed : {I : 𝓦 Μ‡ } (Ξ± : I β†’ D) β†’ is-directed Ξ± β†’ βˆ₯ I βˆ₯
 inhabited-if-directed Ξ± = pr₁

 semidirected-if-directed : {I : 𝓦 Μ‡ } (Ξ± : I β†’ D) β†’ is-directed Ξ±
                               β†’ (i j : I) β†’ βˆƒ k κž‰ I , (Ξ± i βŠ‘ Ξ± k) Γ— (Ξ± j βŠ‘ Ξ± k)
 semidirected-if-directed Ξ± = prβ‚‚

 being-inhabited-is-prop : {I : 𝓦 Μ‡ } β†’ is-prop (is-inhabited I)
 being-inhabited-is-prop = βˆ₯βˆ₯-is-prop

 being-semidirected-is-prop : {I : 𝓦 Μ‡ } (Ξ± : I β†’ D) β†’ is-prop (is-semidirected Ξ±)
 being-semidirected-is-prop Ξ± = Ξ β‚‚-is-prop fe (Ξ» i j β†’ βˆ₯βˆ₯-is-prop)

 being-directed-is-prop : {I : 𝓦 Μ‡ } (Ξ± : I β†’ D) β†’ is-prop (is-directed Ξ±)
 being-directed-is-prop Ξ± =
  Γ—-is-prop being-inhabited-is-prop (being-semidirected-is-prop Ξ±)

 is-directed-complete : 𝓀 βŠ” (π“₯ ⁺) βŠ” 𝓣 Μ‡
 is-directed-complete = (I : π“₯ Μ‡ ) (Ξ± : I β†’ D) β†’ is-directed Ξ± β†’ has-sup Ξ±

 is-sup-is-prop : poset-axioms _βŠ‘_
                β†’ {I : 𝓦 Μ‡ } (d : D) (Ξ± : I β†’ D)
                β†’ is-prop (is-sup d Ξ±)
 is-sup-is-prop (s , p , r , t , a) {I} d Ξ± = Ξ³
  where
   Ξ³ : is-prop (is-sup d Ξ±)
   Ξ³ = Γ—-is-prop (Ξ -is-prop fe (Ξ» i β†’ p (Ξ± i) d))
                 (Ξ β‚‚-is-prop fe (Ξ» x l β†’ p d x))

 sups-are-unique : poset-axioms _βŠ‘_
                 β†’ {I : 𝓦 Μ‡ } (Ξ± : I β†’ D) {x y : D}
                 β†’ is-sup x Ξ± β†’ is-sup y Ξ± β†’ x ＝ y
 sups-are-unique (s , p , r , t , a) {I} Ξ± {x} {y} x-is-sup y-is-sup =
  a x y
   (sup-is-lowerbound-of-upperbounds x-is-sup y (sup-is-upperbound y-is-sup))
   (sup-is-lowerbound-of-upperbounds y-is-sup x (sup-is-upperbound x-is-sup))

 having-sup-is-prop : poset-axioms _βŠ‘_
                    β†’ {I : 𝓦 Μ‡ } (Ξ± : I β†’ D)
                    β†’ is-prop (has-sup Ξ±)
 having-sup-is-prop ax {I} Ξ± Οƒ Ο„ =
  to-subtype-＝ (Ξ» x β†’ is-sup-is-prop ax x Ξ±)
               (sups-are-unique ax Ξ± (prβ‚‚ Οƒ) (prβ‚‚ Ο„))

 dcpo-axioms : 𝓀 βŠ” (π“₯ ⁺) βŠ” 𝓣 Μ‡
 dcpo-axioms = poset-axioms _βŠ‘_ Γ— is-directed-complete

 being-directed-complete-is-prop : dcpo-axioms β†’ is-prop is-directed-complete
 being-directed-complete-is-prop a =
  Π₃-is-prop fe (Ξ» I Ξ± Ξ΄ β†’ having-sup-is-prop (pr₁ a) Ξ±)

 dcpo-axioms-is-prop : is-prop dcpo-axioms
 dcpo-axioms-is-prop = prop-criterion Ξ³
  where
   Ξ³ : dcpo-axioms β†’ is-prop dcpo-axioms
   Ξ³ a = Γ—-is-prop (poset-axioms-is-prop _βŠ‘_)
                   (being-directed-complete-is-prop a)

\end{code}

Since we will also consider dcpos with a least element later, we make the
following definitions.

\begin{code}

 is-least : D β†’ 𝓀 βŠ” 𝓣 Μ‡
 is-least x = βˆ€ (y : D) β†’ x βŠ‘ y

 has-least : 𝓀 βŠ” 𝓣 Μ‡
 has-least = Ξ£ x κž‰ D , is-least x

\end{code}

Added 23 June 2024.

\begin{code}

 is-Ο‰-chain : (β„• β†’ D) β†’ 𝓣 Μ‡
 is-Ο‰-chain Ξ± = (n : β„•) β†’ Ξ± n βŠ‘ Ξ± (succ n)

 is-Ο‰-complete : 𝓀 βŠ” 𝓣 Μ‡
 is-Ο‰-complete = (Ξ± : β„• β†’ D) β†’ is-Ο‰-chain Ξ± β†’ has-sup Ξ±

 module _
         (βŠ‘-refl : is-reflexive _βŠ‘_)
         (βŠ‘-trans : is-transitive _βŠ‘_)
         (Ξ± : β„• β†’ D)
        where

  Ο‰-chains-increase : is-Ο‰-chain Ξ±
                    β†’ (n m : β„•) β†’ n ≀ m β†’ Ξ± n βŠ‘ Ξ± m
  Ο‰-chains-increase c n 0        l =
   transport⁻¹ (Ξ» - β†’ Ξ± - βŠ‘ Ξ± 0) (unique-least n l) (βŠ‘-refl (Ξ± 0))
  Ο‰-chains-increase c n (succ m) l = I (≀-split n m l)
   where
    I : n ≀ m + (n ＝ succ m) β†’ Ξ± n βŠ‘ Ξ± (succ m)
    I (inl k) = βŠ‘-trans (Ξ± n) (Ξ± m) (Ξ± (succ m)) (Ο‰-chains-increase c n m k) (c m)
    I (inr refl) = βŠ‘-refl (Ξ± (succ m))

  Ο‰-chains-are-directed : is-Ο‰-chain Ξ± β†’ is-directed Ξ±
  Ο‰-chains-are-directed c = ∣ 0 ∣ , I
   where
    I : is-semidirected Ξ±
    I n m = ∣ n +' m , II , III ∣
     where
      II : Ξ± n βŠ‘ Ξ± (n +' m)
      II = Ο‰-chains-increase c n (n +' m)
            (cosubtraction n (n +' m) (m , (addition-commutativity m n)))
      III : Ξ± m βŠ‘ Ξ± (n +' m)
      III = Ο‰-chains-increase c m (n +' m)
             (cosubtraction m (n +' m) (n , refl))

\end{code}

End of addition.


We have now developed enough material to define dcpos and we introduce some
convenient projections.

\begin{code}

module _ {𝓀 𝓣 : Universe} where

 open PosetAxioms

 DCPO-structure : 𝓀 Μ‡ β†’ 𝓀 βŠ” (π“₯ ⁺) βŠ” (𝓣 ⁺) Μ‡
 DCPO-structure D = Ξ£ _βŠ‘_ κž‰ (D β†’ D β†’ 𝓣 Μ‡ ), (dcpo-axioms {𝓀} {𝓣} _βŠ‘_)

 DCPO : (𝓀 ⁺) βŠ” (π“₯ ⁺) βŠ” (𝓣 ⁺) Μ‡
 DCPO = Ξ£ D κž‰ 𝓀 Μ‡ , DCPO-structure D

 ⟨_⟩ : DCPO β†’ 𝓀 Μ‡
 ⟨ D , _βŠ‘_ , d ⟩ = D

 underlying-order : (𝓓 : DCPO) β†’ ⟨ 𝓓 ⟩ β†’ ⟨ 𝓓 ⟩ β†’ 𝓣 Μ‡
 underlying-order (D , _βŠ‘_ , d) = _βŠ‘_

 syntax underlying-order 𝓓 x y = x βŠ‘βŸ¨ 𝓓 ⟩ y

 axioms-of-dcpo : (𝓓 : DCPO) β†’ dcpo-axioms (underlying-order 𝓓)
 axioms-of-dcpo (D , _βŠ‘_ , d) = d

 poset-axioms-of-dcpo : (𝓓 : DCPO) β†’ poset-axioms (underlying-order 𝓓)
 poset-axioms-of-dcpo (D , _βŠ‘_ , d) = pr₁ d

 sethood : (𝓓 : DCPO) β†’ is-set ⟨ 𝓓 ⟩
 sethood (D , _βŠ‘_ , (s  , p  , r  , t  , a)  , c ) = s

 prop-valuedness : (𝓓 : DCPO) β†’ is-prop-valued (underlying-order 𝓓 )
 prop-valuedness (D , _βŠ‘_ , (s  , p  , r  , t  , a)  , c ) = p

 reflexivity : (𝓓 : DCPO) β†’ is-reflexive (underlying-order 𝓓)
 reflexivity (D , _βŠ‘_ , (s  , p  , r  , t  , a)  , c ) = r

 transitivity : (𝓓 : DCPO) β†’ is-transitive (underlying-order 𝓓)
 transitivity (D , _βŠ‘_ , (s  , p  , r  , t  , a)  , c ) = t

 antisymmetry : (𝓓 : DCPO) β†’ is-antisymmetric (underlying-order 𝓓)
 antisymmetry (D , _βŠ‘_ , (s  , p  , r  , t  , a)  , c ) = a

\end{code}

Added by Ayberk Tosun on 2024-04-19.

To work with the combinators in `UF.Logic`, it is convenient to have a version
of equality on domain elements that is packaged up with the proof that it is
a proposition.

\begin{code}

 dcpo-equalityβ‚š : (𝓓 : DCPO) β†’ ⟨ 𝓓 ⟩ β†’ ⟨ 𝓓 ⟩ β†’ Ξ© 𝓀
 dcpo-equalityβ‚š 𝓓 x y = (x ＝ y) , sethood 𝓓

 syntax dcpo-equalityβ‚š 𝓓 x y = x οΌβ‚š[ 𝓓 ] y
 infix 2 dcpo-equalityβ‚š

\end{code}

We introduce pretty syntax for chain reasoning with inequalities.
(Cf. ＝⟨_⟩ and ∎ in Id.lagda, β‰ƒβŸ¨_⟩ and β–  in UF.Equiv.lagda)

For example, given (a b c d : ⟨ 𝓓 ⟩) and
u : a βŠ‘βŸ¨ 𝓓 ⟩ b
v : b βŠ‘βŸ¨ 𝓓 ⟩ c
w : c βŠ‘βŸ¨ 𝓓 ⟩ d

this will allow us to write

z : a βŠ‘βŸ¨ 𝓓 ⟩ d
z = a βŠ‘βŸ¨ 𝓓 ⟩[ u ]
    b βŠ‘βŸ¨ 𝓓 ⟩[ v ]
    c βŠ‘βŸ¨ 𝓓 ⟩[ w ]
    d ∎⟨ 𝓓 ⟩

rather than the hard(er) to read

z : a βŠ‘βŸ¨ 𝓓 ⟩ d
z = transitivity 𝓓 a c d z' w
 where
  z' : a βŠ‘βŸ¨ 𝓓 ⟩ c
  z' = transitivity 𝓓 a b c u v

\begin{code}

 transitivity' : (𝓓 : DCPO) (x : ⟨ 𝓓 ⟩) {y z : ⟨ 𝓓 ⟩}
               β†’ x βŠ‘βŸ¨ 𝓓 ⟩ y β†’ y βŠ‘βŸ¨ 𝓓 ⟩ z β†’ x βŠ‘βŸ¨ 𝓓 ⟩ z
 transitivity' 𝓓 x {y} {z} u v = transitivity 𝓓 x y z u v

 syntax transitivity' 𝓓 x u v = x βŠ‘βŸ¨ 𝓓 ⟩[ u ] v
 infixr 0 transitivity'

 syntax reflexivity 𝓓 x = x ∎⟨ 𝓓 ⟩
 infix 1 reflexivity

 has-bottom : DCPO β†’ 𝓀 βŠ” 𝓣 Μ‡
 has-bottom 𝓓 = has-least (underlying-order 𝓓)

\end{code}

Next, we introduce ∐-notation for the supremum of a directed family in a dcpo.

\begin{code}

 directed-completeness : (𝓓 : DCPO) β†’ is-directed-complete (underlying-order 𝓓)
 directed-completeness (D , _βŠ‘_ , a) = prβ‚‚ a

 is-Semidirected : (𝓓 : DCPO) {I : 𝓦 Μ‡ } (Ξ± : I β†’ ⟨ 𝓓 ⟩) β†’ 𝓦 βŠ” 𝓣 Μ‡
 is-Semidirected 𝓓 Ξ± = is-semidirected (underlying-order 𝓓) Ξ±

 is-Directed : (𝓓 : DCPO) {I : 𝓦 Μ‡ } (Ξ± : I β†’ ⟨ 𝓓 ⟩) β†’ 𝓦 βŠ” 𝓣 Μ‡
 is-Directed 𝓓 Ξ± = is-directed (underlying-order 𝓓) Ξ±

 inhabited-if-Directed : (𝓓 : DCPO) {I : 𝓦 Μ‡ } (Ξ± : I β†’ ⟨ 𝓓 ⟩)
                       β†’ is-Directed 𝓓 Ξ±
                       β†’ βˆ₯ I βˆ₯
 inhabited-if-Directed 𝓓 Ξ± = pr₁

 semidirected-if-Directed : (𝓓 : DCPO) {I : 𝓦 Μ‡ } (Ξ± : I β†’ ⟨ 𝓓 ⟩)
                          β†’ is-Directed 𝓓 Ξ±
                          β†’ is-Semidirected 𝓓 Ξ±
 semidirected-if-Directed 𝓓 Ξ± = prβ‚‚

 Ο‰-chains-are-Directed : (𝓓 : DCPO) (Ξ± : β„• β†’ ⟨ 𝓓 ⟩)
                       β†’ is-Ο‰-chain (underlying-order 𝓓) Ξ±
                       β†’ is-Directed 𝓓 Ξ±
 Ο‰-chains-are-Directed 𝓓 Ξ± =
  Ο‰-chains-are-directed (underlying-order 𝓓) (reflexivity 𝓓) (transitivity 𝓓) Ξ±

 ∐ : (𝓓 : DCPO) {I : π“₯ Μ‡ } {Ξ± : I β†’ ⟨ 𝓓 ⟩} β†’ is-Directed 𝓓 Ξ± β†’ ⟨ 𝓓 ⟩
 ∐ 𝓓 {I} {Ξ±} Ξ΄ = pr₁ (directed-completeness 𝓓 I Ξ± Ξ΄)

 ∐-is-sup : (𝓓 : DCPO) {I : π“₯ Μ‡ } {Ξ± : I β†’ ⟨ 𝓓 ⟩} (Ξ΄ : is-Directed 𝓓 Ξ±)
          β†’ is-sup (underlying-order 𝓓) (∐ 𝓓 Ξ΄) Ξ±
 ∐-is-sup 𝓓 {I} {Ξ±} Ξ΄ = prβ‚‚ (directed-completeness 𝓓 I Ξ± Ξ΄)

 ∐-is-upperbound : (𝓓 : DCPO) {I : π“₯ Μ‡ } {Ξ± : I β†’ ⟨ 𝓓 ⟩} (Ξ΄ : is-Directed 𝓓 Ξ±)
                 β†’ is-upperbound (underlying-order 𝓓) (∐ 𝓓 Ξ΄) Ξ±
 ∐-is-upperbound 𝓓 Ξ΄ = pr₁ (∐-is-sup 𝓓 Ξ΄)

 ∐-is-lowerbound-of-upperbounds : (𝓓 : DCPO) {I : π“₯ Μ‡ } {Ξ± : I β†’ ⟨ 𝓓 ⟩}
                                  (Ξ΄ : is-Directed 𝓓 Ξ±)
                                β†’ is-lowerbound-of-upperbounds
                                    (underlying-order 𝓓) (∐ 𝓓 Ξ΄) Ξ±
 ∐-is-lowerbound-of-upperbounds 𝓓 Ξ΄ = prβ‚‚ (∐-is-sup 𝓓 Ξ΄)

\end{code}

Finally, we define (strict) continuous maps between (pointed) dcpos.

\begin{code}

is-continuous : (𝓓 : DCPO {𝓀} {𝓣}) (𝓔 : DCPO {𝓀'} {𝓣'})
              β†’ (⟨ 𝓓 ⟩ β†’ ⟨ 𝓔 ⟩)
              β†’ π“₯ ⁺ βŠ” 𝓀 βŠ” 𝓣 βŠ” 𝓀' βŠ” 𝓣' Μ‡
is-continuous 𝓓 𝓔 f = (I : π“₯ Μ‡ ) (Ξ± : I β†’ ⟨ 𝓓 ⟩) (Ξ΄ : is-Directed 𝓓 Ξ±)
                     β†’ is-sup (underlying-order 𝓔) (f (∐ 𝓓 Ξ΄)) (f ∘ Ξ±)

being-continuous-is-prop : (𝓓 : DCPO {𝓀} {𝓣}) (𝓔 : DCPO {𝓀'} {𝓣'})
                             (f : ⟨ 𝓓 ⟩ β†’ ⟨ 𝓔 ⟩)
                           β†’ is-prop (is-continuous 𝓓 𝓔 f)
being-continuous-is-prop 𝓓 𝓔 f =
 Π₃-is-prop fe (Ξ» I Ξ± Ξ΄ β†’ is-sup-is-prop (underlying-order 𝓔)
                          (pr₁ (axioms-of-dcpo 𝓔))
                          (f (∐ 𝓓 Ξ΄)) (f ∘ Ξ±))

DCPO[_,_] : DCPO {𝓀} {𝓣} β†’ DCPO {𝓀'} {𝓣'} β†’ π“₯ ⁺ βŠ” 𝓀 βŠ” 𝓣 βŠ” 𝓀' βŠ” 𝓣' Μ‡
DCPO[ 𝓓 , 𝓔 ] = Ξ£ f κž‰ (⟨ 𝓓 ⟩ β†’ ⟨ 𝓔 ⟩) , is-continuous 𝓓 𝓔 f

underlying-function : (𝓓 : DCPO {𝓀} {𝓣}) (𝓔 : DCPO {𝓀'} {𝓣'})
                    β†’ DCPO[ 𝓓 , 𝓔 ] β†’ ⟨ 𝓓 ⟩ β†’ ⟨ 𝓔 ⟩
underlying-function 𝓓 𝓔 (f , _) = f

syntax underlying-function 𝓓 𝓔 f = [ 𝓓 , 𝓔 ]⟨ f ⟩

continuity-of-function : (𝓓 : DCPO {𝓀} {𝓣}) (𝓔 : DCPO {𝓀'} {𝓣'}) (f : DCPO[ 𝓓 , 𝓔 ])
                       β†’ is-continuous 𝓓 𝓔 [ 𝓓 ,  𝓔 ]⟨ f ⟩
continuity-of-function 𝓓 𝓔 (_ , c) = c

\end{code}