Tom de Jong, early January 2022.

We define when a dcpo is (structurally) continuous/algebraic and prove the
nullary, unary and binary interpolation properties of the way-below relation in
a continuous dcpo.

We also show that in a continuous dcpo being locally small is equivalent to the
way-below relation having small truth values. Further, being (structurally)
continuous is preserved by taking continuous retracts.

\begin{code}

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

open import MLTT.Spartan hiding (J)
open import UF.FunExt
open import UF.PropTrunc

module DomainTheory.BasesAndContinuity.Continuity
        (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.EquivalenceExamples

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

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

open import DomainTheory.BasesAndContinuity.IndCompletion pt fe π“₯

\end{code}

We first define an untruncated, non-propositional, version of continuity for
dcpos, which we call continuity data. The notion of a continuous dcpo will
then be given by truncating the type of continuity data.

The motivation for our definition of continuity is discussed in
ContinuityDiscussion.lagda.

We use record syntax to have descriptively named projections available without
having to add them as boilerplate.

\begin{code}

record continuity-data  (𝓓 : DCPO {𝓀} {𝓣}) : π“₯ ⁺ βŠ” 𝓀 βŠ” 𝓣 Μ‡ where
 field
  index-of-approximating-family : ⟨ 𝓓 ⟩ β†’ π“₯ Μ‡
  approximating-family : (x : ⟨ 𝓓 ⟩)
                       β†’ (index-of-approximating-family x) β†’ ⟨ 𝓓 ⟩
  approximating-family-is-directed : (x : ⟨ 𝓓 ⟩)
                                   β†’ is-Directed 𝓓 (approximating-family x)
  approximating-family-is-way-below : (x : ⟨ 𝓓 ⟩)
                                    β†’ is-way-upperbound 𝓓 x
                                       (approximating-family x)
  approximating-family-∐-＝ : (x : ⟨ 𝓓 ⟩)
                           β†’ ∐ 𝓓 (approximating-family-is-directed x) ＝ x

 approximating-family-∐-βŠ‘ : (x : ⟨ 𝓓 ⟩)
                          β†’ ∐ 𝓓 (approximating-family-is-directed x) βŠ‘βŸ¨ 𝓓 ⟩ x
 approximating-family-∐-βŠ‘ x = ＝-to-βŠ‘ 𝓓 (approximating-family-∐-＝ x)

 approximating-family-∐-βŠ’ : (x : ⟨ 𝓓 ⟩)
                          β†’ x βŠ‘βŸ¨ 𝓓 ⟩ ∐ 𝓓 (approximating-family-is-directed x)
 approximating-family-∐-βŠ’ x = ＝-to-βŠ’ 𝓓 (approximating-family-∐-＝ x)

\end{code}

NB. We previously used the terminology "structural continuity" instead of
"continuity data".

We now prefer the latter because the word "structure" suggests that we are
interested in preserving this data, but we are not. (E.g., preserving this data
would mean preserving the way-below relation which Scott continuous functions
rarely do, ruling out constant functions with non-compact values for example.)
We only want to stress that we are not dealing with a property and the word
"data" is better for this.

At the moment the code and its comments still use the old terminology, so for
now we have following aliases, although in the future we will likely update the
terminology throughout the development.

\begin{code}

module structurally-continuous = continuity-data
structurally-continuous = continuity-data

is-continuous-dcpo : DCPO {𝓀} {𝓣} β†’ π“₯ ⁺ βŠ” 𝓀 βŠ” 𝓣 Μ‡
is-continuous-dcpo 𝓓 = βˆ₯ structurally-continuous 𝓓 βˆ₯

being-continuous-dcpo-is-prop : (𝓓 : DCPO {𝓀} {𝓣})
                              β†’ is-prop (is-continuous-dcpo 𝓓)
being-continuous-dcpo-is-prop 𝓓 = βˆ₯βˆ₯-is-prop

\end{code}

Similarly, we define when a dcpo has algebraicity data where the
approximating family is required to consist of compact elements.

\begin{code}

record algebraicity-data (𝓓 : DCPO {𝓀} {𝓣}) : π“₯ ⁺ βŠ” 𝓀 βŠ” 𝓣 Μ‡ where
 field
  index-of-compact-family : ⟨ 𝓓 ⟩ β†’ π“₯ Μ‡
  compact-family : (x : ⟨ 𝓓 ⟩) β†’ (index-of-compact-family x) β†’ ⟨ 𝓓 ⟩
  compact-family-is-directed : (x : ⟨ 𝓓 ⟩) β†’ is-Directed 𝓓 (compact-family x)
  compact-family-is-compact : (x : ⟨ 𝓓 ⟩) (i : index-of-compact-family x)
                            β†’ is-compact 𝓓 (compact-family x i)
  compact-family-∐-＝ : (x : ⟨ 𝓓 ⟩) β†’ ∐ 𝓓 (compact-family-is-directed x) ＝ x

 compact-family-is-upperbound : (x : ⟨ 𝓓 ⟩)
                              β†’ is-upperbound (underlying-order 𝓓)
                                              x (compact-family x)
 compact-family-is-upperbound x i =
  compact-family x i                 βŠ‘βŸ¨ 𝓓 ⟩[ β¦…1⦆ ]
  ∐ 𝓓 (compact-family-is-directed x) βŠ‘βŸ¨ 𝓓 ⟩[ β¦…2⦆ ]
  x                                  ∎⟨ 𝓓 ⟩
   where
    β¦…1⦆ = ∐-is-upperbound 𝓓 (compact-family-is-directed x) i
    β¦…2⦆ = ＝-to-βŠ‘ 𝓓 (compact-family-∐-＝ x)

\end{code}

NB. We previously used the terminology "structural algebraicity" instead of
"algebraicity data". Again, we now prefer the latter for the reasons explained
above in the other comment on terminology.

At the moment the code and its comments still use the old terminology, so for
now we have following aliases, although in the future we will likely update the
terminology throughout the development.

\begin{code}

module structurally-algebraic = algebraicity-data
structurally-algebraic = algebraicity-data

is-algebraic-dcpo : (𝓓 : DCPO {𝓀} {𝓣}) β†’ π“₯ ⁺ βŠ” 𝓀 βŠ” 𝓣 Μ‡
is-algebraic-dcpo 𝓓 = βˆ₯ structurally-algebraic 𝓓 βˆ₯

structurally-continuous-if-structurally-algebraic :
   (𝓓 : DCPO {𝓀} {𝓣})
 β†’ structurally-algebraic 𝓓 β†’ structurally-continuous 𝓓
structurally-continuous-if-structurally-algebraic 𝓓 sa =
 record
  { index-of-approximating-family     = index-of-compact-family
  ; approximating-family              = compact-family
  ; approximating-family-is-directed  = compact-family-is-directed
  ; approximating-family-is-way-below = Ξ³
  ; approximating-family-∐-＝          = compact-family-∐-＝
  }
  where
   open structurally-algebraic sa
   Ξ³ : (x : ⟨ 𝓓 ⟩) β†’ is-way-upperbound 𝓓 x (compact-family x)
   Ξ³ x i = β‰ͺ-βŠ‘-to-β‰ͺ 𝓓 (compact-family-is-compact x i)
                      (compact-family-is-upperbound x i)

is-continuous-dcpo-if-algebraic-dcpo : (𝓓 : DCPO {𝓀} {𝓣})
                                     β†’ is-algebraic-dcpo 𝓓
                                     β†’ is-continuous-dcpo 𝓓
is-continuous-dcpo-if-algebraic-dcpo 𝓓 =
 βˆ₯βˆ₯-functor (structurally-continuous-if-structurally-algebraic 𝓓)

\end{code}

We characterize the order in a structurally continuous dcpo using approximating
families.

\begin{code}

module _
        (𝓓 : DCPO {𝓀} {𝓣})
        (C : structurally-continuous 𝓓)
       where

 open structurally-continuous C

 structurally-continuous-βŠ‘-criterion :
    {x y : ⟨ 𝓓 ⟩}
  β†’ ((i : index-of-approximating-family x) β†’ approximating-family x i βŠ‘βŸ¨ 𝓓 ⟩ y)
  β†’ x βŠ‘βŸ¨ 𝓓 ⟩ y
 structurally-continuous-βŠ‘-criterion {x} {y} l =
  transport (Ξ» - β†’ - βŠ‘βŸ¨ 𝓓 ⟩ y) (approximating-family-∐-＝ x) Ξ³
   where
    Ξ³ : ∐ 𝓓 (approximating-family-is-directed x) βŠ‘βŸ¨ 𝓓 ⟩ y
    Ξ³ = ∐-is-lowerbound-of-upperbounds 𝓓 (approximating-family-is-directed x) y l

 structurally-continuous-βŠ‘-criterion' :
    {x y : ⟨ 𝓓 ⟩}
  β†’ ((i : index-of-approximating-family x) β†’ approximating-family x i β‰ͺ⟨ 𝓓 ⟩ y)
  β†’ x βŠ‘βŸ¨ 𝓓 ⟩ y
 structurally-continuous-βŠ‘-criterion' {x} {y} l =
  structurally-continuous-βŠ‘-criterion (Ξ» i β†’ β‰ͺ-to-βŠ‘ 𝓓 (l i))

 structurally-continuous-βŠ‘-criterion'-converse :
    {x y : ⟨ 𝓓 ⟩}
  β†’ x βŠ‘βŸ¨ 𝓓 ⟩ y
  β†’ ((i : index-of-approximating-family x) β†’ approximating-family x i β‰ͺ⟨ 𝓓 ⟩ y)
 structurally-continuous-βŠ‘-criterion'-converse {x} {y} l i =
  β‰ͺ-βŠ‘-to-β‰ͺ 𝓓 (approximating-family-is-way-below x i) l

 structurally-continuous-βŠ‘-criterion-converse :
    {x y : ⟨ 𝓓 ⟩}
  β†’ x βŠ‘βŸ¨ 𝓓 ⟩ y
  β†’ ((i : index-of-approximating-family x) β†’ approximating-family x i βŠ‘βŸ¨ 𝓓 ⟩ y)
 structurally-continuous-βŠ‘-criterion-converse {x} {y} l i =
  β‰ͺ-to-βŠ‘ 𝓓 (structurally-continuous-βŠ‘-criterion'-converse l i)

\end{code}

We also characterize the way-below relation in terms of the order and
approximating families.

\begin{code}

 structurally-continuous-β‰ͺ-criterion :
    {x y : ⟨ 𝓓 ⟩}
  β†’ (βˆƒ i κž‰ index-of-approximating-family y , x βŠ‘βŸ¨ 𝓓 ⟩ approximating-family y i)
  β†’ x β‰ͺ⟨ 𝓓 ⟩ y
 structurally-continuous-β‰ͺ-criterion {x} {y} = βˆ₯βˆ₯-rec (β‰ͺ-is-prop-valued 𝓓) Ξ³
  where
   Ξ³ : (Ξ£ i κž‰ index-of-approximating-family y
            , x βŠ‘βŸ¨ 𝓓 ⟩ approximating-family y i)
     β†’ x β‰ͺ⟨ 𝓓 ⟩ y
   Ξ³ (i , l) = βŠ‘-β‰ͺ-to-β‰ͺ 𝓓 l (approximating-family-is-way-below y i)

 structurally-continuous-β‰ͺ-criterion-converse :
    {x y : ⟨ 𝓓 ⟩}
  β†’ x β‰ͺ⟨ 𝓓 ⟩ y
  β†’ (βˆƒ i κž‰ index-of-approximating-family y , x βŠ‘βŸ¨ 𝓓 ⟩ approximating-family y i)
 structurally-continuous-β‰ͺ-criterion-converse {x} {y} wb =
  wb (index-of-approximating-family y) (approximating-family y)
     (approximating-family-is-directed y) (approximating-family-∐-βŠ’ y)

\end{code}

We set out to prove nullary, unary and binary interpolation for (structurally)
continuous dcpos.

\begin{code}

 β‰ͺ-nullary-interpolation-str : (x : ⟨ 𝓓 ⟩) β†’ βˆƒ y κž‰ ⟨ 𝓓 ⟩ , y β‰ͺ⟨ 𝓓 ⟩ x
 β‰ͺ-nullary-interpolation-str x =
  βˆ₯βˆ₯-functor Ξ³ (inhabited-if-Directed 𝓓 (approximating-family x)
                                        (approximating-family-is-directed x))
   where
    Ξ³ : index-of-approximating-family x β†’ Ξ£ y κž‰ ⟨ 𝓓 ⟩ , y β‰ͺ⟨ 𝓓 ⟩ x
    Ξ³ i = (approximating-family x i , approximating-family-is-way-below x i)

\end{code}

Our proof of the unary interpolation property is inspired by Proposition 2.12 of
"Continuous categories and Exponentiable Toposes" by Peter Johnstone and AndrΓ©
Joyal. The idea is to approximate y by a family Ξ±α΅’, approximate each Ξ±α΅’ by
another family Ξ²α΅’β±Ό, and finally to approximate y as the "sum" of the Ξ²α΅’β±Όs.

\begin{code}

 β‰ͺ-unary-interpolation-str : {x y : ⟨ 𝓓 ⟩} β†’ x β‰ͺ⟨ 𝓓 ⟩ y
                           β†’ βˆƒ d κž‰ ⟨ 𝓓 ⟩ , (x β‰ͺ⟨ 𝓓 ⟩ d) Γ— (d β‰ͺ⟨ 𝓓 ⟩ y)
 β‰ͺ-unary-interpolation-str {x} {y} x-way-below-y = interpol
  where
   IΚΈ : π“₯ Μ‡
   IΚΈ = index-of-approximating-family y
   Ξ±ΚΈ : IΚΈ β†’ ⟨ 𝓓 ⟩
   Ξ±ΚΈ = approximating-family y
   Ξ΄ΚΈ : is-Directed 𝓓 Ξ±ΚΈ
   Ξ΄ΚΈ = approximating-family-is-directed y
   J : (i : IΚΈ) β†’ π“₯ Μ‡
   J i = index-of-approximating-family (Ξ±ΚΈ i)
   Ξ² : (i : IΚΈ) β†’ J i β†’ ⟨ 𝓓 ⟩
   Ξ² i = approximating-family (Ξ±ΚΈ i)
   Ξ΄ : (i : IΚΈ) β†’ is-Directed 𝓓 (Ξ² i)
   Ξ΄ i = approximating-family-is-directed (Ξ±ΚΈ i)

   open Ind-completion 𝓓
   𝓑 : IΚΈ β†’ Ind
   𝓑 i = J i , Ξ² i , Ξ΄ i
   π“˜ : Ind
   π“˜ = Ind-∐ 𝓑 (inhabited-if-Directed 𝓓 Ξ±ΚΈ Ξ΄ΚΈ , Οƒ)
    where
     Οƒ : is-semidirected _≲_ 𝓑
     Οƒ i₁ iβ‚‚ = βˆ₯βˆ₯-functor r (semidirected-if-Directed 𝓓 Ξ±ΚΈ Ξ΄ΚΈ i₁ iβ‚‚)
      where
       r : (Ξ£ i κž‰ IΚΈ , (Ξ±ΚΈ i₁ βŠ‘βŸ¨ 𝓓 ⟩ Ξ±ΚΈ i) Γ— (Ξ±ΚΈ iβ‚‚ βŠ‘βŸ¨ 𝓓 ⟩ Ξ±ΚΈ i))
         β†’ Ξ£ i κž‰ IΚΈ , (𝓑 i₁ ≲ 𝓑 i) Γ— (𝓑 iβ‚‚ ≲ 𝓑 i)
       r (i , u , v) = i , l₁ , lβ‚‚
        where
         w = approximating-family-∐-βŠ’ (Ξ±ΚΈ i)
         l₁ : 𝓑 i₁ ≲ 𝓑 i
         l₁ j = approximating-family-is-way-below (Ξ±ΚΈ i₁) j (J i) (Ξ² i) (Ξ΄ i)
                 (Ξ±ΚΈ i₁     βŠ‘βŸ¨ 𝓓 ⟩[ u ]
                  Ξ±ΚΈ i      βŠ‘βŸ¨ 𝓓 ⟩[ w ]
                  ∐ 𝓓 (Ξ΄ i) ∎⟨ 𝓓 ⟩)
         lβ‚‚ : 𝓑 iβ‚‚ ≲ 𝓑 i
         lβ‚‚ j = approximating-family-is-way-below (Ξ±ΚΈ iβ‚‚) j (J i) (Ξ² i) (Ξ΄ i)
                 (Ξ±ΚΈ iβ‚‚     βŠ‘βŸ¨ 𝓓 ⟩[ v ]
                  Ξ±ΚΈ i      βŠ‘βŸ¨ 𝓓 ⟩[ w ]
                  ∐ 𝓓 (Ξ΄ i) ∎⟨ 𝓓 ⟩)

   K : π“₯ Μ‡
   K = pr₁ π“˜
   Ξ³ : K β†’ ⟨ 𝓓 ⟩
   Ξ³ = pr₁ (prβ‚‚ π“˜)
   Ξ³-is-directed : is-Directed 𝓓 Ξ³
   Ξ³-is-directed = prβ‚‚ (prβ‚‚ π“˜)

   y-below-∐-of-Ξ³ : y βŠ‘βŸ¨ 𝓓 ⟩ ∐ 𝓓 Ξ³-is-directed
   y-below-∐-of-Ξ³ = structurally-continuous-βŠ‘-criterion u
    where
     u : (i : IΚΈ) β†’ Ξ±ΚΈ i βŠ‘βŸ¨ 𝓓 ⟩ ∐ 𝓓 Ξ³-is-directed
     u i = structurally-continuous-βŠ‘-criterion v
      where
       v : (j : J i) β†’ Ξ² i j βŠ‘βŸ¨ 𝓓 ⟩ ∐ 𝓓 Ξ³-is-directed
       v j = ∐-is-upperbound 𝓓 Ξ³-is-directed (i , j)

   x-below-Ξ³ : βˆƒ k κž‰ K , x βŠ‘βŸ¨ 𝓓 ⟩ Ξ³ k
   x-below-γ = x-way-below-y K γ γ-is-directed y-below-∐-of-γ

   interpol : βˆƒ d κž‰ ⟨ 𝓓 ⟩ , (x β‰ͺ⟨ 𝓓 ⟩ d) Γ— (d β‰ͺ⟨ 𝓓 ⟩ y)
   interpol = βˆ₯βˆ₯-functor r lemma
    where
     r : (Ξ£ i κž‰ IΚΈ , Ξ£ j κž‰ J i , (x βŠ‘βŸ¨ 𝓓 ⟩ Ξ² i j)
                               Γ— (Ξ² i j β‰ͺ⟨ 𝓓 ⟩ Ξ±ΚΈ i)
                               Γ— (Ξ±ΚΈ i β‰ͺ⟨ 𝓓 ⟩ y))
       β†’ Ξ£ d κž‰ ⟨ 𝓓 ⟩ , (x β‰ͺ⟨ 𝓓 ⟩ d) Γ— (d β‰ͺ⟨ 𝓓 ⟩ y)
     r (i , j , u , v , w) = (Ξ±ΚΈ i , βŠ‘-β‰ͺ-to-β‰ͺ 𝓓 u v , w)
     lemma : βˆ₯ Ξ£ i κž‰ IΚΈ , Ξ£ j κž‰ J i , (x βŠ‘βŸ¨ 𝓓 ⟩ Ξ² i j)
                                    Γ— (Ξ² i j β‰ͺ⟨ 𝓓 ⟩ Ξ±ΚΈ i)
                                    Γ— (Ξ±ΚΈ i β‰ͺ⟨ 𝓓 ⟩ y) βˆ₯
     lemma = βˆ₯βˆ₯-functor s x-below-Ξ³
      where
       s : (Ξ£ k κž‰ K , x βŠ‘βŸ¨ 𝓓 ⟩ Ξ³ k)
         β†’ Ξ£ i κž‰ IΚΈ , Ξ£ j κž‰ J i , (x βŠ‘βŸ¨ 𝓓 ⟩ Ξ² i j)
                                Γ— (Ξ² i j β‰ͺ⟨ 𝓓 ⟩ Ξ±ΚΈ i)
                                Γ— (Ξ±ΚΈ i β‰ͺ⟨ 𝓓 ⟩ y)
       s ((i , j) , l) = (i , j , l ,
                          approximating-family-is-way-below (Ξ±ΚΈ i) j ,
                          approximating-family-is-way-below y i)

\end{code}

From the unary interpolation property, one quickly derives the binary version,
although the proof involves eliminating several propositional truncations. For
that reason, we use so-called do-notation (which is possible because βˆ₯-βˆ₯ is a
monad) to shorten the proof below. If we write x ← t, then x : X and t : βˆ₯ X βˆ₯.

\begin{code}

 β‰ͺ-binary-interpolation-str : {x y z : ⟨ 𝓓 ⟩} β†’ x β‰ͺ⟨ 𝓓 ⟩ z β†’ y β‰ͺ⟨ 𝓓 ⟩ z
                            β†’ βˆƒ d κž‰ ⟨ 𝓓 ⟩ , (x β‰ͺ⟨ 𝓓 ⟩ d)
                                          Γ— (y β‰ͺ⟨ 𝓓 ⟩ d)
                                          Γ— (d β‰ͺ⟨ 𝓓 ⟩ z)
 β‰ͺ-binary-interpolation-str {x} {y} {z} x-way-below-z y-way-below-z = do
  let Ξ΄ = approximating-family-is-directed z
  let l = approximating-family-∐-βŠ’ z
  (d₁ , x-way-below-d₁ , d₁-way-below-z) ← β‰ͺ-unary-interpolation-str
                                            x-way-below-z
  (dβ‚‚ , y-way-below-dβ‚‚ , dβ‚‚-way-below-z) ← β‰ͺ-unary-interpolation-str
                                            y-way-below-z

  (i₁ , d₁-below-zⁱ₁)                    ← d₁-way-below-z _ _ Ξ΄ l
  (iβ‚‚ , dβ‚‚-below-zⁱ₂)                    ← dβ‚‚-way-below-z _ _ Ξ΄ l

  (i , zⁱ₁-below-zⁱ , zⁱ₂-below-zⁱ)      ← semidirected-if-Directed 𝓓 _ Ξ΄ i₁ iβ‚‚
  let Ξ± = approximating-family z
  let d₁-below-αⁱ = d₁   βŠ‘βŸ¨ 𝓓 ⟩[ d₁-below-zⁱ₁ ]
                    Ξ± i₁ βŠ‘βŸ¨ 𝓓 ⟩[ zⁱ₁-below-zⁱ ]
                    Ξ± i  ∎⟨ 𝓓 ⟩
  let dβ‚‚-below-αⁱ = dβ‚‚   βŠ‘βŸ¨ 𝓓 ⟩[ dβ‚‚-below-zⁱ₂ ]
                    Ξ± iβ‚‚ βŠ‘βŸ¨ 𝓓 ⟩[ zⁱ₂-below-zⁱ ]
                    Ξ± i  ∎⟨ 𝓓 ⟩
  ∣ approximating-family z i , β‰ͺ-βŠ‘-to-β‰ͺ 𝓓 x-way-below-d₁ d₁-below-αⁱ
                             , β‰ͺ-βŠ‘-to-β‰ͺ 𝓓 y-way-below-dβ‚‚ dβ‚‚-below-αⁱ
                             , approximating-family-is-way-below z i ∣

\end{code}

The interpolation properties for continuous dcpos now follow immediately.

\begin{code}

module _
        (𝓓 : DCPO {𝓀} {𝓣})
        (c : is-continuous-dcpo 𝓓)
       where

 β‰ͺ-nullary-interpolation : (x : ⟨ 𝓓 ⟩) β†’ βˆƒ y κž‰ ⟨ 𝓓 ⟩ , y β‰ͺ⟨ 𝓓 ⟩ x
 β‰ͺ-nullary-interpolation x =
  βˆ₯βˆ₯-rec βˆ₯βˆ₯-is-prop (Ξ» C β†’ β‰ͺ-nullary-interpolation-str 𝓓 C x) c

 β‰ͺ-unary-interpolation : {x y : ⟨ 𝓓 ⟩} β†’ x β‰ͺ⟨ 𝓓 ⟩ y
                       β†’ βˆƒ d κž‰ ⟨ 𝓓 ⟩ , (x β‰ͺ⟨ 𝓓 ⟩ d) Γ— (d β‰ͺ⟨ 𝓓 ⟩ y)
 β‰ͺ-unary-interpolation x-way-below-y =
  βˆ₯βˆ₯-rec βˆ₯βˆ₯-is-prop (Ξ» C β†’ β‰ͺ-unary-interpolation-str 𝓓 C x-way-below-y) c

 β‰ͺ-binary-interpolation : {x y z : ⟨ 𝓓 ⟩} β†’ x β‰ͺ⟨ 𝓓 ⟩ z β†’ y β‰ͺ⟨ 𝓓 ⟩ z
                        β†’ βˆƒ d κž‰ ⟨ 𝓓 ⟩ , (x β‰ͺ⟨ 𝓓 ⟩ d)
                                      Γ— (y β‰ͺ⟨ 𝓓 ⟩ d)
                                      Γ— (d β‰ͺ⟨ 𝓓 ⟩ z)
 β‰ͺ-binary-interpolation {x} {y} {z} u v =
  βˆ₯βˆ₯-rec βˆ₯βˆ₯-is-prop (Ξ» C β†’ β‰ͺ-binary-interpolation-str 𝓓 C u v) c

\end{code}

We show that in a (structurally) continuous dcpo local smallness is logically
equivalent to the way-below relation having small values.

\begin{code}

module _
        (𝓓 : DCPO {𝓀} {𝓣})
        (C : structurally-continuous 𝓓)
       where

 open structurally-continuous C

 β‰ͺ-is-small-valued-str : is-locally-small 𝓓
                       β†’ (x y : ⟨ 𝓓 ⟩) β†’ is-small (x β‰ͺ⟨ 𝓓 ⟩ y)
 β‰ͺ-is-small-valued-str ls x y = (βˆƒ i κž‰ I , x βŠ‘β‚› Ξ± i) , ψ
  where
   open is-locally-small ls
   I : π“₯ Μ‡
   I = index-of-approximating-family y
   Ξ± : I β†’ ⟨ 𝓓 ⟩
   Ξ± = approximating-family y
   ψ = (βˆƒ i κž‰ I , x βŠ‘β‚›      Ξ± i) β‰ƒβŸ¨ βˆƒ-cong pt (Ξ» i β†’ βŠ‘β‚›-≃-βŠ‘) ⟩
       (βˆƒ i κž‰ I , x βŠ‘βŸ¨ 𝓓 ⟩  Ξ± i) β‰ƒβŸ¨ e ⟩
       x β‰ͺ⟨ 𝓓 ⟩ y                β– 
    where
     e = logically-equivalent-props-are-equivalent βˆƒ-is-prop (β‰ͺ-is-prop-valued 𝓓)
          (structurally-continuous-β‰ͺ-criterion 𝓓 C)
          (structurally-continuous-β‰ͺ-criterion-converse 𝓓 C)

 β‰ͺ-is-small-valued-str-converse : ((x y : ⟨ 𝓓 ⟩) β†’ is-small (x β‰ͺ⟨ 𝓓 ⟩ y))
                                β†’ is-locally-small 𝓓
 β‰ͺ-is-small-valued-str-converse β‰ͺ-is-small-valued =
  ⌜ local-smallness-equivalent-definitions 𝓓 ⌝⁻¹ Ξ³
   where
    _β‰ͺβ‚›_ : ⟨ 𝓓 ⟩ β†’ ⟨ 𝓓 ⟩ β†’ π“₯ Μ‡
    x β‰ͺβ‚› y = pr₁ (β‰ͺ-is-small-valued x y)
    β‰ͺβ‚›-≃-β‰ͺ : {x y : ⟨ 𝓓 ⟩} β†’ x β‰ͺβ‚› y ≃ x β‰ͺ⟨ 𝓓 ⟩ y
    β‰ͺβ‚›-≃-β‰ͺ {x} {y} = prβ‚‚ (β‰ͺ-is-small-valued x y)
    Ξ³ : (x y : ⟨ 𝓓 ⟩) β†’ is-small (x βŠ‘βŸ¨ 𝓓 ⟩ y)
    Ξ³ x y = (βˆ€ (i : I) β†’ Ξ± i β‰ͺβ‚› y) , ψ
     where
      I : π“₯ Μ‡
      I = index-of-approximating-family x
      Ξ± : I β†’ ⟨ 𝓓 ⟩
      Ξ± = approximating-family x
      ψ = (βˆ€ (i : I) β†’ Ξ± i β‰ͺβ‚›     y) β‰ƒβŸ¨ Ξ -cong fe fe (Ξ» i β†’ β‰ͺβ‚›-≃-β‰ͺ) ⟩
          (βˆ€ (i : I) β†’ Ξ± i β‰ͺ⟨ 𝓓 ⟩ y) β‰ƒβŸ¨ e ⟩
          x βŠ‘βŸ¨ 𝓓 ⟩ y                 β– 
       where
        e = logically-equivalent-props-are-equivalent
             (Ξ -is-prop fe (Ξ» i β†’ β‰ͺ-is-prop-valued 𝓓)) (prop-valuedness 𝓓 x y)
             (structurally-continuous-βŠ‘-criterion' 𝓓 C)
             (structurally-continuous-βŠ‘-criterion'-converse 𝓓 C)

module _
        (pe : Prop-Ext)
        (𝓓 : DCPO {𝓀} {𝓣})
        (c : is-continuous-dcpo 𝓓)
       where

 open import UF.Size hiding (is-small ; is-locally-small)

 abstract -- for performance
  β‰ͺ-is-small-valued : is-locally-small 𝓓
                    β†’ (x y : ⟨ 𝓓 ⟩) β†’ is-small (x β‰ͺ⟨ 𝓓 ⟩ y)
  β‰ͺ-is-small-valued ls x y = βˆ₯βˆ₯-rec p (Ξ» C β†’ β‰ͺ-is-small-valued-str 𝓓 C ls x y) c
   where
    p : is-prop (is-small (x β‰ͺ⟨ 𝓓 ⟩ y))
    p = prop-being-small-is-prop (Ξ» _ β†’ pe) (Ξ» _ _ β†’ fe)
         (x β‰ͺ⟨ 𝓓 ⟩ y) (β‰ͺ-is-prop-valued 𝓓)

  β‰ͺ-is-small-valued-converse : ((x y : ⟨ 𝓓 ⟩) β†’ is-small (x β‰ͺ⟨ 𝓓 ⟩ y))
                             β†’ is-locally-small 𝓓
  β‰ͺ-is-small-valued-converse ws =
   βˆ₯βˆ₯-rec (being-locally-small-is-prop 𝓓 (Ξ» _ β†’ pe))
    (Ξ» C β†’ β‰ͺ-is-small-valued-str-converse 𝓓 C ws) c

\end{code}

Finally, we prove that (structural) continuity is preserved by continuous
retracts.

\begin{code}

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

 open _continuous-retract-of_ ρ

 structural-continuity-of-dcpo-preserved-by-continuous-retract :
    structurally-continuous 𝓔
  β†’ structurally-continuous 𝓓
 structural-continuity-of-dcpo-preserved-by-continuous-retract C =
  record
   { index-of-approximating-family     = Ξ» x β†’ index-of-approximating-family
                                                (s x)
   ; approximating-family              = Ξ» x β†’ r ∘ approximating-family (s x)
   ; approximating-family-is-directed  = lemma₁
   ; approximating-family-is-way-below = lemmaβ‚‚
   ; approximating-family-∐-＝          = lemma₃
   }
   where
    open structurally-continuous C
    Ξ± : (y : ⟨ 𝓔 ⟩) β†’ index-of-approximating-family y β†’ ⟨ 𝓔 ⟩
    Ξ± = approximating-family
    lemma₁ : (x : ⟨ 𝓓 ⟩) β†’ is-Directed 𝓓 (r ∘ Ξ± (s x))
    lemma₁ x = image-is-directed' 𝓔 𝓓 𝕣
                (approximating-family-is-directed (s x))
    lemmaβ‚‚ : (x : ⟨ 𝓓 ⟩) β†’ is-way-upperbound 𝓓 x (r ∘ Ξ± (s x))
    lemmaβ‚‚ x i = continuous-retraction-β‰ͺ-criterion 𝓓 𝓔 ρ (Ξ± (s x) i) x
                  (approximating-family-is-way-below (s x) i)
    lemma₃ : (x : ⟨ 𝓓 ⟩) β†’ ∐ 𝓓 (lemma₁ x) ＝ x
    lemma₃ x = ∐ 𝓓 (lemma₁ x) ＝⟨ β¦…1⦆ ⟩
               r (∐ 𝓔 Ξ΄)      ＝⟨ β¦…2⦆ ⟩
               r (s x)        ＝⟨ β¦…3⦆ ⟩
               x              ∎
     where
      Ξ΄ : is-Directed 𝓔 (Ξ± (s x))
      Ξ΄ = approximating-family-is-directed (s x)
      β¦…1⦆ = (continuous-∐-＝ 𝓔 𝓓 𝕣 Ξ΄) ⁻¹
      β¦…2⦆ = ap r (approximating-family-∐-＝ (s x))
      β¦…3⦆ = s-section-of-r x

 continuity-of-dcpo-preserved-by-continuous-retract : is-continuous-dcpo 𝓔
                                                    β†’ is-continuous-dcpo 𝓓
 continuity-of-dcpo-preserved-by-continuous-retract =
  βˆ₯βˆ₯-functor structural-continuity-of-dcpo-preserved-by-continuous-retract

\end{code}

Added 8 July 2024.

The purpose of the following construction is to show that structural continuity
is not a property of a dcpo.

\begin{code}

structurally-continuous-+-construction :
  (𝓓 : DCPO {𝓀} {𝓣})
 β†’ structurally-continuous 𝓓
 β†’ structurally-continuous 𝓓
structurally-continuous-+-construction 𝓓 sc =
 record
  { index-of-approximating-family = Ξ» x β†’ I x + I x
  ; approximating-family = [Ξ±,Ξ±]
  ; approximating-family-is-directed = Ξ΄'
  ; approximating-family-is-way-below = wb'
  ; approximating-family-∐-＝ = eq'
  }
  where
   open structurally-continuous sc
         renaming (index-of-approximating-family to I ;
                   approximating-family to Ξ± ;
                   approximating-family-is-directed to Ξ΄ ;
                   approximating-family-is-way-below to wb ;
                   approximating-family-∐-＝ to eq)
   [Ξ±,Ξ±] : (x : ⟨ 𝓓 ⟩) β†’ I x + I x β†’ ⟨ 𝓓 ⟩
   [Ξ±,Ξ±] x = cases (Ξ± x) (Ξ± x)

   lemma₁ : {x : ⟨ 𝓓 ⟩} (i : I x) β†’ βˆƒ j κž‰ I x + I x , Ξ± x i βŠ‘βŸ¨ 𝓓 ⟩ [Ξ±,Ξ±] x j
   lemma₁ {x} i = ∣ inl i , reflexivity 𝓓 (Ξ± x i) ∣
   lemmaβ‚‚ : {x : ⟨ 𝓓 ⟩} (j : I x + I x) β†’ βˆƒ i κž‰ I x , [Ξ±,Ξ±] x j βŠ‘βŸ¨ 𝓓 ⟩ Ξ± x i
   lemmaβ‚‚ {x} (inl i) = ∣ i , reflexivity 𝓓 (Ξ± x i) ∣
   lemmaβ‚‚ {x} (inr i) = ∣ i , reflexivity 𝓓 (Ξ± x i) ∣

   Ξ΄' : (x : ⟨ 𝓓 ⟩) β†’ is-Directed 𝓓 ([Ξ±,Ξ±] x)
   Ξ΄' x = directed-if-bicofinal 𝓓 lemma₁ lemmaβ‚‚ (Ξ΄ x)

   wb' : (x : ⟨ 𝓓 ⟩) β†’ is-way-upperbound 𝓓 x ([Ξ±,Ξ±] x)
   wb' x (inl i) = wb x i
   wb' x (inr i) = wb x i

   eq' : (x : ⟨ 𝓓 ⟩) β†’ ∐ 𝓓 (Ξ΄' x) ＝ x
   eq' x = ∐-＝-if-bicofinal 𝓓 lemmaβ‚‚ lemma₁ (Ξ΄' x) (Ξ΄ x) βˆ™ eq x

\end{code}