Please make sure to put your description above the ---, otherwise it will be thrown away and not put in the commit message.

The space below the --- should be left for information that is only interesting before the PR is merged (such as "I need help" or "I'm waiting on this PR" or "Reviewers, what do you think of [alternate design]?")

Note my comments above are far from exhaustive: I just looked for a few examples that were particularly messy. It's certainly not a requirement that you catch all of them, but you're making a tradeoff here between "Greek letters are weird" and "some variables have actively misleading names", and you need to ensure it's not so many that the change is a net downgrade.

I hear your concern and agree this is important. I've checked all of the following to catch as many instances as possible. (This covers all instances you pointed out, and also the comments in #7587.)

• before renaming: audit misleading type names: are X, Y, Z used as variables elsewhere? If so, rename those or convince myself it's fine.

• did I catch all type variables?

  • search for Type and Type*; audit all results
  • types $\iota, \pi$ for indexing is fine
  • use X_i, Y_i etc. for a collection of topological spaces

• rename all occurrences; this ensure documentation is also updated

• generalising universes: try generalising a Type u to Type* (revert if the build fails)
  (Do this in a separate commit, so this can be dropped if needed.)

• Re-use variables if universes match: in theorems only; leave definitions, classes, structures and instances alone.
  (If names were mixed before, renaming may allow to unify things.)

• misleading variable names: all of x : Y, x : Z, y : X, y : Z.
  Often, I can audit all occurrences of z, Z or even y and Y (even in proofs).

• now-suboptimal variable names: a : X etc. (Perhaps, I can even audit all uses of the variable a.)

I am not sure if the last commit is actually a net positive: certainly, the variable name a is used pervasively. I'm open to dropping this one.

✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Thank you for the review. I have addressed both nits (as well as another analogous case in this file.)
bors r+

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style