Tom de Jong, 31 January - 4 February 2022.
Material moved to separate file on 11 June 2022.
Updated with sup-complete ideal completion on 27 June 2024.

Suppose we are given a continuous dcpo D with small basis β : B → D. We show
that D is a continuous retract of the ideal completion Idl(B,⊑) which is an
algebraic dpco with a small compact basis. In fact, we even have an
embedding-projection pair.

We can also consider Idl(B,≪) and we get a continuous dcpo that is isomorphic to
D, but notice that Idl(B,≪) : 𝓥-DCPO {𝓥 ⁺} {𝓥}, while D : 𝓥-DCPO {𝓤} {𝓣}. Thus,
a dcpo with a small basis can essentially be parameterized by a single universe
with a large carrier. Moreover, every dcpo with a small basis can be presented
using ideals.(†)

Similarly, an algebraic dcpo with small compact basis β : B → D is isomorphic to
Idl(B,⊑) and analogous remarks apply in this case.

(†) Here, and similarly elsewhere, we really consider Idl(B,≪ₛ), where ≪ₛ is
    equivalent to ≪ on B, but takes values in 𝓥.

    The size conditions on B and the order are similar to those in Corollary
    2.17 of "Continuous categories and exponentiable toposes" by Johnstone and
    Joyal.

\begin{code}

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

open import MLTT.Spartan hiding (J)

open import UF.FunExt
open import UF.PropTrunc
open import UF.Subsingletons

module DomainTheory.IdealCompletion.Retracts
        (pt : propositional-truncations-exist)
        (fe : Fun-Ext)
        (pe : Prop-Ext)
        (𝓥 : Universe) -- universe where the index types for directedness
                       -- completeness live
       where

open import UF.Equiv
open import UF.Retracts
open import UF.Powerset

open import DomainTheory.Basics.Dcpo pt fe 𝓥
open import DomainTheory.Basics.Miscelanea pt fe 𝓥
open import DomainTheory.Basics.SupComplete 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 PropositionalTruncation pt

\end{code}

We will consider ideal completions of:
(1) a small basis ordered by ⊑;
(2) a small basis ordered by ≪;
(3) a small compact basis order by ⊑.

All of these share some common ingredients, which we capture in the following
module so that we can conveniently reuse them.

\begin{code}

module Idl-retract-common
        (𝓓 : DCPO {𝓤} {𝓣})
        {B : 𝓥 ̇ }
        (β : B   𝓓 )
        (β-is-small-basis : is-small-basis 𝓓 β)
       where

 open is-small-basis β-is-small-basis

\end{code}

However we choose to order the basis, the map that takes an element x : D to the
subset {b : B ∣ b ≪ x} is instrumental. We show that this assignment is
Scott continuous here.

\begin{code}

 ↡ᴮ-subset : (x :  𝓓 )  𝓟 B
 ↡ᴮ-subset x =  b  (b ≪ᴮₛ x , ≪ᴮₛ-is-prop-valued))

 ↡ᴮ-subset-is-inhabited : (x :  𝓓 )   𝕋 (↡ᴮ-subset x) 
 ↡ᴮ-subset-is-inhabited x = inhabited-if-Directed 𝓓 (↡-inclusionₛ x) (↡ᴮₛ-is-directed x)

 ↡ᴮ-is-monotone : (x y :  𝓓 )  x ⊑⟨ 𝓓  y  ↡ᴮ-subset x  ↡ᴮ-subset y
 ↡ᴮ-is-monotone x y x-below-y b b-way-below-x =
  ≪ᴮ-to-≪ᴮₛ (≪-⊑-to-≪ 𝓓 (≪ᴮₛ-to-≪ᴮ b-way-below-x) x-below-y)

 ↡ᴮ-is-continuous : {I : 𝓥 ̇ } {α : I   𝓓 } (δ : is-Directed 𝓓 α)
                   is-sup _⊆_ (↡ᴮ-subset ( 𝓓 δ)) (↡ᴮ-subset  α)
 ↡ᴮ-is-continuous {I} {α} δ = (ub , lb-of-ubs)
  where
   ub : is-upperbound _⊆_ (↡ᴮ-subset ( 𝓓 δ)) (↡ᴮ-subset  α)
   ub i b b-way-below-αᵢ =
    ≪ᴮ-to-≪ᴮₛ (≪-⊑-to-≪ 𝓓 (≪ᴮₛ-to-≪ᴮ b-way-below-αᵢ) (∐-is-upperbound 𝓓 δ i))
   lb-of-ubs : is-lowerbound-of-upperbounds _⊆_
                (↡ᴮ-subset ( 𝓓 δ)) (↡ᴮ-subset  α)
   lb-of-ubs S S-is-ub b b-way-below-∐α =
    ∥∥-rec (∈-is-prop S b) lemma₁ interpolant
     where
      interpolant :  c  B , (β b ≪⟨ 𝓓  β c) × (β c ≪⟨ 𝓓  ( 𝓓 δ))
      interpolant = ≪-unary-interpolation-basis 𝓓 β β-is-small-basis
                     (≪ᴮₛ-to-≪ᴮ b-way-below-∐α)
      lemma₁ : (Σ c  B , (β b ≪⟨ 𝓓  β c) × (β c ≪⟨ 𝓓  ( 𝓓 δ)))
              b  S
      lemma₁ (c , b-way-below-c , c-way-below-∐α) =
       ∥∥-rec (∈-is-prop S b) lemma₂ wb-consequence
        where
         wb-consequence :  i  I , β c ⊑⟨ 𝓓  α i
         wb-consequence = c-way-below-∐α I α δ (reflexivity 𝓓 ( 𝓓 δ))
         lemma₂ : (Σ i  I , β c ⊑⟨ 𝓓  α i)  b  S
         lemma₂ (i , c-below-αᵢ) =
          S-is-ub i b (≪ᴮ-to-≪ᴮₛ (≪-⊑-to-≪ 𝓓 b-way-below-c c-below-αᵢ))

