Proposition dcpo_basis_with_compact_to_compact_basis_laws : compact_basis_laws X B. Proof. refine (_ ,, _ ,, _). - exact HB. - intro x. split. + assert (H := directed_set_el (directed_set_from_basis B x)). revert H. use factor_through_squash. { apply propproperty. } intros b. induction b as [ b p ]. refine (hinhpr (b ,, _)). apply way_below_to_le. exact p. + intros i j. induction i as [ b₁ p₁ ]. induction j as [ b₂ p₂ ]. assert (q₁ : B b₁ ≪ x). { refine (compact_el_way_below_le _ p₁). apply HB. } assert (q₂ : B b₂ ≪ x). { refine (compact_el_way_below_le _ p₂). apply HB. } assert (H := directed_set_top (directed_set_from_basis B x) (b₁ ,, q₁) (b₂ ,, q₂)). revert H. use factor_through_squash. { apply propproperty. } intros t. induction t as [ [ t r₁ ] [ r₂ r₃ ]]. refine (hinhpr ((t ,, _) ,, (r₂ ,, r₃))). apply way_below_to_le. exact r₁. - intro x. split. + intros b. exact (pr2 b). + intros y Hy. use (pr2 (is_least_upperbound_basis B x) y). intros b. induction b as [ b p ]. use (Hy (b ,, _)). apply way_below_to_le. exact p. 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.