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. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.Posets.PointedPosets. 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.Core.CoordinateContinuity. Require Import UniMath.OrderTheory.DCPOs.Examples.BinaryProducts.