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 =
 {- I would use the โŠ‘โŸจ ๐““ (succ n) โŸฉ[ ? ] syntax here, but Agda has trouble
    figuring out some implicit arguments. -}
 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))
{-
 (ฮต n โˆ˜ ฯ€ n โˆ˜ f โˆ˜ ฮต n โˆ˜ ฯ€ n) x โŠ‘โŸจ ๐““ (succ n) โŸฉ[ IH (f (ฮต n (ฯ€ n x)))     ]
 f (ฮต n (ฯ€ n x))               โŠ‘โŸจ ๐““ (succ n) โŸฉ[ m (ฮต n (ฯ€ n x)) x (IH x) ]
 f x                           โˆŽโŸจ ๐““ (succ n) โŸฉ -}
  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}