Proposition Equalizer_map_monotone {X : hSet} (RX : PartialOrder X) (Y : hSet) (f g : X → Y) {W : hSet} (RW : PartialOrder W) {h : W → X} (Rh : is_monotone RW RX h) (p : ∏ (w : W), f(h w) = g(h w)) : is_monotone RW (Equalizer_order RX Y f g) (λ w, h w ,, p w). Proof. intros w₁ w₂ q. apply Rh. exact q. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics.