Proposition is_monotone_depfunction_poset_pr {X : UU} (Y : X → hSet) (RY : ∏ (x : X), PartialOrder (Y x)) (x : X) : is_monotone (depfunction_poset Y RY) (RY x) (λ f, f x). Proof. intros f g p. exact (p x). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics.