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

@[reducible, inline]

abbrev CategoryTheory.EndMonoidal {C : Type u} [Bicategory C] (X : C) : Type v

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

Equations

• CategoryTheory.EndMonoidal X = (X ⟶ X)

instance CategoryTheory.instCategoryEndMonoidal {C : Type u} [Bicategory C] (X : C) : Category.{w, v} (EndMonoidal X)

Equations

• CategoryTheory.instCategoryEndMonoidal X = inferInstance

instance CategoryTheory.instInhabitedEndMonoidal {C : Type u} [Bicategory C] (X : C) : Inhabited (EndMonoidal X)

Equations

• CategoryTheory.instInhabitedEndMonoidal X = { default := CategoryTheory.CategoryStruct.id X }

instance CategoryTheory.instMonoidalCategoryHom {C : Type u} [Bicategory C] (X : C) : MonoidalCategory (X ⟶ X)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.tensorHom_def {C : Type u} [Bicategory C] (X : C) {X₁ Y₁ X₂ Y₂ : X ⟶ X} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : MonoidalCategoryStruct.tensorHom f g = CategoryStruct.comp ((fun {x x_1 : X ⟶ X} (η : x ⟶ x_1) (h : X ⟶ X) => Bicategory.whiskerRight η h) f X₂) ((fun {f x x_1 : X ⟶ X} (η : x ⟶ x_1) => Bicategory.whiskerLeft f η) g)

@[simp]

theorem CategoryTheory.whiskerLeft_def {C : Type u} [Bicategory C] (X : C) {f x✝ x✝¹ : X ⟶ X} (η : x✝ ⟶ x✝¹) : MonoidalCategoryStruct.whiskerLeft f η = Bicategory.whiskerLeft f η

@[simp]

theorem CategoryTheory.associator_def {C : Type u} [Bicategory C] (X : C) (f g h : X ⟶ X) : MonoidalCategoryStruct.associator f g h = Bicategory.associator f g h

@[simp]

theorem CategoryTheory.tensorObj_def {C : Type u} [Bicategory C] (X : C) (f g : X ⟶ X) : MonoidalCategoryStruct.tensorObj f g = CategoryStruct.comp f g

@[simp]

theorem CategoryTheory.tensorUnit_def {C : Type u} [Bicategory C] (X : C) : MonoidalCategoryStruct.tensorUnit (X ⟶ X) = CategoryStruct.id X

@[simp]

theorem CategoryTheory.rightUnitor_def {C : Type u} [Bicategory C] (X : C) (f : X ⟶ X) : MonoidalCategoryStruct.rightUnitor f = Bicategory.rightUnitor f

@[simp]

theorem CategoryTheory.whiskerRight_def {C : Type u} [Bicategory C] (X : C) {x✝ x✝¹ : X ⟶ X} (η : x✝ ⟶ x✝¹) (h : X ⟶ X) : MonoidalCategoryStruct.whiskerRight η h = Bicategory.whiskerRight η h

@[simp]

theorem CategoryTheory.leftUnitor_def {C : Type u} [Bicategory C] (X : C) (f : X ⟶ X) : MonoidalCategoryStruct.leftUnitor f = Bicategory.leftUnitor f