Library structures.Monad

Require Import coqrel.LogicalRelations.
Require Import structures.Lattice.

Class CDMonad (M : Type → cdlattice) :=
  {
    ret {A} : A → M A;
    bind {A} {L : cdlattice} : (A → L) → (M A → L);

    ret_bind {A} :
      ∀ (x : M A),
        bind ret x = x;
    bind_ret {A B} :
      ∀ (f : A → M B) (v : A),
        bind f (ret v) = f v;
    bind_bind {A B C} :
      ∀ (f : A → M B) (g : B → M C) (x : M A),
        bind g (bind f x) = bind (fun v ⇒ bind g (f v)) x;

    bind_sup {A} {L : cdlattice} {I} :
      ∀ (f : A → L) (x : I → M A),
        bind f (lsup x) = lsup (fun i ⇒ bind f (x i));
    bind_inf {A} {L : cdlattice} {I} :
      ∀ (f : A → L) (x : I → M A),
        bind f (linf x) = linf (fun i ⇒ bind f (x i));
  }.