Brendan Hart 2019-2020

Addition by Tom de Jong in July 2024.

\begin{code}

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

open import MLTT.Spartan
open import UF.PropTrunc
open import UF.FunExt

module DomainTheory.Basics.Products
        (pt : propositional-truncations-exist)
        (fe : βˆ€ {𝓀 π“₯} β†’ funext 𝓀 π“₯)
       where

open PropositionalTruncation pt

open import OrderedTypes.Poset fe
open import UF.Base
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.Sets

open PosetAxioms

\end{code}

First, let's define the product of two DCPOs.

\begin{code}

module DcpoProductsGeneral
        (π“₯ : Universe)
       where

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

 module _ {D : 𝓀 Μ‡ } {E : 𝓀' Μ‡ } where

   _βŠ‘-Γ—_ : (D β†’ D β†’ 𝓣 Μ‡ )
         β†’ (E β†’ E β†’ 𝓣' Μ‡ )
         β†’ (D Γ— E β†’ D Γ— E β†’ 𝓣 βŠ” 𝓣' Μ‡ )
   _βŠ‘-Γ—_ _βŠ‘β‚_ _βŠ‘β‚‚_ (a , b) (c , d) = (a βŠ‘β‚ c) Γ— (b βŠ‘β‚‚ d)

   prβ‚βˆ˜Ξ±-is-directed : {I : π“₯ Μ‡ }
                     β†’ {Ξ± : I β†’ D Γ— E}
                     β†’ (_βŠ‘β‚_ : D β†’ D β†’ 𝓣 Μ‡ )
                     β†’ (_βŠ‘β‚‚_ : E β†’ E β†’ 𝓣' Μ‡ )
                     β†’ is-directed (_βŠ‘β‚_ βŠ‘-Γ— _βŠ‘β‚‚_) Ξ±
                     β†’ is-directed _βŠ‘β‚_ (pr₁ ∘ Ξ±)
   prβ‚βˆ˜Ξ±-is-directed {_} {_} {I} {Ξ±} _βŠ‘β‚_ _βŠ‘β‚‚_ Ξ΄ =
    inhabited-if-directed (_βŠ‘β‚_ βŠ‘-Γ— _βŠ‘β‚‚_) Ξ± Ξ΄ , o
     where
      o : (i j : I)
        β†’ βˆƒ k κž‰ I , ((pr₁ ∘ Ξ±) i βŠ‘β‚ (pr₁ ∘ Ξ±) k Γ—
                     (pr₁ ∘ Ξ±) j βŠ‘β‚ (pr₁ ∘ Ξ±) k)
      o i j = βˆ₯βˆ₯-functor
               (Ξ» (a , (b , _) , c , _) β†’ a , b , c)
               (semidirected-if-directed (_βŠ‘β‚_ βŠ‘-Γ— _βŠ‘β‚‚_) Ξ± Ξ΄ i j)

   prβ‚‚βˆ˜Ξ±-is-directed : {I : π“₯ Μ‡ }
                     β†’ {Ξ± : I β†’ D Γ— E}
                     β†’ (_βŠ‘β‚_ : D β†’ D β†’ 𝓣 Μ‡ )
                     β†’ (_βŠ‘β‚‚_ : E β†’ E β†’ 𝓣' Μ‡ )
                     β†’ is-directed (_βŠ‘β‚_ βŠ‘-Γ— _βŠ‘β‚‚_) Ξ±
                     β†’ is-directed _βŠ‘β‚‚_ (prβ‚‚ ∘ Ξ±)
   prβ‚‚βˆ˜Ξ±-is-directed {_} {_} {I} {Ξ±} _βŠ‘β‚_ _βŠ‘β‚‚_ Ξ΄ =
    inhabited-if-directed (_βŠ‘β‚_ βŠ‘-Γ— _βŠ‘β‚‚_) Ξ± Ξ΄ , o
     where
      o : (i j : I)
        β†’ βˆƒ k κž‰ I , ((prβ‚‚ ∘ Ξ±) i βŠ‘β‚‚ (prβ‚‚ ∘ Ξ±) k Γ—
                     (prβ‚‚ ∘ Ξ±) j βŠ‘β‚‚ (prβ‚‚ ∘ Ξ±) k)
      o i j = βˆ₯βˆ₯-functor
               (Ξ» (a , (_  , b) , _ , c) β†’ a , b , c)
               (semidirected-if-directed (_βŠ‘β‚_ βŠ‘-Γ— _βŠ‘β‚‚_) Ξ± Ξ΄ i j)

 infixr 30 _Γ—α΅ˆαΆœα΅–α΅’_

 _Γ—α΅ˆαΆœα΅–α΅’_ : DCPO {𝓀} {𝓣} β†’ DCPO {𝓀'} {𝓣'} β†’ DCPO {𝓀 βŠ” 𝓀'} {𝓣 βŠ” 𝓣'}
 𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔 = (⟨ 𝓓 ⟩ Γ— ⟨ 𝓔 ⟩) ,
             (underlying-order 𝓓) βŠ‘-Γ— (underlying-order 𝓔) ,
             axioms
  where
   axioms : dcpo-axioms (underlying-order 𝓓 βŠ‘-Γ— underlying-order 𝓔)
   axioms = (Γ—-is-set (sethood 𝓓) (sethood 𝓔) , prop , r , t , a) , c
    where
     _βŠ‘π““_ = underlying-order 𝓓
     _βŠ‘π“”_ = underlying-order 𝓔
     _βŠ‘_  = _βŠ‘π““_ βŠ‘-Γ— _βŠ‘π“”_

     prop : is-prop-valued _βŠ‘_
     prop (x₁ , xβ‚‚) (y₁ , yβ‚‚) (a₁ , aβ‚‚) (b₁ , bβ‚‚) =
      to-Γ—-＝
       (prop-valuedness 𝓓 x₁ y₁ a₁ b₁)
       (prop-valuedness 𝓔 xβ‚‚ yβ‚‚ aβ‚‚ bβ‚‚)

     r : is-reflexive _βŠ‘_
     r a = reflexivity 𝓓 (pr₁ a) ,
           reflexivity 𝓔 (prβ‚‚ a)

     t : is-transitive _βŠ‘_
     t (x₁ , xβ‚‚) (y₁ , yβ‚‚) (z₁ , zβ‚‚) (u₁ , uβ‚‚) (v₁ , vβ‚‚) = w₁ , wβ‚‚
      where
       w₁ = x₁ βŠ‘βŸ¨ 𝓓 ⟩[ u₁ ]
            y₁ βŠ‘βŸ¨ 𝓓 ⟩[ v₁ ]
            z₁ ∎⟨ 𝓓 ⟩

       wβ‚‚ = xβ‚‚ βŠ‘βŸ¨ 𝓔 ⟩[ uβ‚‚ ]
            yβ‚‚ βŠ‘βŸ¨ 𝓔 ⟩[ vβ‚‚ ]
            zβ‚‚ ∎⟨ 𝓔 ⟩

     a : is-antisymmetric _βŠ‘_
     a (a , b) (c , d) (a-βŠ‘-c , b-βŠ‘-d) (c-βŠ‘-a , d-βŠ‘-b) =
      to-Γ—-＝
       (antisymmetry 𝓓 a c a-βŠ‘-c c-βŠ‘-a)
       (antisymmetry 𝓔 b d b-βŠ‘-d d-βŠ‘-b)

     c : is-directed-complete _βŠ‘_
     c I Ξ± Ξ΄ = (∐ 𝓓 prβ‚βˆ˜Ξ±-is-dir , ∐ 𝓔 prβ‚‚βˆ˜Ξ±-is-dir) , s
      where
       prβ‚βˆ˜Ξ±-is-dir : is-Directed 𝓓 (pr₁ ∘ Ξ±)
       prβ‚βˆ˜Ξ±-is-dir = prβ‚βˆ˜Ξ±-is-directed _βŠ‘π““_ _βŠ‘π“”_ Ξ΄

       prβ‚‚βˆ˜Ξ±-is-dir : is-Directed 𝓔 (prβ‚‚ ∘ Ξ±)
       prβ‚‚βˆ˜Ξ±-is-dir = prβ‚‚βˆ˜Ξ±-is-directed _βŠ‘π““_ _βŠ‘π“”_ Ξ΄

       s : is-sup _βŠ‘_ (∐ 𝓓 prβ‚βˆ˜Ξ±-is-dir , ∐ 𝓔 prβ‚‚βˆ˜Ξ±-is-dir) Ξ±
       s = is-upper , is-least-upper
        where
         is-upper : is-upperbound _βŠ‘_ (∐ 𝓓 prβ‚βˆ˜Ξ±-is-dir , ∐ 𝓔 prβ‚‚βˆ˜Ξ±-is-dir) Ξ±
         is-upper i = (∐-is-upperbound 𝓓 prβ‚βˆ˜Ξ±-is-dir i ,
                       ∐-is-upperbound 𝓔 prβ‚‚βˆ˜Ξ±-is-dir i)

         is-least-upper : (t : ⟨ 𝓓 ⟩ Γ— ⟨ 𝓔 ⟩)
                        β†’ is-upperbound _βŠ‘_ t Ξ±
                        β†’ _βŠ‘_ (∐ 𝓓 prβ‚βˆ˜Ξ±-is-dir , ∐ 𝓔 prβ‚‚βˆ˜Ξ±-is-dir) t
         is-least-upper t@(x , y) u = lub-of-x , lub-of-y
           where
            x-is-upperbound : is-upperbound _βŠ‘π““_ x (pr₁ ∘ Ξ±)
            x-is-upperbound i = pr₁ (u i)

            y-is-upperbound : is-upperbound _βŠ‘π“”_ y (prβ‚‚ ∘ Ξ±)
            y-is-upperbound i = prβ‚‚ (u i)

            lub-of-x = ∐-is-lowerbound-of-upperbounds 𝓓
                        prβ‚βˆ˜Ξ±-is-dir
                        x
                        x-is-upperbound

            lub-of-y = ∐-is-lowerbound-of-upperbounds
                        𝓔
                        prβ‚‚βˆ˜Ξ±-is-dir
                        y
                        y-is-upperbound
\end{code}

Some useful proofs on products.

\begin{code}

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

   constant-function-is-directed : { I : π“₯ Μ‡ } (h : βˆ₯ I βˆ₯) (d : ⟨ 𝓓 ⟩)
                                 β†’ is-Directed 𝓓 (Ξ» (i : I) β†’ d)
   constant-function-is-directed h d =
    h , Ξ» i j β†’ ∣ i , (reflexivity 𝓓 d , reflexivity 𝓓 d) ∣

   constant-is-∐-of-constant-function : {I : π“₯ Μ‡ }
                                        {d : ⟨ 𝓓 ⟩}
                                        (Ξ΄ : is-Directed 𝓓 (Ξ» (i : I) β†’ d))
                                      β†’ d ＝ ∐ 𝓓 Ξ΄
   constant-is-∐-of-constant-function {I} {d} Ξ΄ = antisymmetry 𝓓 d (∐ 𝓓 Ξ΄) l₁ lβ‚‚
    where
     l₁ : d βŠ‘βŸ¨ 𝓓 ⟩ ∐ 𝓓 Ξ΄
     l₁ = βˆ₯βˆ₯-rec
           (prop-valuedness 𝓓 d (∐ 𝓓 Ξ΄))
           (Ξ» (i : I) β†’ ∐-is-upperbound 𝓓 Ξ΄ i) (pr₁ Ξ΄)

     lβ‚‚ : ∐ 𝓓 Ξ΄ βŠ‘βŸ¨ 𝓓 ⟩ d
     lβ‚‚ = ∐-is-lowerbound-of-upperbounds 𝓓
           Ξ΄
           d
           (Ξ» i β†’ reflexivity 𝓓 d)

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

   prβ‚βˆ˜Ξ±-is-Directed : {I : π“₯ Μ‡ }
                       {Ξ± : I β†’ ⟨ 𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔 ⟩}
                     β†’ is-Directed (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) Ξ±
                     β†’ is-Directed 𝓓 (pr₁ ∘ Ξ±)
   prβ‚βˆ˜Ξ±-is-Directed {I} {Ξ±} Ξ΄ =
    prβ‚βˆ˜Ξ±-is-directed (underlying-order 𝓓) (underlying-order 𝓔) Ξ΄

   prβ‚‚βˆ˜Ξ±-is-Directed : {I : π“₯ Μ‡ }
                       {Ξ± : I β†’ ⟨ 𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔 ⟩}
                     β†’ is-Directed (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) Ξ±
                     β†’ is-Directed 𝓔 (prβ‚‚ ∘ Ξ±)
   prβ‚‚βˆ˜Ξ±-is-Directed = prβ‚‚βˆ˜Ξ±-is-directed (underlying-order 𝓓) (underlying-order 𝓔)

   ⟨pr₁,prβ‚‚βŸ©-is-directed : {I : π“₯ Μ‡ }
                         β†’ {α₁ : I β†’ ⟨ 𝓓 ⟩}
                         β†’ {Ξ±β‚‚ : I β†’ ⟨ 𝓔 ⟩}
                         β†’ is-Directed 𝓓 α₁
                         β†’ is-Directed 𝓔 Ξ±β‚‚
                         β†’ is-Directed (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔)
                            (Ξ» ((i₁ , iβ‚‚) : I Γ— I) β†’ (α₁ i₁ , Ξ±β‚‚ iβ‚‚))

   ⟨pr₁,prβ‚‚βŸ©-is-directed δ₁@(h₁ , s₁) Ξ΄β‚‚@(hβ‚‚ , sβ‚‚) =
    (binary-choice h₁ hβ‚‚) ,
     Ξ» (i₁ , iβ‚‚) (j₁ , jβ‚‚)
       β†’ βˆ₯βˆ₯-functor
          (Ξ» ((a₁ , b₁ , c₁) , (aβ‚‚ , bβ‚‚ , cβ‚‚)) β†’ (a₁ , aβ‚‚) , (b₁ , bβ‚‚) , (c₁ , cβ‚‚))
          (binary-choice (s₁ i₁ j₁) (sβ‚‚ iβ‚‚ jβ‚‚))

   ∐⟨,⟩＝⟨∐,∐⟩ : {I : π“₯ Μ‡ } {Ξ± : I β†’ ⟨ 𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔 ⟩}
               β†’ (Ξ΄ : is-Directed (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) Ξ±)
               β†’ ∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) Ξ΄
               ＝ (∐ 𝓓 (prβ‚βˆ˜Ξ±-is-Directed Ξ΄) , ∐ 𝓔 (prβ‚‚βˆ˜Ξ±-is-Directed Ξ΄))
   ∐⟨,⟩＝⟨∐,∐⟩ {I} {α} δ =
    antisymmetry (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔)
     (∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) Ξ΄)
     (∐ 𝓓 (prβ‚βˆ˜Ξ±-is-Directed Ξ΄) , ∐ 𝓔 (prβ‚‚βˆ˜Ξ±-is-Directed Ξ΄))
     ∐⟨,βŸ©βŠ‘βŸ¨βˆ,∐⟩
     ⟨∐,βˆβŸ©βŠ‘βˆβŸ¨,⟩
     where
       ∐⟨,βŸ©βŠ‘βŸ¨βˆ,∐⟩ : ∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) Ξ΄
                     βŠ‘βŸ¨ 𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔 ⟩
                    (∐ 𝓓 (prβ‚βˆ˜Ξ±-is-Directed Ξ΄) , ∐ 𝓔 (prβ‚‚βˆ˜Ξ±-is-Directed Ξ΄))
       ∐⟨,βŸ©βŠ‘βŸ¨βˆ,∐⟩ = ∐-is-lowerbound-of-upperbounds (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔)
                      Ξ΄
                      (∐ 𝓓 (prβ‚βˆ˜Ξ±-is-Directed Ξ΄) , ∐ 𝓔 (prβ‚‚βˆ˜Ξ±-is-Directed Ξ΄))
                      ∐,∐-is-upperbound
         where
          ∐,∐-is-upperbound : (i : I)
                            β†’ (Ξ± i)
                            βŠ‘βŸ¨ 𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔 ⟩ (∐ 𝓓 (prβ‚βˆ˜Ξ±-is-Directed Ξ΄) ,
                                            ∐ 𝓔 (prβ‚‚βˆ˜Ξ±-is-Directed Ξ΄))
          ∐,∐-is-upperbound i = (∐-is-upperbound 𝓓 (prβ‚βˆ˜Ξ±-is-Directed Ξ΄) i) ,
                                (∐-is-upperbound 𝓔 (prβ‚‚βˆ˜Ξ±-is-Directed Ξ΄) i)

       ⟨∐,βˆβŸ©βŠ‘βˆβŸ¨,⟩ : (∐ 𝓓 (prβ‚βˆ˜Ξ±-is-Directed Ξ΄) , ∐ 𝓔 (prβ‚‚βˆ˜Ξ±-is-Directed Ξ΄))
                  βŠ‘βŸ¨ 𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔 ⟩ (∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) Ξ΄)
       ⟨∐,βˆβŸ©βŠ‘βˆβŸ¨,⟩ = βŠ‘β‚ , βŠ‘β‚‚
         where
          βŠ‘β‚ : (∐ 𝓓 (prβ‚βˆ˜Ξ±-is-Directed Ξ΄)) βŠ‘βŸ¨ 𝓓 ⟩ (pr₁ (∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) Ξ΄))
          βŠ‘β‚ = ∐-is-lowerbound-of-upperbounds 𝓓
                (prβ‚βˆ˜Ξ±-is-Directed Ξ΄)
                (pr₁ (∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) Ξ΄))
                pr₁-∐⟨,⟩-is-upperbound
           where
            pr₁-∐⟨,⟩-is-upperbound : (i : I)
                                   β†’ ((pr₁ ∘ Ξ±) i) βŠ‘βŸ¨ 𝓓 ⟩ (pr₁ (∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) Ξ΄))
            pr₁-∐⟨,⟩-is-upperbound i = pr₁ (∐-is-upperbound (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) Ξ΄ i)

          βŠ‘β‚‚ : ∐ 𝓔 (prβ‚‚βˆ˜Ξ±-is-Directed Ξ΄) βŠ‘βŸ¨ 𝓔 ⟩ prβ‚‚ (∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) Ξ΄)
          βŠ‘β‚‚ = ∐-is-lowerbound-of-upperbounds 𝓔
                (prβ‚‚βˆ˜Ξ±-is-Directed Ξ΄)
                (prβ‚‚ (∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) Ξ΄))
                prβ‚‚-∐⟨,⟩-is-upperbound
           where
            prβ‚‚-∐⟨,⟩-is-upperbound : (i : I)
                                   β†’ ((prβ‚‚ ∘ Ξ±) i) βŠ‘βŸ¨ 𝓔 ⟩ (prβ‚‚ (∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) Ξ΄))
            prβ‚‚-∐⟨,⟩-is-upperbound i = prβ‚‚ (∐-is-upperbound (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) Ξ΄ i)

   ⟨∐,∐⟩＝∐⟨,⟩ : {I : π“₯ Μ‡ }
               β†’ {α₁ : I β†’ ⟨ 𝓓 ⟩}
               β†’ {Ξ±β‚‚ : I β†’ ⟨ 𝓔 ⟩}
               β†’ (δ₁ : is-Directed 𝓓 α₁)
               β†’ (Ξ΄β‚‚ : is-Directed 𝓔 Ξ±β‚‚)
               β†’ (∐ 𝓓 δ₁ , ∐ 𝓔 Ξ΄β‚‚) ＝ ∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) (⟨pr₁,prβ‚‚βŸ©-is-directed δ₁ Ξ΄β‚‚)
   ⟨∐,∐⟩＝∐⟨,⟩ {I} {α₁} {Ξ±β‚‚} δ₁ Ξ΄β‚‚ = antisymmetry (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔)
                                      (∐ 𝓓 δ₁ , ∐ 𝓔 Ξ΄β‚‚)
                                      (∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔)
                                      (⟨pr₁,prβ‚‚βŸ©-is-directed δ₁ Ξ΄β‚‚))
                                      ⟨∐,βˆβŸ©βŠ‘βˆβŸ¨,⟩ ∐⟨,βŸ©βŠ‘βŸ¨βˆ,∐⟩
     where
       ⟨∐,βˆβŸ©βŠ‘βˆβŸ¨,⟩ : (∐ 𝓓 δ₁ , ∐ 𝓔 Ξ΄β‚‚)
                  βŠ‘βŸ¨ 𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔 ⟩ ∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) (⟨pr₁,prβ‚‚βŸ©-is-directed δ₁ Ξ΄β‚‚)
       ⟨∐,βˆβŸ©βŠ‘βˆβŸ¨,⟩ = βŠ‘β‚ , βŠ‘β‚‚
         where
          βŠ‘β‚ : ∐ 𝓓 δ₁ βŠ‘βŸ¨ 𝓓 ⟩ pr₁ (∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) (⟨pr₁,prβ‚‚βŸ©-is-directed δ₁ Ξ΄β‚‚))
          βŠ‘β‚ = ∐-is-lowerbound-of-upperbounds 𝓓
                δ₁
                (pr₁ (∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) (⟨pr₁,prβ‚‚βŸ©-is-directed δ₁ Ξ΄β‚‚)))
                p
           where
            p : (i : I)
              β†’ (α₁ i) βŠ‘βŸ¨ 𝓓 ⟩ (pr₁ (∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) (⟨pr₁,prβ‚‚βŸ©-is-directed δ₁ Ξ΄β‚‚)))
            p i = pr₁ (∐-is-upperbound ((𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔))
                        (⟨pr₁,prβ‚‚βŸ©-is-directed δ₁ Ξ΄β‚‚)
                        (i , i))

          βŠ‘β‚‚ : ∐ 𝓔 Ξ΄β‚‚ βŠ‘βŸ¨ 𝓔 ⟩ prβ‚‚ (∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) (⟨pr₁,prβ‚‚βŸ©-is-directed δ₁ Ξ΄β‚‚))
          βŠ‘β‚‚ = ∐-is-lowerbound-of-upperbounds 𝓔
                Ξ΄β‚‚
                (prβ‚‚ (∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) (⟨pr₁,prβ‚‚βŸ©-is-directed δ₁ Ξ΄β‚‚)))
                p
           where
            p : (i : I)
              β†’ (Ξ±β‚‚ i) βŠ‘βŸ¨ 𝓔 ⟩ (prβ‚‚ (∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) (⟨pr₁,prβ‚‚βŸ©-is-directed δ₁ Ξ΄β‚‚)))
            p i = prβ‚‚ (∐-is-upperbound (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔)
                        (⟨pr₁,prβ‚‚βŸ©-is-directed δ₁ Ξ΄β‚‚)
                        (i , i))


       ∐⟨,βŸ©βŠ‘βŸ¨βˆ,∐⟩ : ∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) (⟨pr₁,prβ‚‚βŸ©-is-directed δ₁ Ξ΄β‚‚)
                  βŠ‘βŸ¨ 𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔 ⟩ (∐ 𝓓 δ₁ , ∐ 𝓔 Ξ΄β‚‚)
       ∐⟨,βŸ©βŠ‘βŸ¨βˆ,∐⟩ = ∐-is-lowerbound-of-upperbounds (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔)
                      (⟨pr₁,prβ‚‚βŸ©-is-directed δ₁ Ξ΄β‚‚)
                      (∐ 𝓓 δ₁ , ∐ 𝓔 Ξ΄β‚‚)
                      upperbound
         where
          upperbound : (i : I Γ— I)
                     β†’ (α₁ (pr₁ i) , Ξ±β‚‚ (prβ‚‚ i)) βŠ‘βŸ¨ 𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔 ⟩ (∐ 𝓓 δ₁ , ∐ 𝓔 Ξ΄β‚‚)
          upperbound i = ∐-is-upperbound 𝓓 δ₁ (pr₁ i) ,
                         ∐-is-upperbound 𝓔 Ξ΄β‚‚ (prβ‚‚ i)

   pr₁-is-continuous : DCPO[ 𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔 , 𝓓 ]
   pr₁-is-continuous = pr₁ , c
    where
     c : is-continuous (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) 𝓓 pr₁
     c I Ξ± Ξ΄ = u , v
      where
       u : is-upperbound (underlying-order 𝓓) (pr₁ (∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) Ξ΄)) (pr₁ ∘ Ξ±)
       u i = pr₁ (∐-is-upperbound (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) Ξ΄ i)

       v : (x : ⟨ 𝓓 ⟩)
         β†’ ((i : I) β†’ (pr₁ (Ξ± i)) βŠ‘βŸ¨ 𝓓 ⟩ x)
         β†’ (pr₁ (∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) Ξ΄)) βŠ‘βŸ¨ 𝓓 ⟩ x
       v x p = transport (Ξ» - β†’ pr₁ - βŠ‘βŸ¨ 𝓓 ⟩ x) (∐⟨,⟩＝⟨∐,∐⟩ Ξ΄) d
        where
         d : pr₁ (∐ 𝓓 (prβ‚βˆ˜Ξ±-is-Directed Ξ΄) , ∐ 𝓔 (prβ‚‚βˆ˜Ξ±-is-Directed Ξ΄)) βŠ‘βŸ¨ 𝓓 ⟩ x
         d = ∐-is-lowerbound-of-upperbounds 𝓓 (prβ‚βˆ˜Ξ±-is-Directed Ξ΄) x p

   prβ‚‚-is-continuous : DCPO[ 𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔 , 𝓔 ]
   prβ‚‚-is-continuous = prβ‚‚ , c
    where
     c : is-continuous (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) 𝓔 prβ‚‚
     c I Ξ± Ξ΄ = u , v
      where
       u : is-upperbound (underlying-order 𝓔) (prβ‚‚ (∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) Ξ΄)) (prβ‚‚ ∘ Ξ±)
       u i = prβ‚‚ (∐-is-upperbound (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) Ξ΄ i)

       v : (y : ⟨ 𝓔 ⟩)
         β†’ ((i : I) β†’ (prβ‚‚ (Ξ± i)) βŠ‘βŸ¨ 𝓔 ⟩ y)
         β†’ (prβ‚‚ (∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) Ξ΄)) βŠ‘βŸ¨ 𝓔 ⟩ y
       v y p = transport (Ξ» - β†’ prβ‚‚ - βŠ‘βŸ¨ 𝓔 ⟩ y) (∐⟨,⟩＝⟨∐,∐⟩ Ξ΄) e
        where
         e : prβ‚‚ (∐ 𝓓 (prβ‚βˆ˜Ξ±-is-Directed Ξ΄) , ∐ 𝓔 (prβ‚‚βˆ˜Ξ±-is-Directed Ξ΄)) βŠ‘βŸ¨ 𝓔 ⟩ y
         e = ∐-is-lowerbound-of-upperbounds 𝓔 (prβ‚‚βˆ˜Ξ±-is-Directed Ξ΄) y p

 infixr 30 _Γ—α΅ˆαΆœα΅–α΅’βŠ₯_

 _Γ—α΅ˆαΆœα΅–α΅’βŠ₯_ : DCPOβŠ₯ {𝓀} {𝓣}
          β†’ DCPOβŠ₯ {𝓀'} {𝓣'}
          β†’ DCPOβŠ₯ {𝓀 βŠ” 𝓀'} {𝓣 βŠ” 𝓣'}
 𝓓 Γ—α΅ˆαΆœα΅–α΅’βŠ₯ 𝓔 = ((𝓓 ⁻) Γ—α΅ˆαΆœα΅–α΅’ (𝓔 ⁻)) , least , p
  where
   least : ⟨ (𝓓 ⁻) Γ—α΅ˆαΆœα΅–α΅’ (𝓔 ⁻) ⟩
   least = βŠ₯ 𝓓 , βŠ₯ 𝓔

   p : is-least (underlying-order ((𝓓 ⁻) Γ—α΅ˆαΆœα΅–α΅’ (𝓔 ⁻))) least
   p x = (βŠ₯-is-least 𝓓 (pr₁ x)) , (βŠ₯-is-least 𝓔 (prβ‚‚ x))

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

   Γ—α΅ˆαΆœα΅–α΅’-assoc₁ : DCPO[ 𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔 Γ—α΅ˆαΆœα΅–α΅’ 𝓕 , (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) Γ—α΅ˆαΆœα΅–α΅’ 𝓕 ]
   Γ—α΅ˆαΆœα΅–α΅’-assoc₁ = f , c
    where
     f : ⟨ 𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔 Γ—α΅ˆαΆœα΅–α΅’ 𝓕 ⟩ β†’ ⟨ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) Γ—α΅ˆαΆœα΅–α΅’ 𝓕 ⟩
     f (d , e , f) = (d , e) , f

     f-is-monotone : is-monotone (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔 Γ—α΅ˆαΆœα΅–α΅’ 𝓕) ((𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) Γ—α΅ˆαΆœα΅–α΅’ 𝓕) f
     f-is-monotone x y p = ((pr₁ p) , (pr₁ (prβ‚‚ p))) , (prβ‚‚ (prβ‚‚ p))

     c : is-continuous (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔 Γ—α΅ˆαΆœα΅–α΅’ 𝓕) ((𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) Γ—α΅ˆαΆœα΅–α΅’ 𝓕) f
     c I Ξ± Ξ΄ = u , v
      where
       assoc-∐ : ⟨ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) Γ—α΅ˆαΆœα΅–α΅’ 𝓕 ⟩
       assoc-∐ = (pr₁ (∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔 Γ—α΅ˆαΆœα΅–α΅’ 𝓕) Ξ΄) ,
                  (pr₁ (prβ‚‚ (∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔 Γ—α΅ˆαΆœα΅–α΅’ 𝓕) Ξ΄)))) ,
                 prβ‚‚ (prβ‚‚ (∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔 Γ—α΅ˆαΆœα΅–α΅’ 𝓕) Ξ΄))

       u : is-upperbound
            (underlying-order ((𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) Γ—α΅ˆαΆœα΅–α΅’ 𝓕))
            assoc-∐
            (Ξ» i β†’ ((pr₁ (Ξ± i)) , (pr₁ (prβ‚‚ (Ξ± i)))) , (prβ‚‚ (prβ‚‚ (Ξ± i))))
       u i = (pr₁ p , pr₁ (prβ‚‚ p)) , prβ‚‚ (prβ‚‚ p)
        where
         p = ∐-is-upperbound (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔 Γ—α΅ˆαΆœα΅–α΅’ 𝓕) Ξ΄ i

       v : (w : ⟨ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) Γ—α΅ˆαΆœα΅–α΅’ 𝓕 ⟩)
         β†’ ((i : I) β†’ f (Ξ± i) βŠ‘βŸ¨ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) Γ—α΅ˆαΆœα΅–α΅’ 𝓕 ⟩ w)
         β†’ f (∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔 Γ—α΅ˆαΆœα΅–α΅’ 𝓕) Ξ΄) βŠ‘βŸ¨ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) Γ—α΅ˆαΆœα΅–α΅’ 𝓕 ⟩ w
       v w@((x , y) , z) p = f-is-monotone (∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔 Γ—α΅ˆαΆœα΅–α΅’ 𝓕) Ξ΄) w' l
         where
          w' = x , (y , z)

          w'-is-upperbound : is-upperbound
                              (underlying-order (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔 Γ—α΅ˆαΆœα΅–α΅’ 𝓕))
                              w'
                              Ξ±
          w'-is-upperbound i = (pr₁ (pr₁ (p i))) , (prβ‚‚ (pr₁ (p i))) , (prβ‚‚ (p i))

          l : ∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔 Γ—α΅ˆαΆœα΅–α΅’ 𝓕) Ξ΄ βŠ‘βŸ¨ 𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔 Γ—α΅ˆαΆœα΅–α΅’ 𝓕 ⟩ w'
          l = ∐-is-lowerbound-of-upperbounds (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔 Γ—α΅ˆαΆœα΅–α΅’ 𝓕)
               Ξ΄
               w'
               w'-is-upperbound

   to-Γ—-DCPO : DCPO[ 𝓓 , 𝓔 ] β†’  DCPO[ 𝓓 , 𝓕 ] β†’ DCPO[ 𝓓 , 𝓔 Γ—α΅ˆαΆœα΅–α΅’ 𝓕 ]
   to-Γ—-DCPO 𝕗@(f , fc) π•˜@(g , gc) = h , hc
    where
     h : ⟨ 𝓓 ⟩ β†’ ⟨ 𝓔 Γ—α΅ˆαΆœα΅–α΅’ 𝓕 ⟩
     h d = f d , g d

     h-is-monotone : is-monotone 𝓓 (𝓔 Γ—α΅ˆαΆœα΅–α΅’ 𝓕) h
     h-is-monotone x y p = monotone-if-continuous 𝓓 𝓔 𝕗 x y p ,
                           monotone-if-continuous 𝓓 𝓕 π•˜ x y p

     hc : is-continuous 𝓓 (𝓔 Γ—α΅ˆαΆœα΅–α΅’ 𝓕) h
     hc I Ξ± Ξ΄ = u , v
      where
       u : is-upperbound (underlying-order (𝓔 Γ—α΅ˆαΆœα΅–α΅’ 𝓕)) (h (∐ 𝓓 Ξ΄)) (h ∘ Ξ±)
       u i = h-is-monotone (Ξ± i) (∐ 𝓓 Ξ΄) (∐-is-upperbound 𝓓 Ξ΄ i)

       v : (t : ⟨ 𝓔 Γ—α΅ˆαΆœα΅–α΅’ 𝓕 ⟩)
         β†’ ((i : I) β†’ (h (Ξ± i)) βŠ‘βŸ¨ 𝓔 Γ—α΅ˆαΆœα΅–α΅’ 𝓕 ⟩ t)
         β†’ (h (∐ 𝓓 Ξ΄)) βŠ‘βŸ¨ 𝓔 Γ—α΅ˆαΆœα΅–α΅’ 𝓕 ⟩ t
       v t@(y , z) p = lf , lg
        where
         lf : f (∐ 𝓓 Ξ΄) βŠ‘βŸ¨ 𝓔 ⟩ y
         lf = transport (Ξ» - β†’ - βŠ‘βŸ¨ 𝓔 ⟩ y) (q ⁻¹) l
          where
           Ξ΅ : is-Directed 𝓔 (f ∘ Ξ±)
           Ξ΅ = image-is-directed 𝓓 𝓔 (monotone-if-continuous 𝓓 𝓔 𝕗) Ξ΄

           q : f (∐ 𝓓 Ξ΄) ＝ ∐ 𝓔 Ξ΅
           q = continuous-∐-＝ 𝓓 𝓔 𝕗 Ξ΄

           l : ∐ 𝓔 Ξ΅ βŠ‘βŸ¨ 𝓔 ⟩ y
           l = ∐-is-lowerbound-of-upperbounds 𝓔 Ξ΅ y (Ξ» i β†’ pr₁ (p i))

         lg : g (∐ 𝓓 Ξ΄) βŠ‘βŸ¨ 𝓕 ⟩ z
         lg = transport (Ξ» - β†’ - βŠ‘βŸ¨ 𝓕 ⟩ z) (q ⁻¹) l
          where
           Ο• : is-Directed 𝓕 (g ∘ Ξ±)
           Ο• = image-is-directed 𝓓 𝓕 (monotone-if-continuous 𝓓 𝓕 π•˜) Ξ΄

           q : g (∐ 𝓓 Ξ΄) ＝ ∐ 𝓕 Ο•
           q = continuous-∐-＝ 𝓓 𝓕 π•˜ Ξ΄

           l : ∐ 𝓕 Ο• βŠ‘βŸ¨ 𝓕 ⟩ z
           l = ∐-is-lowerbound-of-upperbounds 𝓕 Ο• z (Ξ» i β†’ prβ‚‚ (p i))

 module _ (𝓓 : DCPOβŠ₯ {𝓀} {𝓀'})
          (𝓔 : DCPOβŠ₯ {𝓣} {𝓣'})
          (𝓕 : DCPOβŠ₯ {𝓦} {𝓦'})
       where

   Γ—α΅ˆαΆœα΅–α΅’βŠ₯-assoc₁ : DCPOβŠ₯[ 𝓓 Γ—α΅ˆαΆœα΅–α΅’βŠ₯ 𝓔 Γ—α΅ˆαΆœα΅–α΅’βŠ₯ 𝓕 , (𝓓 Γ—α΅ˆαΆœα΅–α΅’βŠ₯ 𝓔) Γ—α΅ˆαΆœα΅–α΅’βŠ₯ 𝓕 ]
   Γ—α΅ˆαΆœα΅–α΅’βŠ₯-assoc₁ = Γ—α΅ˆαΆœα΅–α΅’-assoc₁ (𝓓 ⁻) (𝓔 ⁻) (𝓕 ⁻)

   to-Γ—-DCPOβŠ₯ : DCPOβŠ₯[ 𝓓 , 𝓔 ] β†’ DCPOβŠ₯[ 𝓓 , 𝓕 ] β†’ DCPOβŠ₯[ 𝓓 , 𝓔 Γ—α΅ˆαΆœα΅–α΅’βŠ₯ 𝓕 ]
   to-Γ—-DCPOβŠ₯ f g = to-Γ—-DCPO (𝓓 ⁻) (𝓔 ⁻) (𝓕 ⁻) f g

\end{code}

Added 3 July 2024 by Tom de Jong.

\begin{code}

 Γ—α΅ˆαΆœα΅–α΅’-is-product : (𝓓₁ : DCPO {𝓀} {𝓣}) (𝓓₂ : DCPO {𝓀'} {𝓣'})
                    (𝓔 : DCPO {𝓦} {𝓦'})
                    (f : ⟨ 𝓔 ⟩ β†’ ⟨ 𝓓₁ ⟩) (g : ⟨ 𝓔 ⟩ β†’ ⟨ 𝓓₂ ⟩)
                  β†’ is-continuous 𝓔 𝓓₁ f
                  β†’ is-continuous 𝓔 𝓓₂ g
                  β†’ βˆƒ! k κž‰ (⟨ 𝓔 ⟩ β†’ ⟨ 𝓓₁ Γ—α΅ˆαΆœα΅–α΅’ 𝓓₂ ⟩) ,
                           is-continuous 𝓔 (𝓓₁ Γ—α΅ˆαΆœα΅–α΅’ 𝓓₂) k
                         Γ— pr₁ ∘ k ∼ f
                         Γ— prβ‚‚ ∘ k ∼ g
 Γ—α΅ˆαΆœα΅–α΅’-is-product 𝓓₁ 𝓓₂ 𝓔 f g cf cg =
  (k , k-is-continuous , ∼-refl , ∼-refl) , k-is-unique
   where
    k-bundled : DCPO[ 𝓔 , 𝓓₁ Γ—α΅ˆαΆœα΅–α΅’ 𝓓₂ ]
    k-bundled = to-Γ—-DCPO 𝓔 𝓓₁ 𝓓₂ (f , cf) (g , cg)
    k : ⟨ 𝓔 ⟩ β†’ ⟨ 𝓓₁ Γ—α΅ˆαΆœα΅–α΅’ 𝓓₂ ⟩
    k = pr₁ k-bundled
    k-is-continuous : is-continuous 𝓔 (𝓓₁ Γ—α΅ˆαΆœα΅–α΅’ 𝓓₂) k
    k-is-continuous = prβ‚‚ k-bundled
    k-is-unique : is-central _ (k , k-is-continuous ,
                                (Ξ» x β†’ refl) , (Ξ» x β†’ refl))
    k-is-unique (h , h-cont , h-eqf , h-eqg) =
     to-subtype-＝ (Ξ» j β†’ Γ—-is-prop
                           (being-continuous-is-prop 𝓔 (𝓓₁ Γ—α΅ˆαΆœα΅–α΅’ 𝓓₂) j)
                           (Γ—-is-prop (Ξ -is-prop fe (Ξ» e β†’ sethood 𝓓₁))
                                      (Ξ -is-prop fe (Ξ» e β†’ sethood 𝓓₂))))
                   (dfunext fe (Ξ» e β†’ k e       ＝⟨refl⟩
                                      f e , g e ＝⟨ (eq e ) ⁻¹ ⟩
                                      h e       ∎))
      where
       eq : (e : ⟨ 𝓔 ⟩) β†’ h e ＝ f e , g e
       eq e = apβ‚‚ _,_ (h-eqf e) (h-eqg e)

\end{code}