Tom de Jong, 9 March 2020
Refactored 9 February 2022.

Taking the rounded ideal copmletion of the dyadics (𝔻,β‰Ί) we obtain an example of
a continuous dcpo without any compact elements. Hence, it cannot be algebraic.

\begin{code}

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

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

module DomainTheory.Examples.IdlDyadics
        (pt : propositional-truncations-exist)
        (fe : Fun-Ext)
        (pe : Prop-Ext)
       where

open PropositionalTruncation pt

open import DyadicsInductive.Dyadics
open import DyadicsInductive.DyadicOrder
open import DyadicsInductive.DyadicOrder-PropTrunc pt

open import DomainTheory.Basics.Dcpo pt fe 𝓀₀
open import DomainTheory.Basics.WayBelow pt fe 𝓀₀

open import DomainTheory.BasesAndContinuity.Bases pt fe 𝓀₀
open import DomainTheory.BasesAndContinuity.Continuity pt fe 𝓀₀

open import DomainTheory.IdealCompletion.Properties pt fe pe 𝓀₀

open Ideals-of-small-abstract-basis
      (record
         { basis-carrier = 𝔻
         ; _β‰Ί_ = _β‰Ί_
         ; β‰Ί-prop-valued = Ξ» {x} {y} β†’ β‰Ί-is-prop-valued x y
         ; β‰Ί-trans = Ξ» {x} {y} {z} β†’ β‰Ί-is-transitive x y z
         ; INTβ‚€ = β‰Ί-has-no-left-endpoint
         ; INTβ‚‚ = Ξ» {x} {y} {z} β†’ β‰Ί-interpolationβ‚‚ x y z
        })

Idl-𝔻 : DCPO {𝓀₁} {𝓀₀}
Idl-𝔻 = Idl-DCPO

Idl-𝔻-is-continuous : is-continuous-dcpo Idl-𝔻
Idl-𝔻-is-continuous = Idl-is-continuous-dcpo

Idl-𝔻-has-small-basis : has-specified-small-basis Idl-𝔻
Idl-𝔻-has-small-basis = 𝔻 , ↓_ , ↓-is-small-basis

Idl-𝔻-has-no-compact-elements : (I : Idl) β†’ Β¬ (is-compact Idl-𝔻 I)
Idl-𝔻-has-no-compact-elements I ΞΊ = βˆ₯βˆ₯-rec 𝟘-is-prop Ξ³ g
 where
  Ξ³ : Β¬ (Ξ£ x κž‰ 𝔻 , x ∈ᡒ I Γ— I βŠ‘ (↓ x))
  Ξ³ (x , xI , s) = β‰Ί-to-β‰  {x} {x} r refl
   where
    r : x β‰Ί x
    r = s x xI
  g : βˆƒ x κž‰ 𝔻 , x ∈ᡒ I Γ— I βŠ‘ (↓ x)
  g = Idl-β‰ͺ-in-terms-of-βŠ‘ I I ΞΊ

Idl-𝔻-is-not-algebraic : Β¬ (is-algebraic-dcpo Idl-𝔻)
Idl-𝔻-is-not-algebraic = βˆ₯βˆ₯-rec 𝟘-is-prop Ξ³
 where
  Ξ³ : Β¬ (structurally-algebraic Idl-𝔻)
  Ξ³ str-alg = βˆ₯βˆ₯-rec 𝟘-is-prop r I-inh
   where
    open structurally-algebraic str-alg
    x : 𝔻
    x = middle
    I-inh : βˆ₯ index-of-compact-family (↓ x) βˆ₯
    I-inh = inhabited-if-Directed Idl-𝔻 (compact-family (↓ x))
                                         (compact-family-is-directed (↓ x))
    r : Β¬ (index-of-compact-family (↓ x))
    r i = Idl-𝔻-has-no-compact-elements (compact-family (↓ x) i)
                                        (compact-family-is-compact (↓ x) i)

\end{code}