proposition: Proposition is_directed_map_from_basis (x : X) : is_directed Y (λ (i : basis_below_element B x), f (pr1 i)).
proof: 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.
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