proposition: Proposition prod_dcpo_monotone_lub_const_l {X Y Z : dcpo} (D : directed_set Y) (f : monotone_function (X × Y) Z) (x : X) {I : UU} (i : ∥ I ∥) : ⨆_{prod_directed_set_dcpo (const_directed_set X x I i) D} f = ⨆_{D} (f ·l x).
proof: Proof. use antisymm_dcpo. - use dcpo_lub_is_least. cbn ; intro j. use less_than_dcpo_lub ; cbn. + exact (pr2 j). + apply refl_dcpo. - revert i. use factor_dep_through_squash. { intro. apply propproperty. } intro i. use dcpo_lub_is_least. cbn ; intro j. use less_than_dcpo_lub ; cbn. + exact (i ,, j). + apply refl_dcpo. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.Posets.PointedPosets UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous UniMath.OrderTheory.DCPOs.Core.FubiniTheorem UniMath.OrderTheory.DCPOs.Core.CoordinateContinuity UniMath.OrderTheory.DCPOs.Examples.BinaryProducts