Tom de Jong, late February - early March 2020.
Jan - Mar 2022: Some additions, most notably on embeddings.

We define the way-below relation and the notion of a compact element in a
directed complete poset.

Contents
* Basic properties of the way-below relation and its interaction with the order.
* Definition of a compact element as an element that is way below itself.
* The compact elements are closed under existing finite joins.
* In an embedding-projection pair, the embedding preserves and reflects the
  way-below relation, and hence, compact elements.

\begin{code}

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

open import MLTT.Spartan
open import UF.FunExt
open import UF.PropTrunc

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

open PropositionalTruncation pt

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

open import DomainTheory.Basics.Dcpo pt fe π“₯
open import DomainTheory.Basics.Miscelanea pt fe π“₯

way-below : (𝓓 : DCPO {𝓀} {𝓣}) β†’ ⟨ 𝓓 ⟩ β†’ ⟨ 𝓓 ⟩ β†’ π“₯ ⁺ βŠ” 𝓀 βŠ” 𝓣 Μ‡
way-below 𝓓 x y = (I : π“₯ Μ‡ ) (Ξ± : I β†’ ⟨ 𝓓 ⟩) (Ξ΄ : is-Directed 𝓓 Ξ±)
                β†’ y βŠ‘βŸ¨ 𝓓 ⟩ ∐ 𝓓 Ξ΄
                β†’ βˆƒ i κž‰ I , x βŠ‘βŸ¨ 𝓓 ⟩ Ξ± i

is-way-upperbound : (𝓓 : DCPO {𝓀} {𝓣}) {I : π“₯ Μ‡ } (x : ⟨ 𝓓 ⟩) (Ξ± : I β†’ ⟨ 𝓓 ⟩)
                  β†’ π“₯ ⁺ βŠ” 𝓀 βŠ” 𝓣 Μ‡
is-way-upperbound 𝓓 {I} x Ξ± = (i : I) β†’ Ξ± i β‰ͺ⟨ 𝓓 ⟩ x

syntax way-below 𝓓 x y = x β‰ͺ⟨ 𝓓 ⟩ y

β‰ͺ-to-βŠ‘ : (𝓓 : DCPO {𝓀} {𝓣}) {x y : ⟨ 𝓓 ⟩} β†’ x β‰ͺ⟨ 𝓓 ⟩ y β†’ x βŠ‘βŸ¨ 𝓓 ⟩ y
β‰ͺ-to-βŠ‘ 𝓓 {x} {y} u = βˆ₯βˆ₯-rec (prop-valuedness 𝓓 x y) Ξ³ g
 where
  Ξ± : πŸ™{π“₯} β†’ ⟨ 𝓓 ⟩
  Ξ± ⋆ = y
  Ξ³ : (Ξ£ i κž‰ πŸ™ , x βŠ‘βŸ¨ 𝓓 ⟩ Ξ± i) β†’ x βŠ‘βŸ¨ 𝓓 ⟩ y
  Ξ³ (⋆ , l) = l
  g : βˆƒ i κž‰ πŸ™ , x βŠ‘βŸ¨ 𝓓 ⟩ Ξ± i
  g = u πŸ™ Ξ± Ξ΄ (∐-is-upperbound 𝓓 Ξ΄ ⋆)
   where
    Ξ΄ : is-Directed 𝓓 Ξ±
    Ξ΄ = (∣ ⋆ ∣ , Ξ΅)
     where
      Ξ΅ : (i j : πŸ™)
        β†’ βˆƒ k κž‰ πŸ™ , Ξ± i βŠ‘βŸ¨ 𝓓 ⟩ Ξ± k Γ— Ξ± j βŠ‘βŸ¨ 𝓓 ⟩ Ξ± k
      Ξ΅ ⋆ ⋆ = ∣ ⋆ , reflexivity 𝓓 y , reflexivity 𝓓 y ∣

