Reserved Notation "x ≼ y" (at level 50).

Class PreOrder_p (A:Type) :=
  { rel : A → A → Prop where "x ≼ y" := (rel x y);
    bot : A;
    rel_refl : ∀ x, x ≼ x ;
    rel_trans : ∀ x y z, x ≼ y → y ≼ z → x ≼ z;
    bot_is_least : ∀ a, bot ≼ a
  }.

Notation "x ≼ y" := (rel x y).

Instance PreOrder_forall A (B:A → Type) `{∀ a, PreOrder_p (B a)} :
  PreOrder_p (∀ a, B a) :=
  {| rel := fun f g ⇒ ∀ a, f a ≼ g a;
     bot := fun a ⇒ bot |}.

Record monotone_function X Y `{PreOrder_p X} `{PreOrder_p Y} :=
  Build_Mon
    { f_ord :> X → Y ;
      mon :∀ x y, x ≼ y → f_ord x ≼ f_ord y;
      p_mon : f_ord bot ≼ bot
    }.


Notation "X --> Y" := (monotone_function X Y) (at level 10).