MarLinn monkleyon at gmail.com
Sat Jul 22 15:14:52 UTC 2017

```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

```