Proposition is_monotone_quotient_setquot_pr : is_monotone RX quotient_poset (setquotpr _). Proof. intros x₁ x₂ p. apply hinhpr ; cbn. exact (inr p). Qed.
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.