Proposition is_monotone_depfunction_poset_pair {W : hSet} {X : UU} {Y : X → hSet} {RW : PartialOrder W} {RY : ∏ (x : X), PartialOrder (Y x)} (fs : ∏ (x : X), W → Y x) (Hfs : ∏ (x : X), is_monotone RW (RY x) (fs x)) : is_monotone RW (depfunction_poset Y RY) (λ w x, fs x w). Proof. intros w₁ w₂ p x. exact (Hfs x _ _ p). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics.