Proposition compact_basis_to_dcpo_basis_laws {X : dcpo} (B : compact_basis X) : dcpo_basis_laws X B. Proof. intro x. split. - split. + assert (H := directed_set_el (directed_set_from_compact_basis B x)). revert H. use factor_through_squash ; [ apply propproperty | ]. intro i. refine (hinhpr (pr1 i ,, _)). exact (trans_way_below_le (is_compact_el_basis B (pr1 i)) (pr2 i)). + intros i j. assert (H := directed_set_top (directed_set_from_compact_basis B x) (pr1 i ,, way_below_to_le (pr2 i)) (pr1 j ,, way_below_to_le (pr2 j))). revert H. use factor_through_squash ; [ apply propproperty | ]. intro k. induction k as [ k [ p q ]]. refine (hinhpr ((pr1 k ,, _) ,, p ,, q)). exact (trans_way_below_le (is_compact_el_basis B (pr1 k)) (pr2 k)). - split. + intro i. exact (pr1 (is_least_upperbound_compact_basis B x) (pr1 i ,, way_below_to_le (pr2 i))). + intros y p. use (pr2 (is_least_upperbound_compact_basis B x) y). intro i. use (p (pr1 i ,, _)). exact (trans_way_below_le (is_compact_el_basis B (pr1 i)) (pr2 i)). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets. 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.Continuous. Require Import UniMath.OrderTheory.DCPOs.Basis.Algebraic. Require Import UniMath.OrderTheory.DCPOs.Basis.Basis.