Xia Li-yao

@ekmett That paper states `MonadState` laws in terms of `get` and `modify` (called `update` (`u`) in the paper). ```haskell modify f >> modify g = modify (g . f) --...

For `MonadReader`, may I suggest the following: ```haskell (,) ask ask = (\r -> (r, r)) ask -- ask-ask local f ask = fmap f ask -- local-ask local f...

@ocharles Right, that looks equivalent and simpler. Formally speaking, I'm missing a step to prove that `ask >> ask = ask` implies `(,) ask ask = (\r -> (r, r))...

Interesting, these homomorphisms imply a lot of the laws. For example, *obviously* in `(->)` we can check that `ask >> ask = ask`. Now in a general `MonadReader`, provided `ask...

Thanks for the reminder @recursion-ninja . I think this issue was a victim of "perfect is the enemy of good". There are so many ways to present the laws, and...

@Zemyla Those laws look great! Here they are QuickChecked: https://github.com/Lysxia/checkers-mtl/blob/d30c35ea87d1746bbd2d1728abd0045f8355b650/src/Test/Monad/Cont.hs The tests pass with those monads at least: https://github.com/Lysxia/checkers-mtl/blob/d30c35ea87d1746bbd2d1728abd0045f8355b650/src/Test/Monad/Cont/Checkers.hs#L36-L39

coq-itree 4.0.0 is broken but dev is fixed.

And I can't reproduce the weird CI failure on 8.9

Another option is to deprecate and remove `Show` altogether. Even if we fixed it, it seems a good candidate to put into its own library. I recently created [coq-ceres](https://github.com/Lysxia/coq-ceres) as...

Ceres doesn't currently do any kind of pretty printing, it only writes S-expressions on one line. But the idea is that S-expressions can be formatted independently. So there's going to...