Definition directed_set_comp {X Y : hSet} {PX : PartialOrder X} {PY : PartialOrder Y} (f : monotone_function PX PY) (D : directed_set PX) : directed_set PY. Proof. use (make_directed_set _ D). - exact (λ i, f(D i)). - use (is_directed_comp f (pr2 f)). exact (directed_set_is_directed D). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions.