fact: Record Dijkstra (W : OrderedMonad) : Type := mkDM { dm_tyop :> forall A, W A -> Type ; dm_ret : forall A, forall (a : A), dm_tyop (ret a) ; dm_bind : forall A B (w : W A) (f : A -> W B) (d : dm_tyop w) (g : forall a, dm_tyop (f a)), dm_tyop (bind w f) ; dm_wkn : forall {A} {w w' : W A}, dm_tyop w -> w ≤[W] w' -> dm_tyop w' ; dm_law1 : forall A B (a : A) (f : A -> W B) (g : forall a, dm_tyop (f a)), dm_bind (dm_ret a) g =⟨monad_law1 a f⟩ g a ; dm_law2 : forall A c m , dm_bind m (@dm_ret A) =⟨monad_law2 c⟩ m ; dm_law3 : forall A B C c f g (m : dm_tyop c) (f' : forall (a : A), dm_tyop (f a)) (g' : forall (b : B), @dm_tyop C (g b)), dm_bind (dm_bind m f') g' =⟨monad_law3 c f g⟩ dm_bind m (fun a => dm_bind(f' a) g') ; dm_law4 : forall A w (m:@dm_tyop A w), dm_wkn m (reflexivity _) = m ; dm_law5 : forall A w1 w2 w3 (m:@dm_tyop A w1) (H12 :w1 ≤ w2) (H23 :w2 ≤ w3), dm_wkn m (transitivity H12 H23) = dm_wkn (dm_wkn m H12) H23 ; dm_law6 : forall A B wm wm' wf wf' (m:@dm_tyop A wm) (f : forall (a:A), @dm_tyop B (wf a)) (Hm : wm ≤ wm') (Hf : forall a, wf a ≤ wf' a), (dm_wkn (dm_bind m f) (omon_bind Hm Hf) = dm_bind (dm_wkn m Hm) (fun a => dm_wkn (f a) (Hf a))) }.
imports: Coq(ssreflect ssrfun FunctionalExtensionality) Mon(SPropBase) Coq(Relation_Definitions Morphisms)