Agda-stdlib: Add pointer to `Data.Empty.Polymorphic` in `Data.Empty`

[MirceaS]

https://github.com/agda/agda-stdlib/blob/86e67598652228bf2fb413f9eb777803237c2c36/src/Data/Empty.agda#L11

Is there any particular reason that the Empty Type is not parametrised by an implicit Set level?
I often found myself needing a more general Empty Type. Am I doing something wrong?

[MatthewDaggitt]

See https://github.com/agda/agda-stdlib/blob/86e67598652228bf2fb413f9eb777803237c2c36/src/Data/Empty/Polymorphic.agda#L13

It's not universe polymorphic by default as apparently when it was first defined many years back it resulted in lots of unsolved metas. Unsure whether the situation has improved since then.

[MatthewDaggitt]

We should add a pointer in the file though.

[JacquesCarette]

I've been meaning to do an experiment wrt these unsolved metas (i.e. see how many there are), but I've had essentially negative time since the start of January.