[Agda] Double Negation as Monad

[Martin Escardo]

Peter Hancock wrote:
> I'd just like to mention that 
> A |-> (A -> R) -> R 
> is a monad for any R (needn't be empty.)
> 
> Also
> A |-> (A -> R) -> A
> for which Peirce's law is an algebra, is a monad for any R.
> This was noticed by Escardo and Oliva
> http://www.cs.bham.ac.uk/%7Emhe/papers/selection-escardo-oliva.pdf
> You may find many things of interest in that paper!

Thanks for the free advert! I owe you one. I have coded some of the 
things we did with Paulo Oliva in Agda (particularly Section 7 of the 
above):

   http://www.cs.bham.ac.uk/~mhe/.oliva/peirce.agda

Notes: (1) Agda has changed since I wrote this (in December-May), and in 
particular I understand that the symbol for the universal quantifier, 
which I define in the above file, is now defined by Agda. So I am not 
sure it will compile now.

(2) The definition of the "Peirce shift", needed to get the Peirce 
translation of the axiom of countable choice, needs the termination 
checker disabled (because it amounts to bar recursion, as discussed in 
the above paper with Paulo). We get its double negation translation from 
the Peirce translation, as there is a monad morphism from Peirce to 
double negation. (Also, call/cc belongs naturally to the Peirce monad, 
and navigates to the double negation monad via the monad morphism.)

Martin