Proposition basis_unary_interpolation {x y : X} (p : x ≪ y) : ∃ (i : B), x ≪ B i ∧ B i ≪ y. Proof. assert (H := unary_interpolation CX p). revert H. use factor_through_squash. { apply propproperty. } intro z. induction z as [ z [ q₁ q₂ ] ]. assert (r : y ⊑ ⨆ directed_set_from_basis B y). { rewrite approximating_basis_lub. apply refl_dcpo. } assert (H := q₂ (directed_set_from_basis B y) r). revert H. use factor_through_squash. { apply propproperty. } intro i. induction i as [ [ i s₁ ] s₂ ]. refine (hinhpr (i ,, _ ,, _)). - exact (trans_way_below_le q₁ s₂). - exact s₁. 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.