feat(ipfunctor): add equivalence bridges

[quangvdao]

Problem

IPFunctor.Equiv is stronger than lens and chart equivalence, but the indexed API does not yet provide the expected conversions. The module documentation currently leaves these bridges as a source TODO.

Proposed work

Add conversions from IPFunctor.Equiv to the corresponding lens and chart equivalences. Mirror the naming, identity, composition, inverse, and simplification API provided for PFunctor.Equiv where it applies.

Location

PolyFun/IPFunctor/Equiv/Basic.lean

Acceptance criteria

• Both conversions are available through the public module surface.
• The API includes the expected identity, composition, inverse, and simplification lemmas.
• Focused tests cover both conversions.