proposition: 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: Proof. split. - apply Equalizer_map_monotone. exact Rh. - use subtypePath. { intro. apply setproperty. } cbn. apply (strict_function_on_point Rh). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions