Bundled types
bundled c provides a uniform structure for bundling a type equipped with a type class.
We provide category instances for these in category_theory/unbundled_hom.lean
(for categories with unbundled homs, e.g. topological spaces)
and in category_theory/bundled_hom.lean (for categories with bundled homs, e.g. monoids).
@[nolint]
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.
Equations
- category_theory.bundled.of α = {α := α, str := str}
@[instance]
Equations
- category_theory.bundled.has_coe_to_sort = {S := Type u, coe := category_theory.bundled.α c}
def
category_theory.bundled.map
{c d : Type u → Type v} :
(Π {α : Type u}, c α → d α) → category_theory.bundled c → category_theory.bundled d
Map over the bundled structure