For formal validation of the algebraic structures modeled in refer to Orchard and Petricek Embedding effect systems in Haskell for effect sets union and subeffecting Orchard Wadler and Eades Unifying graded and parameterised monads specifically Definition 21 for the graded monad interpretation McDermott and Uustalu Flexibly Graded Monads and Graded Algebras Note does not claim to fully implement their flexibly graded construction but the work contextualizes graded structures libfn libfn