Definition unit_dcpo_struct : dcpo_struct unitset. Proof. use make_dcpo_struct. - exact unit_PartialOrder. - intros I D HD. use make_lub. + exact tt. + split. * abstract (intro i ; cbn ; exact tt). * abstract (intros i Hi ; cbn ; exact tt). 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.WayBelow. Require Import UniMath.OrderTheory.DCPOs.Basis.Basis. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous.