Library UniMath.OrderTheory.DCPOs.Core.CoordinateContinuity

Require Import UniMath.MoreFoundations.All.
Require Import UniMath.OrderTheory.Posets.Basics.
Require Import UniMath.OrderTheory.Posets.MonotoneFunctions.
Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets.
Require Import UniMath.OrderTheory.DCPOs.Core.Basics.
Require Import UniMath.OrderTheory.DCPOs.Core.ScottContinuous.
Require Import UniMath.OrderTheory.DCPOs.Core.FubiniTheorem.
Require Import UniMath.OrderTheory.DCPOs.Examples.BinaryProducts.

Local Open Scope dcpo.

Section Coordinates.
  Context {X Y Z : dcpo}
          (f : X × Y → Z)
          (Hf₁ : ∏ (x : X), is_scott_continuous Y Z (λ y, f (x ,, y)))
          (Hf₂ : ∏ (y : Y), is_scott_continuous X Z (λ x, f (x ,, y))).

  Lemma scott_continuous_map_coordinates_monotone
    : is_monotone (X × Y) Z f.
  Show proof.
    intros xy₁ xy₂ pq.
    induction xy₁ as [ x₁ y₁ ].
    induction xy₂ as [ x₂ y₂ ].
    induction pq as [ p q ].
    pose (is_scott_continuous_monotone (Hf₁ x₁) _ _ q) as r₁.
    pose (is_scott_continuous_monotone (Hf₂ y₂) _ _ p) as r₂.
    cbn in *.
    exact (trans_PartialOrder Z r₁ r₂).

  Let F : monotone_function (X × Y) Z
    := _ ,, scott_continuous_map_coordinates_monotone.
  Let Fy (D : directed_set (X × Y)) : scott_continuous_map X Z
    := _ ,, Hf₂ (⨆ (π₂ {{ D }})).

  Lemma scott_continuous_map_coordinates_lub
        (D : directed_set (X × Y))
    : F (⨆ D) = ⨆ (F {{ D }}).
  Show proof.
    rewrite prod_dcpo_lub.
    etrans.
    {
      exact (scott_continuous_map_on_lub (Fy D) (π₁ {{ D }})).
    }
    refine (_ @ !(monotone_prod_map_fubini_pair_l _ _)).
    use dcpo_lub_eq_pointwise.
    intro i ; cbn.
    etrans.
    {
      exact (scott_continuous_map_on_lub (_ ,, Hf₁ i) (π₂ {{ D }})).
    }
    use dcpo_lub_eq_pointwise.
    intro.
    apply idpath.

  Proposition scott_continuous_map_coordinates
    : scott_continuous_map (X × Y) Z.
  Show proof.
    refine (f ,, _).
    use is_scott_continuous_chosen_lub.
    - exact scott_continuous_map_coordinates_monotone.
    - intros I D HD.
      exact (scott_continuous_map_coordinates_lub (I ,, D ,, HD)).
End Coordinates.

Proposition is_scott_continuous_coordinates
            {X Y Z : hSet}
            (DX : dcpo_struct X)
            (DY : dcpo_struct Y)
            (DZ : dcpo_struct Z)
            (f : X × Y → Z)
            (Hf₁ : ∏ (x : X), is_scott_continuous DY DZ (λ y, f (x ,, y)))
            (Hf₂ : ∏ (y : Y), is_scott_continuous DX DZ (λ x, f (x ,, y)))
  : is_scott_continuous
      (prod_dcpo_struct DX DY)
      DZ
      f.
Show proof.
  exact (pr2 (@scott_continuous_map_coordinates
                (X ,, DX)
                (Y ,, DY)
                (Z ,, DZ)
                f
                Hf₁
                Hf₂)).