Proposition directed_set_point_map_eq (i : D) (y : Y x) (p : D i = x ,, y) : directed_set_point_map i = y. Proof. refine (_ @ fiber_paths p). unfold directed_set_point_map. apply maponpaths_2. apply setproperty. 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.