fact: Definition pointed_quotient_lower_set {X : hSet} (RX : pointed_PartialOrder X) (I : X → hProp) (I_down : downward_closed RX I) : pointed_PartialOrder (setquotinset (downward_closed_to_eqrel I)) := quotient_lower_set RX I I_down ,, quotient_lower_set_bottom _ _ _ (pr2 RX).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.Posets.PointedPosets