proposition: 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: Proof. intros f g p. exact (p x). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics