proposition: Proposition compact_basis_to_dcpo_basis_laws {X : dcpo} (B : compact_basis X) : dcpo_basis_laws X B.
proof: 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.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous UniMath.OrderTheory.DCPOs.Core.WayBelow UniMath.OrderTheory.DCPOs.Basis.Continuous UniMath.OrderTheory.DCPOs.Basis.Algebraic UniMath.OrderTheory.DCPOs.Basis.Basis