Proposition unit_dcpo_basis_laws : dcpo_basis_laws unit_dcpo unit_dcpo_basis_data. Proof. intro x. split. - split. + refine (hinhpr (tt ,, _)). apply unit_dcpo_way_below. + intros i j. refine (hinhpr ((tt ,, _) ,, (tt ,, tt))). apply unit_dcpo_way_below. - split. + intro ; exact tt. + intros ? ?. exact tt. Qed.
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.