Proposition is_strict_and_monotone_depfunction_pointed_poset_pr {X : UU} (Y : X → hSet) (RY : ∏ (x : X), pointed_PartialOrder (Y x)) (x : X) : is_strict_and_monotone (depfunction_pointed_poset Y RY) (RY x) (λ f, f x). Proof. split. - apply (is_monotone_depfunction_poset_pr Y). - apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions.