refactor(pfunctor): simplify universe annotations

[quangvdao]

Problem

The universe lifting equivalences in PFunctor.Equiv require dense explicit universe annotations. A source TODO asks for a clearer approach.

Proposed work

Review the lifting equivalences and reduce explicit universe arguments where Lean can infer them reliably. Small private helpers are acceptable when they make the public definitions clearer and keep elaboration stable.

Location

PolyFun/PFunctor/Equiv/Basic.lean

Acceptance criteria

• The lifting equivalences compile with fewer or better localized universe annotations.
• The public types and universe generality do not regress.
• Focused tests cover representative mixed universe cases.
• The source TODO is removed.