\end{code}

We show that the supremum of {b : B ∣ b ≪ x} equals x.

\begin{code}

 ∐-of-directed-subset : (I : 𝓟 B)
                       is-Directed 𝓓 (β  𝕋-to-carrier I)
                        𝓓 
 ∐-of-directed-subset I δ =  𝓓 δ

 ↡ᴮ-section-of-∐ : (x :  𝓓 ) (δ : is-Directed 𝓓 (↡-inclusionₛ x))
                  ∐-of-directed-subset (↡ᴮ-subset x) δ  x
 ↡ᴮ-section-of-∐ x δ =  𝓓 δ =⟨ ⦅1⦆ 
                        𝓓 ε =⟨ ⦅2⦆ 
                       x     
  where
   ε : is-Directed 𝓓 (↡-inclusionₛ x)
   ε = ↡ᴮₛ-is-directed x
   ⦅1⦆ = ∐-independent-of-directedness-witness 𝓓 δ ε
   ⦅2⦆ = ↡ᴮₛ-∐-= x

\end{code}

We present some criteria (which will find application later) for the composition
of ↡ᴮ-subset and ∐ to be a deflation, inflation and retraction-section.

\begin{code}

 ↡ᴮ-∐-deflation : (I : 𝓟 B) {δ : is-Directed 𝓓 (β  𝕋-to-carrier I)}
                 ((b c : B)  β b ⊑⟨ 𝓓  β c  c  I  b  I)
                 ↡ᴮ-subset (∐-of-directed-subset I δ)  I
 ↡ᴮ-∐-deflation I {δ} I-lowerset b b-way-below-sup =
  ∥∥-rec (∈-is-prop I b) lemma claim
   where
    claim :  i  𝕋 I , β b ⊑⟨ 𝓓  β ((𝕋-to-carrier I) i)
    claim = ≪ᴮₛ-to-≪ᴮ b-way-below-sup (𝕋 I) (β  𝕋-to-carrier I) δ
             (reflexivity 𝓓 ( 𝓓 δ))
    lemma : (Σ i  𝕋 I , β b ⊑⟨ 𝓓  β ((𝕋-to-carrier I) i))
           b  I
    lemma ((c , c-in-I) , b-below-c) = I-lowerset b c b-below-c c-in-I

 ↡ᴮ-∐-inflation : (I : 𝓟 B) {δ : is-Directed 𝓓 (β  𝕋-to-carrier I)}
                 ((b : B)  b  I   c  B , (c  I) × (β b ≪⟨ 𝓓  β c))
                 I  ↡ᴮ-subset (∐-of-directed-subset I δ)
 ↡ᴮ-∐-inflation I {δ} I-rounded b b-in-I = ∥∥-rec ≪ᴮₛ-is-prop-valued lemma claim
  where
   claim :  c  B , (c  I) × (β b ≪⟨ 𝓓  β c)
   claim = I-rounded b b-in-I
   lemma : (Σ c  B , (c  I) × (β b ≪⟨ 𝓓  β c))
          b ≪ᴮₛ ∐-of-directed-subset I δ
   lemma (c , c-in-I , b-way-below-c) =
    ≪ᴮ-to-≪ᴮₛ (≪-⊑-to-≪ 𝓓 b-way-below-c (∐-is-upperbound 𝓓 δ (c , c-in-I)))

 ∐-↡ᴮ-retract : (I : 𝓟 B) {δ : is-Directed 𝓓 (β  𝕋-to-carrier I)}
               ((b c : B)  β b ⊑⟨ 𝓓  β c  c  I  b  I)
               ((b : B)  b  I   c  B , (c  I) × (β b ≪⟨ 𝓓  β c))
               ↡ᴮ-subset (∐-of-directed-subset I δ)  I
 ∐-↡ᴮ-retract I {δ} cond₁ cond₂ =
  subset-extensionality pe fe (↡ᴮ-∐-deflation I cond₁) (↡ᴮ-∐-inflation I cond₂)

\end{code}

If we assume the existence of some binary relation (which we think of as an
order) on B, then we can give some convenient criteria for ↡ᴮ being a
semidirected and lower-closed.

