proposition: Proposition basis_laws_from_continuous_struct {X : dcpo} (CX : continuous_dcpo_struct X) : dcpo_basis_laws X (basis_data_from_continuous_struct CX).
proof: Proof. intro x. split. - split. + exact (nullary_interpolation CX x). + intros i j. unfold basis_below_element, basis_data_from_continuous_struct in i, j. cbn -[way_below] in i, j. assert (H := binary_interpolation CX (pr2 i) (pr2 j)). revert H. use factor_through_squash. { apply propproperty. } intros z. induction z as [ z [ p₁ [ p₂ p₃ ]]]. refine (hinhpr ((z ,, p₃) ,, _ ,, _)). * apply way_below_to_le. exact p₁. * apply way_below_to_le. exact p₂. - split. + intros i. induction i as [ i p ]. apply way_below_to_le. exact p. + intros y Hy. rewrite <- (approximating_family_lub CX x). use dcpo_lub_is_least. intro i. use (Hy (approximating_family CX x i ,, _)). cbn -[way_below]. apply approximating_family_way_below. 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