Proposition is_directed_map_from_basis (x : X) : is_directed Y (λ (i : basis_below_element B x), f (pr1 i)). Proof. split. - assert (H := directed_set_el (directed_set_from_basis B x)). revert H. use factor_through_squash. { apply propproperty. } intro i. exact (hinhpr i). - intros i j. induction i as [i Hix]. induction j as [j Hjx]. assert (H := basis_binary_interpolation Hix Hjx). revert H. use factor_through_squash. { apply propproperty. } intro k. induction k as [ k [ p [ q r ]]]. refine (hinhpr ((k ,, r) ,, _ ,, _)). + apply Hf. exact p. + apply Hf. exact q. 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.