fact: Definition algebraicity (op : E \o M ~~> M) := forall (A B : UU0) (f : A -> M B) (t : E (M A)), op A t >>= f = op B ((E # (fun m => m >>= f)) t).
imports: ssrmatching mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy