Proposition unary_interpolation : ∃ (z : X), x ≪ z ∧ z ≪ y. Proof. assert (s : y ⊑ ⨆ unary_interpolation_directed_set). { apply continuous_dcpo_struct_approx_le_to_le. intro i. use continuous_dcpo_struct_approx_le_to_le. intro j. use less_than_dcpo_lub. { exact (i ,, j). } apply refl_dcpo. } assert (H := p unary_interpolation_directed_set s). revert H. use factor_through_squash. { apply propproperty. } intro i. induction i as [ i r ]. refine (hinhpr (D (pr1 i) ,, _ ,, _)). - refine (trans_le_way_below r _). apply approximating_family_way_below. - 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.