Tom de Jong, late February, early March 2022.
Updated 27 June 2024.

We use single step functions to construct a small compact basis on the
exponential of dcpos Eᴰ where D and E have small compact bases and E is
sup-complete. This is used in DomainTheory.Bilimits.Dinfinity.lagda to show that
Scott's D∞ has a small compact basis, and hence is algebraic.

We can prove a similar result for dcpos with a small bases that are not
necessarily algebraic, but the formalization of this argument is not entirely
complete, as it depends on a lemma on the sup-completeness of the ideal
completion, see below for details.

\begin{code}

{-# OPTIONS --safe --without-K --lossy-unification #-}
-- The flag --lossy-unification roughly reduces the timechecking
-- time by 50%.

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


module DomainTheory.BasesAndContinuity.StepFunctions
        (pt : propositional-truncations-exist)
        (fe : Fun-Ext)
        (𝓥 : Universe) -- where the index types for directed completeness live
       where

open PropositionalTruncation pt hiding (_∨_)

open import UF.Equiv
open import UF.Subsingletons

open import DomainTheory.Basics.Dcpo pt fe 𝓥
open import DomainTheory.BasesAndContinuity.Bases pt fe 𝓥
open import DomainTheory.BasesAndContinuity.Continuity pt fe 𝓥
open import DomainTheory.Basics.Exponential pt fe 𝓥
open import DomainTheory.Basics.Miscelanea pt fe 𝓥
open import DomainTheory.Basics.Pointed pt fe 𝓥 hiding (⊥ ; ⊥-is-least)
open import DomainTheory.Basics.SupComplete pt fe 𝓥
open import DomainTheory.Basics.WayBelow pt fe 𝓥

\end{code}

We introduce single step functions to show that sup-complete algebraic dcpos are
closed under exponentials, cf. Exercise II-2.31 in "Continuous Lattices and
Domains" by Gierz et al.

Classically, a single step function
⦅ d ⇒ e ⦆ is given like this:
 x ↦ e if d ⊑ x
     ⊥ otherwise

Constructively, we can't expect to make this case distinction, so we define
single step functions using subsingleton suprema instead.

\begin{code}

module single-step-function-def
        (𝓓 : DCPO {𝓤}  {𝓣})
        (𝓔 : DCPO⊥ {𝓤'} {𝓣'})
        (𝓓-is-locally-small : is-locally-small 𝓓)
       where

 open is-locally-small 𝓓-is-locally-small

 ⦅_⇒_⦆ : ⟨ 𝓓 ⟩ → ⟪ 𝓔 ⟫ → ⟨ 𝓓 ⟩ → ⟪ 𝓔 ⟫
 ⦅ d ⇒ e ⦆ x = ∐ˢˢ 𝓔 α (⊑ₛ-is-prop-valued d x)
  where
   α : d ⊑ₛ x → ⟪ 𝓔 ⟫
   α _ = e

 single-step-function-index : ⟨ 𝓓 ⟩ → ⟨ 𝓓 ⟩ →  𝓥 ̇
 single-step-function-index d x = d ⊑ₛ x

 single-step-function-index-is-prop : {d x : ⟨ 𝓓 ⟩}
                                    → is-prop (single-step-function-index d x)
 single-step-function-index-is-prop {d} {x} = ⊑ₛ-is-prop-valued d x

 single-step-function-family : {d x : ⟨ 𝓓 ⟩} (e : ⟪ 𝓔 ⟫)
                             → single-step-function-index d x → ⟪ 𝓔 ⟫
 single-step-function-family e _ = e

 single-step-function-is-continuous : (d : ⟨ 𝓓 ⟩) (e : ⟪ 𝓔 ⟫)
                                    → is-compact 𝓓 d
                                    → is-continuous 𝓓 (𝓔 ⁻) ⦅ d ⇒ e ⦆
 single-step-function-is-continuous d e d-is-compact I α δ = (ub , lb-of-ubs)
  where
   ub : (i : I) → ⦅ d ⇒ e ⦆ (α i) ⊑⟪ 𝓔 ⟫ ⦅ d ⇒ e ⦆ (∐ 𝓓 δ)
   ub i = ∐ˢˢ-is-lowerbound-of-upperbounds 𝓔 (λ _ → e)
           single-step-function-index-is-prop (⦅ d ⇒ e ⦆ (∐ 𝓓 δ))
           (λ p → ∐ˢˢ-is-upperbound 𝓔 (λ _ → e)
                   single-step-function-index-is-prop
                   (d     ⊑ₛ[ p ]
                    α i   ⊑ₛ[ ⌜ ⊑ₛ-≃-⊑ ⌝⁻¹ (∐-is-upperbound 𝓓 δ i) ]
                    ∐ 𝓓 δ ∎ₛ))
   lb-of-ubs : is-lowerbound-of-upperbounds (underlying-order (𝓔 ⁻))
                (⦅ d ⇒ e ⦆ (∐ 𝓓 δ)) (⦅ d ⇒ e ⦆ ∘ α)
   lb-of-ubs y y-is-ub = ∐ˢˢ-is-lowerbound-of-upperbounds 𝓔 (λ _ → e)
                          single-step-function-index-is-prop y γ
    where
     γ : (p : d ⊑ₛ ∐ 𝓓 δ) → e ⊑⟪ 𝓔 ⟫ y
     γ p = ∥∥-rec (prop-valuedness (𝓔 ⁻) e y)
            lemma (d-is-compact I α δ (⌜ ⊑ₛ-≃-⊑ ⌝ p))
      where
       lemma : (Σ i ꞉ I , d ⊑⟨ 𝓓 ⟩ α i)
             → e ⊑⟪ 𝓔 ⟫ y
       lemma (i , u) = e               ⊑⟪ 𝓔 ⟫[ v ]
                       ⦅ d ⇒ e ⦆ (α i) ⊑⟪ 𝓔 ⟫[ y-is-ub i ]
                       y               ∎⟪ 𝓔 ⟫
        where
         v = ∐ˢˢ-is-upperbound 𝓔 (λ _ → e) single-step-function-index-is-prop
              (⌜ ⊑ₛ-≃-⊑ ⌝⁻¹ u)

 ⦅_⇒_⦆[_] : (d : ⟨ 𝓓 ⟩) (e : ⟪ 𝓔 ⟫)
          → is-compact 𝓓 d
          → DCPO[ 𝓓 , 𝓔 ⁻ ]
 ⦅_⇒_⦆[_] d e d-is-compact =
  (⦅ d ⇒ e ⦆ , single-step-function-is-continuous d e d-is-compact)

 below-single-step-function-criterion : (d : ⟨ 𝓓 ⟩) (e : ⟪ 𝓔 ⟫) (κ : is-compact 𝓓 d)
                                        (f : DCPO[ 𝓓 , 𝓔 ⁻ ])
                                      → ⦅ d ⇒ e ⦆[ κ ] ⊑⟨ 𝓓 ⟹ᵈᶜᵖᵒ (𝓔 ⁻) ⟩ f
                                      ↔ e ⊑⟪ 𝓔 ⟫ [ 𝓓 , 𝓔 ⁻ ]⟨ f ⟩ d
 below-single-step-function-criterion d e κ f = ⦅1⦆ , ⦅2⦆
  where
   ⦅1⦆ : ⦅ d ⇒ e ⦆[ κ ] ⊑⟨ 𝓓 ⟹ᵈᶜᵖᵒ (𝓔 ⁻) ⟩ f
       → e ⊑⟪ 𝓔 ⟫ [ 𝓓 , 𝓔 ⁻ ]⟨ f ⟩ d
   ⦅1⦆ u = e                  ⊑⟪ 𝓔 ⟫[ v ]
           ⦅ d ⇒ e ⦆ d        ⊑⟪ 𝓔 ⟫[ u d ]
           [ 𝓓 , 𝓔 ⁻ ]⟨ f ⟩ d ∎⟪ 𝓔 ⟫
    where
     v = ∐ˢˢ-is-upperbound 𝓔 (λ _ → e) single-step-function-index-is-prop
          (⌜ ⊑ₛ-≃-⊑ ⌝⁻¹ (reflexivity 𝓓 d))
   ⦅2⦆ : e ⊑⟪ 𝓔 ⟫ [ 𝓓 , 𝓔 ⁻ ]⟨ f ⟩ d
      → ⦅ d ⇒ e ⦆[ κ ] ⊑⟨ 𝓓 ⟹ᵈᶜᵖᵒ (𝓔 ⁻) ⟩ f
   ⦅2⦆ u x = ∐ˢˢ-is-lowerbound-of-upperbounds 𝓔 (λ _ → e)
              single-step-function-index-is-prop
              ([ 𝓓 , 𝓔 ⁻ ]⟨ f ⟩ x) γ
    where
     γ : (p : d ⊑ₛ x) → e ⊑⟪ 𝓔 ⟫ [ 𝓓 , 𝓔 ⁻ ]⟨ f ⟩ x
     γ p = e                  ⊑⟪ 𝓔 ⟫[ u ]
           [ 𝓓 , 𝓔 ⁻ ]⟨ f ⟩ d ⊑⟪ 𝓔 ⟫[ v ]
           [ 𝓓 , 𝓔 ⁻ ]⟨ f ⟩ x ∎⟪ 𝓔 ⟫
      where
       v = monotone-if-continuous 𝓓 (𝓔 ⁻) f d x (⌜ ⊑ₛ-≃-⊑ ⌝ p)

 single-step-function-is-compact : (d : ⟨ 𝓓 ⟩) (e : ⟪ 𝓔 ⟫)
                                   (κ : is-compact 𝓓 d)
                                 → is-compact (𝓔 ⁻) e
                                 → is-compact (𝓓 ⟹ᵈᶜᵖᵒ (𝓔 ⁻)) ⦅ d ⇒ e ⦆[ κ ]
 single-step-function-is-compact d e κ e-is-compact I g δ e-below-∐g =
  ∥∥-functor lemma
             (e-is-compact I (pointwise-family 𝓓 (𝓔 ⁻) g d)
                           (pointwise-family-is-directed 𝓓 (𝓔 ⁻) g δ d) claim)
   where
    claim : e ⊑⟪ 𝓔 ⟫ ∐ (𝓔 ⁻) (pointwise-family-is-directed 𝓓 (𝓔 ⁻) g δ d)
    claim = lr-implication
             (below-single-step-function-criterion
               d e κ (∐ (𝓓 ⟹ᵈᶜᵖᵒ (𝓔 ⁻)) {I} {g} δ))
             e-below-∐g
    lemma : (Σ i ꞉ I , e ⊑⟪ 𝓔 ⟫ [ 𝓓 , 𝓔 ⁻ ]⟨ g i ⟩ d)
          → (Σ i ꞉ I , ⦅ d ⇒ e ⦆[ κ ] ⊑⟨ 𝓓 ⟹ᵈᶜᵖᵒ (𝓔 ⁻) ⟩ g i)
    lemma (i , u) = (i , v)
     where
      v : ⦅ d ⇒ e ⦆[ κ ] ⊑⟨ 𝓓 ⟹ᵈᶜᵖᵒ (𝓔 ⁻) ⟩ g i
      v = rl-implication
           (below-single-step-function-criterion d e κ (g i)) u

\end{code}

We now work towards constructing a small compact basis for the exponential
𝓓 ⟹ᵈᶜᵖᵒ (𝓔 ⁻). We start with a family of single step functions that we will
later directify by taking finite joins.

\begin{code}

 module single-step-functions-bases
         (Bᴰ Bᴱ : 𝓥 ̇ )
         (βᴰ : Bᴰ → ⟨ 𝓓 ⟩)
         (βᴱ : Bᴱ → ⟪ 𝓔 ⟫)
         (κᴰ : is-small-compact-basis 𝓓     βᴰ)
         (κᴱ : is-small-compact-basis (𝓔 ⁻) βᴱ)
        where

  single-step-functions : Bᴰ × Bᴱ → DCPO[ 𝓓 , 𝓔 ⁻ ]
  single-step-functions (d , e) = ⦅ βᴰ d ⇒ βᴱ e ⦆[ basis-is-compact d ]
   where
    open is-small-compact-basis κᴰ

  module single-step-functions-into-sup-complete-dcpo
          (𝓔-is-sup-complete : is-sup-complete (𝓔 ⁻))
         where

   module _
           (𝕗 : DCPO[ 𝓓 , 𝓔 ⁻ ])
          where

    private
     f : ⟨ 𝓓 ⟩ → ⟪ 𝓔 ⟫
     f = [ 𝓓 , 𝓔 ⁻ ]⟨ 𝕗 ⟩
     f-is-continuous : is-continuous 𝓓 (𝓔 ⁻) f
     f-is-continuous = continuity-of-function 𝓓 (𝓔 ⁻) 𝕗

    open is-sup-complete 𝓔-is-sup-complete

    single-step-functions-below-function :
       (Σ p ꞉ (Bᴰ × Bᴱ) , single-step-functions p ⊑⟨ 𝓓 ⟹ᵈᶜᵖᵒ (𝓔 ⁻) ⟩ 𝕗)
     → DCPO[ 𝓓 , 𝓔 ⁻ ]
    single-step-functions-below-function = single-step-functions ∘ pr₁

    single-step-functions-below-function-sup :
     is-sup (underlying-order (𝓓 ⟹ᵈᶜᵖᵒ (𝓔 ⁻))) 𝕗
            single-step-functions-below-function
    single-step-functions-below-function-sup = (ub , lb-of-ubs)
     where
      ub : is-upperbound (underlying-order (𝓓 ⟹ᵈᶜᵖᵒ (𝓔 ⁻))) 𝕗
            single-step-functions-below-function
      ub = pr₂
      lb-of-ubs :
       is-lowerbound-of-upperbounds (underlying-order (𝓓 ⟹ᵈᶜᵖᵒ (𝓔 ⁻))) 𝕗
        single-step-functions-below-function
      lb-of-ubs 𝕘@(g , _) g-is-ub x = fx-below-gx
       where
        module _ where
         open is-small-compact-basis κᴱ
         claim₁ : (d : Bᴰ) (e : Bᴱ) → e ⊑ᴮₛ f (βᴰ d) → βᴱ e ⊑⟪ 𝓔 ⟫ g (βᴰ d)
         claim₁ d e u =
          lr-implication (below-single-step-function-criterion (βᴰ d) (βᴱ e)
                           (is-small-compact-basis.basis-is-compact κᴰ d) 𝕘)
                           (g-is-ub ((d , e) , v))
           where
            v : single-step-functions (d , e) ⊑⟨ 𝓓 ⟹ᵈᶜᵖᵒ (𝓔 ⁻) ⟩ 𝕗
            v = rl-implication
                 (below-single-step-function-criterion (βᴰ d) (βᴱ e)
                   (is-small-compact-basis.basis-is-compact κᴰ d) 𝕗)
                 (⊑ᴮₛ-to-⊑ᴮ u)
         claim₂ : (d : Bᴰ) → f (βᴰ d) ⊑⟪ 𝓔 ⟫ g (βᴰ d)
         claim₂ d = f (βᴰ d)                             ⊑⟪ 𝓔 ⟫[ ⦅1⦆ ]
                    ∐ (𝓔 ⁻) (↓ᴮₛ-is-directed (f (βᴰ d))) ⊑⟪ 𝓔 ⟫[ ⦅2⦆ ]
                    g (βᴰ d)                             ∎⟪ 𝓔 ⟫
          where
           ⦅1⦆ = ↓ᴮₛ-∐-⊒ (f (βᴰ d))
           ⦅2⦆ = ∐-is-lowerbound-of-upperbounds (𝓔 ⁻) (↓ᴮₛ-is-directed (f (βᴰ d)))
                  (g (βᴰ d)) (λ (e , v) → claim₁ d e v)

        open is-small-compact-basis κᴰ
        δ : is-Directed 𝓓 (↓-inclusionₛ x)
        δ = ↓ᴮₛ-is-directed x
        ε : is-Directed (𝓔 ⁻) (f ∘ ↓-inclusionₛ x)
        ε = image-is-directed' 𝓓 (𝓔 ⁻) 𝕗 δ

        fx-below-gx : f x ⊑⟪ 𝓔 ⟫ g x
        fx-below-gx = f x       ⊑⟪ 𝓔 ⟫[ ⦅1⦆ ]
                      f (∐ 𝓓 δ) ⊑⟪ 𝓔 ⟫[ ⦅2⦆ ]
                      ∐ (𝓔 ⁻) ε ⊑⟪ 𝓔 ⟫[ ⦅3⦆ ]
                      g x       ∎⟪ 𝓔 ⟫
         where
          ⦅1⦆ = ＝-to-⊒ (𝓔 ⁻) (ap f (↓ᴮₛ-∐-＝ x))
          ⦅2⦆ = continuous-∐-⊑ 𝓓 (𝓔 ⁻) 𝕗 δ
          ⦅3⦆ = ∐-is-lowerbound-of-upperbounds (𝓔 ⁻) ε (g x) γ
           where
            γ : is-upperbound (underlying-order (𝓔 ⁻)) (g x) (f ∘ ↓-inclusionₛ x)
            γ (d , u) = f (βᴰ d) ⊑⟪ 𝓔 ⟫[ claim₂ d ]
                        g (βᴰ d) ⊑⟪ 𝓔 ⟫[ v        ]
                        g x      ∎⟪ 𝓔 ⟫
             where
              v = monotone-if-continuous 𝓓 (𝓔 ⁻) 𝕘 (βᴰ d) x (⊑ᴮₛ-to-⊑ᴮ u)

\end{code}

Now we are in position to show that the exponential has a small compact basis.

\begin{code}

module _
        (𝓓 : DCPO {𝓤} {𝓣})
        (𝓔 : DCPO⊥ {𝓤'} {𝓣'})
        (𝓔-is-sup-complete : is-sup-complete (𝓔 ⁻))
        (Bᴰ Bᴱ : 𝓥 ̇ )
        (βᴰ : Bᴰ → ⟨ 𝓓 ⟩)
        (βᴱ : Bᴱ → ⟪ 𝓔 ⟫)
        (κᴰ : is-small-compact-basis 𝓓     βᴰ)
        (κᴱ : is-small-compact-basis (𝓔 ⁻) βᴱ)
       where

 private
  exp-is-sup-complete : is-sup-complete (𝓓 ⟹ᵈᶜᵖᵒ (𝓔 ⁻))
  exp-is-sup-complete = exponential-is-sup-complete 𝓓 (𝓔 ⁻) 𝓔-is-sup-complete

 open sup-complete-dcpo (𝓓 ⟹ᵈᶜᵖᵒ (𝓔 ⁻)) exp-is-sup-complete
 open single-step-function-def 𝓓 𝓔 (locally-small-if-small-compact-basis 𝓓 βᴰ κᴰ)
 open single-step-functions-bases Bᴰ Bᴱ βᴰ βᴱ κᴰ κᴱ

 private
  B : 𝓥 ̇
  B = domain (directify single-step-functions)
  β : B → DCPO[ 𝓓 , 𝓔 ⁻ ]
  β = directify single-step-functions

 exponential-has-small-compact-basis : Prop-Ext
                                     → is-small-compact-basis (𝓓 ⟹ᵈᶜᵖᵒ (𝓔 ⁻)) β
 exponential-has-small-compact-basis pe =
  record
   { basis-is-compact = ⦅1⦆
   ; ⊑ᴮ-is-small      = ⦅2⦆
   ; ↓ᴮ-is-directed   = ⦅3⦆
   ; ↓ᴮ-is-sup        = ⦅4⦆
   }
   where
    ⦅1⦆ : (b : B) → is-compact (𝓓 ⟹ᵈᶜᵖᵒ (𝓔 ⁻)) (β b)
    ⦅1⦆ = directify-is-compact single-step-functions
          (λ (d , e) → single-step-function-is-compact (βᴰ d) (βᴱ e)
                        (is-small-compact-basis.basis-is-compact κᴰ d)
                        (is-small-compact-basis.basis-is-compact κᴱ e))
    ⦅2⦆ : (f : ⟨ 𝓓 ⟹ᵈᶜᵖᵒ (𝓔 ⁻) ⟩) (b : B)
        → is-small (β b ⊑⟨ 𝓓 ⟹ᵈᶜᵖᵒ (𝓔 ⁻) ⟩ f)
    ⦅2⦆ f b = ⌜ local-smallness-equivalent-definitions (𝓓 ⟹ᵈᶜᵖᵒ (𝓔 ⁻)) ⌝
               exp-is-locally-small (β b) f
     where
      exp-is-locally-small : is-locally-small (𝓓 ⟹ᵈᶜᵖᵒ (𝓔 ⁻))
      exp-is-locally-small =
       locally-small-exponential-criterion pe 𝓓 (𝓔 ⁻)
        ∣ Bᴰ , βᴰ , compact-basis-is-basis 𝓓 βᴰ κᴰ ∣
        (locally-small-if-small-compact-basis (𝓔 ⁻) βᴱ κᴱ)
    ⦅3⦆ : (f : ⟨ 𝓓 ⟹ᵈᶜᵖᵒ (𝓔 ⁻) ⟩)
        → is-Directed (𝓓 ⟹ᵈᶜᵖᵒ (𝓔 ⁻)) (↓-inclusion (𝓓 ⟹ᵈᶜᵖᵒ (𝓔 ⁻)) β f)
    ⦅3⦆ f = directify-↓-is-directed single-step-functions {f}
    ⦅4⦆ : (f : ⟨ 𝓓 ⟹ᵈᶜᵖᵒ (𝓔 ⁻) ⟩)
        → is-sup (underlying-order (𝓓 ⟹ᵈᶜᵖᵒ (𝓔 ⁻))) f
           (↓-inclusion (𝓓 ⟹ᵈᶜᵖᵒ (𝓔 ⁻)) β f)
    ⦅4⦆ (f , f-is-cts) =
     directify-↓-sup single-step-functions {f , f-is-cts}
      (single-step-functions-below-function-sup (f , f-is-cts))
        where
         open single-step-functions-into-sup-complete-dcpo 𝓔-is-sup-complete

 exponential-has-specified-small-compact-basis : Prop-Ext
  → has-specified-small-compact-basis (𝓓 ⟹ᵈᶜᵖᵒ (𝓔 ⁻))
 exponential-has-specified-small-compact-basis pe =
  (B , β , exponential-has-small-compact-basis pe)

 exponential-is-structurally-algebraic : Prop-Ext
                                       → structurally-algebraic (𝓓 ⟹ᵈᶜᵖᵒ (𝓔 ⁻))
 exponential-is-structurally-algebraic pe =
  structurally-algebraic-if-specified-small-compact-basis (𝓓 ⟹ᵈᶜᵖᵒ (𝓔 ⁻))
   (exponential-has-specified-small-compact-basis pe)

 exponential-is-algebraic : Prop-Ext → is-algebraic-dcpo (𝓓 ⟹ᵈᶜᵖᵒ (𝓔 ⁻))
 exponential-is-algebraic pe = ∣ exponential-is-structurally-algebraic pe ∣

\end{code}

The fact that sup-complete (algebraic) dcpos with small compact bases are closed
under exponentials can be used to show that the same holds for sup-complete
(continuous) dcpos with small bases.

The proof outline, which Martín Escardó explained to me, is as follows:

Start with dcpos 𝓓 and 𝓔 with small bases βᴰ : Bᴰ → 𝓓 and βᴱ : Bᴱ → 𝓔. Then
𝓓 and 𝓔 are continuous retracts of dcpos 𝓓' and 𝓔' respectively both with small
compact bases, using the ideal completions of the bases.

Moreover, these retracts induce a continuous retract of the exponentials:
(𝓓 ⟹ᵈᶜᵖᵒ 𝓔) is a continuous retract of (𝓓' ⟹ᵈᶜᵖᵒ 𝓔')
and the latter is algebraic with a small compact basis by the above. Finally, we
can use the continuous retract to give a small basis on (𝓓 ⟹ᵈᶜᵖᵒ 𝓔).

NB: The above proof outline depends on the fact that 𝓔' and (hence)
(𝓓' ⟹ᵈᶜᵖᵒ 𝓔') are sup-complete. This can be shown by using the concrete
definition of 𝓔' as the ideal completion of βᴱ and by ensuring that the basis βᴱ
is closed under finite joins to begin with.
This was formalized on 27 June 2024. Prior to this, the sup-completeness of 𝓔'
was an assumption to an anonymous module.

\begin{code}

module _
        (pe : Prop-Ext)
        (𝓓 : DCPO {𝓤} {𝓣})
        (𝓔 : DCPO {𝓤'} {𝓣'})
        {Bᴰ Bᴱₚᵣₑ : 𝓥 ̇ }
        (βᴰ : Bᴰ → ⟨ 𝓓 ⟩)
        (βᴱₚᵣₑ : Bᴱₚᵣₑ → ⟨ 𝓔 ⟩)
        (βᴰ-is-small-basis : is-small-basis 𝓓 βᴰ)
        (βᴱₚᵣₑ-is-small-basis : is-small-basis 𝓔 βᴱₚᵣₑ)
        (𝓔-is-sup-complete : is-sup-complete 𝓔)
       where

 open import DomainTheory.IdealCompletion.Retracts pt fe pe 𝓥

\end{code}

As a first step, we construct a new basis of 𝓔 which is guaranteed to have
finite joins.

\begin{code}

 private
  𝓔-has-finite-joins : has-finite-joins 𝓔
  𝓔-has-finite-joins = sup-complete-dcpo-has-finite-joins 𝓔 𝓔-is-sup-complete

  refined-basis : Σ B ꞉ 𝓥 ̇ , Σ β ꞉ (B → ⟨ 𝓔 ⟩) ,
                  Σ p ꞉ is-small-basis 𝓔 β ,
                  basis-has-finite-joins 𝓔 β p 𝓔-has-finite-joins
  refined-basis = refine-basis-to-have-finite-joins 𝓔 βᴱₚᵣₑ
                                                    βᴱₚᵣₑ-is-small-basis
                                                    𝓔-has-finite-joins

  Bᴱ : 𝓥 ̇
  Bᴱ = pr₁ refined-basis
  βᴱ : Bᴱ → ⟨ 𝓔 ⟩
  βᴱ = pr₁ (pr₂ refined-basis)
  βᴱ-is-small-basis : is-small-basis 𝓔 βᴱ
  βᴱ-is-small-basis = pr₁ (pr₂ (pr₂ refined-basis))
  βᴱ-has-finite-joins : basis-has-finite-joins 𝓔 βᴱ βᴱ-is-small-basis
                                                    𝓔-has-finite-joins
  βᴱ-has-finite-joins = pr₂ (pr₂ (pr₂ (refined-basis)))

\end{code}

We now proceed with the proof as outlined above.

\begin{code}

  module _ where
   open Idl-continuous-retract-of-algebraic 𝓓 βᴰ βᴰ-is-small-basis
   𝓓' : DCPO {𝓥 ⁺} {𝓥}
   𝓓' = Idl-DCPO
   𝓓-continuous-retract-of-𝓓' : 𝓓 continuous-retract-of 𝓓'
   𝓓-continuous-retract-of-𝓓' = Idl-continuous-retract
  module _ where
   open Idl-continuous-retract-of-algebraic 𝓔 βᴱ βᴱ-is-small-basis
   𝓔' : DCPO {𝓥 ⁺} {𝓥}
   𝓔' = Idl-DCPO
   𝓔-continuous-retract-of-𝓔' : 𝓔 continuous-retract-of 𝓔'
   𝓔-continuous-retract-of-𝓔' = Idl-continuous-retract
   𝓔'-is-sup-complete : is-sup-complete 𝓔'
   𝓔'-is-sup-complete =
    Idl-is-sup-complete-if-basis-has-finite-joins 𝓔-is-sup-complete
                                                  βᴱ-has-finite-joins

  exp-continuous-retract : (𝓓 ⟹ᵈᶜᵖᵒ 𝓔) continuous-retract-of (𝓓' ⟹ᵈᶜᵖᵒ 𝓔')
  exp-continuous-retract =
   record
    { s               = s
    ; r               = r
    ; s-section-of-r  = s-section-of-r
    ; s-is-continuous = s-is-cts
    ; r-is-continuous = r-is-cts
    }
    where
     module _ where
      open _continuous-retract-of_ 𝓓-continuous-retract-of-𝓓'
      sᴰ = s
      rᴰ = r
      sᴰ-is-cts = s-is-continuous
      rᴰ-is-cts = r-is-continuous
      rᴰ-sᴰ-equation = s-section-of-r
     module _ where
      open _continuous-retract-of_ 𝓔-continuous-retract-of-𝓔'
      sᴱ = s
      rᴱ = r
      sᴱ-is-cts = s-is-continuous
      rᴱ-is-cts = r-is-continuous
      rᴱ-sᴱ-equation = s-section-of-r
     s : ⟨ 𝓓 ⟹ᵈᶜᵖᵒ 𝓔 ⟩ → ⟨ 𝓓' ⟹ᵈᶜᵖᵒ 𝓔' ⟩
     s f = DCPO-∘₃ 𝓓' 𝓓 𝓔 𝓔' (rᴰ , rᴰ-is-cts) f (sᴱ , sᴱ-is-cts)
     r : ⟨ 𝓓' ⟹ᵈᶜᵖᵒ 𝓔' ⟩ → ⟨ 𝓓 ⟹ᵈᶜᵖᵒ 𝓔 ⟩
     r g = DCPO-∘₃ 𝓓 𝓓' 𝓔' 𝓔 (sᴰ , sᴰ-is-cts) g (rᴱ , rᴱ-is-cts)
     s-section-of-r : r ∘ s ∼ id
     s-section-of-r (f , _) = to-continuous-function-＝ 𝓓 𝓔 γ
      where
       γ : rᴱ ∘ sᴱ ∘ f ∘ rᴰ ∘ sᴰ ∼ f
       γ x = (rᴱ ∘ sᴱ ∘ f ∘ rᴰ ∘ sᴰ) x ＝⟨ rᴱ-sᴱ-equation ((f ∘ rᴰ ∘ sᴰ) x) ⟩
             (f ∘ rᴰ ∘ sᴰ) x           ＝⟨ ap f (rᴰ-sᴰ-equation x) ⟩
             f x                       ∎
     s-is-cts : is-continuous (𝓓 ⟹ᵈᶜᵖᵒ 𝓔) (𝓓' ⟹ᵈᶜᵖᵒ 𝓔') s
     s-is-cts = DCPO-∘₃-is-continuous₂ 𝓓' 𝓓 𝓔 𝓔'
                 (rᴰ , rᴰ-is-cts) (sᴱ , sᴱ-is-cts)
     r-is-cts : is-continuous (𝓓' ⟹ᵈᶜᵖᵒ 𝓔') (𝓓 ⟹ᵈᶜᵖᵒ 𝓔) r
     r-is-cts = DCPO-∘₃-is-continuous₂ 𝓓 𝓓' 𝓔' 𝓔
                 (sᴰ , sᴰ-is-cts) (rᴱ , rᴱ-is-cts)

  open sup-complete-dcpo 𝓔' 𝓔'-is-sup-complete
  open has-finite-joins (sup-complete-dcpo-has-finite-joins 𝓔' 𝓔'-is-sup-complete)

  exp-has-small-compact-basis : has-specified-small-compact-basis (𝓓' ⟹ᵈᶜᵖᵒ 𝓔')
  exp-has-small-compact-basis =
   exponential-has-specified-small-compact-basis
    𝓓' (𝓔' , ⊥ , ⊥-is-least)
    𝓔'-is-sup-complete
    Bᴰ' Bᴱ' βᴰ' βᴱ' κᴰ' κᴱ' pe
     where
      module _ where
       open Idl-continuous-retract-of-algebraic 𝓓 βᴰ βᴰ-is-small-basis
       small-compact-basisᴰ' : has-specified-small-compact-basis 𝓓'
       small-compact-basisᴰ' = Idl-has-specified-small-compact-basis
                                (λ _ → ⊑ᴮ-is-reflexive)
       Bᴰ' : 𝓥 ̇
       Bᴰ' = pr₁ small-compact-basisᴰ'
       βᴰ' : Bᴰ' → ⟨ 𝓓' ⟩
       βᴰ' = pr₁ (pr₂ small-compact-basisᴰ')
       κᴰ' : is-small-compact-basis 𝓓' βᴰ'
       κᴰ' = pr₂ (pr₂ small-compact-basisᴰ')
      module _ where
       open Idl-continuous-retract-of-algebraic 𝓔 βᴱ βᴱ-is-small-basis
       small-compact-basisᴱ' : has-specified-small-compact-basis 𝓔'
       small-compact-basisᴱ' = Idl-has-specified-small-compact-basis
                                (λ _ → ⊑ᴮ-is-reflexive)
       Bᴱ' : 𝓥 ̇
       Bᴱ' = pr₁ small-compact-basisᴱ'
       βᴱ' : Bᴱ' → ⟨ 𝓔' ⟩
       βᴱ' = pr₁ (pr₂ small-compact-basisᴱ')
       κᴱ' : is-small-compact-basis 𝓔' βᴱ'
       κᴱ' = pr₂ (pr₂ small-compact-basisᴱ')

 exponential-has-specified-small-basis : has-specified-small-basis (𝓓 ⟹ᵈᶜᵖᵒ 𝓔)
 exponential-has-specified-small-basis = B , r ∘ β ,
  small-basis-from-continuous-retract pe (𝓓 ⟹ᵈᶜᵖᵒ 𝓔) (𝓓' ⟹ᵈᶜᵖᵒ 𝓔')
   exp-continuous-retract β (compact-basis-is-basis (𝓓' ⟹ᵈᶜᵖᵒ 𝓔') β κ)
    where
     open _continuous-retract-of_ exp-continuous-retract
     exp-small-compact-basis : has-specified-small-compact-basis (𝓓' ⟹ᵈᶜᵖᵒ 𝓔')
     exp-small-compact-basis = exp-has-small-compact-basis
     B : 𝓥 ̇
     B = pr₁ exp-has-small-compact-basis
     β : B → DCPO[ 𝓓' , 𝓔' ]
     β = pr₁ (pr₂ exp-has-small-compact-basis)
     κ : is-small-compact-basis (𝓓' ⟹ᵈᶜᵖᵒ 𝓔') β
     κ = pr₂ (pr₂ exp-has-small-compact-basis)

\end{code}