proposition: Proposition isrefl_quotient_lower_set_order : isrefl quotient_lower_set_order.
proof: Proof. use setquotunivprop. intro x ; cbn in *. apply hinhpr. exact (inr (refl_PartialOrder RX x)). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.Posets.PointedPosets