mathlib3 documentation

category_theory.concrete_category.bundled

Bundled types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source
@[nolint]
structure category_theory.bundled (c : Type u → Type v) :
Type (max (u+1) v)
  • α : Type ?
  • str : c self.α . "apply_instance"

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

Instances for category_theory.bundled
source
def category_theory.bundled.of {c : Type u → Type v} (α : Type u) [str : c α] :
category_theory.bundled c

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

Equations
source
@[protected, instance]
def category_theory.bundled.has_coe_to_sort {c : Type u → Type v} :
has_coe_to_sort (category_theory.bundled c) (Type u)
Equations
source
@[simp]
theorem category_theory.bundled.coe_mk {c : Type u → Type v} (α : Type u) (str : c α . "apply_instance") :
↥{α := α, str := str} = α
source
@[reducible]
def category_theory.bundled.map {c d : Type u → Type v} (f : Π {α : Type u}, c α → d α) (b : category_theory.bundled c) :
category_theory.bundled d

Map over the bundled structure

Equations