Proposition isaprop_is_monotone {X₁ X₂ : hSet} (R₁ : PartialOrder X₁) (R₂ : PartialOrder X₂) (f : X₁ → X₂) : isaprop (is_monotone R₁ R₂ f). Proof. repeat (use impred ; intro). apply (pr1 R₂). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics.