Proposition basis_binary_interpolation {x₁ x₂ y : X} (p₁ : x₁ ≪ y) (p₂ : x₂ ≪ y) : ∃ (i : B), x₁ ≪ B i ∧ x₂ ≪ B i ∧ B i ≪ y. Proof. assert (H := binary_interpolation CX p₁ p₂). revert H. use factor_through_squash. { apply propproperty. } intro z. induction z as [ z [ q₁ [ q₂ q₃ ] ] ]. assert (H := basis_unary_interpolation q₃). revert H. use factor_through_squash. { apply propproperty. } intro i. induction i as [ i [ r₁ r₂ ]]. refine (hinhpr (i ,, _ ,, _ ,, _)). - exact (trans_way_below q₁ r₁). - exact (trans_way_below q₂ r₁). - exact r₂. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.ScottContinuous. Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous. Section ScottContinuousFromBasis. End ScottContinuousFromBasis.