proposition: Proposition directed_set_point_map_eq (i : D) (y : Y x) (p : D i = x ,, y) : directed_set_point_map i = y.
proof: Proof. refine (_ @ fiber_paths p). unfold directed_set_point_map. apply maponpaths_2. apply setproperty. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.OrderTheory.Posets UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous