Proposition nullary_interpolation (x : X) : ∃ (y : X), y ≪ x. Proof. pose (D := approximating_family CX x). assert (H := directed_set_el D). revert H. use factor_through_squash. { apply propproperty. } intro i. refine (hinhpr (D i ,, _)). apply approximating_family_way_below. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow.