proposition: Proposition unit_dcpo_way_below (x y : unit_dcpo) : x ≪ y.
proof: Proof. intros D HD. assert (H := directed_set_el D). revert H. use factor_through_squash. { apply propproperty. } intro d. exact (hinhpr (d ,, tt)). Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.PointedPosets UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous UniMath.OrderTheory.DCPOs.Core.WayBelow UniMath.OrderTheory.DCPOs.Basis.Basis UniMath.OrderTheory.DCPOs.Basis.Continuous