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