Library CatSem.CAT.rich_monads

Require Export CatSem.CAT.monad_h_module.
Require Export CatSem.CAT.cat_INDEXED_TYPE.
Require Export CatSem.CAT.orders.
Require Export CatSem.CAT.ind_potype.

Generalizable All Variables.

Set Implicit Arguments.
Unset Strict Implicit.

Unset Automatic Introduction.

Section defs.

Variable T : Type.

Notation "'IT'" := (ITYPE T).
Notation "'IP'" := (IPO T).

Section order_stuff.

Class Rel (X : Type) := rel : relation X.

Class ITrel (X : IT) := itrel :> forall t, Rel (X t).

Class ITpo (X : IT)(H:ITrel X) : Prop :=
  itpo :> forall t, PreOrder (@itrel _ _ t).

Variables A B : IT.
Variable f : A ---> B.

Class ITproper (Xa : ITrel A) (Xb : ITrel B) :=
   itproper :> forall t, Proper (itrel (t:=t) ==> @itrel _ _ t) (@f t).

End order_stuff.

End defs.