Proposition monotone_function_isPartialOrder : isPartialOrder monotone_function_order. Proof. simple refine ((_ ,, _) ,, _). - exact (λ f g h p q x, trans_PartialOrder RY (p x) (q x)). - exact (λ f x, refl_PartialOrder RY (pr1 f x)). - intros f g p q. use eq_monotone_function. intro x. exact (antisymm_PartialOrder RY (p x) (q x)). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics.