Include proofs?

[davdar]

There are lots of proofs that I could include if it's valuable to do so.

• That my monad transformer is indeed a monad (satisfying monad laws)
  • This isn't so long. it relies on the functor laws for the underlying join-semilattice functor though, so that means more category theory language :(
• That my mappings from (a -> m(b)) to (Sigma -> Sigma) are actually themselves Galois connections.
  • These proofs require alpha and gamma to be homomorphisms between categories, and the proofs are more involved.
• That my monad transformer combinations are ordered path-sensitive <= flow-sensitive <= flow-insensitive. I actually haven't done these proofs yet, but I imagine they're simple (since they reduce to proving ordered-ness for monad transformers piecewise).

[davdar]

The verdict from the Skype call:

• State the theorem and key lemmas for the monad transformer proof.
• Definitely state the theorems and properties for Galois connections transporting Galois connections.
• The path-sensitive <= flow-sensitive <= flow-insensitive property is better handled in a discussion of this being a language-independent framework.