Definition monotone_function_hSet {X₁ X₂ : hSet} (R₁ : PartialOrder X₁) (R₂ : PartialOrder X₂) : hSet. Proof. use make_hSet. - exact (monotone_function R₁ R₂). - use isaset_total2. + use funspace_isaset. exact (pr2 X₂). + intro f. apply isasetaprop. apply isaprop_is_monotone. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics.