Wrong name? isInitialPunit : IsInitial PEmpty

Stream: mathlib4

[IntGrah]

/-- The initial object in `Type u` is `PEmpty`. -/
CategoryTheory.Limits.Types.isInitialPunit.{u} : IsInitial PEmpty.{u + 1}

[Aaron Liu]

definitely wrong name

[Aaron Liu]

docs#CategoryTheory.Limits.Types.isInitialPunit

[IntGrah]

https://github.com/leanprover-community/mathlib4/pull/34964

[IntGrah]

I also notice the dual theorem is named isTerminalPunit. The lowercase u in Punit is bugging me. More generally, there are 17 hits for Punit and 1315 hits for PUnit. Also 3 hits for Pempty and 280 hits for PEmpty.

[Yury G. Kudryashov]

I guess, these Punits and Pemptys came from mathport. Do you have time to prepare a PR fixing all these names and adding all non-instance theorems/definitions back as deprecated aliases?

[IntGrah]

Probably not, I'm afraid someone else will have to do it.

[IntGrah]

There's also def pUnitFoo and def punitFoo

[Ruben Van de Velde]

Would you mind filing an issue, in that case?

[Michael Rothgang]

I'm working on the two remaining "Pempty"s.

[Michael Rothgang]

#34971

[Michael Rothgang]

#34972 is a WIP PR for the Punits (update: should pass CI now)

[Christian Merten]

You beat me (#34973) :D

[Christian Merten]

I thought this is a good test case for the commit verification CI step, but apparently it is failing in the "Post or update comment" step. (https://github.com/leanprover-community/mathlib4/actions/runs/21796757425/job/62885536927?pr=34973)

[IntGrah]

Thanks guys

[IntGrah]

There's also Ulift ULift which also affects import names...