refactor(monad): settle morphism hierarchy

[quangvdao]

Problem

The monad morphism and equivalence modules contain source TODOs about finer homomorphism structures and matching type classes. The intended relationship with Mathlib's existing abstractions is not yet settled.

Proposed work

Review NatHom, MonadHom, NatEquiv, and MonadEquiv against the current Mathlib API. Decide whether PolyFun should add smaller Pure, Bind, and monad layers, upstream the missing generality, or reduce the local surface by reusing upstream definitions.

Locations

• PolyFun/Control/Monad/Hom.lean
• PolyFun/Control/Monad/Equiv.lean

Acceptance criteria

• The hierarchy has one documented canonical design.
• Type classes are added only where type class search should use them.
• Existing downstream uses continue to compile or receive a documented migration.
• The source TODOs are removed.