[Agda] Definition of Modal Operators

[Lukas Stoll]

Dear all,

a modal operator, as defined in [1], is a map defined on all universes.
I was suprised to learn that the following definition works in agda:

record ModalOperator : Setω where
   field
     ◯ : {ℓ : Level} → Type ℓ → Type ℓ
     η : A → ◯ A

Do you think this is a good definition for a modal operator?

Best Regards,
Lukas

[1]: Rijke, Shulman, Spitters. "Modalities in homotopy type theory". 
https://arxiv.org/abs/1706.07526