Definition strict_and_monotone_function_set {X Y : hSet} (RX : pointed_PartialOrder X) (RY : pointed_PartialOrder Y) : hSet. Proof. use make_hSet. - exact (strict_and_monotone_function RX RY). - abstract (use isaset_total2 ; [ use funspace_isaset ; apply Y | intro f ; apply isasetaprop ; apply isaprop_is_strict_and_monotone ]). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions.