Ah thanks. The issues leading to "2-monads" came up recently when doing some programming in Coq and needing to prove that the environments actually do contain what they purport to, so that variables can be safely dereferenced (i.e. proving that I don't need to use the Maybe monad). I've seen ideas similar to this all over the place (e.g. Hinze's Lifting Lemma (http://www.comlab.ox.ac.uk/ralf.hinze/WG2.8//26/slides/ralf.pdf)), hence assuming it's well-known. Not to mention that monoids/categories are utterly ubiquitous.

But considering some of the mysticism around "those ineffable monads", I figured it'd be of general interest (ala the link to Dan's other post). There's much more to axiomatizing "computation" than monads, but people get so hung up on unknown terminology. (And welcome to LJ, Ed :)
This account has disabled anonymous posting.
If you don't have an account you can create one now.
HTML doesn't work in the subject.
More info about formatting

If you are unable to use this captcha for any reason, please contact us by email at support@dreamwidth.org

April 2019

S M T W T F S
 123456
78910111213
14151617181920
212223242526 27
282930    

Tags

Page generated 12 Jun 2025 01:11 am
Powered by Dreamwidth Studios