Proposition Equalizer_map_strict_and_monotone {W : hSet} (RW : pointed_PartialOrder W) {h : W → X} (Rh : is_strict_and_monotone RW RX h) (p : ∏ (w : W), f(h w) = g(h w)) : is_strict_and_monotone RW Equalizer_pointed_PartialOrder (λ w, h w ,, p w). Proof. split. - apply Equalizer_map_monotone. exact Rh. - use subtypePath. { intro. apply setproperty. } cbn. apply (strict_function_on_point Rh). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions.