Definition pointed_quotient_poset {X : hSet} (RX : pointed_PartialOrder X) (I : X → hProp) (I_down : downward_closed RX I) (eqX : eqrel X) (H : ∏ (x₁ x₂ : X), eqX x₁ x₂ <-> downward_closed_to_eqrel I x₁ x₂) : pointed_PartialOrder (setquotinset eqX) := quotient_poset RX I I_down eqX H ,, quotient_poset_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.