Agda Supports Eta - Cont is a monad

Since Agda 2 now supports eta in the definitional equality, here is a celebratory proof that Cont is a monad!

module eta where

data _==_ {T : Set} : T -> T -> Set where refl : (x : T) -> x == x

cont : Set -> Set -> Set
cont a r = (a -> r) -> r

return : forall {a r} -> a -> cont a r
return a f = f a

_>>=_ : forall {a b r} -> cont a r -> (a -> cont b r) -> cont b r
m >>= k = \c -> m (\a -> k a c)

cont-left-identity : forall {a b r} -> (o : a) -> (f : a -> cont b r) ->
 (return o >>= f) == f o
cont-left-identity o f = refl (f o)

cont-right-identity : forall {a r} -> (n : cont a r) ->
 (n >>= return) == n
cont-right-identity n = refl n

cont-associativity : forall {a b c r} -> (n : cont a r) -> (f : a -> cont b r) -> (g : b -> cont c r) ->
 ((n >>= f) >>= g) == (n >>= (\x -> (f x) >>= g))
cont-associativity n f g = refl ((n >>= f) >>= g)