bundled c provides a uniform structure for bundling a type equipped with a type class.
We provide category instances for these in unbundled_hom.lean (for categories with unbundled homs, e.g. topological spaces) and in bundled_hom.lean (for categories with bundled homs, e.g. monoids).
bundled is a type bundled with a type class instance for that type. Only the type class is exposed as a parameter.
A generic function for lifting a type equipped with an instance to a bundled object.
Map over the bundled structure