Definition prod_dcpo_struct {X Y : hSet} (DX : dcpo_struct X) (DY : dcpo_struct Y) : dcpo_struct (X × Y)%set. Proof. use make_dcpo_struct. - exact (prod_PartialOrder DX DY). - intros I D HD. use prod_lub. + use (dcpo_struct_lub DX (λ i, pr1 (D i))). abstract (use (is_directed_comp _ _ HD) ; apply dirprod_pr1_is_monotone). + use (dcpo_struct_lub DY (λ i, pr2 (D i))). abstract (use (is_directed_comp _ _ HD) ; apply dirprod_pr2_is_monotone). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.PointedPosets. 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.Core.ScottTopology. Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow. Require Import UniMath.OrderTheory.DCPOs.Basis.Basis. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous. Require Import UniMath.OrderTheory.DCPOs.Elements.Maximal.