Functor is a weak typeclass; the only thing it implies about □ is that □(a→b)→□a→□b (which we already know to be true). So the idea of using Functor was just to make the minimum possible assumption.
I don't know enough Haskell to answer your question, but if you can write it in Scala I'll give it a go.
The problem is that Functor's operation isn't quite what you wrote, but rather (a→b)→□a→□b, which is way too strong. I don't think it holds in provability logic. That's why I want to define an even weaker typeclass Prov, but I'm not sure what methods it should have, apart from dup and mp.
If you give me some Scala code, I think I'll be able to make sense of it :-)
If it's worth saying, but not worth its own post (even in Discussion), then it goes here.
Notes for future OT posters:
1. Please add the 'open_thread' tag.
2. Check if there is an active Open Thread before posting a new one. (Immediately before; refresh the list-of-threads page before posting.)
3. Open Threads should be posted in Discussion, and not Main.
4. Open Threads should start on Monday, and end on Sunday.