Issue998d.agda:7,9-10
ℓ != ℓ of type Level
(because one is a variable and one a defined identifier)
when checking that the expression A has type Set ℓ