Algebra and `Type*`

Stream: mathlib4

[Martin Dvořák]

Do we want to change Type u to Type* along the entire algebraic hierarchy?
As far as I know, most of the classes have arguments in Type* already.

[Yaël Dillies]

... so long as the universe is unnecessary, yes

[Yaël Dillies]

In fact, I meant to make this a technical debt task. Let me add it quick

[Martin Dvořák]

OK, I'll do it.

[Martin Dvořák]

When we are at it, would it be possible to upstream Type* to Std and similarly change Zero, Add, Sub, Mul, and so on?

[Eric Wieser]

Maybe it's worth remembering that this change almost always has no effect; the only reason to apply it is that it protects against accidental universe monomorphism

[Martin Dvořák]

I was less concerned about that (after all, code review should have caught such mistakes) and more concerned about cognitive load from having extra variables (albeit universe variables are less visible).

[Eric Wieser]

* creates more load, because now your goal view has u_1 and u_2 instead of u and v

[Martin Dvořák]

Ah, true. Am I the only one who reads the code tho?

[Eric Wieser]

Martin Dvořák said:

code review should have caught such mistakes

Usually this is quite hard to spot by eye, as X : Type u could be hundreds of lines above Y : Type u (and not part of the diff)

[Martin Dvořák]

Good point!