Definition prodtofun_monotone_function {W X₁ X₂ : hSet} {RW : PartialOrder W} {R₁ : PartialOrder X₁} {R₂ : PartialOrder X₂} (f : monotone_function RW R₁) (g : monotone_function RW R₂) : monotone_function RW (prod_PartialOrder R₁ R₂) := _ ,, prodtofun_is_monotone (pr2 f) (pr2 g).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics.