Proposition discrete_dcpo_basis_laws : dcpo_basis_laws (discrete_dcpo X) discrete_dcpo_basis_data. 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.
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.