Proposition is_strict_and_monotone_depfunction_pointed_poset_pair {W : hSet} {X : UU} {Y : X → hSet} {RW : pointed_PartialOrder W} {RY : ∏ (x : X), pointed_PartialOrder (Y x)} (fs : ∏ (x : X), W → Y x) (Hfs : ∏ (x : X), is_strict_and_monotone RW (RY x) (fs x)) : is_strict_and_monotone RW (depfunction_pointed_poset Y RY) (λ w x, fs x w). Proof. split. - apply is_monotone_depfunction_poset_pair. intro x. exact (Hfs x). - use funextsec. intro x ; cbn. apply (strict_function_on_point (Hfs x)). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions.