Is there a reason not to use an existing library?

What library did you have in mind? (I tend to accidentally reinvent the wheel a bunch.)

My reason for adding this is to make writing some TemplateMonad code that manages some state on the side a bit easier, in writing automation for proving well-typedness of quotation. It doesn't seem worth it to add another dependency to MetaCoq just for this purpose, unless we want to rip out all the monad utils and replace them with whatever library we'd be using.

• ExtLib has a fairly complete monad library. The itrees work is building on that. I am not certain the status of the theory.
• stdpp has some as well, but it is smaller.
• I'm less certain about other things, but MathClasses probably has something.

Writing a good monad library with theory is not easy due to universes (stdpp has some issues with this) and some of the issues that you highlighted in your paper on category theory in Coq. This is the main reason that I think it would useful to not build another library.

Is the ExtLib library universe polymorphic and cumulative? (It looks like right now it's universe polymorphic but not cumulative, which will break some of the MetaCoq code IIRC.) If so, I'd be happy to have the MetaCoq monad library replaced with that (assuming everyone is on board with adding the dependency), though I don't think I have the time to make the replacement myself.

Note, however, that MetaCoq doesn't need any theory associated with the monad operations, because the library is just for convenient syntax for running template programs, and there's no reasoning that needs to be done about them. Similarly, I'm adding a state monad here so that I can get easy management of state when using the template monad, and don't need any fancy theory.

It would be fine to depend on extlib from my viewpoint. This also avoids unintentional universe/notation clashes when using both MetaCoq and extlib