Proposition monotone_fubini_swap {X Y Z : dcpo} (f : monotone_function (X × Y) Z) (D : directed_set (X × Y)) : ⨆_{π₁ {{D}}} fubini_monotone_function_l f D = ⨆_{π₂ {{D}}} fubini_monotone_function_r f D. Proof. rewrite <- monotone_prod_map_fubini_pair_l. rewrite <- monotone_prod_map_fubini_pair_r. 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.Examples.BinaryProducts.