\begin{code}

 module _
         (_≺_ : B  B  𝓥 ̇ )
        where

  ↡ᴮ-lowerset-criterion : (x :  𝓓 )
                         ((b c : B)  b  c  β b ⊑⟨ 𝓓  β c)
                         (b c : B)  b  c  c  ↡ᴮ-subset x  b  ↡ᴮ-subset x
  ↡ᴮ-lowerset-criterion x β-mon b c b-below-c c-way-below-x =
   ≪ᴮ-to-≪ᴮₛ (⊑-≪-to-≪ 𝓓 (β-mon b c b-below-c) (≪ᴮₛ-to-≪ᴮ c-way-below-x))

  ↡ᴮ-semidirected-set-criterion : (x :  𝓓 )
                                 ((b c : B)  β b ≪⟨ 𝓓  β c  b  c)
                                 (a b : B)  a  ↡ᴮ-subset x  b  ↡ᴮ-subset x
                                  c  B , c  ↡ᴮ-subset x × (a  c) × (b  c)
  ↡ᴮ-semidirected-set-criterion x β-mon a b a-way-below-x b-way-below-x =
   ∥∥-functor h (≪-binary-interpolation-basis 𝓓 β β-is-small-basis
                 (≪ᴮₛ-to-≪ᴮ a-way-below-x)
                 (≪ᴮₛ-to-≪ᴮ b-way-below-x))
    where
     h : (Σ c  B , (β a ≪⟨ 𝓓  β c) × (β b ≪⟨ 𝓓  β c) × (β c ≪⟨ 𝓓  x))
        (Σ c  B , c  ↡ᴮ-subset x × (a  c) × (b  c))
     h (c , a-way-below-c , b-way-below-c , c-way-below-x) =
      (c , ≪ᴮ-to-≪ᴮₛ c-way-below-x , β-mon a c a-way-below-c
                                   , β-mon b c b-way-below-c)

\end{code}

A major application of the theory of rounded ideals is the following: a
continuous dcpo D with a small basis β : B → D is a continous retract (in fact,
we have an embedding-projection pair) of an algebraic dcpo, namely of Idl(B,⊑).

\begin{code}

module Idl-continuous-retract-of-algebraic
        (𝓓 : DCPO {𝓤} {𝓣})
        {B : 𝓥 ̇ }
        (β : B   𝓓 )
        (β-is-small-basis : is-small-basis 𝓓 β)
       where

 open is-small-basis β-is-small-basis
 open is-locally-small (locally-small-if-small-basis 𝓓 β β-is-small-basis)

 _⊑ᴮ_ : B  B  𝓥 ̇
 b ⊑ᴮ b' = β b ⊑ₛ β b'

 ⊑ᴮ-≃-⊑ : {b b' : B}  (b ⊑ᴮ b')  (β b ⊑⟨ 𝓓  β b')
 ⊑ᴮ-≃-⊑ {b} {b'} = ⊑ₛ-≃-⊑

 ⊑ᴮ-is-prop-valued : {b b' : B}  is-prop (b ⊑ᴮ b')
 ⊑ᴮ-is-prop-valued = equiv-to-prop ⊑ᴮ-≃-⊑ (prop-valuedness 𝓓 _ _)

 ⊑ᴮ-is-reflexive : {b : B}  b ⊑ᴮ b
 ⊑ᴮ-is-reflexive =  ⊑ᴮ-≃-⊑ ⌝⁻¹ (reflexivity 𝓓 _)

 ⊑ᴮ-is-transitive : {b b' b'' : B}  b ⊑ᴮ b'  b' ⊑ᴮ b''  b ⊑ᴮ b''
 ⊑ᴮ-is-transitive u v =  ⊑ᴮ-≃-⊑ ⌝⁻¹
                         (transitivity 𝓓 _ _ _ ( ⊑ᴮ-≃-⊑  u) ( ⊑ᴮ-≃-⊑  v))

 ⊑ᴮ-reflexive-abstract-basis : reflexive-abstract-basis
 ⊑ᴮ-reflexive-abstract-basis = record
                                { basis-carrier = B
                                ; _≺_ = _⊑ᴮ_
                                ; ≺-prop-valued = ⊑ᴮ-is-prop-valued
                                ; ≺-trans = ⊑ᴮ-is-transitive
                                ; ≺-refl = ⊑ᴮ-is-reflexive
                                }

 ⊑ᴮ-abstract-basis : abstract-basis
 ⊑ᴮ-abstract-basis = reflexive-abstract-basis-to-abstract-basis
                      ⊑ᴮ-reflexive-abstract-basis

 open Ideals-of-small-abstract-basis ⊑ᴮ-abstract-basis public
 open Idl-retract-common 𝓓 β β-is-small-basis public
 open Idl-mediating 𝓓 β  ⊑ᴮ-≃-⊑  public

 to-Idl :  𝓓   Idl
 to-Idl x = (Bₓ , Bₓ-is-lowerset , Bₓ-is-directed-set)
  where
   Bₓ : 𝓟 B
   Bₓ = ↡ᴮ-subset x
   Bₓ-is-lowerset : is-lowerset Bₓ
   Bₓ-is-lowerset = ↡ᴮ-lowerset-criterion _⊑ᴮ_ x  b c   ⊑ᴮ-≃-⊑ )
   Bₓ-is-semidirected-set : is-semidirected-set Bₓ
   Bₓ-is-semidirected-set =
    ↡ᴮ-semidirected-set-criterion _⊑ᴮ_ x
      b c b-way-below-c   ⊑ᴮ-≃-⊑ ⌝⁻¹ (≪-to-⊑ 𝓓 b-way-below-c))
   Bₓ-is-directed-set : is-directed-set Bₓ
   Bₓ-is-directed-set = (↡ᴮ-subset-is-inhabited x , Bₓ-is-semidirected-set)

 from-Idl : Idl   𝓓 
 from-Idl I = Idl-mediating-map I

 Idl-retract : retract  𝓓  of Idl
 Idl-retract = (r , s , γ)
  where
   s :  𝓓   Idl
   s = to-Idl
   r : Idl   𝓓 
   r = from-Idl
   γ : (x :  𝓓 )  r (s x)  x
   γ x = ↡ᴮ-section-of-∐ x (Idl-mediating-directed (s x))

 Idl-deflation : (I : Idl)  to-Idl (from-Idl I) ⊑⟨ Idl-DCPO  I
 Idl-deflation 𝕀@(I , I-is-ideal) = ↡ᴮ-∐-deflation I γ
  where
   γ : (b c : B)  β b ⊑⟨ 𝓓  β c  c  I  b  I
   γ b c b-below-c c-in-I = ideals-are-lowersets I I-is-ideal b c claim c-in-I
    where
     claim : b ⊑ᴮ c
     claim =  ⊑ᴮ-≃-⊑ ⌝⁻¹ b-below-c

 to-Idl-is-continuous : is-continuous 𝓓 Idl-DCPO to-Idl
 to-Idl-is-continuous I α δ =
  Idl-sups-from-powerset (to-Idl  α) (to-Idl ( 𝓓 δ)) (↡ᴮ-is-continuous δ)

 from-Idl-is-continuous : is-continuous Idl-DCPO 𝓓 from-Idl
 from-Idl-is-continuous = Idl-mediating-map-is-continuous

 Idl-continuous-retract : 𝓓 continuous-retract-of Idl-DCPO
 Idl-continuous-retract =
  record
   { s               = to-Idl
   ; r               = from-Idl
   ; s-section-of-r  = retract-condition Idl-retract
   ; s-is-continuous = to-Idl-is-continuous
   ; r-is-continuous = from-Idl-is-continuous
   }

 Idl-embedding-projection-pair : embedding-projection-pair-between 𝓓 Idl-DCPO
 Idl-embedding-projection-pair =
  record
    { e               = to-Idl
    ; p               = from-Idl
    ; e-section-of-p  = retract-condition Idl-retract
    ; e-p-deflation   = Idl-deflation
    ; e-is-continuous = to-Idl-is-continuous
    ; p-is-continuous = from-Idl-is-continuous
    }

 Idl-is-algebraic : is-algebraic-dcpo Idl-DCPO
 Idl-is-algebraic = Idl-is-algebraic-dcpo  b  ⊑ᴮ-is-reflexive)

