Definition eval_monotone_function : monotone_function (prod_PartialOrder RX monotone_function_PartialOrder) RY. Proof. simple refine (_ ,, _) ; cbn. - exact (λ xf, pr2 xf (pr1 xf)). - abstract (intros xf yg pq ; induction xf as [ x f ] ; induction yg as [ y g ] ; induction pq as [ p q ] ; cbn in * ; exact (trans_PartialOrder RY (q x) (pr2 g x y p))). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics.