[Agda] Universe level checking

[Martin Escardo]

I am generalizing some old code by replacing `Set` with `Set ?` and 
using ctrl-C-S to fill such holes when possible.

Am I right to think there is a problem with the following?

```
_∼_ : {ℓ ℓ' : Level} {X : Set ℓ} {Y : Set ℓ'}
     → (X → Y) → (X → Y) → Set (ℓ ⊔ ℓ')
f ∼ g = ∀ x → f x ≡ g x

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 ℓ'`.

It shouldn't be possible to construct something in a small universe 
using ingredients from a large universe without the risk of paradox (but 
I haven't paused to try to exploit this to get a contradiction).

Martin