Definition strict_and_monotone_PartialOrder : PartialOrder (strict_and_monotone_function_set PX PY). Proof. simple refine (_ ,, _) ; cbn. - exact (λ f g, ∀ (x : X), PY (f x) (g x)). - refine ((_ ,, _) ,, _). + abstract (intros f g h p q x ; exact (trans_PartialOrder PY (p x) (q x))). + abstract (intros f x ; exact (refl_PartialOrder PY (f x))). + abstract (intros f g p q ; use eq_strict_and_monotone_function ; intro x ; exact (antisymm_PartialOrder PY (p x) (q x))). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions.