Proposition monotone_fubini_swap' {X Y Z : dcpo} (D₁ : directed_set X) (D₂ : directed_set Y) (f : monotone_function (X × Y) Z) : ⨆_{D₁} (fubini_monotone_function_l f (prod_directed_set D₁ D₂)) = ⨆_{D₂} (fubini_monotone_function_r f (prod_directed_set D₁ D₂)). Proof. refine (_ @ monotone_fubini_swap f (prod_directed_set D₁ D₂) @ _). - use antisymm_dcpo. + use dcpo_lub_is_least. cbn ; intro i. use dcpo_lub_is_least. cbn ; intro j. use less_than_dcpo_lub. * exact (i ,, pr2 j). * cbn. use less_than_dcpo_lub. ** exact (i ,, pr2 j). ** cbn. apply refl_dcpo. + use dcpo_lub_is_least. cbn ; intro i. use dcpo_lub_is_least. cbn ; intro j. use less_than_dcpo_lub. * exact (pr1 i). * cbn. use less_than_dcpo_lub. ** exact j. ** cbn. apply refl_dcpo. - use antisymm_dcpo. + use dcpo_lub_is_least. cbn ; intro i. use dcpo_lub_is_least. cbn ; intro j. use less_than_dcpo_lub. * exact (pr2 i). * cbn. use less_than_dcpo_lub. ** exact j. ** cbn. apply refl_dcpo. + use dcpo_lub_is_least. cbn ; intro i. use dcpo_lub_is_least. cbn ; intro j. use less_than_dcpo_lub. * exact (pr1 j ,, i). * cbn. use less_than_dcpo_lub. ** exact (pr1 j ,, i). ** cbn. apply refl_dcpo. 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.Examples.BinaryProducts.