Tom de Jong, May 2019.
Major additions January 2020.
Added sup-complete exponentials somewhere in February - March 2022.

We construct the exponential (pointed) dcpos (𝓓 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔) and (𝓓 βŸΉα΅ˆαΆœα΅–α΅’βŠ₯ 𝓔) for
(pointed) dcpos 𝓓 and 𝓔. We also show that if 𝓔 is sup-complete, then the
exponential (𝓓 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔) is also sup-complete (even if 𝓓 isn't). This comes in
useful when proving that exponentials of sup-complete dcpos are algebraic.

\begin{code}

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

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

module DomainTheory.Basics.Exponential
        (pt : propositional-truncations-exist)
        (fe : Fun-Ext)
        (π“₯ : Universe)
       where

open PropositionalTruncation pt

open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.Sets
open import UF.Sets-Properties

open import DomainTheory.Basics.Dcpo pt fe π“₯
open import DomainTheory.Basics.Miscelanea pt fe π“₯
open import DomainTheory.Basics.Pointed pt fe π“₯
open import DomainTheory.Basics.SupComplete pt fe π“₯

open import OrderedTypes.Poset fe

module _ (𝓓 : DCPO {𝓀} {𝓣})
         (𝓔 : DCPO {𝓀'} {𝓣'})
       where

 _hom-βŠ‘_ : DCPO[ 𝓓 , 𝓔 ] β†’ DCPO[ 𝓓 , 𝓔 ] β†’ 𝓀 βŠ” 𝓣' Μ‡
 (f , _) hom-βŠ‘ (g , _) = βˆ€ d β†’ f d βŠ‘βŸ¨ 𝓔 ⟩ g d

 pointwise-family : {I : π“₯ Μ‡ } (Ξ± : I β†’ DCPO[ 𝓓 , 𝓔 ]) β†’ ⟨ 𝓓 ⟩ β†’ I β†’ ⟨ 𝓔 ⟩
 pointwise-family Ξ± d i = underlying-function 𝓓 𝓔 (Ξ± i) d

 pointwise-family-is-directed : {I : π“₯ Μ‡ } (Ξ± : I β†’ DCPO[ 𝓓 , 𝓔 ])
                                (Ξ΄ : is-directed _hom-βŠ‘_ Ξ±)
                                (d : ⟨ 𝓓 ⟩)
                              β†’ is-directed (underlying-order 𝓔)
                                 (pointwise-family Ξ± d)
 pointwise-family-is-directed {I} Ξ± Ξ΄ d = a , b
  where
   a : βˆ₯ I βˆ₯
   a = inhabited-if-directed _hom-βŠ‘_ Ξ± Ξ΄
   b : is-semidirected (underlying-order 𝓔) (pointwise-family Ξ± d)
   b i j = do
    (k , l , m) ← semidirected-if-directed _hom-βŠ‘_ Ξ± Ξ΄ i j
    ∣ k , l d , m d ∣

 continuous-functions-sup : {I : π“₯ Μ‡ } (Ξ± : I β†’ DCPO[ 𝓓 , 𝓔 ])
                          β†’ is-directed _hom-βŠ‘_ Ξ± β†’ DCPO[ 𝓓 , 𝓔 ]
 continuous-functions-sup {I} Ξ± Ξ΄ = f , c
  where
   Ξ΅ : (d : ⟨ 𝓓 ⟩) β†’ is-directed (underlying-order 𝓔) (pointwise-family Ξ± d)
   Ξ΅ = pointwise-family-is-directed Ξ± Ξ΄
   f : ⟨ 𝓓 ⟩ β†’ ⟨ 𝓔 ⟩
   f d = ∐ 𝓔 (Ξ΅ d)
   c : is-continuous 𝓓 𝓔 f
   c J Ξ² Ο† = ub , lb-of-ubs
    where
     ub : (j : J) β†’ f (Ξ² j) βŠ‘βŸ¨ 𝓔 ⟩ f (∐ 𝓓 Ο†)
     ub j = f (Ξ² j)         βŠ‘βŸ¨ 𝓔 ⟩[ reflexivity 𝓔 (f (Ξ² j)) ]
            ∐ 𝓔 (Ξ΅ (Ξ² j))   βŠ‘βŸ¨ 𝓔 ⟩[ ∐-is-monotone 𝓔 (Ξ΅ (Ξ² j)) (Ξ΅ (∐ 𝓓 Ο†)) h ]
            ∐ 𝓔 (Ξ΅ (∐ 𝓓 Ο†)) βŠ‘βŸ¨ 𝓔 ⟩[ reflexivity 𝓔 (f (∐ 𝓓 Ο†)) ]
            f (∐ 𝓓 Ο†)       ∎⟨ 𝓔 ⟩
      where
       h : (i : I) β†’ [ 𝓓 , 𝓔 ]⟨ Ξ± i ⟩ (Ξ² j) βŠ‘βŸ¨ 𝓔 ⟩ [ 𝓓 , 𝓔 ]⟨ Ξ± i ⟩ (∐ 𝓓 Ο†)
       h i = monotone-if-continuous 𝓓 𝓔 (Ξ± i) (Ξ² j) (∐ 𝓓 Ο†)
              (∐-is-upperbound 𝓓 Ο† j)
     lb-of-ubs : is-lowerbound-of-upperbounds (underlying-order 𝓔) (f (∐ 𝓓 Ο†))
                  (f ∘ β)
     lb-of-ubs e l = f (∐ 𝓓 Ο†)       βŠ‘βŸ¨ 𝓔 ⟩[ reflexivity 𝓔 (f (∐ 𝓓 Ο†)) ]
                     ∐ 𝓔 (Ξ΅ (∐ 𝓓 Ο†)) βŠ‘βŸ¨ 𝓔 ⟩[ u ]
                     e               ∎⟨ 𝓔 ⟩
      where
       u = ∐-is-lowerbound-of-upperbounds 𝓔 (Ξ΅ (∐ 𝓓 Ο†)) e v
        where
         v : (i : I) β†’ [ 𝓓 , 𝓔 ]⟨ Ξ± i ⟩ (∐ 𝓓 Ο†) βŠ‘βŸ¨ 𝓔 ⟩ e
         v i = [ 𝓓 , 𝓔 ]⟨ Ξ± i ⟩ (∐ 𝓓 Ο†)             βŠ‘βŸ¨ 𝓔 ⟩[ l₁ ]
               ∐ 𝓔 (image-is-directed' 𝓓 𝓔 (Ξ± i) Ο†) βŠ‘βŸ¨ 𝓔 ⟩[ lβ‚‚ ]
               e                                    ∎⟨ 𝓔 ⟩
          where
           l₁ = continuous-∐-βŠ‘ 𝓓 𝓔 (Ξ± i) Ο†
           lβ‚‚ = ∐-is-lowerbound-of-upperbounds 𝓔
                 (image-is-directed' 𝓓 𝓔 (Ξ± i) Ο†) e w
            where
             w : (j : J) β†’ [ 𝓓 , 𝓔 ]⟨ Ξ± i ⟩ (Ξ² j) βŠ‘βŸ¨ 𝓔 ⟩ e
             w j = [ 𝓓 , 𝓔 ]⟨ Ξ± i ⟩ (Ξ² j) βŠ‘βŸ¨ 𝓔 ⟩[ ∐-is-upperbound 𝓔 (Ξ΅ (Ξ² j)) i ]
                   ∐ 𝓔 (Ξ΅ (Ξ² j))          βŠ‘βŸ¨ 𝓔 ⟩[ reflexivity 𝓔 (f (Ξ² j)) ]
                   f (Ξ² j)                βŠ‘βŸ¨ 𝓔 ⟩[ l j ]
                   e                      ∎⟨ 𝓔 ⟩

infixr 20 _βŸΉα΅ˆαΆœα΅–α΅’_

_βŸΉα΅ˆαΆœα΅–α΅’_ : DCPO {𝓀} {𝓣} β†’ DCPO {𝓀'} {𝓣'}
        β†’ DCPO {(π“₯ ⁺) βŠ” 𝓀 βŠ” 𝓣 βŠ” 𝓀' βŠ” 𝓣'} {𝓀 βŠ” 𝓣'}
𝓓 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔 = DCPO[ 𝓓 , 𝓔 ] , _βŠ‘_ , pa , dc
 where
  _βŠ‘_ = 𝓓 hom-βŠ‘ 𝓔
  pa : PosetAxioms.poset-axioms _βŠ‘_
  pa = s , p , r , t , a
   where
    open PosetAxioms _βŠ‘_
    s : is-set DCPO[ 𝓓 , 𝓔 ]
    s = subsets-of-sets-are-sets (⟨ 𝓓 ⟩ β†’ ⟨ 𝓔 ⟩) (is-continuous 𝓓 𝓔)
         (Ξ -is-set fe (Ξ» x β†’ sethood 𝓔))
         (Ξ» {f} β†’ being-continuous-is-prop 𝓓 𝓔 f)
    p : (f g : DCPO[ 𝓓 , 𝓔 ]) β†’ is-prop (f βŠ‘ g)
    p (f , _) (g , _) = Ξ -is-prop fe (Ξ» x β†’ prop-valuedness 𝓔 (f x) (g x))
    r : (f : DCPO[ 𝓓 , 𝓔 ]) β†’ f βŠ‘ f
    r (f , _) x = reflexivity 𝓔 (f x)
    t : (f g h : DCPO[ 𝓓 , 𝓔 ]) β†’ f βŠ‘ g β†’ g βŠ‘ h β†’ f βŠ‘ h
    t (f , _) (g , _) (h , _) l m x = transitivity 𝓔 (f x) (g x) (h x)
                                      (l x) (m x)
    a : (f g : DCPO[ 𝓓 , 𝓔 ]) β†’ f βŠ‘ g β†’ g βŠ‘ f β†’ f ＝ g
    a f g l m = to-continuous-function-＝ 𝓓 𝓔
                 (Ξ» x β†’ antisymmetry 𝓔 ([ 𝓓 , 𝓔 ]⟨ f ⟩ x) ([ 𝓓 , 𝓔 ]⟨ g ⟩ x)
                  (l x) (m x))
  dc : is-directed-complete _βŠ‘_
  dc I Ξ± Ξ΄ = (continuous-functions-sup 𝓓 𝓔 Ξ± Ξ΄) , u , v
   where
    u : (i : I) β†’ Ξ± i βŠ‘ continuous-functions-sup 𝓓 𝓔 Ξ± Ξ΄
    u i d = ∐-is-upperbound 𝓔 (pointwise-family-is-directed 𝓓 𝓔 Ξ± Ξ΄ d) i
    v : (g : DCPO[ 𝓓 , 𝓔 ])
      β†’ ((i : I) β†’ Ξ± i βŠ‘ g)
      β†’ continuous-functions-sup 𝓓 𝓔 Ξ± Ξ΄ βŠ‘ g
    v (g , _) l d = ∐-is-lowerbound-of-upperbounds 𝓔
                     (pointwise-family-is-directed 𝓓 𝓔 Ξ± Ξ΄ d)
                     (g d) (Ξ» (i : I) β†’ l i d)


infixr 20 _βŸΉα΅ˆαΆœα΅–α΅’βŠ₯_

_βŸΉα΅ˆαΆœα΅–α΅’βŠ₯_ : DCPOβŠ₯ {𝓀} {𝓣} β†’ DCPOβŠ₯ {𝓀'} {𝓣'}
         β†’ DCPOβŠ₯ {(π“₯ ⁺) βŠ” 𝓀 βŠ” 𝓣 βŠ” 𝓀' βŠ” 𝓣'} {𝓀 βŠ” 𝓣'}
𝓓 βŸΉα΅ˆαΆœα΅–α΅’βŠ₯ 𝓔 = (𝓓 ⁻) βŸΉα΅ˆαΆœα΅–α΅’ (𝓔 ⁻) , h
 where
  h : has-least (underlying-order ((𝓓 ⁻) βŸΉα΅ˆαΆœα΅–α΅’ (𝓔 ⁻)))
  h = ((Ξ» _ β†’ βŠ₯ 𝓔) ,
      constant-functions-are-continuous (𝓓 ⁻) (𝓔 ⁻)) ,
      (Ξ» g d β†’ βŠ₯-is-least 𝓔 (underlying-function (𝓓 ⁻) (𝓔 ⁻) g d))

_βŸΉα΅ˆαΆœα΅–α΅’βŠ₯'_ : DCPO {𝓀} {𝓣} β†’ DCPOβŠ₯ {𝓀'} {𝓣'}
          β†’ DCPOβŠ₯ {(π“₯ ⁺) βŠ” 𝓀 βŠ” 𝓣 βŠ” 𝓀' βŠ” 𝓣'} {𝓀 βŠ” 𝓣'}
𝓓 βŸΉα΅ˆαΆœα΅–α΅’βŠ₯' 𝓔 = 𝓓 βŸΉα΅ˆαΆœα΅–α΅’ (𝓔 ⁻) , h
 where
  h : has-least (underlying-order (𝓓 βŸΉα΅ˆαΆœα΅–α΅’ (𝓔 ⁻)))
  h = ((Ξ» _ β†’ βŠ₯ 𝓔) ,
      constant-functions-are-continuous 𝓓 (𝓔 ⁻)) ,
      (Ξ» g d β†’ βŠ₯-is-least 𝓔 (underlying-function 𝓓 (𝓔 ⁻) g d))

\end{code}

Now that we have constructed exponentials, we can state and prove additional
continuity results regarding composition of continuous functions.

(These results are used in constructing Scott's D∞ in
DomainTheory.Bilimits.Dinfinity.lagda.)

\begin{code}

DCPO-∘-is-monotone₁ : (𝓓 : DCPO {𝓀} {𝓣})
                      (𝓔 : DCPO {𝓀'} {𝓣'})
                      (𝓔' : DCPO {𝓦} {𝓦'})
                      (f : DCPO[ 𝓓 , 𝓔 ])
                    β†’ is-monotone (𝓔 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔') (𝓓 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔') (DCPO-∘ 𝓓 𝓔 𝓔' f)
DCPO-∘-is-monotone₁ 𝓓 𝓔 𝓔' (f , cf) g h l x = l (f x)

DCPO-∘-is-monotoneβ‚‚ : (𝓓 : DCPO {𝓀} {𝓣})
                      (𝓔 : DCPO {𝓀'} {𝓣'})
                      (𝓔' : DCPO {𝓦} {𝓦'})
                      (g : DCPO[ 𝓔 , 𝓔' ])
                    β†’ is-monotone (𝓓 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔) (𝓓 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔')
                       (Ξ» f β†’ DCPO-∘ 𝓓 𝓔 𝓔' f g)
DCPO-∘-is-monotoneβ‚‚ 𝓓 𝓔 𝓔' g (f , cf) (h , ch) l x =
 monotone-if-continuous 𝓔 𝓔' g (f x) (h x) (l x)

DCPO-∘-is-continuous₁ : (𝓓 : DCPO {𝓀} {𝓣})
                        (𝓔 : DCPO {𝓀'} {𝓣'})
                        (𝓔' : DCPO {𝓦} {𝓦'})
                        (f : DCPO[ 𝓓 , 𝓔 ])
                      β†’ is-continuous (𝓔 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔') (𝓓 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔') (DCPO-∘ 𝓓 𝓔 𝓔' f)
DCPO-∘-is-continuous₁ 𝓓 𝓔 𝓔' f I Ξ± Ξ΄ =
 transport (Ξ» - β†’ is-sup (underlying-order (𝓓 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔')) - (DCPO-∘ 𝓓 𝓔 𝓔' f ∘ Ξ±))
  (Ξ³ ⁻¹) (∐-is-sup (𝓓 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔') {I} {Ξ²} Ξ΅)
  where
     Ξ² : I β†’ ⟨ 𝓓 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔' ⟩
     Ξ² i = DCPO-∘ 𝓓 𝓔 𝓔' f (Ξ± i)
     Ξ΅ : is-Directed (𝓓 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔') Ξ²
     Ξ΅ = image-is-directed (𝓔 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔') (𝓓 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔') {DCPO-∘ 𝓓 𝓔 𝓔' f}
          (DCPO-∘-is-monotone₁ 𝓓 𝓔 𝓔' f) {I} {Ξ±} Ξ΄
     Ξ³ : DCPO-∘ 𝓓 𝓔 𝓔' f (∐ (𝓔 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔') {I} {Ξ±} Ξ΄) ＝ ∐ (𝓓 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔') {I} {Ξ²} Ξ΅
     Ξ³ = to-continuous-function-＝ 𝓓 𝓔' ψ
      where
       ψ : (x : ⟨ 𝓓 ⟩)
         β†’ [ 𝓔 , 𝓔' ]⟨ (∐ (𝓔 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔') {I} {Ξ±} Ξ΄) ⟩ ([ 𝓓 , 𝓔 ]⟨ f ⟩ x)
         ＝ ∐ 𝓔' (pointwise-family-is-directed 𝓓 𝓔' Ξ² Ξ΅ x)
       ψ x = [ 𝓔 , 𝓔' ]⟨ (∐ (𝓔 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔') {I} {Ξ±} Ξ΄) ⟩ ([ 𝓓 , 𝓔 ]⟨ f ⟩ x) ＝⟨ e₁ ⟩
             ∐ 𝓔' Ξ΅'                                                     ＝⟨ eβ‚‚ ⟩
             ∐ 𝓔' (pointwise-family-is-directed 𝓓 𝓔' Ξ² Ξ΅ x) ∎
        where
         Ξ΅' : is-Directed 𝓔' (pointwise-family 𝓔 𝓔' Ξ± ([ 𝓓 , 𝓔 ]⟨ f ⟩ x))
         Ξ΅' = pointwise-family-is-directed 𝓔 𝓔' Ξ± Ξ΄ ([ 𝓓 , 𝓔 ]⟨ f ⟩ x)
         e₁ = refl
         eβ‚‚ = ∐-independent-of-directedness-witness 𝓔' Ξ΅'
               (pointwise-family-is-directed 𝓓 𝓔' Ξ² Ξ΅ x)

DCPO-∘-is-continuousβ‚‚ : (𝓓 : DCPO {𝓀} {𝓣})
                        (𝓔 : DCPO {𝓀'} {𝓣'})
                        (𝓔' : DCPO {𝓦} {𝓦'})
                        (g : DCPO[ 𝓔 , 𝓔' ])
                      β†’ is-continuous (𝓓 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔) (𝓓 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔')
                         (Ξ» f β†’ DCPO-∘ 𝓓 𝓔 𝓔' f g)
DCPO-∘-is-continuousβ‚‚ 𝓓 𝓔 𝓔' g I Ξ± Ξ΄ =
 transport
  (Ξ» - β†’ is-sup (underlying-order (𝓓 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔')) - ((Ξ» f β†’ DCPO-∘ 𝓓 𝓔 𝓔' f g) ∘ Ξ±))
  (Ξ³ ⁻¹) (∐-is-sup (𝓓 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔') {I} {Ξ²} Ξ΅)
   where
    Ξ² : I β†’ ⟨ 𝓓 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔' ⟩
    Ξ² i = DCPO-∘ 𝓓 𝓔 𝓔' (Ξ± i) g
    Ξ΅ : is-Directed (𝓓 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔') Ξ²
    Ξ΅ = image-is-directed (𝓓 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔) (𝓓 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔') {Ξ» f β†’ DCPO-∘ 𝓓 𝓔 𝓔' f g}
         (DCPO-∘-is-monotoneβ‚‚ 𝓓 𝓔 𝓔' g) {I} {Ξ±} Ξ΄
    Ξ³ : DCPO-∘ 𝓓 𝓔 𝓔' (∐ (𝓓 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔) {I} {Ξ±} Ξ΄) g ＝ ∐ (𝓓 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔') {I} {Ξ²} Ξ΅
    Ξ³ = to-continuous-function-＝ 𝓓 𝓔' ψ
     where
      ψ : (x : ⟨ 𝓓 ⟩)
        β†’ [ 𝓔 , 𝓔' ]⟨ g ⟩ ([ 𝓓 , 𝓔 ]⟨ ∐ (𝓓 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔) {I} {Ξ±} Ξ΄ ⟩ x)
        ＝ ∐ 𝓔' (pointwise-family-is-directed 𝓓 𝓔' Ξ² Ξ΅ x)
      ψ x = [ 𝓔 , 𝓔' ]⟨ g ⟩ ([ 𝓓 , 𝓔 ]⟨ ∐ (𝓓 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔) {I} {Ξ±} Ξ΄ ⟩ x) ＝⟨ refl ⟩
            [ 𝓔 , 𝓔' ]⟨ g ⟩ (∐ 𝓔 Ξ΅')                                 ＝⟨ e₁ ⟩
            ∐ 𝓔' Ξ΅''                                                 ＝⟨ eβ‚‚ ⟩
            ∐ 𝓔' (pointwise-family-is-directed 𝓓 𝓔' Ξ² Ξ΅ x)           ∎
       where
        Ξ΅' : is-Directed 𝓔 (pointwise-family 𝓓 𝓔 Ξ± x)
        Ξ΅' = pointwise-family-is-directed 𝓓 𝓔 Ξ± Ξ΄ x
        Ξ΅'' : is-Directed 𝓔' ([ 𝓔 , 𝓔' ]⟨ g ⟩ ∘ pointwise-family 𝓓 𝓔 Ξ± x)
        Ξ΅'' = image-is-directed' 𝓔 𝓔' g Ξ΅'
        e₁ = continuous-∐-＝ 𝓔 𝓔' g Ξ΅'
        eβ‚‚ = ∐-independent-of-directedness-witness 𝓔' Ξ΅''
              (pointwise-family-is-directed 𝓓 𝓔' Ξ² Ξ΅ x)

DCPO-βˆ˜β‚ƒ-is-continuousβ‚‚ : {𝓦₁ 𝓣₁ 𝓦₂ 𝓣₂ 𝓦₃ 𝓣₃ 𝓦₄ 𝓣₄ : Universe}
                         (𝓓₁ : DCPO {𝓦₁} {𝓣₁}) (𝓓₂ : DCPO {𝓦₂} {𝓣₂})
                         (𝓓₃ : DCPO {𝓦₃} {𝓣₃}) (𝓓₄ : DCPO {𝓦₄} {𝓣₄})
                         (f : DCPO[ 𝓓₁ , 𝓓₂ ]) (h : DCPO[ 𝓓₃ , 𝓓₄ ])
                       β†’ is-continuous (𝓓₂ βŸΉα΅ˆαΆœα΅–α΅’ 𝓓₃) (𝓓₁ βŸΉα΅ˆαΆœα΅–α΅’ 𝓓₄)
                          (Ξ» g β†’ DCPO-βˆ˜β‚ƒ 𝓓₁ 𝓓₂ 𝓓₃ 𝓓₄ f g h)
DCPO-βˆ˜β‚ƒ-is-continuousβ‚‚ 𝓓₁ 𝓓₂ 𝓓₃ 𝓓₄ f h =
 ∘-is-continuous (𝓓₂ βŸΉα΅ˆαΆœα΅–α΅’ 𝓓₃) (𝓓₂ βŸΉα΅ˆαΆœα΅–α΅’ 𝓓₄) (𝓓₁ βŸΉα΅ˆαΆœα΅–α΅’ 𝓓₄)
  (Ξ» g β†’ DCPO-∘ 𝓓₂ 𝓓₃ 𝓓₄ g h) (DCPO-∘ 𝓓₁ 𝓓₂ 𝓓₄ f)
  (DCPO-∘-is-continuousβ‚‚ 𝓓₂ 𝓓₃ 𝓓₄ h) (DCPO-∘-is-continuous₁ 𝓓₁ 𝓓₂ 𝓓₄ f)

\end{code}

When 𝓔 is sup-complete, then the exponential (𝓓 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔) is also sup-complete
(even if 𝓓 isn't). This comes in useful when proving that exponentials of
sup-complete dcpos are algebraic.

\begin{code}

module _
        (𝓓 : DCPO {𝓀} {𝓣})
        (𝓔 : DCPO {𝓀'} {𝓣'})
        (𝓔-is-sup-complete : is-sup-complete 𝓔)
       where

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

 sup-of-continuous-functions : {I : π“₯ Μ‡ } β†’ (I β†’ DCPO[ 𝓓 , 𝓔 ]) β†’ DCPO[ 𝓓 , 𝓔 ]
 sup-of-continuous-functions {I} Ξ± = (f , c)
  where
   f : ⟨ 𝓓 ⟩ β†’ ⟨ 𝓔 ⟩
   f x = ⋁ (pointwise-family 𝓓 𝓔 Ξ± x)
   c : is-continuous 𝓓 𝓔 f
   c J Ξ² Ξ΄ = (ub , lb-of-ubs)
    where
     ub : is-upperbound (underlying-order 𝓔) (f (∐ 𝓓 Ξ΄)) (f ∘ Ξ²)
     ub i = ⋁-is-lowerbound-of-upperbounds
             (pointwise-family 𝓓 𝓔 Ξ± (Ξ² i)) (f (∐ 𝓓 Ξ΄)) Ξ³
      where
       Ξ³ : is-upperbound (underlying-order 𝓔) (f (∐ 𝓓 Ξ΄))
            (pointwise-family 𝓓 𝓔 Ξ± (Ξ² i))
       Ξ³ j = [ 𝓓 , 𝓔 ]⟨ Ξ± j ⟩ (Ξ² i)   βŠ‘βŸ¨ 𝓔 ⟩[ β¦…1⦆ ]
             [ 𝓓 , 𝓔 ]⟨ Ξ± j ⟩ (∐ 𝓓 Ξ΄) βŠ‘βŸ¨ 𝓔 ⟩[ β¦…2⦆ ]
             f (∐ 𝓓 Ξ΄)                 ∎⟨ 𝓔 ⟩
        where
         β¦…1⦆ = monotone-if-continuous 𝓓 𝓔 (Ξ± j) (Ξ² i) (∐ 𝓓 Ξ΄)
               (∐-is-upperbound 𝓓 Ξ΄ i)
         β¦…2⦆ = ⋁-is-upperbound (pointwise-family 𝓓 𝓔 Ξ± (∐ 𝓓 Ξ΄)) j
     lb-of-ubs : is-lowerbound-of-upperbounds (underlying-order 𝓔) (f (∐ 𝓓 Ξ΄))
                  (f ∘ β)
     lb-of-ubs y y-is-ub =
      ⋁-is-lowerbound-of-upperbounds (pointwise-family 𝓓 𝓔 Ξ± (∐ 𝓓 Ξ΄))
       y Ξ³
        where
         Ξ³ : is-upperbound (underlying-order 𝓔) y
              (pointwise-family 𝓓 𝓔 Ξ± (∐ 𝓓 Ξ΄))
         Ξ³ i = [ 𝓓 , 𝓔 ]⟨ Ξ± i ⟩ (∐ 𝓓 Ξ΄) βŠ‘βŸ¨ 𝓔 ⟩[ β¦…1⦆ ]
               ∐ 𝓔 Ξ΅                    βŠ‘βŸ¨ 𝓔 ⟩[ β¦…2⦆ ]
               y                        ∎⟨ 𝓔 ⟩
          where
           Ξ΅ : is-Directed 𝓔 ([ 𝓓 , 𝓔 ]⟨ Ξ± i ⟩ ∘ Ξ²)
           Ξ΅ = image-is-directed' 𝓓 𝓔 (Ξ± i) Ξ΄
           β¦…1⦆ = continuous-∐-βŠ‘ 𝓓 𝓔 (Ξ± i) Ξ΄
           β¦…2⦆ = ∐-is-lowerbound-of-upperbounds 𝓔 Ξ΅ y h
            where
             h : is-upperbound (underlying-order 𝓔) y ([ 𝓓 , 𝓔 ]⟨ Ξ± i ⟩ ∘ Ξ²)
             h j = [ 𝓓 , 𝓔 ]⟨ Ξ± i ⟩ (Ξ² j) βŠ‘βŸ¨ 𝓔 ⟩[ ⦅†⦆ ]
                   f (Ξ² j)                 βŠ‘βŸ¨ 𝓔 ⟩[ y-is-ub j ]
                   y                       ∎⟨ 𝓔 ⟩
              where
               ⦅†⦆ = ⋁-is-upperbound (pointwise-family 𝓓 𝓔 Ξ± (Ξ² j)) i

 exponential-is-sup-complete : is-sup-complete (𝓓 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔)
 exponential-is-sup-complete =
  record
   { ⋁        = Ξ» {I} Ξ± β†’ sup-of-continuous-functions Ξ±
   ; ⋁-is-sup = Ξ» {I} β†’ lemma
   }
   where
    lemma : {I : π“₯ Μ‡ } (Ξ± : I β†’ DCPO[ 𝓓 , 𝓔 ])
          β†’ is-sup (underlying-order (𝓓 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔))
             (sup-of-continuous-functions Ξ±) Ξ±
    lemma {I} Ξ± = (ub , lb-of-ubs)
     where
      ub : is-upperbound (underlying-order (𝓓 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔))
            (sup-of-continuous-functions Ξ±) Ξ±
      ub i x = ⋁-is-upperbound (pointwise-family 𝓓 𝓔 Ξ± x) i
      lb-of-ubs : is-lowerbound-of-upperbounds (underlying-order (𝓓 βŸΉα΅ˆαΆœα΅–α΅’ 𝓔))
                   (sup-of-continuous-functions Ξ±) Ξ±
      lb-of-ubs g g-is-ub x =
       ⋁-is-lowerbound-of-upperbounds (pointwise-family 𝓓 𝓔 Ξ± x)
                                      ([ 𝓓 , 𝓔 ]⟨ g ⟩ x) (Ξ» i β†’ g-is-ub i x)

\end{code}