Proposition basis_nullary_interpolation (x : X) : ∃ (i : B), B i ≪ x. Proof. assert (H := nullary_interpolation CX x). revert H. use factor_through_squash. { apply propproperty. } intro y. induction y as [ y p ]. assert (H := directed_set_el (directed_set_from_basis B y)). revert H. use factor_through_squash. { apply propproperty. } intro i. induction i as [ i q ]. refine (hinhpr (i ,, _)). exact (trans_way_below q 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. Section ScottContinuousFromBasis. End ScottContinuousFromBasis.