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).

Note: this structure will be deprecated in the future in favor of defining the category manually and then providing the ConcreteCategory instance on top of this. See ConcreteCategory/Basic.lean for more details.

structure CategoryTheory.Bundled (c : Type u → Type v) : Type (max (u + 1) v)

Bundled is a type bundled with a type class instance for that type. Only the type class is exposed as a parameter.

• α : Type u

  The underlying type of the bundled type

• str : c ↑self

  The corresponding instance of the bundled type class

def CategoryTheory.Bundled.of {c : Type u → Type v} (α : Type u) [str : c α] : Bundled c

A generic function for lifting a type equipped with an instance to a bundled object.

Equations

• CategoryTheory.Bundled.of α = { α := α, str := str }

instance CategoryTheory.Bundled.coeSort {c : Type u → Type v} : CoeSort (Bundled c) (Type u)

Equations

• CategoryTheory.Bundled.coeSort = { coe := CategoryTheory.Bundled.α }

theorem CategoryTheory.Bundled.coe_mk {c : Type u → Type v} (α : Type u) (str : c α) : ↑{ α := α, str := str } = α

@[reducible, inline]

abbrev CategoryTheory.Bundled.map {c d : Type u → Type v} (f : {α : Type u} → c α → d α) (b : Bundled c) : Bundled d

Map over the bundled structure

Equations

• CategoryTheory.Bundled.map f b = { α := ↑b, str := f b.str }