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