This sounds very interesting, thank you. So if I understand correctly, (––>) is supposed to mean “something like implication”? So far so good, but I fail to grasp that in a more precise way because the law makes no sense to me yet. Or rather, something seems to be missing? I suppose it's because I don't have the mathematical perspective to get that part. Even such common things like “Left Adjoints” fail to click in my head, so they're missing on my side… So the operations have the types (∧) ∷ Monad m ⇒ m a → (a → m ()) → m a (≤) ∷ SetLike m ⇒ m a → m a → Bool -- implicitely (––>) ∷ (Eq a) ⇒ m a → m a → a → m () Because (≤) returns something non-monadic, the only way the law makes sense is if it's bracketed like this: (x ∧ f) ≤ y iff f ≤ (x ––> y) Because of the left side, f must have type (a → m ()). That makes sense because (x ––> y) has that same type. But now (≤) has to be defined over this type of functor. In other words you seem to claim this type of functors is “set-like”? I assume the definition is something like f ≤ g iff ∀ x.f x ≤ g x ? I'm still not sure what that would mean for the law, but it seems like the first step towards understanding it a bit. Cheers, MarLinn