proposition: 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: Proof. rewrite <- monotone_prod_map_fubini_pair_l. rewrite <- monotone_prod_map_fubini_pair_r. apply idpath. Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous UniMath.OrderTheory.DCPOs.Examples.BinaryProducts