[Agda] Universe level checking

[Stefan Monnier]

> retraction-section : {ℓ ℓ' : Level} {X : Set ℓ} {Y : Set ℓ'}
>                    → (X → Y) → (Y → X) → Set ℓ'
> retraction-section r s = r ∘ s ∼ id
[...]
> I would have thought that the type of `retraction-section r s` should be
> `Set (ℓ ⊔ ℓ')` rather than ` Set ℓ'`.

`r ∘ s` has type `Y -> Y`, where `Y : Set ℓ'`, so `Y -> Y : Set ℓ'`.
I don't see any reason for `ℓ` to appear in there at all.

It's perfectly OK for a function to return a value in a smaller universe
than some of its arguments.  It's the *type* of that function which will
belong to a larger universe.  E.g.

   (X → Y) : Set (ℓ ⊔ ℓ')

and

   (X → Y) → (Y → X) → Set ℓ'  :  Set (ℓ ⊔ (succ ℓ'))


-- Stefan