Bundled types #
Bundled c
provides a uniform structure for bundling a type equipped with a type class.
We provide Category
instances for these in
Mathlib/CategoryTheory/HasForget/UnbundledHom.lean
(for categories with unbundled homs, e.g. topological spaces)
and in Mathlib/CategoryTheory/HasForget/BundledHom.lean
(for categories with bundled homs, e.g. monoids).
A generic function for lifting a type equipped with an instance to a bundled object.