The current world of type theory proof assistants is ruled by the "Pick Your Poison" principle.
1. With Agda, you have something that has the appearance of a reasonable system, but if you dig into how it works, you become very scared and see that it is more bug than functionality.
2. With Rocq, you have something that has a lot of really thoughtful people with a good understanding of type theory working on it, but they are weighed down by decades old design mistakes (founts of soundness bugs) that probably cannot be unwound ever. The old practices are risky in terms of soundness, and doing things right from now might not be enough.
3. With Lean, you have something that's really thoughtfully engineered in some ways, but which (due to hubris) has begun to accumulate so much technical debt and soundness issues that it is unclear whether it can be fixed without new leadership. Current practices are risky in terms of soundness, as we have seen.
I sincerely want us to have more options. I don't think it is healthy for this area to be ruled by one system. I believe that is very risky, and I also believe it is stifling. I am sorry if that upsets you or amuses you. I'm sorry if you find it annoying and vindictive. I find it important.