Tom de Jong, 12 May 2020 - 9 June 2020.
We construct Scott's famous nontrivial pointed dcpo D∞ for which D∞ is
isomorphic to its own function space and prove that it is algebraic.
The construction of D∞ is based on Scott's "Continuous lattices"
(doi:10.1007/BFB0073967), specifically pages 126--128.
\begin{code}
{-# OPTIONS --safe --without-K --lossy-unification #-}
\end{code}
We use the flag --lossy-unification to speed up the type-checking.
This flag was kindly implemented by Andrea Vezzosi upon request.
Documentation for the flag (written by Andrea Vezzosi) can be found here:
https://agda.readthedocs.io/en/latest/language/lossy-unification.html
The most important takeaway from the documentation is that the flag is sound:
"[...] if Agda accepts code with the flag enabled it should also accept it
without the flag (with enough resources, and possibly needing extra type
annotations)."
A related issue (originally opened by Wolfram Kahl in 2015) can be found here:
https://github.com/agda/agda/issues/1625
\begin{code}
open import MLTT.Spartan
open import UF.FunExt
open import UF.PropTrunc
open import UF.Subsingletons
module DomainTheory.Bilimits.Dinfinity
(pt : propositional-truncations-exist)
(fe : Fun-Ext)
(pe : Prop-Ext)
where
open PropositionalTruncation pt
open import UF.Base
open import UF.Subsingletons-Properties
open import DomainTheory.Basics.Dcpo pt fe 𝓤₀
open import DomainTheory.Basics.Exponential pt fe 𝓤₀
open import DomainTheory.Basics.Miscelanea pt fe 𝓤₀
open import DomainTheory.Basics.Pointed pt fe 𝓤₀
open import DomainTheory.Bilimits.Sequential pt fe 𝓤₁ 𝓤₁
open import DomainTheory.Lifting.LiftingSet pt fe 𝓤₀ pe
open import Naturals.Order hiding (subtraction')
open import Naturals.Addition renaming (_+_ to _+'_)
open import Notation.Order
\end{code}
We start by defining the ℕ-indexed diagram of iterated exponentials.
\begin{code}
𝓓⊥ : ℕ → DCPO⊥ {𝓤₁} {𝓤₁}
𝓓⊥ zero = 𝓛-DCPO⊥ {𝓤₀} {𝟙{𝓤₀}} (props-are-sets 𝟙-is-prop)
𝓓⊥ (succ n) = 𝓓⊥ n ⟹ᵈᶜᵖᵒ⊥ 𝓓⊥ n
𝓓 : ℕ → DCPO {𝓤₁} {𝓤₁}
𝓓 n = pr₁ (𝓓⊥ n)
𝓓-diagram : (n : ℕ)
→ DCPO[ 𝓓 n , 𝓓 (succ n) ]
× DCPO[ 𝓓 (succ n) , 𝓓 n ]
𝓓-diagram zero = (e₀ , e₀-continuity) , p₀ , p₀-continuity
where
e₀ : ⟨ 𝓓 0 ⟩ → ⟨ 𝓓 1 ⟩
e₀ x = (λ y → x) , (constant-functions-are-continuous (𝓓 0) (𝓓 0))
e₀-continuity : is-continuous (𝓓 0) (𝓓 1) e₀
e₀-continuity I α δ = ub , lb-of-ubs
where
ub : (i : I) → e₀ (α i) ⊑⟨ (𝓓 1) ⟩ e₀ (∐ (𝓓 0) δ)
ub i y = α i ⊑⟨ 𝓓 0 ⟩[ ∐-is-upperbound (𝓓 0) δ i ]
∐ (𝓓 0) δ ∎⟨ 𝓓 0 ⟩
lb-of-ubs : is-lowerbound-of-upperbounds (underlying-order (𝓓 1))
(e₀ (∐ (𝓓 0) δ)) (λ x → e₀ (α x))
lb-of-ubs (g , c) ub y =
∐-is-lowerbound-of-upperbounds (𝓓 0) δ (g y) (λ i → ub i y)
p₀ : ⟨ 𝓓 1 ⟩ → ⟨ 𝓓 0 ⟩
p₀ (f , c) = f (⊥ (𝓓⊥ 0))
p₀-continuity : is-continuous (𝓓 1) (𝓓 0) p₀
p₀-continuity I α δ = ub , lb-of-ubs
where
ub : (i : I) → p₀ (α i) ⊑⟨ 𝓓 0 ⟩ p₀ (∐ (𝓓 1) {I} {α} δ)
ub i = ∐-is-upperbound (𝓓 1) {I} {α} δ i (⊥ (𝓓⊥ 0))
lb-of-ubs : is-lowerbound-of-upperbounds (underlying-order (𝓓 0))
(p₀ (∐ (𝓓 1) {I} {α} δ)) (λ x → p₀ (α x))
lb-of-ubs y ub =
∐-is-lowerbound-of-upperbounds (𝓓 0) ε y ub
where
ε : is-Directed (𝓓 0) (pointwise-family (𝓓 0) (𝓓 0) α (⊥ (𝓓⊥ 0)))
ε = pointwise-family-is-directed (𝓓 0) (𝓓 0) α δ (⊥ (𝓓⊥ 0))
𝓓-diagram (succ n) = (e , e-continuity) , (p , p-continuity)
where
IH : DCPO[ 𝓓 n , 𝓓 (succ n) ] × DCPO[ 𝓓 (succ n) , 𝓓 n ]
IH = 𝓓-diagram n
eₙ : DCPO[ 𝓓 n , 𝓓 (succ n) ]
eₙ = pr₁ IH
pₙ : DCPO[ 𝓓 (succ n) , 𝓓 n ]
pₙ = pr₂ IH
e : ⟨ 𝓓 (succ n) ⟩ → ⟨ 𝓓 (succ (succ n)) ⟩
e f = DCPO-∘₃ (𝓓 (succ n)) (𝓓 n) (𝓓 n) (𝓓 (succ n)) pₙ f eₙ
e-continuity : is-continuous (𝓓 (succ n)) (𝓓 (succ (succ n))) e
e-continuity = ∘-is-continuous
(𝓓 (succ n))
((𝓓 n) ⟹ᵈᶜᵖᵒ (𝓓 (succ n)))
(𝓓 (succ (succ n)))
(λ f → DCPO-∘ (𝓓 n) (𝓓 n) (𝓓 (succ n)) f eₙ)
(DCPO-∘ (𝓓 (succ n)) (𝓓 n) (𝓓 (succ n)) pₙ)
(DCPO-∘-is-continuous₂ (𝓓 n) (𝓓 n) (𝓓 (succ n)) eₙ)
(DCPO-∘-is-continuous₁ (𝓓 (succ n)) (𝓓 n)
(𝓓 (succ n)) pₙ)
p : ⟨ 𝓓 (succ (succ n)) ⟩ → ⟨ 𝓓 (succ n) ⟩
p f = DCPO-∘₃ (𝓓 n) (𝓓 (succ n)) (𝓓 (succ n)) (𝓓 n) eₙ f pₙ
p-continuity : is-continuous (𝓓 (succ (succ n))) (𝓓 (succ n)) p
p-continuity = ∘-is-continuous
(𝓓 (succ (succ n)))
((𝓓 n) ⟹ᵈᶜᵖᵒ (𝓓 (succ n)))
(𝓓 (succ n))
(DCPO-∘ (𝓓 n) (𝓓 (succ n)) (𝓓 (succ n)) eₙ)
(λ f → DCPO-∘ (𝓓 n) (𝓓 (succ n)) (𝓓 n) f pₙ)
(DCPO-∘-is-continuous₁ (𝓓 n) (𝓓 (succ n))
(𝓓 (succ n)) eₙ)
(DCPO-∘-is-continuous₂ (𝓓 n) (𝓓 (succ n)) (𝓓 n) pₙ)
π' : (n : ℕ) → DCPO[ 𝓓 (succ n) , 𝓓 n ]
π' n = pr₂ (𝓓-diagram n)
π : (n : ℕ) → ⟨ 𝓓 (succ n) ⟩ → ⟨ 𝓓 n ⟩
π n = underlying-function (𝓓 (succ n)) (𝓓 n) (π' n)
π-is-continuous : (n : ℕ) → is-continuous (𝓓 (succ n)) (𝓓 n) (π n)
π-is-continuous n = pr₂ (pr₂ (𝓓-diagram n))
ε' : (n : ℕ) → DCPO[ 𝓓 n , 𝓓 (succ n) ]
ε' n = pr₁ (𝓓-diagram n)
ε : (n : ℕ) → ⟨ 𝓓 n ⟩ → ⟨ 𝓓 (succ n) ⟩
ε n = underlying-function (𝓓 n) (𝓓 (succ n)) (ε' n)
ε-is-continuous : (n : ℕ) → is-continuous (𝓓 n) (𝓓 (succ n)) (ε n)
ε-is-continuous n = pr₂ (pr₁ (𝓓-diagram n))
π-on-0 : (f : ⟨ 𝓓 0 ⟩ → ⟨ 𝓓 0 ⟩) (c : is-continuous (𝓓 0) (𝓓 0) f)
→ π 0 (f , c) ＝ f (⊥ (𝓓⊥ 0))
π-on-0 f c = refl
π-on-succ : (n : ℕ) (f : ⟨ 𝓓 (succ n) ⟩ → ⟨ 𝓓 (succ n) ⟩)
(c : is-continuous (𝓓 (succ n)) (𝓓 (succ n)) f)
→ [ 𝓓 n , 𝓓 n ]⟨ π (succ n) (f , c) ⟩ ＝ π n ∘ f ∘ ε n
π-on-succ n f c = refl
π-on-succ' : (n : ℕ) (f : DCPO[ 𝓓 (succ n) , 𝓓 (succ n) ])
→ [ 𝓓 n , 𝓓 n ]⟨ π (succ n) f ⟩
＝ π n ∘ [ 𝓓 (succ n) , 𝓓 (succ n) ]⟨ f ⟩ ∘ ε n
π-on-succ' n f = refl
ε-on-0 : (x : ⟨ 𝓓 0 ⟩) → [ 𝓓 0 , 𝓓 0 ]⟨ ε 0 x ⟩ ＝ (λ y → x)
ε-on-0 x = refl
ε-on-succ : (n : ℕ) (f : ⟨ 𝓓 n ⟩ → ⟨ 𝓓 n ⟩) (c : is-continuous (𝓓 n) (𝓓 n) f)
→ [ 𝓓 (succ n) , 𝓓 (succ n) ]⟨ ε (succ n) (f , c) ⟩ ＝ ε n ∘ f ∘ π n
ε-on-succ n f c = refl
ε-section-of-π : (n : ℕ) → π n ∘ ε n ∼ id
ε-section-of-π zero x = refl
ε-section-of-π (succ n) (f , _) = to-continuous-function-＝ (𝓓 n) (𝓓 n) γ
where
γ : π n ∘ ε n ∘ f ∘ π n ∘ ε n ∼ f
γ x = (π n ∘ ε n ∘ f ∘ π n ∘ ε n) x ＝⟨ IH (f (π n (ε n x))) ⟩
(f ∘ π n ∘ ε n) x ＝⟨ ap f (IH x) ⟩
f x ∎
where
IH : π n ∘ ε n ∼ id
IH = ε-section-of-π n
επ-deflation : (n : ℕ) (f : ⟨ 𝓓 (succ n) ⟩) → ε n (π n f) ⊑⟨ 𝓓 (succ n) ⟩ f
επ-deflation zero (f , c) x =
f (⊥ (𝓓⊥ 0)) ⊑⟨ 𝓓 0 ⟩[ m (⊥ (𝓓⊥ 0)) x (⊥-is-least (𝓓⊥ 0) x) ]
f x ∎⟨ 𝓓 0 ⟩
where
m : is-monotone (𝓓 0) (𝓓 0) f
m = monotone-if-continuous (𝓓 0) (𝓓 0) (f , c)
επ-deflation (succ n) (f , c) x =
transitivity (𝓓 (succ n))
((ε n ∘ π n ∘ f ∘ ε n ∘ π n) x) (f (ε n (π n x))) (f x)
(IH (f (ε n (π n x))))
(m (ε n (π n x)) x (IH x))
where
IH : (g : ⟨ 𝓓 (succ n) ⟩) → ε n (π n g) ⊑⟨ 𝓓 (succ n) ⟩ g
IH = επ-deflation n
m : is-monotone (𝓓 (succ n)) (𝓓 (succ n)) f
m = monotone-if-continuous (𝓓 (succ n)) (𝓓 (succ n)) (f , c)
\end{code}
With the diagram defined, we consider its bilimit D∞.
\begin{code}
open SequentialDiagram
𝓓 ε π
επ-deflation
ε-section-of-π
ε-is-continuous
π-is-continuous
public
π-exp-to-succ : (n : ℕ) → ⟨ 𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞ ⟩ → ⟨ 𝓓 (succ n) ⟩
π-exp-to-succ n f = DCPO-∘₃ (𝓓 n) 𝓓∞ 𝓓∞ (𝓓 n) (ε∞' n) f (π∞' n)
π-exp-to-succ-is-continuous : (n : ℕ)
→ is-continuous (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞) (𝓓 (succ n))
(π-exp-to-succ n)
π-exp-to-succ-is-continuous n =
DCPO-∘₃-is-continuous₂ (𝓓 n) 𝓓∞ 𝓓∞ (𝓓 n) (ε∞' n) (π∞' n)
π-exp : (n : ℕ) → ⟨ 𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞ ⟩ → ⟨ 𝓓 n ⟩
π-exp zero = π 0 ∘ π-exp-to-succ 0
π-exp (succ n) = π-exp-to-succ n
π-exp-is-continuous : (n : ℕ) → is-continuous (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞) (𝓓 n) (π-exp n)
π-exp-is-continuous zero = ∘-is-continuous (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞) (𝓓 1) (𝓓 0)
(π-exp-to-succ 0) (π 0)
(π-exp-to-succ-is-continuous 0) (π-is-continuous 0)
π-exp-is-continuous (succ n) = π-exp-to-succ-is-continuous n
π-exp-commutes-with-π : (n : ℕ) → π n ∘ π-exp (succ n) ∼ π-exp n
π-exp-commutes-with-π zero f = refl
π-exp-commutes-with-π (succ n) (f , c) =
to-continuous-function-＝ (𝓓 n) (𝓓 n) γ
where
h : DCPO[ 𝓓 (succ n) , 𝓓 (succ n) ]
h = DCPO-∘₃ (𝓓 (succ n)) 𝓓∞ 𝓓∞ (𝓓 (succ n))
(ε∞' (succ n)) (f , c) (π∞' (succ n))
γ : ([ 𝓓 n , 𝓓 n ]⟨ π (succ n) h ⟩) ∼ π∞ n ∘ f ∘ ε∞ n
γ x = [ 𝓓 n , 𝓓 n ]⟨ (π (succ n) h) ⟩ x ＝⟨ e₁ ⟩
(π n ∘ [ 𝓓 (succ n) , 𝓓 (succ n) ]⟨ h ⟩ ∘ ε n) x ＝⟨ refl ⟩
(π n ∘ π∞ (succ n) ∘ f') x ＝⟨ e₂ ⟩
(π⁺ {n} {succ n} (≤-succ n) ∘ π∞ (succ n) ∘ f') x ＝⟨ e₃ ⟩
(π∞ n ∘ f ∘ ε∞ (succ n) ∘ ε n) x ＝⟨ e₄ ⟩
(π∞ n ∘ f ∘ ε∞ (succ n) ∘ ε⁺ {n} {succ n} (≤-succ n)) x ＝⟨ e₅ ⟩
(π∞ n ∘ f ∘ ε∞ n) x ∎
where
f' : ⟨ 𝓓 n ⟩ → ⟨ 𝓓∞ ⟩
f' = f ∘ ε∞ (succ n) ∘ ε n
e₁ = happly (π-on-succ' n h) x
e₂ = π-in-terms-of-π⁺ n (π∞ (succ n) (f' x))
e₃ = π∞-commutes-with-πs n (succ n) (≤-succ n)
(f (ε∞ (succ n) (ε n x)))
e₄ = ap (π∞ n ∘ f ∘ ε∞ (succ n)) (ε-in-terms-of-ε⁺ n x)
e₅ = ap (π∞ n ∘ f) (ε∞-commutes-with-εs n (succ n) (≤-succ n) x)
π-exp-commutes-with-π⁺ : (n m : ℕ) (l : n ≤ m) → π⁺ {n} {m} l ∘ π-exp m ∼ π-exp n
π-exp-commutes-with-π⁺ n m l = commute-with-πs-lemma (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞)
π-exp π-exp-commutes-with-π n m l
open DcpoCone (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞) π-exp π-exp-is-continuous π-exp-commutes-with-π⁺
π-exp∞ : ⟨ 𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞ ⟩ → ⟨ 𝓓∞ ⟩
π-exp∞ = limit-mediating-arrow
π-exp∞-is-continuous : is-continuous (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞) 𝓓∞ π-exp∞
π-exp∞-is-continuous = limit-mediating-arrow-is-continuous
π-exp∞' : DCPO[ 𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞ , 𝓓∞ ]
π-exp∞' = π-exp∞ , π-exp∞-is-continuous
\end{code}
The point is to prove that the map π-exp∞ : ⟨ 𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞ ⟩ → ⟨ 𝓓∞ ⟩ is an
isomorphism.
\begin{code}
ε-exp-from-succ : (n : ℕ) → ⟨ 𝓓 (succ n) ⟩ → ⟨ 𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞ ⟩
ε-exp-from-succ n f = DCPO-∘₃ 𝓓∞ (𝓓 n) (𝓓 n) 𝓓∞ (π∞' n) f (ε∞' n)
ε-exp-from-succ-is-continuous : (n : ℕ)
→ is-continuous (𝓓 (succ n)) (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞)
(ε-exp-from-succ n)
ε-exp-from-succ-is-continuous n = DCPO-∘₃-is-continuous₂ 𝓓∞ (𝓓 n) (𝓓 n) 𝓓∞
(π∞' n) (ε∞' n)
ε-exp : (n : ℕ) → ⟨ 𝓓 n ⟩ → ⟨ 𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞ ⟩
ε-exp zero = ε-exp-from-succ 0 ∘ ε 0
ε-exp (succ n) = ε-exp-from-succ n
ε-exp-is-continuous : (n : ℕ) → is-continuous (𝓓 n) (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞) (ε-exp n)
ε-exp-is-continuous zero = ∘-is-continuous (𝓓 0) (𝓓 1) (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞)
(ε 0) (ε-exp-from-succ 0)
(ε-is-continuous 0) (ε-exp-from-succ-is-continuous 0)
ε-exp-is-continuous (succ n) = ε-exp-from-succ-is-continuous n
ε-exp-commutes-with-ε : (n : ℕ) → ε-exp (succ n) ∘ ε n ∼ ε-exp n
ε-exp-commutes-with-ε zero x = refl
ε-exp-commutes-with-ε (succ n) (f , c) =
to-continuous-function-＝ 𝓓∞ 𝓓∞ γ
where
ε-exp₁ : ⟨ 𝓓∞ ⟩ → ⟨ 𝓓∞ ⟩
ε-exp₁ = [ 𝓓∞ , 𝓓∞ ]⟨ ε-exp (succ (succ n)) (ε (succ n) (f , c)) ⟩
ε-exp₂ : ⟨ 𝓓∞ ⟩ → ⟨ 𝓓∞ ⟩
ε-exp₂ = [ 𝓓∞ , 𝓓∞ ]⟨ ε-exp (succ n) (f , c) ⟩
γ : ε-exp₁ ∼ ε-exp₂
γ σ = ε-exp₁ σ ＝⟨ refl ⟩
(ε∞ (succ n) ∘ ε n ∘ h) σ ＝⟨ e₁ ⟩
(ε∞ (succ n) ∘ ε⁺ {n} {succ n} (≤-succ n) ∘ h) σ ＝⟨ e₂ ⟩
(ε∞ n ∘ h) σ ＝⟨ refl ⟩
(ε∞ n ∘ f ∘ π n ∘ π∞ (succ n)) σ ＝⟨ e₃ ⟩
(ε∞ n ∘ f ∘ π⁺ {n} {succ n} (≤-succ n) ∘ π∞ (succ n)) σ ＝⟨ e₄ ⟩
(ε∞ n ∘ f ∘ π∞ n) σ ＝⟨ refl ⟩
ε-exp₂ σ ∎
where
h : ⟨ 𝓓∞ ⟩ → ⟨ 𝓓 n ⟩
h = f ∘ π n ∘ π∞ (succ n)
e₁ = ap (ε∞ (succ n)) (ε-in-terms-of-ε⁺ n (h σ))
e₂ = ε∞-commutes-with-εs n (succ n) (≤-succ n) (h σ)
e₃ = ap (ε∞ n ∘ f) (π-in-terms-of-π⁺ n (π∞ (succ n) σ))
e₄ = ap (ε∞ n ∘ f) (π∞-commutes-with-πs n (succ n) (≤-succ n) σ)
ε-exp-commutes-with-ε⁺ : (n m : ℕ) (l : n ≤ m) → ε-exp m ∘ ε⁺ {n} {m} l ∼ ε-exp n
ε-exp-commutes-with-ε⁺ n m l = commute-with-εs-lemma (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞) ε-exp
ε-exp-commutes-with-ε n m l
open DcpoCocone (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞) ε-exp ε-exp-is-continuous ε-exp-commutes-with-ε⁺
ε-exp∞ : ⟨ 𝓓∞ ⟩ → ⟨ 𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞ ⟩
ε-exp∞ = colimit-mediating-arrow
ε-exp∞-is-continuous : is-continuous 𝓓∞ (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞) ε-exp∞
ε-exp∞-is-continuous = colimit-mediating-arrow-is-continuous
ε-exp∞' : DCPO[ 𝓓∞ , 𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞ ]
ε-exp∞' = ε-exp∞ , ε-exp∞-is-continuous
\end{code}
The map ε-exp∞ : ⟨ 𝓓∞ ⟩ → ⟨ 𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞ ⟩ is going to be the desired inverse of
π-exp∞.
\begin{code}
ε-exp-family : ⟨ 𝓓∞ ⟩ → ℕ → ⟨ 𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞ ⟩
ε-exp-family σ n = ε-exp (succ n) (⦅ σ ⦆ (succ n))
ε-exp-family-is-directed : (σ : ⟨ 𝓓∞ ⟩)
→ is-Directed (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞) (ε-exp-family σ)
ε-exp-family-is-directed σ = ∣ 0 ∣ , γ
where
γ : is-semidirected (underlying-order (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞)) (ε-exp-family σ)
γ n m = ∥∥-functor g h
where
δ : is-Directed (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞) (colimit-family σ)
δ = colimit-family-is-directed σ
h : ∃ k ꞉ ℕ , colimit-family σ (succ n) ⊑⟨ 𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞ ⟩ colimit-family σ k
× colimit-family σ (succ m) ⊑⟨ 𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞ ⟩ colimit-family σ k
h = semidirected-if-Directed (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞) (colimit-family σ) δ
(succ n) (succ m)
g : (Σ k ꞉ ℕ , colimit-family σ (succ n) ⊑⟨ 𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞ ⟩ colimit-family σ k
× colimit-family σ (succ m) ⊑⟨ 𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞ ⟩ colimit-family σ k)
→ Σ k ꞉ ℕ , ε-exp-family σ n ⊑⟨ 𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞ ⟩ ε-exp-family σ k
× ε-exp-family σ m ⊑⟨ 𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞ ⟩ ε-exp-family σ k
g (k , lₙ , lₘ) = k , lₙ' , lₘ'
where
lₖ : colimit-family σ k ⊑⟨ 𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞ ⟩ ε-exp-family σ k
lₖ = colimit-family-is-monotone σ k (succ k) (≤-succ k)
lₙ' : ε-exp-family σ n ⊑⟨ 𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞ ⟩ ε-exp-family σ k
lₙ' = transitivity (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞)
(ε-exp-family σ n) (colimit-family σ k) (ε-exp-family σ k)
lₙ lₖ
lₘ' : ε-exp-family σ m ⊑⟨ 𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞ ⟩ ε-exp-family σ k
lₘ' = transitivity (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞)
(ε-exp-family σ m) (colimit-family σ k) (ε-exp-family σ k)
lₘ lₖ
ε-exp∞-alt : (σ : ⟨ 𝓓∞ ⟩)
→ ε-exp∞ σ ＝ ∐ (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞) (ε-exp-family-is-directed σ)
ε-exp∞-alt σ = antisymmetry (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞) (ε-exp∞ σ) (∐ (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞) δ₂) a b
where
δ₁ : is-Directed (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞) (colimit-family σ)
δ₁ = colimit-family-is-directed σ
δ₂ : is-Directed (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞) (ε-exp-family σ)
δ₂ = ε-exp-family-is-directed σ
a : ε-exp∞ σ ⊑⟨ 𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞ ⟩ ∐ (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞) δ₂
a = ∐-is-monotone (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞) δ₁ δ₂ γ
where
γ : (n : ℕ)
→ colimit-family σ n ⊑⟨ 𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞ ⟩ ε-exp-family σ n
γ n = colimit-family-is-monotone σ n (succ n) (≤-succ n)
b : ∐ (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞) δ₂ ⊑⟨ 𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞ ⟩ ε-exp∞ σ
b = ∐-is-lowerbound-of-upperbounds (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞) δ₂ (ε-exp∞ σ) γ
where
γ : is-upperbound (underlying-order (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞))
(ε-exp∞ σ) (ε-exp-family σ)
γ n = ∐-is-upperbound (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞) δ₁ (succ n)
π-exp-family : ⟨ 𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞ ⟩ → ℕ → ⟨ 𝓓∞ ⟩
π-exp-family φ n = ε∞ (succ n) (π-exp (succ n) φ)
\end{code}
In the code below we would like to write things as
x ⊑⟨ 𝓓∞ ⟩[ u ]
y ⊑⟨ 𝓓∞ ⟩[ v ]
z ∎⟨ 𝓓∞ ⟩
However, Agda has trouble figuring out some implicit arguments. (I believe
because it can't 'see' the additional witnesses (of continuity, etc.) that the
underlying functions of x, y and z are equipped with.)
Not using the _⊑⟨_⟩[_] syntax in favour of using transitivity directly and
explicitly naming all its arguments solves the above problem, but it doesn't
read very well.
Instead, we solve the problem by noting that the order on 𝓓∞ is pointwise and
that therefore we are really proving that for every i : ℕ we have
⦅ x ⦆ i ⊑⟨ 𝓓 i ⟩[ u i ]
⦅ y ⦆ i ⊑⟨ 𝓓 i ⟩[ v i ]
⦅ z ⦆ i ∎⟨ 𝓓 i ⟩
\begin{code}
π-exp-family-is-directed : (φ : ⟨ 𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞ ⟩)
→ is-Directed 𝓓∞ (π-exp-family φ)
π-exp-family-is-directed φ = ∣ 0 ∣ , γ
where
γ : is-semidirected (underlying-order 𝓓∞) (π-exp-family φ)
γ n m = ∥∥-functor g h
where
σ : ⟨ 𝓓∞ ⟩
σ = π-exp∞ φ
δ : is-Directed 𝓓∞ (ε∞-family σ)
δ = ε∞-family-is-directed σ
h : ∃ k ꞉ ℕ , ε∞-family σ (succ n) ⊑⟨ 𝓓∞ ⟩ ε∞-family σ k
× ε∞-family σ (succ m) ⊑⟨ 𝓓∞ ⟩ ε∞-family σ k
h = semidirected-if-Directed 𝓓∞ (ε∞-family σ) δ (succ n) (succ m)
g : (Σ k ꞉ ℕ , ε∞-family σ (succ n) ⊑⟨ 𝓓∞ ⟩ ε∞-family σ k
× ε∞-family σ (succ m) ⊑⟨ 𝓓∞ ⟩ ε∞-family σ k)
→ Σ k ꞉ ℕ , π-exp-family φ n ⊑⟨ 𝓓∞ ⟩ π-exp-family φ k
× π-exp-family φ m ⊑⟨ 𝓓∞ ⟩ π-exp-family φ k
g (k , lₙ , lₘ) = k , lₙ' , lₘ'
where
lₖ : ε∞-family σ k ⊑⟨ 𝓓∞ ⟩ ε∞-family σ (succ k)
lₖ = ε∞-family-is-monotone σ k (succ k) (≤-succ k)
lₙ' : π-exp-family φ n ⊑⟨ 𝓓∞ ⟩ π-exp-family φ k
lₙ' i =
⦅ π-exp-family φ n ⦆ i ⊑⟨ 𝓓 i ⟩[ reflexivity 𝓓∞ (π-exp-family φ n) i ]
⦅ ε∞-family σ (succ n) ⦆ i ⊑⟨ 𝓓 i ⟩[ lₙ i ]
⦅ ε∞-family σ k ⦆ i ⊑⟨ 𝓓 i ⟩[ lₖ i ]
⦅ ε∞-family σ (succ k) ⦆ i ⊑⟨ 𝓓 i ⟩[ reflexivity 𝓓∞ (π-exp-family φ k) i ]
⦅ π-exp-family φ k ⦆ i ∎⟨ 𝓓 i ⟩
lₘ' : π-exp-family φ m ⊑⟨ 𝓓∞ ⟩ π-exp-family φ k
lₘ' i =
⦅ π-exp-family φ m ⦆ i ⊑⟨ 𝓓 i ⟩[ reflexivity 𝓓∞ (π-exp-family φ m) i ]
⦅ ε∞-family σ (succ m) ⦆ i ⊑⟨ 𝓓 i ⟩[ lₘ i ]
⦅ ε∞-family σ k ⦆ i ⊑⟨ 𝓓 i ⟩[ lₖ i ]
⦅ ε∞-family σ (succ k) ⦆ i ⊑⟨ 𝓓 i ⟩[ reflexivity 𝓓∞ (π-exp-family φ k) i ]
⦅ π-exp-family φ k ⦆ i ∎⟨ 𝓓 i ⟩
π-exp∞-alt : (φ : ⟨ 𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞ ⟩)
→ π-exp∞ φ ＝ ∐ 𝓓∞ (π-exp-family-is-directed φ)
π-exp∞-alt φ = σ ＝⟨ ∐-of-ε∞s σ ⟩
∐ 𝓓∞ (ε∞-family-is-directed σ) ＝⟨ γ ⟩
∐ 𝓓∞ (π-exp-family-is-directed φ) ∎
where
σ : ⟨ 𝓓∞ ⟩
σ = π-exp∞ φ
γ : ∐ 𝓓∞ (ε∞-family-is-directed σ) ＝ ∐ 𝓓∞ (π-exp-family-is-directed φ)
γ = antisymmetry 𝓓∞ (∐ 𝓓∞ δ₁) (∐ 𝓓∞ δ₂) a b
where
δ₁ : is-Directed 𝓓∞ (ε∞-family σ)
δ₁ = ε∞-family-is-directed σ
δ₂ : is-Directed 𝓓∞ (π-exp-family φ)
δ₂ = π-exp-family-is-directed φ
a : ∐ 𝓓∞ δ₁ ⊑⟨ 𝓓∞ ⟩ ∐ 𝓓∞ δ₂
a = ∐-is-monotone 𝓓∞ δ₁ δ₂ h
where
h : (n : ℕ) → ε∞-family σ n ⊑⟨ 𝓓∞ ⟩ π-exp-family φ n
h n i = ⦅ ε∞-family σ n ⦆ i ⊑⟨ 𝓓 i ⟩[ ε∞-family-is-monotone σ n (succ n) (≤-succ n) i ]
⦅ ε∞-family σ (succ n) ⦆ i ⊑⟨ 𝓓 i ⟩[ reflexivity 𝓓∞ (ε∞-family σ (succ n)) i ]
⦅ π-exp-family φ n ⦆ i ∎⟨ 𝓓 i ⟩
b : ∐ 𝓓∞ δ₂ ⊑⟨ 𝓓∞ ⟩ ∐ 𝓓∞ δ₁
b = ∐-is-lowerbound-of-upperbounds 𝓓∞ δ₂ (∐ 𝓓∞ δ₁) h
where
h : is-upperbound (underlying-order 𝓓∞) (∐ 𝓓∞ δ₁) (π-exp-family φ)
h n i = ⦅ π-exp-family φ n ⦆ i ⊑⟨ 𝓓 i ⟩[ reflexivity 𝓓∞ (π-exp-family φ n) i ]
⦅ ε∞-family σ (succ n) ⦆ i ⊑⟨ 𝓓 i ⟩[ ∐-is-upperbound 𝓓∞ δ₁ (succ n) i ]
⦅ ∐ 𝓓∞ δ₁ ⦆ i ∎⟨ 𝓓 i ⟩
π-exp-family-is-monotone : (φ : ⟨ 𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞ ⟩) {n m : ℕ} → n ≤ m
→ π-exp-family φ n ⊑⟨ 𝓓∞ ⟩ π-exp-family φ m
π-exp-family-is-monotone φ {n} {m} l i =
⦅ π-exp-family φ n ⦆ i ⊑⟨ 𝓓 i ⟩[ reflexivity 𝓓∞ (π-exp-family φ n) i ]
⦅ ε∞-family (π-exp∞ φ) (succ n) ⦆ i ⊑⟨ 𝓓 i ⟩[ u i ]
⦅ ε∞-family (π-exp∞ φ) (succ m) ⦆ i ⊑⟨ 𝓓 i ⟩[ reflexivity 𝓓∞ (π-exp-family φ m) i ]
⦅ π-exp-family φ m ⦆ i ∎⟨ 𝓓 i ⟩
where
u = ε∞-family-is-monotone (π-exp∞ φ) (succ n) (succ m) l
π-exp-family-is-monotone' : (φ ψ : ⟨ 𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞ ⟩) {n : ℕ}
→ φ ⊑⟨ 𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞ ⟩ ψ
→ π-exp-family φ n ⊑⟨ 𝓓∞ ⟩ π-exp-family ψ n
π-exp-family-is-monotone' φ ψ {n} l i =
⦅ π-exp-family φ n ⦆ i ⊑⟨ 𝓓 i ⟩[ u₁ i ]
⦅ ε∞ (succ n) (π-exp (succ n) φ) ⦆ i ⊑⟨ 𝓓 i ⟩[ u₂ i ]
⦅ ε∞ (succ n) (π-exp (succ n) ψ) ⦆ i ⊑⟨ 𝓓 i ⟩[ u₃ i ]
⦅ π-exp-family ψ n ⦆ i ∎⟨ 𝓓 i ⟩
where
u₁ = reflexivity 𝓓∞ (ε∞ (succ n) (π-exp (succ n) φ))
u₂ = monotone-if-continuous (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞) 𝓓∞ f φ ψ l
where
f : DCPO[ 𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞ , 𝓓∞ ]
f = DCPO-∘ (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞) (𝓓 (succ n)) 𝓓∞
(π-exp (succ n) , π-exp-is-continuous (succ n))
(ε∞' (succ n))
u₃ = reflexivity 𝓓∞ (ε∞ (succ n) (π-exp (succ n) ψ))
ε-exp-family-is-monotone : (σ : ⟨ 𝓓∞ ⟩) {n m : ℕ} → n ≤ m
→ ε-exp-family σ n ⊑⟨ 𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞ ⟩ ε-exp-family σ m
ε-exp-family-is-monotone σ {n} {m} l =
colimit-family-is-monotone σ (succ n) (succ m) l
ε-exp-family-is-monotone' : (σ τ : ⟨ 𝓓∞ ⟩) {n : ℕ} → σ ⊑⟨ 𝓓∞ ⟩ τ
→ ε-exp-family σ n ⊑⟨ 𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞ ⟩ ε-exp-family τ n
ε-exp-family-is-monotone' σ τ {n} l ρ i =
⦅ [ 𝓓∞ , 𝓓∞ ]⟨ ε-exp-family σ n ⟩ ρ ⦆ i ⊑⟨ 𝓓 i ⟩[ u₁ i ]
⦅ (ε∞ n ∘ [ 𝓓 n , 𝓓 n ]⟨ ⦅ σ ⦆ (succ n) ⟩ ∘ π∞ n) ρ ⦆ i ⊑⟨ 𝓓 i ⟩[ u₂ i ]
⦅ (ε∞ n ∘ [ 𝓓 n , 𝓓 n ]⟨ ⦅ τ ⦆ (succ n) ⟩ ∘ π∞ n) ρ ⦆ i ⊑⟨ 𝓓 i ⟩[ u₃ i ]
⦅ [ 𝓓∞ , 𝓓∞ ]⟨ ε-exp-family τ n ⟩ ρ ⦆ i ∎⟨ 𝓓 i ⟩
where
u₁ = reflexivity 𝓓∞ ([ 𝓓∞ , 𝓓∞ ]⟨ ε-exp-family σ n ⟩ ρ)
u₂ = monotone-if-continuous (𝓓 n) 𝓓∞ (ε∞' n)
([ 𝓓 n , 𝓓 n ]⟨ ⦅ σ ⦆ (succ n) ⟩ (π∞ n ρ))
([ 𝓓 n , 𝓓 n ]⟨ ⦅ τ ⦆ (succ n) ⟩ (π∞ n ρ))
(l (succ n) (π∞ n ρ))
u₃ = reflexivity 𝓓∞ ([ 𝓓∞ , 𝓓∞ ]⟨ ε-exp-family τ n ⟩ ρ)
\end{code}
Finally, we have established enough material to prove that ε-exp∞ is the inverse
of π-exp∞.
\begin{code}
ε-exp∞-section-of-π-exp∞ : π-exp∞ ∘ ε-exp∞ ∼ id
ε-exp∞-section-of-π-exp∞ σ =
π-exp∞ (ε-exp∞ σ) ＝⟨ ap π-exp∞ (ε-exp∞-alt σ) ⟩
π-exp∞ (∐ (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞) δ₁) ＝⟨ e₁ ⟩
∐ 𝓓∞ {ℕ} {λ n → (π-exp∞ ∘ ε-exp-family σ) n} δ₂ ＝⟨ ∐-family-＝ 𝓓∞ p δ₂ ⟩
∐ 𝓓∞ {ℕ} {λ n → ∐ 𝓓∞ {ℕ} {λ m → f n m} (δ₃ n)} δ₄ ＝⟨ e₂ ⟩
∐ 𝓓∞ {ℕ} {λ n → ε∞ n (⦅ σ ⦆ n)} δ₅ ＝⟨ (∐-of-ε∞s σ) ⁻¹ ⟩
σ ∎
where
f : ℕ → ℕ → ⟨ 𝓓∞ ⟩
f n m = π-exp-family (ε-exp-family σ n) m
δ₁ : is-Directed (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞) (ε-exp-family σ)
δ₁ = ε-exp-family-is-directed σ
δ₂ : is-Directed 𝓓∞ (π-exp∞ ∘ ε-exp-family σ)
δ₂ = image-is-directed' (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞) 𝓓∞ π-exp∞' δ₁
δ₃ : (n : ℕ) → is-Directed 𝓓∞ (π-exp-family (ε-exp-family σ n))
δ₃ n = π-exp-family-is-directed (ε-exp-family σ n)
p : π-exp∞ ∘ ε-exp-family σ ＝ λ n → ∐ 𝓓∞ (δ₃ n)
p = dfunext fe (λ n → π-exp∞-alt (ε-exp-family σ n))
δ₄ : is-Directed 𝓓∞ (λ n → ∐ 𝓓∞ (δ₃ n))
δ₄ = transport (is-Directed 𝓓∞) p δ₂
δ₅ : is-Directed 𝓓∞ (ε∞-family σ)
δ₅ = ε∞-family-is-directed σ
e₁ = continuous-∐-＝ (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞) 𝓓∞ π-exp∞' δ₁
e₂ = antisymmetry 𝓓∞ (∐ 𝓓∞ δ₄) (∐ 𝓓∞ δ₅) l₁ l₂
where
r : (n : ℕ) → f n n ＝ ε∞-family σ (succ n)
r n = ap (ε∞ (succ n)) γ
where
γ : π-exp (succ n) (ε-exp-family σ n) ＝ ⦅ σ ⦆ (succ n)
γ = to-continuous-function-＝ (𝓓 n) (𝓓 n) ψ
where
σ' : ⟨ 𝓓 n ⟩ → ⟨ 𝓓 n ⟩
σ' = [ 𝓓 n , 𝓓 n ]⟨ ⦅ σ ⦆ (succ n) ⟩
ψ : π∞ n ∘ ε∞ n ∘ σ' ∘ π∞ n ∘ ε∞ n ∼ σ'
ψ x = (π∞ n ∘ ε∞ n ∘ σ' ∘ π∞ n ∘ ε∞ n) x ＝⟨ p₁ ⟩
(σ' ∘ π∞ n ∘ ε∞ n) x ＝⟨ p₂ ⟩
σ' x ∎
where
p₁ = ε∞-section-of-π∞ (σ' (π∞ n (ε∞ n x)))
p₂ = ap σ' (ε∞-section-of-π∞ x)
l₁ : ∐ 𝓓∞ δ₄ ⊑⟨ 𝓓∞ ⟩ ∐ 𝓓∞ δ₅
l₁ = ∐-is-lowerbound-of-upperbounds 𝓓∞ δ₄ (∐ 𝓓∞ δ₅) γ
where
γ : is-upperbound (underlying-order 𝓓∞) (∐ 𝓓∞ δ₅) (λ n → ∐ 𝓓∞ (δ₃ n))
γ n = ∐-is-lowerbound-of-upperbounds 𝓓∞ (δ₃ n) (∐ 𝓓∞ δ₅) ψ
where
ψ : is-upperbound (underlying-order 𝓓∞) (∐ 𝓓∞ δ₅) (f n)
ψ m i = ⦅ f n m ⦆ i ⊑⟨ 𝓓 i ⟩[ u₁ i ]
⦅ f (n +' m) m ⦆ i ⊑⟨ 𝓓 i ⟩[ u₂ i ]
⦅ f (n +' m) (n +' m) ⦆ i ⊑⟨ 𝓓 i ⟩[ u₃ i ]
⦅ ε∞-family σ (succ (n +' m)) ⦆ i ⊑⟨ 𝓓 i ⟩[ u₄ i ]
⦅ ∐ 𝓓∞ δ₅ ⦆ i ∎⟨ 𝓓 i ⟩
where
u₁ = π-exp-family-is-monotone'
(ε-exp-family σ n) (ε-exp-family σ (n +' m))
(ε-exp-family-is-monotone σ (≤-+ n m))
u₂ = π-exp-family-is-monotone (ε-exp-family σ (n +' m)) (≤-+' n m)
u₃ = ＝-to-⊑ 𝓓∞ (r (n +' m))
u₄ = ∐-is-upperbound 𝓓∞ δ₅ (succ (n +' m))
l₂ : ∐ 𝓓∞ δ₅ ⊑⟨ 𝓓∞ ⟩ ∐ 𝓓∞ δ₄
l₂ = ∐-is-lowerbound-of-upperbounds 𝓓∞ δ₅ (∐ 𝓓∞ δ₄) γ
where
γ : is-upperbound (underlying-order 𝓓∞) (∐ 𝓓∞ δ₄) (ε∞-family σ)
γ n i =
⦅ ε∞-family σ n ⦆ i ⊑⟨ 𝓓 i ⟩[ u i ]
⦅ ε∞-family σ (succ n) ⦆ i ⊑⟨ 𝓓 i ⟩[ ＝-to-⊒ 𝓓∞ (r n) i ]
⦅ f n n ⦆ i ⊑⟨ 𝓓 i ⟩[ ∐-is-upperbound 𝓓∞ (δ₃ n) n i ]
⦅ ∐ 𝓓∞ (δ₃ n) ⦆ i ⊑⟨ 𝓓 i ⟩[ ∐-is-upperbound 𝓓∞ δ₄ n i ]
⦅ ∐ 𝓓∞ δ₄ ⦆ i ∎⟨ 𝓓 i ⟩
where
u = ε∞-family-is-monotone σ n (succ n) (≤-succ n)
π-exp∞-section-of-ε-exp∞ : ε-exp∞ ∘ π-exp∞ ∼ id
π-exp∞-section-of-ε-exp∞ φ =
ε-exp∞ (π-exp∞ φ) ＝⟨ e₁ ⟩
ε-exp∞ (∐ 𝓓∞ δ₁) ＝⟨ e₂ ⟩
∐ 𝓔 {ℕ} {λ n → (ε-exp∞ ∘ π-exp-family φ) n} δ₂ ＝⟨ e₃ ⟩
∐ 𝓔 {ℕ} {λ n → ∐ 𝓔 {ℕ} {λ m → f' n m} (δ₃ n)} δ₄ ＝⟨ e₄ ⟩
∐ 𝓔 {ℕ} {λ n → f' n n} δ₅ ＝⟨ e₅ ⟩
∐ 𝓔 {ℕ} {λ n → g' n n} δ₆ ＝⟨ e₆ ⟩
DCPO-∘₃ 𝓓∞ 𝓓∞ 𝓓∞ 𝓓∞ s φ s ＝⟨ e₇ ⟩
φ ∎
where
𝓔 : DCPO {𝓤₁} {𝓤₁}
𝓔 = 𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞
ϕ : ⟨ 𝓓∞ ⟩ → ⟨ 𝓓∞ ⟩
ϕ = [ 𝓓∞ , 𝓓∞ ]⟨ φ ⟩
f' : ℕ → ℕ → ⟨ 𝓔 ⟩
f' n m = ε-exp-family (π-exp-family φ n) m
f : ℕ → ℕ → ⟨ 𝓓∞ ⟩ → ⟨ 𝓓∞ ⟩
f n m = [ 𝓓∞ , 𝓓∞ ]⟨ f' n m ⟩
f'-mon : (n₁ n₂ m₁ m₂ : ℕ) → n₁ ≤ n₂ → m₁ ≤ m₂ → f' n₁ m₁ ⊑⟨ 𝓔 ⟩ f' n₂ m₂
f'-mon n₁ n₂ m₁ m₂ lₙ lₘ σ i = ⦅ f n₁ m₁ σ ⦆ i ⊑⟨ 𝓓 i ⟩[ u₁ i ]
⦅ f n₂ m₁ σ ⦆ i ⊑⟨ 𝓓 i ⟩[ u₂ i ]
⦅ f n₂ m₂ σ ⦆ i ∎⟨ 𝓓 i ⟩
where
u₁ = ε-exp-family-is-monotone' (π-exp-family φ n₁) (π-exp-family φ n₂)
(π-exp-family-is-monotone φ lₙ) σ
u₂ = ε-exp-family-is-monotone (π-exp-family φ n₂) lₘ σ
g' : ℕ → ℕ → ⟨ 𝓔 ⟩
g' n m = DCPO-∘₃ 𝓓∞ 𝓓∞ 𝓓∞ 𝓓∞ (ε∞π∞-family m) φ (ε∞π∞-family n)
g : ℕ → ℕ → ⟨ 𝓓∞ ⟩ → ⟨ 𝓓∞ ⟩
g n m = [ 𝓓∞ , 𝓓∞ ]⟨ g' n m ⟩
g'-mon : (n₁ n₂ m₁ m₂ : ℕ) → n₁ ≤ n₂ → m₁ ≤ m₂ → g' n₁ m₁ ⊑⟨ 𝓔 ⟩ g' n₂ m₂
g'-mon n₁ n₂ m₁ m₂ lₙ lₘ σ i = ⦅ g n₁ m₁ σ ⦆ i ⊑⟨ 𝓓 i ⟩[ u₁ i ]
⦅ g n₂ m₁ σ ⦆ i ⊑⟨ 𝓓 i ⟩[ u₂ i ]
⦅ g n₂ m₂ σ ⦆ i ∎⟨ 𝓓 i ⟩
where
u₁ = ε∞π∞-family-is-monotone lₙ ((ϕ ∘ ε∞ m₁ ∘ π∞ m₁) σ)
u₂ = monotone-if-continuous 𝓓∞ 𝓓∞ (ε∞π∞-family n₂)
((ϕ ∘ ε∞ m₁ ∘ π∞ m₁) σ) ((ϕ ∘ ε∞ m₂ ∘ π∞ m₂) σ)
(monotone-if-continuous 𝓓∞ 𝓓∞ φ
(ε∞ m₁ (π∞ m₁ σ)) (ε∞ m₂ (π∞ m₂ σ))
(ε∞π∞-family-is-monotone lₘ σ))
q : (λ n → f' n n) ＝ (λ n → g' n n)
q = dfunext fe γ
where
γ : (λ n → f' n n) ∼ (λ n → g' n n)
γ n = to-continuous-function-＝ 𝓓∞ 𝓓∞ γ'
where
γ' : f n n ∼ g n n
γ' σ =
f n n σ ＝⟨ refl ⟩
(ε∞ n ∘ [ 𝓓 n , 𝓓 n ]⟨ π∞ (succ n) (ε∞ (succ n) ψ) ⟩ ∘ π∞ n) σ ＝⟨ q' ⟩
(ε∞ n ∘ [ 𝓓 n , 𝓓 n ]⟨ ψ ⟩ ∘ π∞ n) σ ＝⟨ refl ⟩
(ε∞ n ∘ π∞ n ∘ ϕ ∘ ε∞ n ∘ π∞ n) σ ＝⟨ refl ⟩
g n n σ ∎
where
ψ : DCPO[ 𝓓 n , 𝓓 n ]
ψ = DCPO-∘₃ (𝓓 n) 𝓓∞ 𝓓∞ (𝓓 n) (ε∞' n) φ (π∞' n)
q' = ap (λ - → (ε∞ n ∘ [ 𝓓 n , 𝓓 n ]⟨ - ⟩ ∘ π∞ n) σ)
(ε∞-section-of-π∞ ψ)
s : ⟨ 𝓔 ⟩
s = ∐ 𝓔 ε∞π∞-family-is-directed
δ₁ = π-exp-family-is-directed φ
δ₂ = image-is-directed' 𝓓∞ 𝓔 ε-exp∞' δ₁
δ₃ : (n : ℕ) → is-Directed 𝓔 (ε-exp-family (π-exp-family φ n))
δ₃ n = ε-exp-family-is-directed (π-exp-family φ n)
p : ε-exp∞ ∘ π-exp-family φ ＝ (λ n → ∐ 𝓔 (δ₃ n))
p = dfunext fe (λ n → ε-exp∞-alt (π-exp-family φ n))
δ₄ : is-Directed 𝓔 (λ n → ∐ 𝓔 (δ₃ n))
δ₄ = (transport (is-Directed 𝓔) p δ₂)
δ₅ : is-Directed 𝓔 (λ n → f' n n)
δ₅ = ∣ 0 ∣ , δ₅'
where
δ₅' : is-semidirected (underlying-order 𝓔) (λ n → f' n n)
δ₅' n m = ∣ n +' m , uₙ , uₘ ∣
where
uₙ : f' n n ⊑⟨ 𝓔 ⟩ f' (n +' m) (n +' m)
uₙ = f'-mon n (n +' m) n (n +' m) (≤-+ n m) (≤-+ n m)
uₘ : f' m m ⊑⟨ 𝓔 ⟩ f' (n +' m) (n +' m)
uₘ = f'-mon m (n +' m) m (n +' m) (≤-+' n m) (≤-+' n m)
δ₆ : is-Directed 𝓔 (λ n → g' n n)
δ₆ = transport (is-Directed 𝓔) q δ₅
e₁ = ap ε-exp∞ (π-exp∞-alt φ)
e₂ = continuous-∐-＝ 𝓓∞ 𝓔 ε-exp∞' δ₁
e₃ = ∐-family-＝ 𝓔 p δ₂
e₅ = ∐-family-＝ 𝓔 q δ₅
e₄ = antisymmetry 𝓔 (∐ 𝓔 δ₄) (∐ 𝓔 δ₅) l₁ l₂
where
l₁ : ∐ 𝓔 δ₄ ⊑⟨ 𝓔 ⟩ ∐ 𝓔 δ₅
l₁ = ∐-is-lowerbound-of-upperbounds 𝓔 δ₄ (∐ 𝓔 δ₅) γ
where
γ : is-upperbound (underlying-order 𝓔) (∐ 𝓔 δ₅) (λ n → ∐ 𝓔 (δ₃ n))
γ n = ∐-is-lowerbound-of-upperbounds 𝓔 (δ₃ n) (∐ 𝓔 δ₅) γ'
where
γ' : is-upperbound (underlying-order 𝓔) (∐ 𝓔 δ₅) (λ m → f' n m)
γ' m = transitivity 𝓔 (f' n m) (f' (n +' m) (n +' m)) (∐ 𝓔 δ₅)
(f'-mon n (n +' m) m (n +' m) (≤-+ n m) (≤-+' n m))
(∐-is-upperbound 𝓔 δ₅ (n +' m))
l₂ : ∐ 𝓔 δ₅ ⊑⟨ 𝓔 ⟩ ∐ 𝓔 δ₄
l₂ = ∐-is-lowerbound-of-upperbounds 𝓔 δ₅ (∐ 𝓔 δ₄) γ
where
γ : is-upperbound (underlying-order 𝓔) (∐ 𝓔 δ₄) (λ n → f' n n)
γ n = transitivity 𝓔 (f' n n) (∐ 𝓔 (δ₃ n)) (∐ 𝓔 δ₄)
(∐-is-upperbound 𝓔 (δ₃ n) n)
(∐-is-upperbound 𝓔 δ₄ n)
e₇ = DCPO-∘₃ 𝓓∞ 𝓓∞ 𝓓∞ 𝓓∞ s φ s ＝⟨ p₁ ⟩
DCPO-∘₃ 𝓓∞ 𝓓∞ 𝓓∞ 𝓓∞ ι φ ι ＝⟨ p₂ ⟩
φ ∎
where
ι : DCPO[ 𝓓∞ , 𝓓∞ ]
ι = id , id-is-continuous 𝓓∞
p₁ = ap₂ (λ -₁ -₂ → DCPO-∘₃ 𝓓∞ 𝓓∞ 𝓓∞ 𝓓∞ -₁ φ -₂) e e
where
e : s ＝ ι
e = ∐-of-ε∞π∞s-is-id
p₂ = to-continuous-function-＝ 𝓓∞ 𝓓∞ (λ σ → 𝓻𝓮𝒻𝓵 (ϕ σ))
e₆ = antisymmetry 𝓔 (∐ 𝓔 δ₆) (DCPO-∘₃ 𝓓∞ 𝓓∞ 𝓓∞ 𝓓∞ s φ s) l₁ l₂
where
s₁ : ⟨ 𝓓∞ ⟩ → ⟨ 𝓓∞ ⟩
s₁ = [ 𝓓∞ , 𝓓∞ ]⟨ s ⟩
l₁ : ∐ 𝓔 δ₆ ⊑⟨ 𝓔 ⟩ DCPO-∘₃ 𝓓∞ 𝓓∞ 𝓓∞ 𝓓∞ s φ s
l₁ = ∐-is-lowerbound-of-upperbounds 𝓔 δ₆ (DCPO-∘₃ 𝓓∞ 𝓓∞ 𝓓∞ 𝓓∞ s φ s) γ
where
γ : is-upperbound (underlying-order 𝓔) (DCPO-∘₃ 𝓓∞ 𝓓∞ 𝓓∞ 𝓓∞ s φ s)
(λ n → g' n n)
γ n σ i = ⦅ g n n σ ⦆ i ⊑⟨ 𝓓 i ⟩[ u₁ i ]
⦅ (ε∞ n ∘ π∞ n ∘ ϕ ∘ ε∞ n ∘ π∞ n) σ ⦆ i ⊑⟨ 𝓓 i ⟩[ u₂ i ]
⦅ (s₁ ∘ ϕ) (ε∞ n (π∞ n σ)) ⦆ i ⊑⟨ 𝓓 i ⟩[ u₃ i ]
⦅ (s₁ ∘ ϕ ∘ s₁) σ ⦆ i ∎⟨ 𝓓 i ⟩
where
δ : is-Directed 𝓓∞ (pointwise-family 𝓓∞ 𝓓∞ ε∞π∞-family
((ϕ ∘ ε∞ n ∘ π∞ n) σ))
δ = pointwise-family-is-directed 𝓓∞ 𝓓∞ ε∞π∞-family
ε∞π∞-family-is-directed ((ϕ ∘ ε∞ n ∘ π∞ n) σ)
δ' : is-Directed 𝓓∞ (pointwise-family 𝓓∞ 𝓓∞ ε∞π∞-family σ)
δ' = pointwise-family-is-directed 𝓓∞ 𝓓∞ ε∞π∞-family
ε∞π∞-family-is-directed σ
u₁ = reflexivity 𝓓∞ (g n n σ)
u₂ = ∐-is-upperbound 𝓓∞ δ n
u₃ = monotone-if-continuous 𝓓∞ 𝓓∞ (DCPO-∘ 𝓓∞ 𝓓∞ 𝓓∞ φ s)
(ε∞ n (π∞ n σ)) (s₁ σ) (∐-is-upperbound 𝓓∞ δ' n)
l₂ : DCPO-∘₃ 𝓓∞ 𝓓∞ 𝓓∞ 𝓓∞ s φ s ⊑⟨ 𝓔 ⟩ ∐ 𝓔 δ₆
l₂ σ = ∐-is-lowerbound-of-upperbounds 𝓓∞ δ ([ 𝓓∞ , 𝓓∞ ]⟨ ∐ 𝓔 δ₆ ⟩ σ) γ
where
δ : is-Directed 𝓓∞ (pointwise-family 𝓓∞ 𝓓∞ ε∞π∞-family (ϕ (s₁ σ)))
δ = pointwise-family-is-directed 𝓓∞ 𝓓∞ ε∞π∞-family
ε∞π∞-family-is-directed (ϕ (s₁ σ))
γ : is-upperbound (underlying-order 𝓓∞) ([ 𝓓∞ , 𝓓∞ ]⟨ ∐ 𝓔 δ₆ ⟩ σ)
(pointwise-family 𝓓∞ 𝓓∞ ε∞π∞-family (ϕ (s₁ σ)))
γ n i =
⦅ (ε∞ n ∘ π∞ n ∘ ϕ ∘ s₁) σ ⦆ i ⊑⟨ 𝓓 i ⟩[ continuous-∐-⊑ 𝓓∞ 𝓓∞ h δ₁' i ]
⦅ ∐ 𝓓∞ δ₂' ⦆ i ⊑⟨ 𝓓 i ⟩[ γ₁ i ]
⦅ [ 𝓓∞ , 𝓓∞ ]⟨ ∐ 𝓔 δ₆ ⟩ σ ⦆ i ∎⟨ 𝓓 i ⟩
where
h : DCPO[ 𝓓∞ , 𝓓∞ ]
h = DCPO-∘₃ 𝓓∞ 𝓓∞ (𝓓 n) 𝓓∞ φ (π∞' n) (ε∞' n)
δ₁' : is-Directed 𝓓∞ (pointwise-family 𝓓∞ 𝓓∞ ε∞π∞-family σ)
δ₁' = pointwise-family-is-directed 𝓓∞ 𝓓∞ ε∞π∞-family
ε∞π∞-family-is-directed σ
δ₂' : is-Directed 𝓓∞
(λ m → (ε∞ n ∘ π∞ n ∘ ϕ ∘ ε∞ m ∘ π∞ m) σ)
δ₂' = image-is-directed' 𝓓∞ 𝓓∞ h δ₁'
γ₁ : ∐ 𝓓∞ δ₂' ⊑⟨ 𝓓∞ ⟩ [ 𝓓∞ , 𝓓∞ ]⟨ ∐ 𝓔 δ₆ ⟩ σ
γ₁ = ∐-is-lowerbound-of-upperbounds 𝓓∞ δ₂'
([ 𝓓∞ , 𝓓∞ ]⟨ ∐ 𝓔 δ₆ ⟩ σ) γ₂
where
γ₂ : is-upperbound (underlying-order 𝓓∞) ([ 𝓓∞ , 𝓓∞ ]⟨ ∐ 𝓔 δ₆ ⟩ σ)
(λ m → (ε∞ n ∘ π∞ n ∘ ϕ ∘ ε∞ m ∘ π∞ m) σ)
γ₂ m i = ⦅ (ε∞ n ∘ π∞ n ∘ ϕ ∘ ε∞ m ∘ π∞ m) σ ⦆ i ⊑⟨ 𝓓 i ⟩[ u₁ i ]
⦅ g n m σ ⦆ i ⊑⟨ 𝓓 i ⟩[ u₂ i ]
⦅ g (n +' m) m σ ⦆ i ⊑⟨ 𝓓 i ⟩[ u₃ i ]
⦅ g (n +' m) (n +' m) σ ⦆ i ⊑⟨ 𝓓 i ⟩[ u₄ i ]
⦅ [ 𝓓∞ , 𝓓∞ ]⟨ ∐ 𝓔 δ₆ ⟩ σ ⦆ i ∎⟨ 𝓓 i ⟩
where
δ₃' : is-Directed 𝓓∞ (pointwise-family 𝓓∞ 𝓓∞ (λ k → g' k k) σ)
δ₃' = pointwise-family-is-directed 𝓓∞ 𝓓∞ (λ k → g' k k) δ₆ σ
u₁ = reflexivity 𝓓∞ (g n m σ)
u₂ = g'-mon n (n +' m) m m (≤-+ n m) (≤-refl m) σ
u₃ = g'-mon (n +' m) (n +' m) m (n +' m)
(≤-refl (n +' m)) (≤-+' n m) σ
u₄ = ∐-is-upperbound 𝓓∞ δ₃' (n +' m)
\end{code}
Hence, D∞ is isomorphic (as a dcpo) to its self-exponential (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞).
\begin{code}
𝓓∞-isomorphic-to-its-self-exponential : 𝓓∞ ≃ᵈᶜᵖᵒ (𝓓∞ ⟹ᵈᶜᵖᵒ 𝓓∞)
𝓓∞-isomorphic-to-its-self-exponential =
ε-exp∞ , π-exp∞ , ε-exp∞-section-of-π-exp∞ , π-exp∞-section-of-ε-exp∞ ,
ε-exp∞-is-continuous , π-exp∞-is-continuous
\end{code}
But actually we want D∞ to be a pointed dcpo and we want it to be isomorphic to
the pointed exponential (𝓓∞⊥ ⟹ᵈᶜᵖᵒ⊥ 𝓓∞⊥), which we prove now.
\begin{code}
π-is-strict : (n : ℕ) → is-strict (𝓓⊥ (succ n)) (𝓓⊥ n) (π n)
π-is-strict zero = refl
π-is-strict (succ n) = to-continuous-function-＝ (𝓓 n) (𝓓 n) γ
where
f' : ⟨ 𝓓 (succ (succ n)) ⟩
f' = ⊥ (𝓓⊥ (succ (succ n)))
f : ⟨ 𝓓 (succ n) ⟩ → ⟨ 𝓓 (succ n) ⟩
f = [ 𝓓 (succ n) , 𝓓 (succ n) ]⟨ f' ⟩
γ : [ 𝓓 n , 𝓓 n ]⟨ π (succ n) f' ⟩ ∼ [ 𝓓 n , 𝓓 n ]⟨ ⊥ (𝓓⊥ (succ n)) ⟩
γ x = [ 𝓓 n , 𝓓 n ]⟨ π (succ n) f' ⟩ x ＝⟨ refl ⟩
(π n ∘ f ∘ ε n) x ＝⟨ refl ⟩
π n (⊥ (𝓓⊥ (succ n))) ＝⟨ IH ⟩
[ 𝓓 n , 𝓓 n ]⟨ ⊥ (𝓓⊥ (succ n)) ⟩ x ∎
where
IH : π n (⊥ (𝓓⊥ (succ n))) ＝ ⊥ (𝓓⊥ n)
IH = π-is-strict n
π⁺-is-strict-helper : (n m k : ℕ) (p : n +' k ＝ m)
→ is-strict (𝓓⊥ m) (𝓓⊥ n) (π⁺-helper n m k p)
π⁺-is-strict-helper n n zero refl = refl
π⁺-is-strict-helper n m (succ k) refl =
π⁺-helper n m (succ k) refl (⊥ (𝓓⊥ m)) ＝⟨ refl ⟩
π⁺-helper n (n +' k) k refl (π (n +' k) (⊥ (𝓓⊥ m))) ＝⟨ q ⟩
π⁺-helper n (n +' k) k refl (⊥ (𝓓⊥ (n +' k))) ＝⟨ IH ⟩
⊥ (𝓓⊥ n) ∎
where
q = ap (π⁺-helper n (n +' k) k refl) (π-is-strict (n +' k))
IH = π⁺-is-strict-helper n (n +' k) k refl
π⁺-is-strict : (n m : ℕ) (l : n ≤ m) → is-strict (𝓓⊥ m) (𝓓⊥ n) (π⁺ l)
π⁺-is-strict n m l = π⁺-is-strict-helper n m k p
where
k : ℕ
k = pr₁ (subtraction' n m l)
p : n +' k ＝ m
p = pr₂ (subtraction' n m l)
𝓓∞-has-least : has-least (underlying-order 𝓓∞)
𝓓∞-has-least = (σ⊥ , p) , q
where
σ⊥ : (n : ℕ) → ⟨ 𝓓 n ⟩
σ⊥ n = ⊥ (𝓓⊥ n)
p : (n m : ℕ) (l : n ≤ m) → π⁺ l (σ⊥ m) ＝ σ⊥ n
p = π⁺-is-strict
q : is-least (underlying-order 𝓓∞) (σ⊥ , p)
q τ n = ⊥-is-least (𝓓⊥ n) (⦅ τ ⦆ n)
𝓓∞⊥ : DCPO⊥ {𝓤₁} {𝓤₁}
𝓓∞⊥ = 𝓓∞ , 𝓓∞-has-least
𝓓∞⊥-strict-isomorphic-to-its-self-exponential : 𝓓∞⊥ ≃ᵈᶜᵖᵒ⊥ (𝓓∞⊥ ⟹ᵈᶜᵖᵒ⊥ 𝓓∞⊥)
𝓓∞⊥-strict-isomorphic-to-its-self-exponential =
≃ᵈᶜᵖᵒ-to-≃ᵈᶜᵖᵒ⊥ 𝓓∞⊥ (𝓓∞⊥ ⟹ᵈᶜᵖᵒ⊥ 𝓓∞⊥) 𝓓∞-isomorphic-to-its-self-exponential
\end{code}
Of course, for the above to be interesting, we want 𝓓∞ to be nontrivial, i.e. it
has an element σ₀ such that σ₀ is not the least element, which we prove now.
\begin{code}
σ₀ : ⟨ 𝓓∞ ⟩
σ₀ = σ , p
where
x₀ : ⟨ 𝓓 0 ⟩
x₀ = 𝟙 , id , 𝟙-is-prop
σ : (n : ℕ) → ⟨ 𝓓 n ⟩
σ n = ε⁺ {0} {n} ⋆ x₀
p : (n m : ℕ) (l : n ≤ m) → π⁺ l (σ m) ＝ σ n
p n m l = π⁺ {n} {m} l (ε⁺ {0} {m} ⋆ x₀) ＝⟨ e₁ ⟩
(π⁺ {n} {m} l ∘ ε⁺ {n} {m} l ∘ ε⁺ {0} {n} ⋆) x₀ ＝⟨ e₂ ⟩
ε⁺ {0} {n} ⋆ x₀ ∎
where
e₁ = ap (π⁺ {n} {m} l) ((ε⁺-comp ⋆ l x₀) ⁻¹)
e₂ = ε⁺-section-of-π⁺ l (ε⁺ {0} {n} ⋆ x₀)
𝓓∞⊥-is-nontrivial : σ₀ ≠ ⊥ 𝓓∞⊥
𝓓∞⊥-is-nontrivial e = 𝟘-is-not-𝟙 (γ ⁻¹)
where
e₀ : ⦅ σ₀ ⦆ 0 ＝ ⊥ (𝓓⊥ 0)
e₀ = ap (λ - → ⦅ - ⦆ 0) e
γ : 𝟙 ＝ 𝟘
γ = ap pr₁ e₀
\end{code}
Finally, we prove that 𝓓∞ is an algebraic dcpo. We use that our starting dcpo is
sup-complete and has a small compact basis, and that both these things are closed
under taking exponentials.
\begin{code}
open import DomainTheory.Basics.SupComplete pt fe 𝓤₀
open import DomainTheory.BasesAndContinuity.Bases pt fe 𝓤₀
open import DomainTheory.BasesAndContinuity.Continuity pt fe 𝓤₀
open import DomainTheory.BasesAndContinuity.StepFunctions pt fe 𝓤₀
open import DomainTheory.Lifting.LiftingSetAlgebraic pt pe fe 𝓤₀
𝓓s-are-sup-complete : (n : ℕ) → is-sup-complete (𝓓 n)
𝓓s-are-sup-complete zero = lifting-of-prop-is-sup-complete 𝟙-is-prop
𝓓s-are-sup-complete (succ n) = exponential-is-sup-complete (𝓓 n) (𝓓 n)
(𝓓s-are-sup-complete n)
𝓓∞-has-specified-small-compact-basis : has-specified-small-compact-basis 𝓓∞
𝓓∞-has-specified-small-compact-basis = 𝓓∞-has-small-compact-basis γ
where
γ : (n : ℕ) → has-specified-small-compact-basis (𝓓 n)
γ zero = 𝓛-has-specified-small-compact-basis (props-are-sets 𝟙-is-prop)
γ (succ n) = exponential-has-specified-small-compact-basis
(𝓓 n) (𝓓⊥ n)
(𝓓s-are-sup-complete n)
B B β β β-is-compact-small-basis β-is-compact-small-basis
pe
where
IH : has-specified-small-compact-basis (𝓓 n)
IH = γ n
B : 𝓤₀ ̇
B = pr₁ IH
β : B → ⟨ 𝓓 n ⟩
β = pr₁ (pr₂ IH)
β-is-compact-small-basis : is-small-compact-basis (𝓓 n) β
β-is-compact-small-basis = pr₂ (pr₂ IH)
𝓓∞-is-algebraic-dcpo : is-algebraic-dcpo 𝓓∞
𝓓∞-is-algebraic-dcpo =
is-algebraic-dcpo-if-unspecified-small-compact-basis 𝓓∞
∣ 𝓓∞-has-specified-small-compact-basis ∣
\end{code}