Mathlib.CategoryTheory.ConcreteCategory.Bundled

Module docstring

{"# 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). "}

CategoryTheory.Bundled structure

(c : Type u → Type v)

Full source

/-- `Bundled` is a type bundled with a type class instance for that type. Only
the type class is exposed as a parameter. -/
structure Bundled (c : Type u → Type v) : Type max (u + 1) v where
  /-- The underlying type of the bundled type -/
  α : Type u
  /-- The corresponding instance of the bundled type class -/
  str : c α := by infer_instance

Bundled Type with Type Class Instance

Informal description

The structure `Bundled c` represents a type bundled with an instance of a type class `c` for that type. Here, `c` is a type class that takes a type as input and produces a type as output. The bundled type exposes only the type class instance as a parameter.

CategoryTheory.Bundled.of definition

{c : Type u → Type v} (α : Type u) [str : c α] : Bundled c

Full source

/-- A generic function for lifting a type equipped with an instance to a bundled object. -/
def of {c : Type u → Type v} (α : Type u) [str : c α] : Bundled c :=
  ⟨α, str⟩

Bundled type construction

Informal description

Given a type class `c` and a type `α` equipped with an instance `str` of `c α`, the function `Bundled.of` constructs a bundled object of type `Bundled c` containing `α` and its instance `str`.

CategoryTheory.Bundled.coeSort instance

: CoeSort (Bundled c) (Type u)

Full source

instance coeSort : CoeSort (Bundled c) (Type u) :=
  ⟨Bundled.α⟩

Coercion from Bundled Types to Their Underlying Types

Informal description

For any type class `c` and bundled type `Bundled c`, there is a canonical coercion from `Bundled c` to `Type u` that extracts the underlying type.

CategoryTheory.Bundled.coe_mk theorem

(α) (str) : (@Bundled.mk c α str : Type u) = α

Full source

theorem coe_mk (α) (str) : (@Bundled.mk c α str : Type u) = α :=
  rfl

Coercion of Bundled Structure Equals Original Type

Informal description

For any type `α` equipped with a type class instance `str : c α`, the coercion of the bundled structure `Bundled.mk c α str` to a type is equal to `α` itself. That is, `(Bundled.mk c α str : Type u) = α`.

CategoryTheory.Bundled.map abbrev

(f : ∀ {α}, c α → d α) (b : Bundled c) : Bundled d

Full source

/-- Map over the bundled structure -/
abbrev map (f : ∀ {α}, c α → d α) (b : Bundled c) : Bundled d :=
  ⟨b, f b.str⟩

Mapping Bundled Type Class Instances

Informal description

Given a function $f$ that maps instances of type class $c$ for any type $\alpha$ to instances of type class $d$ for the same type, and given a bundled type $b$ with an instance of $c$, the operation `Bundled.map` produces a new bundled type with an instance of $d$ obtained by applying $f$ to the instance of $c$ in $b$.