proposition: Proposition nullary_interpolation (x : X) : ∃ (y : X), y ≪ x.
proof: 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.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.WayBelow