βŠ‘-β‰ͺ-βŠ‘-to-β‰ͺ : (𝓓 : DCPO {𝓀} {𝓣}) {a b c d : ⟨ 𝓓 ⟩}
           β†’ a βŠ‘βŸ¨ 𝓓 ⟩ b
           β†’ b β‰ͺ⟨ 𝓓 ⟩ c
           β†’ c βŠ‘βŸ¨ 𝓓 ⟩ d
           β†’ a β‰ͺ⟨ 𝓓 ⟩ d
βŠ‘-β‰ͺ-βŠ‘-to-β‰ͺ 𝓓 {a} {b} {c} {d} l₁ u lβ‚‚ I Ξ± Ξ΄ m = Ξ³
 where
  Ξ³ : βˆƒ i κž‰ I , a βŠ‘βŸ¨ 𝓓 ⟩ Ξ± i
  Ξ³ = βˆ₯βˆ₯-functor g h
   where
    g : (Ξ£ i κž‰ I , b βŠ‘βŸ¨ 𝓓 ⟩ Ξ± i)
      β†’ (Ξ£ i κž‰ I , a βŠ‘βŸ¨ 𝓓 ⟩ Ξ± i)
    g (i , u) = (i , v)
     where
      v = a   βŠ‘βŸ¨ 𝓓 ⟩[ l₁ ]
          b   βŠ‘βŸ¨ 𝓓 ⟩[ u  ]
          Ξ± i ∎⟨ 𝓓 ⟩
    h : βˆƒ i κž‰ I , b βŠ‘βŸ¨ 𝓓 ⟩ Ξ± i
    h = u I Ξ± Ξ΄ l
     where
      l = c     βŠ‘βŸ¨ 𝓓 ⟩[ lβ‚‚ ]
          d     βŠ‘βŸ¨ 𝓓 ⟩[ m  ]
          ∐ 𝓓 Ξ΄ ∎⟨ 𝓓 ⟩

βŠ‘-β‰ͺ-to-β‰ͺ : (𝓓 : DCPO {𝓀} {𝓣}) {x y z : ⟨ 𝓓 ⟩}
         β†’ x βŠ‘βŸ¨ 𝓓 ⟩ y
         β†’ y β‰ͺ⟨ 𝓓 ⟩ z
         β†’ x β‰ͺ⟨ 𝓓 ⟩ z
βŠ‘-β‰ͺ-to-β‰ͺ 𝓓 {x} {y} {z} l u = βŠ‘-β‰ͺ-βŠ‘-to-β‰ͺ 𝓓 l u (reflexivity 𝓓 z)

β‰ͺ-βŠ‘-to-β‰ͺ : (𝓓 : DCPO {𝓀} {𝓣}) {x y z : ⟨ 𝓓 ⟩}
         β†’ x β‰ͺ⟨ 𝓓 ⟩ y
         β†’ y βŠ‘βŸ¨ 𝓓 ⟩ z
         β†’ x β‰ͺ⟨ 𝓓 ⟩ z
β‰ͺ-βŠ‘-to-β‰ͺ 𝓓 {x} {y} {z} = βŠ‘-β‰ͺ-βŠ‘-to-β‰ͺ 𝓓 (reflexivity 𝓓 x)

β‰ͺ-is-prop-valued : (𝓓 : DCPO {𝓀} {𝓣}) {x y : ⟨ 𝓓 ⟩} β†’ is-prop (x β‰ͺ⟨ 𝓓 ⟩ y)
β‰ͺ-is-prop-valued 𝓓 = Ξ β‚„-is-prop fe (Ξ» I Ξ± Ξ΄ u β†’ βˆ₯βˆ₯-is-prop)

β‰ͺ-is-antisymmetric : (𝓓 : DCPO {𝓀} {𝓣}) {x y : ⟨ 𝓓 ⟩}
                   β†’ x β‰ͺ⟨ 𝓓 ⟩ y β†’ y β‰ͺ⟨ 𝓓 ⟩ x β†’ x = y
β‰ͺ-is-antisymmetric 𝓓 {x} {y} u v =
 antisymmetry 𝓓 x y (β‰ͺ-to-βŠ‘ 𝓓 u) (β‰ͺ-to-βŠ‘ 𝓓 v)

β‰ͺ-is-transitive : (𝓓 : DCPO {𝓀} {𝓣}) {x y z : ⟨ 𝓓 ⟩}
                β†’ x β‰ͺ⟨ 𝓓 ⟩ y β†’ y β‰ͺ⟨ 𝓓 ⟩ z β†’ x β‰ͺ⟨ 𝓓 ⟩ z
β‰ͺ-is-transitive 𝓓 {x} {y} {z} u v I Ξ± Ξ΄ l = u I Ξ± Ξ΄ k
 where
  k = y     βŠ‘βŸ¨ 𝓓 ⟩[ β‰ͺ-to-βŠ‘ 𝓓 v ]
      z     βŠ‘βŸ¨ 𝓓 ⟩[ l ]
      ∐ 𝓓 Ξ΄ ∎⟨ 𝓓 ⟩

\end{code}

An element is called compact if it way below itself.

\begin{code}

is-compact : (𝓓 : DCPO {𝓀} {𝓣}) β†’ ⟨ 𝓓 ⟩ β†’ π“₯ ⁺ βŠ” 𝓀 βŠ” 𝓣 Μ‡
is-compact 𝓓 x = x β‰ͺ⟨ 𝓓 ⟩ x

being-compact-is-prop : (𝓓 : DCPO {𝓀} {𝓣}) (x : ⟨ 𝓓 ⟩)
                      β†’ is-prop (is-compact 𝓓 x)
being-compact-is-prop 𝓓 x = β‰ͺ-is-prop-valued 𝓓

compact-βŠ‘-≃-β‰ͺ : (𝓓 : DCPO {𝓀} {𝓣}) {x : ⟨ 𝓓 ⟩}
              β†’ is-compact 𝓓 x
              β†’ {y : ⟨ 𝓓 ⟩}
              β†’ (x βŠ‘βŸ¨ 𝓓 ⟩ y) ≃ (x β‰ͺ⟨ 𝓓 ⟩ y)
compact-βŠ‘-≃-β‰ͺ 𝓓 {x} c {y} =
 logically-equivalent-props-are-equivalent
  (prop-valuedness 𝓓 x y) (β‰ͺ-is-prop-valued 𝓓)
  (β‰ͺ-βŠ‘-to-β‰ͺ 𝓓 c)
  (β‰ͺ-to-βŠ‘ 𝓓)

\end{code}

The compact elements are closed under existing finite joins.

\begin{code}

module _ where
 open import DomainTheory.Basics.Pointed pt fe π“₯

 βŠ₯-is-compact : (𝓓 : DCPOβŠ₯ {𝓀} {𝓣}) β†’ is-compact (𝓓 ⁻) (βŠ₯ 𝓓)
 βŠ₯-is-compact 𝓓 I Ξ± Ξ΄ _ = βˆ₯βˆ₯-functor h (inhabited-if-Directed (𝓓 ⁻) Ξ± Ξ΄)
  where
   h : I β†’ Ξ£ i κž‰ I , βŠ₯ 𝓓 βŠ‘βŸͺ 𝓓 ⟫ Ξ± i
   h i = (i , βŠ₯-is-least 𝓓 (Ξ± i))

 βŠ₯-β‰ͺ : (𝓓 : DCPOβŠ₯ {𝓀} {𝓣}) (x : βŸͺ 𝓓 ⟫) β†’ βŠ₯ 𝓓 β‰ͺ⟨ 𝓓 ⁻ ⟩ x
 βŠ₯-β‰ͺ 𝓓 x = β‰ͺ-βŠ‘-to-β‰ͺ (𝓓 ⁻) (βŠ₯-is-compact 𝓓) (βŠ₯-is-least 𝓓 x)

