proposition: 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: 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.
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