Proposition binary_interpolation {x₁ x₂ y : X} (p₁ : x₁ ≪ y) (p₂ : x₂ ≪ y) : ∃ (z : X), x₁ ≪ z ∧ x₂ ≪ z ∧ z ≪ y. Proof. pose (D := approximating_family CX y). assert (s : y ⊑ ⨆ D). { unfold D. rewrite approximating_family_lub. apply refl_dcpo. } assert (z₁ := unary_interpolation p₁). revert z₁. use factor_through_squash. { apply propproperty. } intro z₁. induction z₁ as [ z₁ [ q₁ r₁ ]]. assert (H := r₁ D s). revert H. use factor_through_squash. { apply propproperty. } intro H. induction H as [ i₁ H₁ ]. assert (z₂ := unary_interpolation p₂). revert z₂. use factor_through_squash. { apply propproperty. } intro z₂. induction z₂ as [ z₂ [ q₂ r₂ ]]. assert (H := r₂ D s). revert H. use factor_through_squash. { apply propproperty. } intro H. induction H as [ i₂ H₂ ]. assert (H := directed_set_top D i₁ i₂). revert H. use factor_through_squash. { apply propproperty. } intros H. induction H as [ k [ w₁ w₂ ]]. refine (hinhpr (D k ,, _ ,, _ ,, _)). - exact (trans_way_below_le q₁ (trans_dcpo H₁ w₁)). - exact (trans_way_below_le q₂ (trans_dcpo H₂ w₂)). - 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.