proposition: 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: Proof. split. - apply (is_monotone_depfunction_poset_pr Y). - apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions