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).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.Posets.PointedPosets.