Definition is_monotone_inl : is_monotone PX coproduct_PartialOrder inl.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions.