Definition inl_monotone_function : monotone_function PX coproduct_PartialOrder := _ ,, is_monotone_inl.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions.