[Agda] Levels and Containers

[Manuel Bärenz]

Dear Agda people, especially stdlib people,

In the definition of Data.Container, is there a reason why the level of
the container is the same as the level of the functor argument?

The definition is:

-- stdlib code

record Container (ℓ : Level) : Set (suc ℓ) where
  constructor _▷_
  field
    Shape    : Set ℓ
    Position : Shape → Set ℓ

open Container public

-- The semantics ("extension") of a container.

⟦_⟧ : ∀ {ℓ} → Container ℓ → Set ℓ → Set ℓ
⟦ C ⟧ X = Σ[ s ∈ Shape C ] (Position C s → X)

-- stlib code ends

It's possible to generalise the last two lines to:

⟦_⟧ : ∀ {ℓ₁ ℓ₂} → Container ℓ₁ → Set ℓ₂ → Set (ℓ₁ ⊔ ℓ₂)
⟦ C ⟧ X = Σ[ s ∈ Shape C ] (Position C s → X)

For my project, this would be great. (I've done that change in my local
copy.) You have to make some type signatures slightly more verbose,
otherwise there are unsolved metas, but it's not a big deal.

Is there any deeper reason why the stdlib type signature is so special?

Manuel