open import Cubical.Foundations.Prelude

module DCPO.Constructions.BinaryProduct (ℓi : Level) where

open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Transport

open import Cubical.Data.Sigma

open import Cubical.HITs.PropositionalTruncation as ∥₁

open import Cubical.Relation.Binary.Order.Poset

open import DCPO ℓi

private
  variable
    ℓa ℓb ℓd ℓe ℓf ℓt ℓt' ℓt'' : Level

⊑× : {A : Type ℓa} {B : Type ℓb} (_⊑₁_ : A → A → Type ℓt) (_⊑₂_ : B → B → Type ℓt')
   → A × B → A × B → Type (ℓ-max ℓt ℓt')
⊑× _⊑₁_ _⊑₂_ (a , b) (a' , b') = a ⊑₁ a' × b ⊑₂ b'

module _ {A : Type ℓa} {B : Type ℓb}
         {_⊑₁_ : A → A → Type ℓt} {_⊑₂_ : B → B → Type ℓt'}
         (isPosetA : IsPoset _⊑₁_) (isPosetB : IsPoset _⊑₂_) where
  open IsPoset

  isPoset⊑× : IsPoset (⊑× _⊑₁_ _⊑₂_)
  isPoset⊑× .is-set = isSet× (isPosetA .is-set) (isPosetB .is-set)
  isPoset⊑× .is-prop-valued (a , b) (a' , b') = isProp× (isPosetA .is-prop-valued a a') (isPosetB .is-prop-valued b b')
  isPoset⊑× .is-refl (a , b) = isPosetA .is-refl a , isPosetB .is-refl b
  isPoset⊑× .is-trans (a₁ , b₁) (a₂ , b₂) (a₃ , b₃) (a₁⊑a₂ , b₁⊑b₂) (a₂⊑a₃ , b₂⊑b₃) = isPosetA .is-trans a₁ a₂ a₃ a₁⊑a₂ a₂⊑a₃ , isPosetB .is-trans b₁ b₂ b₃ b₁⊑b₂ b₂⊑b₃
  isPoset⊑× .is-antisym (a , b) (a' , b') (a⊑a' , b⊑b') (a'⊑a , b'⊑b) = ≡-× (isPosetA .is-antisym a a' a⊑a' a'⊑a) (isPosetB .is-antisym b b' b⊑b' b'⊑b)

module _ {A : Type ℓa} {B : Type ℓb}
         (_⊑₁_ : A → A → Type ℓt) (_⊑₂_ : B → B → Type ℓt')
         {I : Type ℓi} {α : I → A × B}
         (δ : isDirected (⊑× _⊑₁_ _⊑₂_) α) where
  fstIsDirected : isDirected _⊑₁_ (fst ∘ α)
  fstIsDirected =
    inhabitedIfDirected (⊑× _⊑₁_ _⊑₂_) δ ,
    λ i j →
      ∥₁.map
        (λ (k , αᵢ⊑αₖ , αⱼ⊑αₖ)  → k , fst αᵢ⊑αₖ , fst αⱼ⊑αₖ)
        (semidirectedIfDirected (⊑× _⊑₁_ _⊑₂_) δ i j)

  sndIsDirected : isDirected _⊑₂_ (snd ∘ α)
  sndIsDirected =
    inhabitedIfDirected (⊑× _⊑₁_ _⊑₂_) δ ,
    λ i j →
      ∥₁.map
        (λ (k , αᵢ⊑αₖ , αⱼ⊑αₖ)  → k , snd αᵢ⊑αₖ , snd αⱼ⊑αₖ)
        (semidirectedIfDirected (⊑× _⊑₁_ _⊑₂_) δ i j)

module _ (D : DCPO ℓd ℓt) (E : DCPO ℓe ℓt') where
  private
    _⊑_ = ⊑× (order D) (order E)

  fstIsDirected' : {I : Type ℓi} {α : I → ⟨ D ⟩ × ⟨ E ⟩}
                 → (δ : isDirected _⊑_ α)
                 → isDirected (order D) (fst ∘ α)
  fstIsDirected' δ = fstIsDirected (order D) (order E) δ

  sndIsDirected' : {I : Type ℓi} {α : I → ⟨ D ⟩ × ⟨ E ⟩}
                 → (δ : isDirected _⊑_ α)
                 → isDirected (order E) (snd ∘ α)
  sndIsDirected' δ = sndIsDirected (order D) (order E) δ

  pairOfSupsIsSup : {I : Type ℓi} {α : I → ⟨ D ⟩ × ⟨ E ⟩}
                  → (δ : isDirected (order D) (fst ∘ α))
                  → (ε : isDirected (order E) (snd ∘ α))
                  → isSup _⊑_ (∐ D δ , ∐ E ε) α
  pairOfSupsIsSup δ ε =
    (λ i → ∐isUpperbound D δ i , ∐isUpperbound E ε i) ,
    λ v vIsUpper →
      ∐isLowerBoundOfUpperbounds D δ (fst v) (fst ∘ vIsUpper) ,
      ∐isLowerBoundOfUpperbounds E ε (snd v) (snd ∘ vIsUpper)

  _×ᵈᶜᵖᵒ_ : DCPO (ℓ-max ℓd ℓe) (ℓ-max ℓt ℓt')
  _×ᵈᶜᵖᵒ_ = dcpo (⟨ D ⟩ × ⟨ E ⟩) _⊑_ (isPoset⊑× (posetAxioms D) (posetAxioms E)) dc
    where
      dc : isDirectedComplete _⊑_
      dc δ = (∐ D (fstIsDirected' δ) , ∐ E (sndIsDirected' δ)) ,
             pairOfSupsIsSup (fstIsDirected' δ) (sndIsDirected' δ)

module _ (D : DCPO ℓd ℓt) (E : DCPO ℓe ℓt') where
  fstIsContinuous : isContinuous (D ×ᵈᶜᵖᵒ E) D fst
  fstIsContinuous I α δ = ∐isSup D (fstIsDirected' D E δ)

  sndIsContinuous : isContinuous (D ×ᵈᶜᵖᵒ E) E snd
  sndIsContinuous I α δ = ∐isSup E (sndIsDirected' D E δ)

pairing : {ℓ ℓ' ℓ'' : Level} {X : Type ℓ} {Y : X → Type ℓ'} {Z : X → Type ℓ''}
        → ((x : X) → Y x)
        → ((x : X) → Z x)
        → (x : X) → Y x × Z x
pairing f g x = f x , g x

pairingIsContinuous : (D : DCPO ℓd ℓt) (E : DCPO ℓe ℓt') (F : DCPO ℓf ℓt'')
                    → (f : ⟨ D ⟩ → ⟨ E ⟩)
                    → (g : ⟨ D ⟩ → ⟨ F ⟩)
                    → isContinuous D E f
                    → isContinuous D F g
                    → isContinuous D (E ×ᵈᶜᵖᵒ F) (pairing f g)
pairingIsContinuous D E F f g fCont gCont I α δ =
  subst⁻ (λ - → isSup (order (E ×ᵈᶜᵖᵒ F)) - (pairing f g ∘ α))
    (≡-× (continuous∐≡ D E f fCont δ) (continuous∐≡ D F g gCont δ))
    (pairOfSupsIsSup E F
      (isContinuous→imageIsDirected D E f fCont δ)
      (isContinuous→imageIsDirected D F g gCont δ))