Definition is_monotone_set_in (x : X) : is_monotone (PY x) coproduct_set_PartialOrder (λ (y : Y x), x ,, y).
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions.