Definition inr_monotone_function : monotone_function PY coproduct_PartialOrder := _ ,, is_monotone_inr.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions.