Lemma scott_continuous_map_coordinates_lub (D : directed_set (X × Y)) : F (⨆ D) = ⨆ (F {{ D }}). 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. Qed.
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.