Definition monotone_function_order : hrel (monotone_function_hSet RX RY). Proof. intros f g ; cbn in *. use make_hProp. - exact (∏ (x : X), RY (f x) (g x)). - abstract (use impred ; intro ; apply (pr1 RY)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics.