∀(a : Type) → ../../../../../Prelude/Monoid (Optional a)