proposition: Proposition discrete_dcpo_basis_laws : dcpo_basis_laws (discrete_dcpo X) discrete_dcpo_basis_data.
proof: Proof. intro x. split. - split. + refine (hinhpr (x ,, _)). apply discrete_eq_to_way_below. apply idpath. + intros i j. induction i as [ y₁ p₁ ]. induction j as [ y₂ p₂ ]. simple refine (hinhpr ((_ ,, _) ,, _ ,, _)). * exact x. * apply discrete_eq_to_way_below. apply idpath. * apply discrete_way_below_to_eq. exact p₁. * apply discrete_way_below_to_eq. exact p₂. - split. + intros y. induction y as [ y p ]. apply discrete_way_below_to_eq. exact p. + intros y Hy. refine (Hy (x ,, _)). apply discrete_eq_to_way_below. apply idpath. 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