fact: Definition set_in_monotone_function (x : X) : monotone_function (PY x) coproduct_set_PartialOrder := _ ,, is_monotone_set_in x.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions