Show HN: Containers for Lean 4 (polynomial functors, with M-types)

TL;DR: lean-containers is a type-safe, mathematically rigorous container library for Lean 4. It provides container signatures, polynomial functors, W-types (initial algebras), M-types (final coalgebras), and a battery of production-grade operations with lawful functor instances, proofs, and a minimal runtime footprint. Built for people who want correct-by-construction data structures in Lean—both for research and real systems. Repo: https://github.com/fraware/lean-containers https://github.com/fraware/lean-containers Status: Production Ready | Version: 1.0.0 | Lean: 4.8.0+