function types form a monad in exactly one way. (this uses `coq-ext-lib` so you can't roll it in jscoq)

ArrowMonad.v

From ExtLib Require Import Monad.

Section ArrowMonad.
  Context (A : Type).

  Instance CodArrowMonad : Monad (fun B => A -> B).
  Proof.
    constructor.
    - intros B y x.
      apply y.
    - intros B C alpha Beta x.
      specialize (alpha x).
      apply (Beta alpha x).
  Defined.
     
  (* TODO: impossibility proof of the `Monad (fun B => B -> A)`*)
End ArrowMonad.