proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions