mathlib3 documentation

category_theory.bicategory.End

Endomorphisms of an object in a bicategory, as a monoidal category. #

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

@[protected, instance]

def category_theory.End_monoidal.category {C : Type u_1} [category_theory.bicategory C] (X : C) :

category_theory.category (category_theory.End_monoidal X)

def category_theory.End_monoidal {C : Type u_1} [category_theory.bicategory C] (X : C) :

Type u_3

The endomorphisms of an object in a bicategory can be considered as a monoidal category.

Equations

category_theory.End_monoidal X = (X ⟶ X)

Instances for category_theory.End_monoidal

@[protected, instance]

def category_theory.End_monoidal.inhabited {C : Type u_1} [category_theory.bicategory C] (X : C) :

inhabited (category_theory.End_monoidal X)

Equations

category_theory.End_monoidal.inhabited X = {default := 𝟙 X}

@[protected, instance]

def category_theory.End_monoidal.monoidal_category {C : Type u_1} [category_theory.bicategory C] (X : C) :

category_theory.monoidal_category (category_theory.End_monoidal X)

Equations

category_theory.End_monoidal.monoidal_category X = {tensor_obj := λ (f g : category_theory.End_monoidal X), f ≫ g, tensor_hom := λ (f g h i : category_theory.End_monoidal X) (η : f ⟶ g) (θ : h ⟶ i), category_theory.bicategory.whisker_right η h ≫ category_theory.bicategory.whisker_left g θ, tensor_id' := _, tensor_comp' := _, tensor_unit := 𝟙 X, associator := λ (f g h : category_theory.End_monoidal X), category_theory.bicategory.associator f g h, associator_naturality' := _, left_unitor := λ (f : category_theory.End_monoidal X), category_theory.bicategory.left_unitor f, left_unitor_naturality' := _, right_unitor := λ (f : category_theory.End_monoidal X), category_theory.bicategory.right_unitor f, right_unitor_naturality' := _, pentagon' := _, triangle' := _}