restoring compilation in Rocq 9.4alpha

[rmatthes]

the essential problem is that "is" is now a keyword, the solution in sync with UniMath PR2083

but there is a type-checking error in Initiality/SyntacticCategory.v as well, which is not dealt with in the first commit, however, it is solved in 2720547 , but the solution is partly ugly.

[nmvdw]

Thanks for the fix! The solution in SyntacticCategory.v is fine, I think. Perhaps some arguments can be replaced by _ to make this step more readable, but I do not know whether the unifier will be able to deduce these arguments.

[rmatthes]

Thank you @nmvdw for having looked through it. Ideally, the author of this formalization (@peterlefanulumsdaine) could try to figure out what went wrong before this fix, maybe a coercion that is no longer applied by the system. However, there is currently strictly no need to make an effort towards reestablishing the previous elegant proof scripts. Only one place in my fix is ugly. It can easily wait until 9.4alpha has become an official release and then the working environment.