Proposition is_directed_directed_set_point : is_directed (Y x) directed_set_point_map. Proof. split. - exact (directed_set_el D). - intros i j. assert (w := directed_set_top D i j). revert w. use factor_through_squash. { apply propproperty. } intros t. induction t as [ t [ [ p₁ q₁ ] [ p₂ q₂ ] ]] ; cbn in p₁, p₂. assert (q := H t). revert q. use factor_through_squash. { apply propproperty. } intros [ y r ]. refine (hinhpr (t ,, _)). rewrite (directed_set_point_map_eq t _ r). induction (D t) as [ dt dt' ]. assert (s := total2_paths_equiv _ _ _ (!r)). clear r. induction s as [ s₁ s₂ ]. cbn in p₁, p₂, s₁, s₂. induction s₁ ; cbn in s₂. induction s₂. assert (D i = x ,, transportf (λ z, Y z) p₁ (pr2 (D i))) as ri. { use total2_paths_b. - exact p₁. - cbn. rewrite transportbfinv. apply idpath. } rewrite (directed_set_point_map_eq i _ ri). assert (D j = x ,, transportf (λ z, Y z) p₂ (pr2 (D j))) as rj. { use total2_paths_b. - exact p₂. - cbn. rewrite transportbfinv. apply idpath. } rewrite (directed_set_point_map_eq j _ rj). induction (D i) as [ di di' ]. induction (D j) as [ dj dj' ]. cbn in *. induction p₁, p₂ ; cbn in *. exact (q₁ ,, q₂). Qed.
Require Import UniMath.Foundations.All. 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.