Proposition basis_laws_from_continuous_struct {X : dcpo} (CX : continuous_dcpo_struct X) : dcpo_basis_laws X (basis_data_from_continuous_struct CX). 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.
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. Section ScottContinuousFromBasis. End ScottContinuousFromBasis.