Section 6.3.2. asks to "construct a monad transformer `ManyT` based on the definition of `Many`". The exercise seems to be less trivial than intended. Please see [#new members > Stuck on ManyT in "Functional Programming in Lean"](https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Stuck.20on.20ManyT.20in.20.22Functional.20Programming.20in.20Lean.22/with/558631563) for more information.