Definition lam_monotone_function {Z : hSet} {RZ : PartialOrder Z} (f : monotone_function (prod_PartialOrder RX RZ) RY) : monotone_function RZ monotone_function_PartialOrder. Proof. simple refine (_ ,, _) ; cbn. - intro z. simple refine (_ ,, _). + exact (λ x, f (x ,, z)). + abstract (intros x₁ x₂ p ; apply f ; cbn ; refine (p ,, _) ; apply refl_PartialOrder). - abstract (intros z₁ z₂ p x ; cbn ; apply f ; cbn ; exact (refl_PartialOrder RX x ,, p)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics.