proposition: 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: Proof. use subtypePath. { intro. apply isaprop_is_monotone. } use funextsec. exact p. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics