proposition: Proposition basis_nullary_interpolation (x : X) : ∃ (i : B), B i ≪ x.
proof: 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.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous UniMath.OrderTheory.DCPOs.Core.WayBelow UniMath.OrderTheory.DCPOs.Basis.Continuous