open import Cubical.Foundations.Prelude

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

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

open import Cubical.HITs.PropositionalTruncation as ∥₁

open import Cubical.Relation.Binary.Order.Poset

open import DCPO ℓi

private
  variable
    ℓa ℓb ℓd ℓt : Level

pointwiseFamily : {I : Type ℓi} {A : Type ℓa} {B : A → Type ℓb}
                → (α : I → (a : A) → B a)
                → (a : A) → I → B a
pointwiseFamily α a i = α i a

module _ (A : Type ℓa) {B : A → Type ℓb} (_⊑ᵇ_ : {a : A} → B a → B a → Type ℓt) where
  ⊑Π : ((a : A) → B a) → ((a : A) → B a) → Type (ℓ-max ℓa ℓt)
  ⊑Π f g = (a : A) → f a ⊑ᵇ g a

  pointwiseFamilyIsDirected : {I : Type ℓi} {α : I → (a : A) → B a}
                            → (δ : isDirected ⊑Π α)
                            → (a : A) → isDirected _⊑ᵇ_ (pointwiseFamily α a)
  pointwiseFamilyIsDirected δ a =
    inhabitedIfDirected ⊑Π δ ,
    λ i j →
      ∥₁.map
        (λ (k , αᵢ⊑αₖ , αⱼ⊑αₖ) → k , αᵢ⊑αₖ a , αⱼ⊑αₖ a)
        (semidirectedIfDirected ⊑Π δ i j)

  module _ (isPosetB : (a : A) → IsPoset (_⊑ᵇ_ {a = a})) where
    open IsPoset

    isPoset⊑Π : IsPoset ⊑Π
    isPoset⊑Π .is-set = isSetΠ (λ a → isPosetB a .is-set)
    isPoset⊑Π .is-prop-valued f g = isPropΠ (λ a → isPosetB a .is-prop-valued (f a) (g a))
    isPoset⊑Π .is-refl f a = isPosetB a .is-refl (f a)
    isPoset⊑Π .is-trans f g h f⊑g g⊑h a = isPosetB a .is-trans (f a) (g a) (h a) (f⊑g a) (g⊑h a)
    isPoset⊑Π .is-antisym f g f⊑g g⊑f = funExt (λ a → isPosetB a .is-antisym (f a) (g a) (f⊑g a) (g⊑f a))

module _ (A : Type ℓa) (D : A → DCPO ℓd ℓt) where
  private
    _⊑ᵈ_ : {a : A} → ⟨ D a ⟩ → ⟨ D a ⟩ → Type ℓt
    _⊑ᵈ_ {a} = order (D a)
    _⊑_ : ((a : A) → ⟨ D a ⟩) → ((a : A) → ⟨ D a ⟩) → Type (ℓ-max ℓa ℓt)
    _⊑_ = ⊑Π A _⊑ᵈ_

  pointwiseFamilyIsDirected' : {I : Type ℓi} {α : I → (a : A) → ⟨ D a ⟩}
                             → (δ : isDirected _⊑_ α)
                             → (a : A) → isDirected _⊑ᵈ_ (pointwiseFamily α a)
  pointwiseFamilyIsDirected' = pointwiseFamilyIsDirected A _⊑ᵈ_

  familyOfSupsIsSup : {I : Type ℓi} {α : I → (a : A) → ⟨ D a ⟩}
                    → (δ : isDirected _⊑_ α)
                    → isSup _⊑_ (λ a → ∐ (D a) (pointwiseFamilyIsDirected' δ a)) α
  familyOfSupsIsSup δ =
    (λ i a → ∐isUpperbound (D a) (pointwiseFamilyIsDirected' δ a) i) ,
    (λ v vIsUpper a →
      ∐isLowerBoundOfUpperbounds (D a) (pointwiseFamilyIsDirected' δ a) (v a)
        λ i → vIsUpper i a)

  Πᵈᶜᵖᵒ : DCPO (ℓ-max ℓa ℓd) (ℓ-max ℓa ℓt)
  Πᵈᶜᵖᵒ = dcpo ((a : A) → ⟨ D a ⟩) _⊑_ (isPoset⊑Π A _⊑ᵈ_ (posetAxioms ∘ D)) dc
    where
      dc : isDirectedComplete _⊑_
      dc δ = (λ a → ∐ (D a) (pointwiseFamilyIsDirected' δ a)) ,
             familyOfSupsIsSup δ