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

(pt : propositional-truncations-exist)
(fe : Fun-Ext)
(pe : Prop-Ext)
where

open PropositionalTruncation 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.IdealCompletion pt fe pe π€β
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}