\end{code}

Added 27 June 2024.
Taking the ideal completion of a small basis closed under finite joins of a
sup-complete dcpo yields another sup-complete dcpo.

\begin{code}

 module _
         (fj : has-finite-joins 𝓓)
         (bfj : basis-has-finite-joins 𝓓 β β-is-small-basis fj)
        where

  open basis-has-finite-joins bfj
  open has-finite-joins fj

  ideals-contain-⊥ : (I : Idl)  ⊥ᴮ ∈ᵢ I
  ideals-contain-⊥ I =
   ∥∥-rec (∈-is-prop (carrier I) ⊥ᴮ) h
          (ideals-are-inhabited (carrier I) (ideality I))
    where
     h : (Σ b  B , b  carrier I)  ⊥ᴮ  carrier I
     h (b , b-in-I) = ideals-are-lowersets (carrier I) (ideality I) ⊥ᴮ b
                       ( ⊑ᴮ-≃-⊑ ⌝⁻¹ (⊥ᴮ-is-least _))
                       b-in-I

  ideals-are-closed-under-∨ : (I : Idl) {a b : B}
                             a ∈ᵢ I  b ∈ᵢ I  a ∨ᴮ b ∈ᵢ I
  ideals-are-closed-under-∨ I {a} {b} a-in-I b-in-I =
   ∥∥-rec (∈-is-prop (carrier I) (a ∨ᴮ b)) h
          (ideals-are-semidirected (carrier I) (ideality I) a b a-in-I b-in-I)
    where
     h : (Σ c  B , c ∈ᵢ I × (a ⊑ᴮ c) × (b ⊑ᴮ c))  a ∨ᴮ b ∈ᵢ I
     h (c , c-in-I , u , v) =
      ideals-are-lowersets (carrier I) (ideality I)
                           (a ∨ᴮ b) c
                           ( ⊑ᴮ-≃-⊑ ⌝⁻¹ (∨ᴮ-is-lowerbound-of-upperbounds
                                           ( ⊑ᴮ-≃-⊑  u) ( ⊑ᴮ-≃-⊑  v)))
                           c-in-I

  Idl-is-sup-complete-if-basis-has-finite-joins' : is-sup-complete Idl-DCPO
  Idl-is-sup-complete-if-basis-has-finite-joins' =
   dcpo-with-finite-joins-is-sup-complete Idl-DCPO γ
    where
     ⊥Idl : Idl
     ⊥Idl =  b  b ⊑ᴮ ⊥ᴮ , ⊑ᴮ-is-prop-valued) ,
             b c b-below-c c-below-⊥  ⊑ᴮ-is-transitive b-below-c c-below-⊥) ,
             ⊥ᴮ , ⊑ᴮ-is-reflexive  ,
             b c b-below-⊥ c-below-⊥   ⊥ᴮ , ⊑ᴮ-is-reflexive ,
                                           b-below-⊥ , c-below-⊥ )

     ⊥Idl-is-least : is-least (underlying-order Idl-DCPO) ⊥Idl
     ⊥Idl-is-least I b b-below-⊥ =
      ideals-are-lowersets (carrier I) (ideality I)
                           b ⊥ᴮ b-below-⊥ (ideals-contain-⊥ I)

     _∨Idl_ : Idl  Idl  Idl
     I ∨Idl J = K , K-is-lowerset , K-is-inhabited , K-is-semidirected
      where
       K : 𝓟 B
       K b =  (Σ c  B , Σ d  B , c ∈ᵢ I × d ∈ᵢ J × (b ⊑ᴮ (c ∨ᴮ d)))  ,
             ∥∥-is-prop

       K-is-lowerset : is-lowerset K
       K-is-lowerset b₁ b₂ b₁-below-b₂ =
        ∥∥-functor
          (c , d , c-in-I , d-in-J , b₂-below-join)
            (c , d , c-in-I , d-in-J ,
              ⊑ᴮ-is-transitive b₁-below-b₂ b₂-below-join))

       K-is-inhabited : is-inhabited-set K
       K-is-inhabited =  ⊥ᴮ ,  ⊥ᴮ , ⊥ᴮ ,
                                 ideals-contain-⊥ I , ideals-contain-⊥ J ,
                                  ⊑ᴮ-≃-⊑ ⌝⁻¹ (⊥ᴮ-is-least _)  

       K-is-semidirected : is-semidirected-set K
       K-is-semidirected b₁ b₂ = ∥∥-functor₂ h
        where
         h : (Σ c₁  B , Σ d₁  B , c₁ ∈ᵢ I × d₁ ∈ᵢ J × (b₁ ⊑ᴮ c₁ ∨ᴮ d₁))
            (Σ c₂  B , Σ d₂  B , c₂ ∈ᵢ I × d₂ ∈ᵢ J × (b₂ ⊑ᴮ c₂ ∨ᴮ d₂))
            Σ b  B , b  K × (b₁ ⊑ᴮ b) × (b₂ ⊑ᴮ b)
         h (c₁ , d₁ , c₁-in-I , d₁-in-J , u)
           (c₂ , d₂ , c₂-in-I , d₂-in-J , v) = b₁ ∨ᴮ b₂ ,
                                               join-in-K ,
                                                ⊑ᴮ-≃-⊑ ⌝⁻¹ ∨ᴮ-is-upperbound₁ ,
                                                ⊑ᴮ-≃-⊑ ⌝⁻¹ ∨ᴮ-is-upperbound₂
          where
           join-in-K : b₁ ∨ᴮ b₂  K
           join-in-K =  c₁ ∨ᴮ c₂ , d₁ ∨ᴮ d₂ ,
                         ideals-are-closed-under-∨ I c₁-in-I c₂-in-I ,
                         ideals-are-closed-under-∨ J d₁-in-J d₂-in-J ,
                          ⊑ᴮ-≃-⊑ ⌝⁻¹ (∨ᴮ-is-lowerbound-of-upperbounds ⦅1⦆ ⦅2⦆) 
            where
             ⦅1⦆ = β b₁                        ⊑⟨ 𝓓 ⟩[  ⊑ᴮ-≃-⊑  u ]
                  β (c₁ ∨ᴮ d₁)                 ⊑⟨ 𝓓 ⟩[ w ]
                  β ((c₁ ∨ᴮ c₂) ∨ᴮ (d₁ ∨ᴮ d₂)) ∎⟨ 𝓓 
              where
               w = ∨ᴮ-is-lowerbound-of-upperbounds
                    (transitivity 𝓓 _ _ _ ∨ᴮ-is-upperbound₁ ∨ᴮ-is-upperbound₁)
                    (transitivity 𝓓 _ _ _ ∨ᴮ-is-upperbound₁ ∨ᴮ-is-upperbound₂)
             ⦅2⦆ = β b₂                        ⊑⟨ 𝓓 ⟩[  ⊑ᴮ-≃-⊑  v ]
                  β (c₂ ∨ᴮ d₂)                 ⊑⟨ 𝓓 ⟩[ w ]
                  β ((c₁ ∨ᴮ c₂) ∨ᴮ (d₁ ∨ᴮ d₂)) ∎⟨ 𝓓 
              where
               w = ∨ᴮ-is-lowerbound-of-upperbounds
                    (transitivity 𝓓 _ _ _ ∨ᴮ-is-upperbound₂ ∨ᴮ-is-upperbound₁)
                    (transitivity 𝓓 _ _ _ ∨ᴮ-is-upperbound₂ ∨ᴮ-is-upperbound₂)

     ∨Idl-is-sup : (I J : Idl)
                  is-sup (underlying-order Idl-DCPO) (I ∨Idl J)
                          (∨-family Idl-DCPO I J)
     ∨Idl-is-sup I J = ub , lb-of-ubs
      where
       ub : is-upperbound (underlying-order Idl-DCPO) (I ∨Idl J)
                          (∨-family Idl-DCPO I J)
       ub (inl _) b b-in-I =  b , ⊥ᴮ , b-in-I , ideals-contain-⊥ J ,
                                ⊑ᴮ-≃-⊑ ⌝⁻¹ ∨ᴮ-is-upperbound₁ 
       ub (inr _) c c-in-J =  ⊥ᴮ , c , ideals-contain-⊥ I , c-in-J ,
                                ⊑ᴮ-≃-⊑ ⌝⁻¹ ∨ᴮ-is-upperbound₂ 
       lb-of-ubs : is-lowerbound-of-upperbounds (underlying-order Idl-DCPO)
                    (I ∨Idl J) (∨-family Idl-DCPO I J)
       lb-of-ubs L L-ub b b-in-join =
        ∥∥-rec (∈-is-prop (carrier L) b) h b-in-join
         where
          h : (Σ c  B , Σ d  B , (c ∈ᵢ I) × (d ∈ᵢ J) × (b ⊑ᴮ c ∨ᴮ d))
             b  carrier L
          h (c , d , c-in-I , d-in-J , p) =
           ideals-are-lowersets (carrier L) (ideality L) b (c ∨ᴮ d) p
            (ideals-are-closed-under-∨ L
              (L-ub (inl ) c c-in-I) (L-ub (inr ) d d-in-J))

     γ : has-finite-joins Idl-DCPO
     γ = record
          {           = ⊥Idl ;
            ⊥-is-least = ⊥Idl-is-least ;
            _∨_        = _∨Idl_ ;
            ∨-is-sup   = ∨Idl-is-sup
          }