binary-join-is-compact : (𝓓 : DCPO {𝓀} {𝓣}) {x y z : ⟨ 𝓓 ⟩}
                       β†’ x βŠ‘βŸ¨ 𝓓 ⟩ z β†’ y βŠ‘βŸ¨ 𝓓 ⟩ z
                       β†’ ((d : ⟨ 𝓓 ⟩) β†’ x βŠ‘βŸ¨ 𝓓 ⟩ d β†’ y βŠ‘βŸ¨ 𝓓 ⟩ d β†’ z βŠ‘βŸ¨ 𝓓 ⟩ d)
                       β†’ is-compact 𝓓 x β†’ is-compact 𝓓 y β†’ is-compact 𝓓 z
binary-join-is-compact
 𝓓 {x} {y} {z} x-below-z y-below-z z-lb-of-ubs x-cpt y-cpt = Ξ³
  where
   Ξ³ : is-compact 𝓓 z
   Ξ³ I Ξ± Ξ΄ z-below-∐α = βˆ₯βˆ₯-recβ‚‚ βˆƒ-is-prop f
                         (x-cpt I Ξ± Ξ΄ (x     βŠ‘βŸ¨ 𝓓 ⟩[ x-below-z ]
                                       z     βŠ‘βŸ¨ 𝓓 ⟩[ z-below-∐α ]
                                       ∐ 𝓓 Ξ΄ ∎⟨ 𝓓 ⟩))
                         (y-cpt I Ξ± Ξ΄ (y     βŠ‘βŸ¨ 𝓓 ⟩[ y-below-z ]
                                       z     βŠ‘βŸ¨ 𝓓 ⟩[ z-below-∐α ]
                                       ∐ 𝓓 Ξ΄ ∎⟨ 𝓓 ⟩))
    where
     f : (Ξ£ i κž‰ I , x βŠ‘βŸ¨ 𝓓 ⟩ Ξ± i)
       β†’ (Ξ£ j κž‰ I , y βŠ‘βŸ¨ 𝓓 ⟩ Ξ± j)
       β†’ (βˆƒ k κž‰ I , z βŠ‘βŸ¨ 𝓓 ⟩ Ξ± k)
     f (i , x-below-Ξ±α΅’) (j , y-below-Ξ±β±Ό) =
      βˆ₯βˆ₯-functor g (semidirected-if-Directed 𝓓 Ξ± Ξ΄ i j)
       where
        g : (Ξ£ k κž‰ I , (Ξ± i βŠ‘βŸ¨ 𝓓 ⟩ Ξ± k) Γ— (Ξ± j βŠ‘βŸ¨ 𝓓 ⟩ Ξ± k))
          β†’ Ξ£ k κž‰ I , z βŠ‘βŸ¨ 𝓓 ⟩ Ξ± k
        g (k , lα΅’ , lβ±Ό) =
         (k , z-lb-of-ubs (Ξ± k)
               (x   βŠ‘βŸ¨ 𝓓 ⟩[ x-below-Ξ±α΅’ ]
                Ξ± i βŠ‘βŸ¨ 𝓓 ⟩[ lα΅’ ]
                Ξ± k ∎⟨ 𝓓 ⟩)
               (y   βŠ‘βŸ¨ 𝓓 ⟩[ y-below-Ξ±β±Ό ]
                Ξ± j βŠ‘βŸ¨ 𝓓 ⟩[ lβ±Ό ]
                Ξ± k ∎⟨ 𝓓 ⟩))

\end{code}

If we have a continuous section s with continuous retraction r, then y β‰ͺ s x
implies r y β‰ͺ x for all elements x and y.

\begin{code}

module _
        (𝓓 : DCPO {𝓀} {𝓣})
        (𝓔 : DCPO {𝓀'} {𝓣'})
        (ρ : 𝓓 continuous-retract-of 𝓔)
       where

 open _continuous-retract-of_ ρ

 continuous-retraction-β‰ͺ-criterion : (y : ⟨ 𝓔 ⟩) (x : ⟨ 𝓓 ⟩)
                                   β†’ y β‰ͺ⟨ 𝓔 ⟩ s x
                                   β†’ r y β‰ͺ⟨ 𝓓 ⟩ x
 continuous-retraction-β‰ͺ-criterion y x y-way-below-sx I Ξ± Ξ΄ x-below-∐α =
  βˆ₯βˆ₯-functor h (y-way-below-sx I (s ∘ Ξ±) Ξ΅ l)
   where
    Ξ΅ : is-Directed 𝓔 (s ∘ Ξ±)
    Ξ΅ = image-is-directed' 𝓓 𝓔 𝕀 Ξ΄
    l : s x βŠ‘βŸ¨ 𝓔 ⟩ ∐ 𝓔 Ξ΅
    l = s x       βŠ‘βŸ¨ 𝓔 ⟩[ monotone-if-continuous 𝓓 𝓔 𝕀 x (∐ 𝓓 Ξ΄) x-below-∐α ]
        s (∐ 𝓓 Ξ΄) βŠ‘βŸ¨ 𝓔 ⟩[ continuous-∐-βŠ‘ 𝓓 𝓔 𝕀 Ξ΄ ]
        ∐ 𝓔 Ξ΅     ∎⟨ 𝓔 ⟩
    h : (Ξ£ i κž‰ I , y βŠ‘βŸ¨ 𝓔 ⟩ s (Ξ± i))
      β†’ (Ξ£ i κž‰ I , r y βŠ‘βŸ¨ 𝓓 ⟩ Ξ± i)
    h (i , u) = (i , v)
     where
      v = r y         βŠ‘βŸ¨ 𝓓 ⟩[ monotone-if-continuous 𝓔 𝓓 𝕣 y (s (Ξ± i)) u ]
          r (s (Ξ± i)) βŠ‘βŸ¨ 𝓓 ⟩[ =-to-βŠ‘ 𝓓 (s-section-of-r (Ξ± i)) ]
          Ξ± i         ∎⟨ 𝓓 ⟩

\end{code}

In an embedding-projection pair, the embedding preserves and reflects the
way-below relation, and hence, compact elements.

\begin{code}

module _
        (𝓓 : DCPO {𝓀}  {𝓣} )
        (𝓔 : DCPO {𝓀'} {𝓣'})
        (Ξ΅ : ⟨ 𝓓 ⟩ β†’ ⟨ 𝓔 ⟩)
        (Ξ΅-is-continuous : is-continuous 𝓓 𝓔 Ξ΅)
        (Ο€ : ⟨ 𝓔 ⟩ β†’ ⟨ 𝓓 ⟩)
        (Ο€-is-continuous : is-continuous 𝓔 𝓓 Ο€)
        (Ο€-Ξ΅-retraction : (x : ⟨ 𝓓 ⟩) β†’ Ο€ (Ξ΅ x) = x)
        (Ξ΅-Ο€-deflation : (y : ⟨ 𝓔 ⟩) β†’ Ξ΅ (Ο€ y) βŠ‘βŸ¨ 𝓔 ⟩ y)
       where

 embeddings-preserve-β‰ͺ : (x y : ⟨ 𝓓 ⟩) β†’ x β‰ͺ⟨ 𝓓 ⟩ y β†’ Ξ΅ x β‰ͺ⟨ 𝓔 ⟩ Ξ΅ y
 embeddings-preserve-β‰ͺ x y x-way-below-y I Ξ± Ξ΄ Ξ΅x-below-∐α =
  βˆ₯βˆ₯-functor h (x-way-below-y I (Ο€ ∘ Ξ±) Ξ΄' y-below-βˆΟ€Ξ±)
   where
    Ξ΄' : is-Directed 𝓓 (Ο€ ∘ Ξ±)
    Ξ΄' = image-is-directed' 𝓔 𝓓 (Ο€ , Ο€-is-continuous) Ξ΄
    y-below-βˆΟ€Ξ± = y         βŠ‘βŸ¨ 𝓓 ⟩[ β¦…1⦆ ]
                  Ο€ (Ξ΅ y)   βŠ‘βŸ¨ 𝓓 ⟩[ β¦…2⦆ ]
                  Ο€ (∐ 𝓔 Ξ΄) βŠ‘βŸ¨ 𝓓 ⟩[ β¦…3⦆ ]
                  ∐ 𝓓 Ξ΄'    ∎⟨ 𝓓 ⟩
     where
      β¦…1⦆ = =-to-βŠ‘ 𝓓 ((Ο€-Ξ΅-retraction y) ⁻¹)
      β¦…2⦆ = monotone-if-continuous 𝓔 𝓓 (Ο€ , Ο€-is-continuous) (Ξ΅ y) (∐ 𝓔 Ξ΄)
             Ρx-below-∐α
      β¦…3⦆ = continuous-∐-βŠ‘ 𝓔 𝓓 (Ο€ , Ο€-is-continuous) Ξ΄
    h : (Ξ£ i κž‰ I , x   βŠ‘βŸ¨ 𝓓 ⟩ Ο€ (Ξ± i))
      β†’ (Ξ£ i κž‰ I , Ξ΅ x βŠ‘βŸ¨ 𝓔 ⟩ Ξ± i)
    h (i , u) = (i , (Ξ΅ x         βŠ‘βŸ¨ 𝓔 ⟩[ β¦…1⦆ ]
                      Ξ΅ (Ο€ (Ξ± i)) βŠ‘βŸ¨ 𝓔 ⟩[ β¦…2⦆ ]
                      Ξ± i         ∎⟨ 𝓔 ⟩))
     where
      β¦…1⦆ = monotone-if-continuous 𝓓 𝓔 (Ξ΅ , Ξ΅-is-continuous) x (Ο€ (Ξ± i)) u
      β¦…2⦆ = Ξ΅-Ο€-deflation (Ξ± i)

 embeddings-preserve-compactness : (x : ⟨ 𝓓 ⟩)
                                 β†’ is-compact 𝓓 x β†’ is-compact 𝓔 (Ξ΅ x)
 embeddings-preserve-compactness x = embeddings-preserve-β‰ͺ x x

 embeddings-reflect-β‰ͺ : (x y : ⟨ 𝓓 ⟩) β†’ Ξ΅ x β‰ͺ⟨ 𝓔 ⟩ Ξ΅ y β†’ x β‰ͺ⟨ 𝓓 ⟩ y
 embeddings-reflect-β‰ͺ x y l = transport (Ξ» - β†’ - β‰ͺ⟨ 𝓓 ⟩ y) (Ο€-Ξ΅-retraction x) lem
  where
   lem : Ο€ (Ξ΅ x) β‰ͺ⟨ 𝓓 ⟩ y
   lem = continuous-retraction-β‰ͺ-criterion 𝓓 𝓔 ρ (Ξ΅ x) y l
    where
     ρ : 𝓓 continuous-retract-of 𝓔
     ρ = record
           { s = Ξ΅
           ; r = Ο€
           ; s-section-of-r = Ο€-Ξ΅-retraction
           ; s-is-continuous = Ξ΅-is-continuous
           ; r-is-continuous = Ο€-is-continuous
           }

 embeddings-reflect-compactness : (x : ⟨ 𝓓 ⟩)
                                β†’ is-compact 𝓔 (Ξ΅ x)
                                β†’ is-compact 𝓓 x
 embeddings-reflect-compactness x = embeddings-reflect-β‰ͺ x x

\end{code}