On 4/23/19 3:15 AM, Andreas Abel wrote: > Good initiative, Li-yao! > > To find out whether the laws are complete, I suggest to formalize the > theory of these monad in a theorem prover like Agda and prove the > completeness there. Thanks Andreas. That's a good idea, I will work on a formalization! Li-yao