\end{code}

Repackaged, we get the desired result:

\begin{code}

 Idl-is-sup-complete-if-basis-has-finite-joins :
    (c : is-sup-complete 𝓓)
   basis-has-finite-joins 𝓓 β β-is-small-basis
                           (sup-complete-dcpo-has-finite-joins 𝓓 c)
   is-sup-complete Idl-DCPO
 Idl-is-sup-complete-if-basis-has-finite-joins c =
  Idl-is-sup-complete-if-basis-has-finite-joins'
   (sup-complete-dcpo-has-finite-joins 𝓓 c)

\end{code}

Of course, given a continuous dcpo D with small basis β : B → D, we can also
consider Idl(B,≪) which is isomorphic to D.

\begin{code}

module Idl-continuous
        (𝓓 : DCPO {𝓤} {𝓣})
        {B : 𝓥 ̇ }
        (β : B   𝓓 )
        (β-is-small-basis : is-small-basis 𝓓 β)
       where

 open is-small-basis β-is-small-basis

 _≺_ : B  B  𝓥 ̇
 b  b' = b ≪ᴮₛ β b'

 ≺-≃-≪ : {b b' : B}  (b  b')  (β b ≪⟨ 𝓓  β b')
 ≺-≃-≪ {b} {b'} = ≪ᴮₛ-≃-≪ᴮ

 ≺-is-prop-valued : {b b' : B}  is-prop (b  b')
 ≺-is-prop-valued = equiv-to-prop ≺-≃-≪ (≪-is-prop-valued 𝓓)

 ≺-is-transitive : {b b' b'' : B}  b  b'  b'  b''  b  b''
 ≺-is-transitive u v =
   ≺-≃-≪ ⌝⁻¹ (≪-is-transitive 𝓓 ( ≺-≃-≪  u) ( ≺-≃-≪  v))

 ≺-INT₀ : (b : B)   c  B , c  b
 ≺-INT₀ b = ∥∥-functor h
             (≪-nullary-interpolation-basis 𝓓 β β-is-small-basis (β b))
  where
   h : (Σ c  B , β c ≪⟨ 𝓓  β b)  (Σ c  B , c  b)
   h (c , c-way-below-b) = (c ,  ≺-≃-≪ ⌝⁻¹ c-way-below-b)

 ≺-INT₂ : {b₁ b₂ b : B}  b₁  b  b₂  b
          c  B , (b₁  c) × (b₂  c) × (c  b)
 ≺-INT₂ {b₁} {b₂} {b} b₁-below-b b₂-below-b =
  ∥∥-functor h (≪-binary-interpolation-basis 𝓓 β β-is-small-basis
                ( ≺-≃-≪  b₁-below-b) ( ≺-≃-≪  b₂-below-b))
   where
    h : (Σ c  B , (β b₁ ≪⟨ 𝓓  β c)
                 × (β b₂ ≪⟨ 𝓓  β c)
                 × (β c ≪⟨ 𝓓  β b))
       (Σ c  B , (b₁  c) × (b₂  c) × (c  b))
    h (c , u , v , w) = (c ,  ≺-≃-≪ ⌝⁻¹ u ,  ≺-≃-≪ ⌝⁻¹ v ,  ≺-≃-≪ ⌝⁻¹ w)

 ≪-abstract-basis : abstract-basis
 ≪-abstract-basis = record
                     { basis-carrier = B
                     ; _≺_ = _≺_
                     ; ≺-prop-valued = ≺-is-prop-valued
                     ; ≺-trans = ≺-is-transitive
                     ; INT₀ = ≺-INT₀
                     ; INT₂ = ≺-INT₂
                     }

 open Ideals-of-small-abstract-basis ≪-abstract-basis
 open Idl-retract-common 𝓓 β β-is-small-basis
 open Idl-mediating 𝓓 β (≪-to-⊑ 𝓓   ≺-≃-≪ )

 to-Idl :  𝓓   Idl
 to-Idl x = (Bₓ , Bₓ-is-lowerset , Bₓ-is-directed-set)
  where
   Bₓ : 𝓟 B
   Bₓ = ↡ᴮ-subset x
   Bₓ-is-lowerset : is-lowerset Bₓ
   Bₓ-is-lowerset = ↡ᴮ-lowerset-criterion _≺_ x
                      b c b-below-c  ≪-to-⊑ 𝓓 ( ≺-≃-≪  b-below-c))
   Bₓ-is-semidirected-set : is-semidirected-set Bₓ
   Bₓ-is-semidirected-set = ↡ᴮ-semidirected-set-criterion _≺_ x
                              b c   ≺-≃-≪ ⌝⁻¹)
   Bₓ-is-directed-set : is-directed-set Bₓ
   Bₓ-is-directed-set = (↡ᴮ-subset-is-inhabited x , Bₓ-is-semidirected-set)

 from-Idl : Idl   𝓓 
 from-Idl I = Idl-mediating-map I

 to-Idl-is-continuous : is-continuous 𝓓 Idl-DCPO to-Idl
 to-Idl-is-continuous I α δ =
  Idl-sups-from-powerset (to-Idl  α) (to-Idl ( 𝓓 δ)) (↡ᴮ-is-continuous δ)

 from-Idl-is-continuous : is-continuous Idl-DCPO 𝓓 from-Idl
 from-Idl-is-continuous = Idl-mediating-map-is-continuous

 to-Idl-section-of-from-Idl : from-Idl  to-Idl  id
 to-Idl-section-of-from-Idl x =
  ↡ᴮ-section-of-∐ x (Idl-mediating-directed (to-Idl x))

 from-Idl-section-of-to-Idl : to-Idl  from-Idl  id
 from-Idl-section-of-to-Idl 𝕀@(I , I-is-ideal) =
  to-subtype-=  J  being-ideal-is-prop J) (∐-↡ᴮ-retract I claim₁ claim₂)
   where
    claim₁ : (b c : B)  β b ⊑⟨ 𝓓  β c  c  I  b  I
    claim₁ b c b-below-c c-in-I = ∥∥-rec (∈-is-prop I b) h (roundedness 𝕀 c-in-I)
     where
      h : (Σ c'  B , c'  I × (c  c'))  b  I
      h (c' , c'-in-I , c-way-below-c') =
       ideals-are-lowersets I I-is-ideal b c' l c'-in-I
        where
         l : b  c'
         l = (≪ᴮ-to-≪ᴮₛ (⊑-≪-to-≪ 𝓓 b-below-c (≪ᴮₛ-to-≪ᴮ c-way-below-c')))
    claim₂ : (b : B)  b  I   c  B , c  I × β b ≪⟨ 𝓓  β c
    claim₂ b b-in-I = ∥∥-functor h (roundedness 𝕀 b-in-I)
     where
      h : (Σ c  B , c  I × b  c)
         (Σ c  B , c  I × β b ≪⟨ 𝓓  β c)
      h (c , c-in-I , b-below-c) = (c , c-in-I ,  ≺-≃-≪  b-below-c)

 Idl-≃ : 𝓓 ≃ᵈᶜᵖᵒ Idl-DCPO
 Idl-≃ = (to-Idl , from-Idl , to-Idl-section-of-from-Idl
                            , from-Idl-section-of-to-Idl ,
          to-Idl-is-continuous , from-Idl-is-continuous)

\end{code}

Finally, if D is an algebraic dpco with small compact basis β : B → D, then
Idl(B,⊑) is isomorphic to D.

\begin{code}

module Idl-algebraic
        (𝓓 : DCPO {𝓤} {𝓣})
        {B : 𝓥 ̇ }
        (β : B   𝓓 )
        (β-is-small-compact-basis : is-small-compact-basis 𝓓 β)
       where

 open is-small-compact-basis β-is-small-compact-basis
 open Idl-continuous-retract-of-algebraic 𝓓 β
       (compact-basis-is-basis 𝓓 β β-is-small-compact-basis)

 Idl-≃ : 𝓓 ≃ᵈᶜᵖᵒ Idl-DCPO
 Idl-≃ = (to-Idl , from-Idl , retract-condition Idl-retract
                            , from-Idl-section-of-to-Idl ,
          to-Idl-is-continuous , from-Idl-is-continuous)
  where
   -- This is where we use --lossy-unification
   from-Idl-section-of-to-Idl : (I :  Idl-DCPO )  to-Idl (from-Idl I)  I
   from-Idl-section-of-to-Idl I =
    antisymmetry Idl-DCPO (to-Idl (from-Idl I)) I (Idl-deflation I) inflationary
     where
      inflationary : I ⊑⟨ Idl-DCPO  to-Idl (from-Idl I)
      inflationary = ↡ᴮ-∐-inflation (carrier I) condition
       where
        condition : (b : B)  b ∈ᵢ I   c  B , c ∈ᵢ I × (β b ≪⟨ 𝓓  β c)
        condition b b-in-I =  b , b-in-I , basis-is-compact b 

\end{code}

Added 8 July 2024.

We summarise the above in three logical characterisations.

\begin{code}

open Ideals-of-small-abstract-basis

has-specified-small-basis-iff-to-ideal-completion :
   (𝓓 : DCPO {𝓤} {𝓣})
  has-specified-small-basis 𝓓
  (Σ ab  abstract-basis , (𝓓 ≃ᵈᶜᵖᵒ Idl-DCPO ab))
has-specified-small-basis-iff-to-ideal-completion 𝓓 = I , II
 where
  open Idl-continuous
  I : has-specified-small-basis 𝓓
     Σ ab  abstract-basis , (𝓓 ≃ᵈᶜᵖᵒ Idl-DCPO ab)
  I (B , β , β-is-small-basis) = ≪-abstract-basis 𝓓 β β-is-small-basis ,
                                 Idl-≃ 𝓓 β β-is-small-basis
  II : (Σ ab  abstract-basis , (𝓓 ≃ᵈᶜᵖᵒ Idl-DCPO ab))
      has-specified-small-basis 𝓓
  II (ab , iso) = small-basis-from-≃ᵈᶜᵖᵒ pe
                   (Idl-DCPO ab) 𝓓
                   (≃ᵈᶜᵖᵒ-inv 𝓓 (Idl-DCPO ab) iso)
                   (Idl-has-specified-small-basis ab)


private
 ρ = reflexive-abstract-basis-to-abstract-basis

has-specified-small-compact-basis-reflexive-ideal-completion :
   (𝓓 : DCPO {𝓤} {𝓣})
  has-specified-small-compact-basis 𝓓
  (Σ rab  reflexive-abstract-basis ,
          (𝓓 ≃ᵈᶜᵖᵒ Idl-DCPO (ρ rab)))
has-specified-small-compact-basis-reflexive-ideal-completion 𝓓 = I , II
 where
  open Idl-algebraic
  open Idl-continuous-retract-of-algebraic
       hiding (Idl-DCPO ; Idl-has-specified-small-compact-basis)

  I : has-specified-small-compact-basis 𝓓
     Σ rab  reflexive-abstract-basis , (𝓓 ≃ᵈᶜᵖᵒ Idl-DCPO (ρ rab))
  I (B , β , β-is-small-compact-basis) =
   ⊑ᴮ-reflexive-abstract-basis 𝓓 β β-sb ,
   Idl-≃ 𝓓 β β-is-small-compact-basis
    where
     β-sb = compact-basis-is-basis 𝓓 β β-is-small-compact-basis

  II : (Σ rab  reflexive-abstract-basis , (𝓓 ≃ᵈᶜᵖᵒ Idl-DCPO (ρ rab)))
      has-specified-small-compact-basis 𝓓
  II (rab , iso) =
   small-compact-basis-from-≃ᵈᶜᵖᵒ pe
    (Idl-DCPO (ρ rab)) 𝓓
    (≃ᵈᶜᵖᵒ-inv 𝓓 (Idl-DCPO (ρ rab)) iso)
    (Idl-has-specified-small-compact-basis (ρ rab)  b  ≺-refl))
    where
     open reflexive-abstract-basis rab

has-specified-small-basis-iff-retract-of-dcpo-with-small-compact-basis :
   (𝓓 : DCPO {𝓤} {𝓣})
   has-specified-small-basis 𝓓
   (Σ 𝓔  DCPO {𝓥 } {𝓥} , has-specified-small-compact-basis 𝓔
                           × 𝓓 continuous-retract-of 𝓔)
has-specified-small-basis-iff-retract-of-dcpo-with-small-compact-basis 𝓓 = I , II
 where
  open Idl-algebraic
  open Idl-continuous-retract-of-algebraic
       hiding (Idl-DCPO ; Idl-has-specified-small-compact-basis)

  I : has-specified-small-basis 𝓓
     Σ 𝓔  DCPO {𝓥 } {𝓥} , has-specified-small-compact-basis 𝓔
                           × 𝓓 continuous-retract-of 𝓔
  I (B , β , β-sb) = Idl-DCPO ab ,
                     Idl-has-specified-small-compact-basis ab
                       b  ⊑ᴮ-is-reflexive 𝓓 β β-sb) ,
                     Idl-continuous-retract 𝓓 β β-sb
   where
    ab : abstract-basis
    ab = ⊑ᴮ-abstract-basis 𝓓 β β-sb

  II : (Σ 𝓔  DCPO {𝓥 } {𝓥} , has-specified-small-compact-basis 𝓔
                             × 𝓓 continuous-retract-of 𝓔)
      has-specified-small-basis 𝓓
  II (𝓔 , (B , β , β-scb) , cr) =
   B , r  β ,
   small-basis-from-continuous-retract pe 𝓓 𝓔 cr β
                                       (compact-basis-is-basis 𝓔 β β-scb)
    where
     open _continuous-retract-of_ cr

\end{code}