Documentation

Mathlib.CategoryTheory.ConcreteCategory.Bundled

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/ConcreteCategory/UnbundledHom.lean (for categories with unbundled homs, e.g. topological spaces) and in Mathlib/CategoryTheory/ConcreteCategory/BundledHom.lean (for categories with bundled homs, e.g. monoids).

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

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

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

    Equations
    Instances For
      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 : Type u → Type v} {d : Type u → Type v} (f : {α : Type u} → c αd α) (b : CategoryTheory.Bundled c) :

      Map over the bundled structure

      Equations
      Instances For