Definition is_monotone_inr : is_monotone PY coproduct_PartialOrder inr.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions.