Just for fun, monads as modalities is missing:

https://hackage.haskell.org/package/Agda-2.6.4.2/docs/Agda-S...