Definition struct_dcppo_laws : hset_struct_laws struct_dcppo_data. Proof. split5. - intro X. apply isaset_dcppo_struct. - intros X Y px py f. apply isaprop_is_scott_continuous. - intros X PX ; cbn in *. apply id_is_scott_continuous. - intros X Y Z PX PY PZ f g Pf Pg. exact (comp_is_scott_continuous Pf Pg). - intros X PX PX' p q ; cbn in *. exact (eq_dcppo_struct _ _ p q). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.DCPOs. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.CartesianStructure. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.StructureLimitsAndColimits.