Definition is_monotone {X₁ X₂ : hSet} (R₁ : PartialOrder X₁) (R₂ : PartialOrder X₂) (f : X₁ → X₂) : UU := ∏ (x₁ x₂ : X₁), R₁ x₁ x₂ → R₂ (f x₁) (f x₂).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics.