Simcha van Collem, 12th October 2023

For a locally small dcpo 𝓓, whose carrier type lives in π“₯, we can construct
continuous and algebraic structures from their respective properties. We do this
by making a canonical choice for the approximating and compact families:
the approximating family at x consists of all elements way below x, and the
compact family at x consists of all compact elements ordered below x. Their
index types live in π“₯, as we assumed the carrier type of 𝓓 to live in π“₯ and 𝓓 is
locally small.

To prove the required properties for these families, we can access the
unspecified continuous/algebraic structure, as we are proving a proposition.

\begin{code}

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

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

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

open PropositionalTruncation pt

open import UF.Base hiding (_β‰ˆ_)
open import UF.Equiv

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

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.Continuity pt fe π“₯

module _
        (pe : Prop-Ext)
        (𝓓 : DCPO {π“₯} {𝓣})
        (ls : is-locally-small 𝓓)
       where

 structurally-continuous-if-continuous : is-continuous-dcpo 𝓓
                                       β†’ structurally-continuous 𝓓
 structurally-continuous-if-continuous c =
  record
   { index-of-approximating-family = index
   ; approximating-family = family
   ; approximating-family-is-directed = family-is-directed
   ; approximating-family-is-way-below = family-is-way-below
   ; approximating-family-∐-= = family-∐-=
   }
   where
    _β‰ͺβ‚›_ : ⟨ 𝓓 ⟩ β†’ ⟨ 𝓓 ⟩ β†’ π“₯ Μ‡
    x β‰ͺβ‚› y = resized (x β‰ͺ⟨ 𝓓 ⟩ y) (β‰ͺ-is-small-valued pe 𝓓 c ls x y)

    β‰ͺβ‚›-≃-β‰ͺ : {x y : ⟨ 𝓓 ⟩} β†’ x β‰ͺβ‚› y ≃ x β‰ͺ⟨ 𝓓 ⟩ y
    β‰ͺβ‚›-≃-β‰ͺ = resizing-condition (β‰ͺ-is-small-valued pe 𝓓 c ls _ _)

    β‰ͺβ‚›-to-β‰ͺ : {x y : ⟨ 𝓓 ⟩} β†’ x β‰ͺβ‚› y β†’ x β‰ͺ⟨ 𝓓 ⟩ y
    β‰ͺβ‚›-to-β‰ͺ = ⌜ β‰ͺβ‚›-≃-β‰ͺ ⌝

    β‰ͺ-to-β‰ͺβ‚› : {x y : ⟨ 𝓓 ⟩} β†’ x β‰ͺ⟨ 𝓓 ⟩ y β†’ x β‰ͺβ‚› y
    β‰ͺ-to-β‰ͺβ‚› = ⌜ β‰ͺβ‚›-≃-β‰ͺ ⌝⁻¹

    index : ⟨ 𝓓 ⟩ β†’ π“₯ Μ‡
    index x = Ξ£ y κž‰ ⟨ 𝓓 ⟩ , y β‰ͺβ‚› x

    make-index : {x : ⟨ 𝓓 ⟩} (y : ⟨ 𝓓 ⟩) β†’ y β‰ͺ⟨ 𝓓 ⟩ x β†’ index x
    make-index {x} y yβ‰ͺx = y , β‰ͺ-to-β‰ͺβ‚› yβ‰ͺx

    family : (x : ⟨ 𝓓 ⟩) β†’ index x β†’ ⟨ 𝓓 ⟩
    family x = pr₁

    family-is-directed : (x : ⟨ 𝓓 ⟩) β†’ is-Directed 𝓓 (family x)
    family-is-directed x = βˆ₯βˆ₯-rec (being-directed-is-prop _ (family x)) Ξ³ c
     where
      Ξ³ : structurally-continuous 𝓓 β†’ is-Directed 𝓓 (family x)
      Ξ³ sc = family-is-inhabited , family-is-semidirected
       where
        open structurally-continuous sc

        approximating-family-index-to-index : (i : index-of-approximating-family x)
                                            β†’ index x
        approximating-family-index-to-index i =
         make-index (approximating-family x i)
          (approximating-family-is-way-below x i)

        family-is-inhabited : βˆ₯ index x βˆ₯
        family-is-inhabited =
         βˆ₯βˆ₯-functor
          approximating-family-index-to-index
          (inhabited-if-Directed 𝓓 _ (approximating-family-is-directed x))

        family-is-semidirected : is-Semidirected 𝓓 (family x)
        family-is-semidirected (y₁ , y₁β‰ͺβ‚›x) (yβ‚‚ , yβ‚‚β‰ͺβ‚›x) =
         βˆ₯βˆ₯-recβ‚‚ βˆƒ-is-prop f h1 h2
         where
          f : Ξ£ i κž‰ index-of-approximating-family x , y₁ βŠ‘βŸ¨ 𝓓 ⟩ approximating-family x i
            β†’ Ξ£ j κž‰ index-of-approximating-family x , yβ‚‚ βŠ‘βŸ¨ 𝓓 ⟩ approximating-family x j
            β†’ βˆƒ k κž‰ index x , y₁ βŠ‘βŸ¨ 𝓓 ⟩ family x k Γ—
                              yβ‚‚ βŠ‘βŸ¨ 𝓓 ⟩ family x k
          f (i , yβ‚βŠ‘Ξ±α΅’) (j , yβ‚‚βŠ‘Ξ±β±Ό) =
           βˆ₯βˆ₯-functor g (semidirected-if-Directed 𝓓 _ (approximating-family-is-directed x) i j)
           where
            g : Ξ£ k κž‰ index-of-approximating-family x ,
                 approximating-family x i βŠ‘βŸ¨ 𝓓 ⟩ approximating-family x k Γ—
                 approximating-family x j βŠ‘βŸ¨ 𝓓 ⟩ approximating-family x k
              β†’ Ξ£ k κž‰ index x ,
                 y₁ βŠ‘βŸ¨ 𝓓 ⟩ family x k Γ—
                 yβ‚‚ βŠ‘βŸ¨ 𝓓 ⟩ family x k
            g (k , Ξ±α΅’βŠ‘Ξ±β‚– , Ξ±β±ΌβŠ‘Ξ±β‚–) =
             approximating-family-index-to-index k ,
             transitivity 𝓓 _ _ _ yβ‚βŠ‘Ξ±α΅’ Ξ±α΅’βŠ‘Ξ±β‚– ,
             transitivity 𝓓 _ _ _ yβ‚‚βŠ‘Ξ±β±Ό Ξ±β±ΌβŠ‘Ξ±β‚–

          h1 : βˆƒ i κž‰ index-of-approximating-family x , y₁ βŠ‘βŸ¨ 𝓓 ⟩ approximating-family x i
          h1 = (β‰ͺβ‚›-to-β‰ͺ y₁β‰ͺβ‚›x) _ _ (approximating-family-is-directed x)
                (approximating-family-∐-βŠ’ x)

          h2 : βˆƒ i κž‰ index-of-approximating-family x , yβ‚‚ βŠ‘βŸ¨ 𝓓 ⟩ approximating-family x i
          h2 = (β‰ͺβ‚›-to-β‰ͺ yβ‚‚β‰ͺβ‚›x) _ _ (approximating-family-is-directed x)
                (approximating-family-∐-βŠ’ x)

    family-is-way-below : (x : ⟨ 𝓓 ⟩) β†’ is-way-upperbound 𝓓 x (family x)
    family-is-way-below x (y , yβ‰ͺβ‚›x) = β‰ͺβ‚›-to-β‰ͺ yβ‰ͺβ‚›x

    family-∐-= : (x : ⟨ 𝓓 ⟩) β†’ ∐ 𝓓 (family-is-directed x) = x
    family-∐-= x = βˆ₯βˆ₯-rec (sethood 𝓓) Ξ³ c
     where
      Ξ³ : structurally-continuous 𝓓 β†’ ∐ 𝓓 (family-is-directed x) = x
      Ξ³ sc = antisymmetry 𝓓 _ _
              (∐-is-lowerbound-of-upperbounds 𝓓 _ _
                Ξ» (y , yβ‰ͺβ‚›x) β†’ β‰ͺ-to-βŠ‘ 𝓓 (β‰ͺβ‚›-to-β‰ͺ yβ‰ͺβ‚›x))
              (x                                        βŠ‘βŸ¨ 𝓓 ⟩[ β¦…1⦆ ]
               ∐ 𝓓 (approximating-family-is-directed x) βŠ‘βŸ¨ 𝓓 ⟩[ β¦…2⦆ ]
               ∐ 𝓓 (family-is-directed x)               ∎⟨ 𝓓 ⟩)
       where
        open structurally-continuous sc

        β¦…1⦆ = approximating-family-∐-βŠ’ x

        β¦…2⦆ : ∐ 𝓓 (approximating-family-is-directed x) βŠ‘βŸ¨ 𝓓 ⟩ ∐ 𝓓 (family-is-directed x)
        β¦…2⦆ = ∐-is-lowerbound-of-upperbounds 𝓓 _ _
              Ξ» i β†’ ∐-is-upperbound 𝓓 (family-is-directed x)
                     (make-index
                      (approximating-family x i)
                      (approximating-family-is-way-below x i))

 structurally-algebraic-if-algebraic : is-algebraic-dcpo 𝓓
                                     β†’ structurally-algebraic 𝓓
 structurally-algebraic-if-algebraic a =
  record
   { index-of-compact-family = index
   ; compact-family = family
   ; compact-family-is-directed = family-is-directed
   ; compact-family-is-compact = family-is-compact
   ; compact-family-∐-= = family-∐-=
   }
   where
    open is-locally-small ls

    _β‰ͺβ‚›_ : ⟨ 𝓓 ⟩ β†’ ⟨ 𝓓 ⟩ β†’ π“₯ Μ‡
    x β‰ͺβ‚› y = resized (x β‰ͺ⟨ 𝓓 ⟩ y)
               (β‰ͺ-is-small-valued pe 𝓓
                (is-continuous-dcpo-if-algebraic-dcpo 𝓓 a) ls x y)

    β‰ͺβ‚›-≃-β‰ͺ : {x y : ⟨ 𝓓 ⟩} β†’ x β‰ͺβ‚› y ≃ x β‰ͺ⟨ 𝓓 ⟩ y
    β‰ͺβ‚›-≃-β‰ͺ = resizing-condition
                (β‰ͺ-is-small-valued pe 𝓓
                 (is-continuous-dcpo-if-algebraic-dcpo 𝓓 a) ls _ _)

    β‰ͺβ‚›-to-β‰ͺ : {x y : ⟨ 𝓓 ⟩} β†’ x β‰ͺβ‚› y β†’ x β‰ͺ⟨ 𝓓 ⟩ y
    β‰ͺβ‚›-to-β‰ͺ = ⌜ β‰ͺβ‚›-≃-β‰ͺ ⌝

    β‰ͺ-to-β‰ͺβ‚› : {x y : ⟨ 𝓓 ⟩} β†’ x β‰ͺ⟨ 𝓓 ⟩ y β†’ x β‰ͺβ‚› y
    β‰ͺ-to-β‰ͺβ‚› = ⌜ β‰ͺβ‚›-≃-β‰ͺ ⌝⁻¹

    index : ⟨ 𝓓 ⟩ β†’ π“₯ Μ‡
    index x = Ξ£ y κž‰ ⟨ 𝓓 ⟩ , (y β‰ͺβ‚› y) Γ— (y βŠ‘β‚› x)

    make-index : {x : ⟨ 𝓓 ⟩} β†’ (y : ⟨ 𝓓 ⟩) β†’ is-compact 𝓓 y β†’ y βŠ‘βŸ¨ 𝓓 ⟩ x β†’ index x
    make-index y yβ‰ͺy yβŠ‘x = y , β‰ͺ-to-β‰ͺβ‚› yβ‰ͺy , βŠ‘-to-βŠ‘β‚› yβŠ‘x

    family : (x : ⟨ 𝓓 ⟩) β†’ index x β†’ ⟨ 𝓓 ⟩
    family x = pr₁

    family-is-directed : (x : ⟨ 𝓓 ⟩) β†’ is-Directed 𝓓 (family x)
    family-is-directed x = βˆ₯βˆ₯-rec (being-directed-is-prop _ (family x)) Ξ³ a
     where
      Ξ³ : structurally-algebraic 𝓓 β†’ is-Directed 𝓓 (family x)
      Ξ³ sa = family-is-inhabited , family-is-semidirected
       where
        open structurally-algebraic sa

        compact-family-index-to-index : (i : index-of-compact-family x)
                                      β†’ index x
        compact-family-index-to-index i =
         make-index
          (compact-family x i)
          (compact-family-is-compact x i)
          (compact-family-is-upperbound x i)
         where
          β¦…1⦆ = ∐-is-upperbound 𝓓 (compact-family-is-directed x) i
          β¦…2⦆ = =-to-βŠ‘ 𝓓 (compact-family-∐-= x)

        family-is-inhabited : βˆ₯ index x βˆ₯
        family-is-inhabited =
         βˆ₯βˆ₯-functor
          compact-family-index-to-index
          (inhabited-if-Directed 𝓓 _ (compact-family-is-directed x))

        family-is-semidirected : is-Semidirected 𝓓 (family x)
        family-is-semidirected (y₁ , y₁β‰ͺβ‚›y₁ , yβ‚βŠ‘β‚›x) (yβ‚‚ , yβ‚‚β‰ͺβ‚›yβ‚‚ , yβ‚‚βŠ‘β‚›x) =
         βˆ₯βˆ₯-recβ‚‚ βˆƒ-is-prop f h1 h2
         where
          f : Ξ£ i κž‰ index-of-compact-family x , y₁ βŠ‘βŸ¨ 𝓓 ⟩ compact-family x i
            β†’ Ξ£ j κž‰ index-of-compact-family x , yβ‚‚ βŠ‘βŸ¨ 𝓓 ⟩ compact-family x j
            β†’ βˆƒ k κž‰ index x , y₁ βŠ‘βŸ¨ 𝓓 ⟩ family x k Γ—
                              yβ‚‚ βŠ‘βŸ¨ 𝓓 ⟩ family x k
          f (i , yβ‚βŠ‘Ξ±α΅’) (j , yβ‚‚βŠ‘Ξ±β±Ό) =
           βˆ₯βˆ₯-functor g (semidirected-if-Directed 𝓓 _ (compact-family-is-directed x) i j)
           where
            g : Ξ£ k κž‰ index-of-compact-family x ,
                 compact-family x i βŠ‘βŸ¨ 𝓓 ⟩ compact-family x k Γ—
                 compact-family x j βŠ‘βŸ¨ 𝓓 ⟩ compact-family x k
              β†’ Ξ£ k κž‰ index x ,
                 y₁ βŠ‘βŸ¨ 𝓓 ⟩ family x k Γ—
                 yβ‚‚ βŠ‘βŸ¨ 𝓓 ⟩ family x k
            g (k , Ξ±α΅’βŠ‘Ξ±β‚– , Ξ±β±ΌβŠ‘Ξ±β‚–) =
             compact-family-index-to-index k ,
             transitivity 𝓓 _ _ _ yβ‚βŠ‘Ξ±α΅’ Ξ±α΅’βŠ‘Ξ±β‚– ,
             transitivity 𝓓 _ _ _ yβ‚‚βŠ‘Ξ±β±Ό Ξ±β±ΌβŠ‘Ξ±β‚–

          h1 : βˆƒ i κž‰ index-of-compact-family x , y₁ βŠ‘βŸ¨ 𝓓 ⟩ compact-family x i
          h1 = β‰ͺ-βŠ‘-to-β‰ͺ 𝓓 (β‰ͺβ‚›-to-β‰ͺ y₁β‰ͺβ‚›y₁) (βŠ‘β‚›-to-βŠ‘ yβ‚βŠ‘β‚›x) _ _ _
                (=-to-βŠ’ 𝓓 (compact-family-∐-= x))

          h2 : βˆƒ j κž‰ index-of-compact-family x , yβ‚‚ βŠ‘βŸ¨ 𝓓 ⟩ compact-family x j
          h2 = β‰ͺ-βŠ‘-to-β‰ͺ 𝓓 (β‰ͺβ‚›-to-β‰ͺ yβ‚‚β‰ͺβ‚›yβ‚‚) (βŠ‘β‚›-to-βŠ‘ yβ‚‚βŠ‘β‚›x) _ _ _
                (=-to-βŠ’ 𝓓 (compact-family-∐-= x))

    family-is-compact : (x : ⟨ 𝓓 ⟩) (i : index x) β†’ is-compact 𝓓 (family x i)
    family-is-compact x (y , yβ‰ͺβ‚›y , yβŠ‘β‚›x) = β‰ͺβ‚›-to-β‰ͺ yβ‰ͺβ‚›y

    family-∐-= : (x : ⟨ 𝓓 ⟩) β†’ ∐ 𝓓 (family-is-directed x) = x
    family-∐-= x = βˆ₯βˆ₯-rec (sethood 𝓓) Ξ³ a
     where
      Ξ³ : structurally-algebraic 𝓓 β†’ ∐ 𝓓 (family-is-directed x) = x
      Ξ³ sa = antisymmetry 𝓓 _ _
              (∐-is-lowerbound-of-upperbounds 𝓓 _ _
                Ξ» (y , yβ‰ͺβ‚›y , yβŠ‘β‚›x) β†’ βŠ‘β‚›-to-βŠ‘ yβŠ‘β‚›x)
              (x                                  βŠ‘βŸ¨ 𝓓 ⟩[ β¦…1⦆ ]
               ∐ 𝓓 (compact-family-is-directed x) βŠ‘βŸ¨ 𝓓 ⟩[ β¦…2⦆ ]
               ∐ 𝓓 (family-is-directed x)         ∎⟨ 𝓓 ⟩)
       where
        open structurally-algebraic sa

        β¦…1⦆ = =-to-βŠ’ 𝓓 (compact-family-∐-= x)

        β¦…2⦆ : ∐ 𝓓 (compact-family-is-directed x) βŠ‘βŸ¨ 𝓓 ⟩ ∐ 𝓓 (family-is-directed x)
        β¦…2⦆ = ∐-is-lowerbound-of-upperbounds 𝓓 _ _ g
         where
          g : (i : index-of-compact-family x)
            β†’ compact-family x i βŠ‘βŸ¨ 𝓓 ⟩ ∐ 𝓓 (family-is-directed x)
          g i = ∐-is-upperbound 𝓓 (family-is-directed x)
                 (make-index
                  (compact-family x i)
                  (compact-family-is-compact x i)
                  (compact-family-is-upperbound x i))

\end{code}