Proposition is_directed_all_inr_directed_set_to_right : is_directed Y all_inr_directed_set_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 [ H₁ H₂ ]]. assert (q := H t). revert q. use factor_through_squash. { apply propproperty. } intros [ y Hy ]. rewrite Hy in H₁, H₂. pose (wi := D i). assert (pi : wi = D i) by apply idpath. pose (wj := D j). assert (pj : wj = D j) by apply idpath. induction wi as [ xi | yi ]. + rewrite <- pi in H₁. cbn in H₁. exact (fromempty H₁). + induction wj as [ xj | yj ]. * rewrite <- pj in H₂. cbn in H₂. exact (fromempty H₂). * rewrite <- pi in H₁. rewrite <- pj in H₂. cbn in H₁, H₂. refine (hinhpr (t ,, _)). rewrite (all_inr_directed_set_map_eq t y Hy). rewrite (all_inr_directed_set_map_eq i yi (!pi)). rewrite (all_inr_directed_set_map_eq j yj (!pj)). split. ** exact H₁. ** exact H₂. 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.