Definition all_inr_directed_set_map_help (i : D) (w : X ⨿ Y) (r : w = D i) : Y. Proof. induction w as [ x | y ]. - abstract (apply fromempty ; assert (bot := H i) ; revert bot ; use factor_through_squash ; [ apply isapropempty | ] ; intros dy ; destruct dy as [ y p ] ; exact (negpathsii1ii2 _ _ (r @ p))). - exact y. Defined.
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.