Proposition eq_monotone_function {X₁ X₂ : hSet} {R₁ : PartialOrder X₁} {R₂ : PartialOrder X₂} (f g : monotone_function R₁ R₂) (p : ∏ (x : X₁), f x = g x) : f = g. Proof. use subtypePath. { intro. apply isaprop_is_monotone. } use funextsec. exact p. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics.