Definition quotient_lower_set_bottom (pX : bottom_element RX) : bottom_element quotient_lower_set. Proof. simple refine (_ ,, _). - exact (setquotpr _ (pr1 pX)). - abstract (use setquotunivprop' ; [ intro ; apply propproperty | ] ; intro y ; exact (hinhpr (inr (pr2 pX y)))). Defined.
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.