Tom de Jong, May 2019.
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-β_ Ξ±)
β 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 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 ]
where
u = β-is-lowerbound-of-upperbounds π (Ξ΅ (β π Ο)) e v
where
v : (i : I) β [ π , π ]β¨ Ξ± i β© (β π Ο) ββ¨ π β© e
v i = [ π , π ]β¨ Ξ± i β© (β π Ο)             ββ¨ π β©[ lβ ]
β π (image-is-directed' π π (Ξ± i) Ο) ββ¨ π β©[ lβ ]
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 ]

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 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β¦ ]
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 ]
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}