Brendan Hart 2019-2020

\begin{code}

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

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

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

open PropositionalTruncation pt

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

open DcpoProductsGeneral π“₯

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

 continuousβ†’continuous-in-pr₁ : DCPO[ 𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔 , 𝓕 ] β†’ ⟨ 𝓔 ⟩ β†’ DCPO[ 𝓓 , 𝓕 ]
 continuousβ†’continuous-in-pr₁ (f , f-is-continuous) e =
  (Ξ» d β†’ f (d , e)) , continuous
   where
    continuous : is-continuous 𝓓 𝓕 (Ξ» d β†’ f (d , e))
    continuous I Ξ± Ξ΄ = u , v
     where
      u : is-upperbound (underlying-order 𝓕) (f (∐ 𝓓 Ξ΄ , e)) (Ξ» i β†’ f (Ξ± i , e))
      u i = monotone-if-continuous
             (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔)
             𝓕
             (f , f-is-continuous)
             (Ξ± i , e)
             (∐ 𝓓 Ξ΄ , e)
             (∐-is-upperbound 𝓓 Ξ΄ i , reflexivity 𝓔 e)
      v : (z : ⟨ 𝓕 ⟩)
        β†’ ((i : I) β†’ (f (Ξ± i , e)) βŠ‘βŸ¨ 𝓕 ⟩ z)
        β†’ (f (∐ 𝓓 Ξ΄ , e)) βŠ‘βŸ¨ 𝓕 ⟩ z
      v z p = transport
               (Ξ» - β†’ - βŠ‘βŸ¨ 𝓕 ⟩ z)
               (e₁ ⁻¹)
               (∐-is-lowerbound-of-upperbounds
                 𝓕
                 iβ†’f⟨αi,e⟩-is-directed
                 z
                 z-is-upperbound)
        where
         _β†’e-is-directed : is-Directed 𝓔 (Ξ» _ β†’ e)
         _β†’e-is-directed = constant-function-is-directed
                            𝓔
                            (inhabited-if-directed (underlying-order 𝓓) Ξ± Ξ΄)
                            e

         iβ†’βŸ¨Ξ±i,e⟩-is-directed : is-Directed (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) (Ξ» i β†’ Ξ± (pr₁ i) , e)
         iβ†’βŸ¨Ξ±i,e⟩-is-directed = ⟨pr₁,prβ‚‚βŸ©-is-directed 𝓓 𝓔 Ξ΄ _β†’e-is-directed

         iβ†’f⟨αi,e⟩-is-directed : is-Directed 𝓕 (Ξ» i β†’ f (Ξ± (pr₁ i ) , e))
         iβ†’f⟨αi,e⟩-is-directed =
          image-is-directed
           (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔)
           𝓕
           (monotone-if-continuous (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) 𝓕 (f , f-is-continuous))
           iβ†’βŸ¨Ξ±i,e⟩-is-directed

         z-is-upperbound : is-upperbound
                             (underlying-order 𝓕)
                             z
                             (Ξ» i β†’ f (Ξ± (pr₁ i) , e))
         z-is-upperbound i = p (pr₁ i)
         e₁ : f (∐ 𝓓 Ξ΄ , e) ＝ ∐ 𝓕 iβ†’f⟨αi,e⟩-is-directed
         e₁ = f (∐ 𝓓 Ξ΄ , e)                          ＝⟨ i ⟩
              f (∐ 𝓓 Ξ΄ , ∐ 𝓔 _β†’e-is-directed)        ＝⟨ ii ⟩
              f (∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) iβ†’βŸ¨Ξ±i,e⟩-is-directed) ＝⟨ iii ⟩
              ∐ 𝓕 iβ†’f⟨αi,e⟩-is-directed              ∎
          where
           i   = ap (Ξ» - β†’ f (∐ 𝓓 Ξ΄ , -))
                    (constant-is-∐-of-constant-function 𝓔 _β†’e-is-directed)
           ii  = ap (Ξ» - β†’ f -) (⟨∐,∐⟩＝∐⟨,⟩ 𝓓 𝓔 Ξ΄ _β†’e-is-directed)
           iii = continuous-∐-＝
                  (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔)
                  𝓕 (f , f-is-continuous)
                  iβ†’βŸ¨Ξ±i,e⟩-is-directed

 continuousβ†’continuous-in-prβ‚‚ : DCPO[ 𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔 , 𝓕 ] β†’ ⟨ 𝓓 ⟩ β†’ DCPO[ 𝓔 , 𝓕 ]
 continuousβ†’continuous-in-prβ‚‚ 𝕗@(f , f-is-continuous) d =
  (Ξ» e β†’ f (d , e)) , continuous
   where
    continuous : is-continuous 𝓔 𝓕 (Ξ» e β†’ f (d , e))
    continuous I Ξ± Ξ΄ = u , v
      where
        u : is-upperbound (underlying-order 𝓕) (f (d , ∐ 𝓔 Ξ΄)) (Ξ» z β†’ f (d , Ξ± z))
        u i = monotone-if-continuous (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔)
               𝓕
               𝕗
               (d , Ξ± i)
               (d , ∐ 𝓔 Ξ΄)
               ((reflexivity 𝓓 d) , (∐-is-upperbound 𝓔 Ξ΄ i))

        v : (z : ⟨ 𝓕 ⟩)
          β†’ ((i : I) β†’ (f (d , Ξ± i)) βŠ‘βŸ¨ 𝓕 ⟩ z)
          β†’ (f (d , ∐ 𝓔 Ξ΄)) βŠ‘βŸ¨ 𝓕 ⟩ z
        v z p = transport
                 (Ξ» - β†’ - βŠ‘βŸ¨ 𝓕 ⟩ z)
                 (e ⁻¹)
                 (∐-is-lowerbound-of-upperbounds
                   𝓕
                   iβ†’f⟨d,Ξ±i⟩-is-directed
                   z
                   z-is-upperbound)
          where
           _β†’d-is-directed : is-Directed 𝓓 (Ξ» _ β†’ d)
           _β†’d-is-directed = constant-function-is-directed
                              𝓓
                              (inhabited-if-directed (underlying-order 𝓔) Ξ± Ξ΄)
                              d

           iβ†’βŸ¨d,Ξ±i⟩-is-directed : is-Directed (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) (Ξ» i β†’ d , Ξ± (prβ‚‚ i))
           iβ†’βŸ¨d,Ξ±i⟩-is-directed = ⟨pr₁,prβ‚‚βŸ©-is-directed 𝓓 𝓔 _β†’d-is-directed Ξ΄

           iβ†’f⟨d,Ξ±i⟩-is-directed : is-Directed 𝓕 (Ξ» i β†’ f (d , Ξ± (prβ‚‚ i)))
           iβ†’f⟨d,Ξ±i⟩-is-directed = image-is-directed
                                    (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔)
                                    𝓕
                                    (monotone-if-continuous (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) 𝓕 𝕗)
                                    iβ†’βŸ¨d,Ξ±i⟩-is-directed

           z-is-upperbound : is-upperbound
                               (underlying-order 𝓕)
                               z
                               (Ξ» i β†’ f (d , Ξ± (prβ‚‚ i)))
           z-is-upperbound i = p (prβ‚‚ i)

           e : f (d , ∐ 𝓔 Ξ΄) ＝ ∐ 𝓕 iβ†’f⟨d,Ξ±i⟩-is-directed
           e = f (d , ∐ 𝓔 Ξ΄)                          ＝⟨ i ⟩
               f (∐ 𝓓 _β†’d-is-directed , ∐ 𝓔 Ξ΄)        ＝⟨ ii ⟩
               f (∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) iβ†’βŸ¨d,Ξ±i⟩-is-directed) ＝⟨ iii ⟩
               ∐ 𝓕 iβ†’f⟨d,Ξ±i⟩-is-directed              ∎
                  where
                   i   = ap (Ξ» - β†’ f (- , ∐ 𝓔 Ξ΄))
                            (constant-is-∐-of-constant-function
                              𝓓 _β†’d-is-directed)
                   ii  = ap (Ξ» - β†’ f -)
                            (⟨∐,∐⟩＝∐⟨,⟩ 𝓓 𝓔 _β†’d-is-directed Ξ΄)
                   iii = continuous-∐-＝ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) 𝓕 𝕗 iβ†’βŸ¨d,Ξ±i⟩-is-directed

 continuous-in-argumentsβ†’continuous : (f : ⟨ 𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔 ⟩ β†’ ⟨ 𝓕 ⟩)
                                    β†’ (βˆ€ e β†’ is-continuous 𝓓 𝓕 (Ξ» d β†’ f (d , e)))
                                    β†’ (βˆ€ d β†’ is-continuous 𝓔 𝓕 (Ξ» e β†’ f (d , e)))
                                    β†’ is-continuous (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) 𝓕 f
 continuous-in-argumentsβ†’continuous f p₁ pβ‚‚ I Ξ± Ξ΄ = u , v
  where
   f-is-monotone : is-monotone (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) 𝓕 f
   f-is-monotone x@(x₁ , xβ‚‚) y@(y₁ , yβ‚‚) (l₁ , lβ‚‚) =
    transitivity 𝓕 (f x) (f (x₁ , yβ‚‚)) (f y) m₁ mβ‚‚
    where
     m₁ : f x βŠ‘βŸ¨ 𝓕 ⟩ f (x₁ , yβ‚‚)
     m₁ = monotone-if-continuous 𝓔 𝓕
          ((Ξ» e β†’ f (x₁ , e)) , pβ‚‚ x₁)
          xβ‚‚
          yβ‚‚
          lβ‚‚

     mβ‚‚ : f (x₁ , yβ‚‚) βŠ‘βŸ¨ 𝓕 ⟩ f y
     mβ‚‚ = monotone-if-continuous 𝓓 𝓕
           ((Ξ» d β†’ f (d , yβ‚‚)) , p₁ yβ‚‚)
           x₁
           y₁
           l₁

   u : is-upperbound (underlying-order 𝓕) (f (∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) Ξ΄)) (f ∘ α)
   u i = transport (Ξ» - β†’ (f ∘ Ξ±) i βŠ‘βŸ¨ 𝓕 ⟩ f -) (∐⟨,⟩＝⟨∐,∐⟩ 𝓓 𝓔 Ξ΄ ⁻¹) e₁
    where
     d = prβ‚βˆ˜Ξ±-is-Directed 𝓓 𝓔 Ξ΄
     e = prβ‚‚βˆ˜Ξ±-is-Directed 𝓓 𝓔 Ξ΄

     e₁ : (f ∘ Ξ±) i βŠ‘βŸ¨ 𝓕 ⟩ f (∐ 𝓓 d , ∐ 𝓔 e)
     e₁ = transitivity 𝓕
           ((f ∘ α) i)
           (f (pr₁ (Ξ± i) ,
            ∐ 𝓔 e)) (f (∐ 𝓓 d ,
            ∐ 𝓔 e))
           eβ‚…
           eβ‚„
      where
       eβ‚„ : f (pr₁ (Ξ± i) , ∐ 𝓔 e) βŠ‘βŸ¨ 𝓕 ⟩ f (∐ 𝓓 d , ∐ 𝓔 e)
       eβ‚„ = monotone-if-continuous 𝓓 𝓕
             ((Ξ» x β†’ f (x , ∐ 𝓔 e)) ,
              p₁ (∐ 𝓔 e))
             (pr₁ (Ξ± i))
             (∐ 𝓓 d)
             (∐-is-upperbound 𝓓 d i)

       eβ‚… : f (pr₁ (Ξ± i) , prβ‚‚ (Ξ± i)) βŠ‘βŸ¨ 𝓕 ⟩ f (pr₁ (Ξ± i) , ∐ 𝓔 e)
       eβ‚… = monotone-if-continuous 𝓔 𝓕
             ((Ξ» e β†’ f (pr₁ (Ξ± i) , e)) , pβ‚‚ (pr₁ (Ξ± i)))
             (prβ‚‚ (Ξ± i))
             (∐ 𝓔 e)
             (∐-is-upperbound 𝓔 e i)

   v : (z : ⟨ 𝓕 ⟩)
     β†’ ((i : I) β†’ f (Ξ± i) βŠ‘βŸ¨ 𝓕 ⟩ z)
     β†’ f (∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) Ξ΄) βŠ‘βŸ¨ 𝓕 ⟩ z
   v z p = transport (Ξ» - β†’ - βŠ‘βŸ¨ 𝓕 ⟩ z) (e₆ ⁻¹) p₃
    where
     d = prβ‚βˆ˜Ξ±-is-Directed 𝓓 𝓔 Ξ΄
     e = prβ‚‚βˆ˜Ξ±-is-Directed 𝓓 𝓔 Ξ΄

     de : is-Directed 𝓕 Ξ» i β†’ f (pr₁ (Ξ± i) , ∐ 𝓔 e)
     de = image-is-directed 𝓓 𝓕
           (monotone-if-continuous 𝓓 𝓕
             ((Ξ» - β†’ f (- , ∐ 𝓔 e)) ,
              p₁ (∐ 𝓔 e)))
           d

     f∘α-is-directed : is-Directed 𝓕 (f ∘ Ξ±)
     f∘α-is-directed = inhabited-if-directed (underlying-order (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔)) Ξ± Ξ΄ ,
                       order
      where
       order : (i j : I)
             β†’ βˆƒ k κž‰ I , (underlying-order 𝓕 ((f ∘ Ξ±) i) ((f ∘ Ξ±) k) Γ—
                          underlying-order 𝓕 ((f ∘ Ξ±) j) ((f ∘ Ξ±) k))
       order i j = βˆ₯βˆ₯-functor
                    (Ξ» (a , b , c) β†’ a , f-is-monotone (Ξ± i) (Ξ± a) b ,
                                         f-is-monotone (Ξ± j) (Ξ± a) c)
                    (semidirected-if-directed
                      (underlying-order (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔))
                      Ξ±
                      Ξ΄
                      i
                      j)

     e₆ = f (∐ (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔) Ξ΄) ＝⟨ ii ⟩
          f (∐ 𝓓 d , ∐ 𝓔 e)   ＝⟨ iii ⟩
          ∐ 𝓕 de              ＝⟨ iv ⟩
          ∐ 𝓕 f∘α-is-directed ∎
      where
       ii  = ap (Ξ» - β†’ f -) (∐⟨,⟩＝⟨∐,∐⟩ 𝓓 𝓔 Ξ΄)
       iii = continuous-∐-＝ 𝓓 𝓕
              ((Ξ» d β†’ f (d , ∐ 𝓔 e)) ,
               p₁ (∐ 𝓔 e))
              d
       iv  = antisymmetry 𝓕 (∐ 𝓕 de) (∐ 𝓕 f∘α-is-directed) l₁ lβ‚‚
        where
         lβ‚‚ : ∐ 𝓕 f∘α-is-directed βŠ‘βŸ¨ 𝓕 ⟩ ∐ 𝓕 de
         lβ‚‚ = ∐-is-lowerbound-of-upperbounds 𝓕 f∘α-is-directed (∐ 𝓕 de) uβ‚‚
          where
           uβ‚‚ : is-upperbound
                 (underlying-order 𝓕)
                 (∐ 𝓕 de)
                 (Ξ» i β†’ f (pr₁ (Ξ± i) , prβ‚‚ (Ξ± i)))
           uβ‚‚ i = transitivity 𝓕
                   (f (Ξ± i))
                   (f (pr₁ (Ξ± i) , ∐ 𝓔 e))
                   (∐ 𝓕 de)
                   pβ‚„
                   pβ‚…
            where
              pβ‚„ : f (pr₁ (Ξ± i) , prβ‚‚ (Ξ± i)) βŠ‘βŸ¨ 𝓕 ⟩ f (pr₁ (Ξ± i) , ∐ 𝓔 e)
              pβ‚„ = monotone-if-continuous 𝓔 𝓕
                    ((Ξ» e β†’ f (pr₁ (Ξ± i) , e)) ,
                     pβ‚‚ (pr₁ (Ξ± i)))
                    (prβ‚‚ (Ξ± i))
                    (∐ 𝓔 e)
                    (∐-is-upperbound 𝓔 e i)

              pβ‚… : f (pr₁ (Ξ± i) , ∐ 𝓔 e) βŠ‘βŸ¨ 𝓕 ⟩ ∐ 𝓕 de
              pβ‚… = ∐-is-upperbound 𝓕 de i

         l₁ : ∐ 𝓕 de βŠ‘βŸ¨ 𝓕 ⟩ ∐ 𝓕 f∘α-is-directed
         l₁ = ∐-is-lowerbound-of-upperbounds 𝓕 de (∐ 𝓕 f∘α-is-directed) uβ‚‚
          where
           uβ‚‚ : is-upperbound
                 (underlying-order 𝓕)
                 (∐ 𝓕 f∘α-is-directed)
                 (Ξ» i β†’ f (pr₁ (Ξ± i) , ∐ 𝓔 e))
           uβ‚‚ i = prβ‚‚ (pβ‚‚ (pr₁ (Ξ± i))
                   I
                   (prβ‚‚ ∘ Ξ±)
                   e)
                   (∐ 𝓕 f∘α-is-directed)
                   upper
             where
              upper : (i₁ : I)
                    β†’ (f (pr₁ (Ξ± i) , prβ‚‚ (Ξ± i₁))) βŠ‘βŸ¨ 𝓕 ⟩ (∐ 𝓕 f∘α-is-directed)
              upper j = βˆ₯βˆ₯-rec
                         (prop-valuedness 𝓕
                           (f (pr₁ (Ξ± i) , prβ‚‚ (Ξ± j)))
                           (∐ 𝓕 f∘α-is-directed))
                         p₃
                         (semidirected-if-directed
                           (underlying-order (𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔))
                           Ξ±
                           Ξ΄
                           i
                           j)
               where
                p₃ : (Ξ£ k κž‰ I , ((Ξ± i) βŠ‘βŸ¨ 𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔 ⟩ (Ξ± k) Γ—
                                 (Ξ± j) βŠ‘βŸ¨ 𝓓 Γ—α΅ˆαΆœα΅–α΅’ 𝓔 ⟩ (Ξ± k)))
                   β†’ (f (pr₁ (Ξ± i) , prβ‚‚ (Ξ± j))) βŠ‘βŸ¨ 𝓕 ⟩ (∐ 𝓕 f∘α-is-directed)
                p₃ (k , (a , _) , (_ , b)) =
                 transitivity 𝓕
                  (f (pr₁ (Ξ± i) , prβ‚‚ (Ξ± j)))
                  ((f ∘ α) k)
                  (∐ 𝓕 f∘α-is-directed)
                  (f-is-monotone
                    (pr₁ (Ξ± i) , prβ‚‚ (Ξ± j))
                    (Ξ± k)
                    (a , b))
                  (∐-is-upperbound 𝓕 f∘α-is-directed k)

     p₃ : ∐ 𝓕 f∘α-is-directed βŠ‘βŸ¨ 𝓕 ⟩ z
     p₃ = ∐-is-lowerbound-of-upperbounds 𝓕 f∘α-is-directed z p

\end{code}