does not compile with Coq 8.20 release candidate 1

[rmatthes]

In CI, it was visible that Coq dev (an alpha version of Coq 8.21) does not compile this satellite, but it is even worse.

The first error message is:

coqc TypeTheory/TypeTheory/Auxiliary/Auxiliary.{glob,vo} (exit 1) File "./TypeTheory/TypeTheory/Auxiliary/Auxiliary.v", line 15, characters 0-43: Error: Universe inconsistency. Cannot enforce UU.u0 <= PartA.cast.u1 because PartA.cast.u1 <= PartA.cast.u0 < UU.u0.