@[reducible, inline]

abbrev Definition_1_10_1 {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X : C) : Type (max u_1 u_2)

Definition 1.10.1 (EGNO): A right dual of an object X in a monoidal category C is an object X* equipped with evaluation and coevaluation morphisms satisfying the triangle identities.

@[reducible, inline]

abbrev Definition_1_10_2 {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X : C) : Type (max u_1 u_2)

Definition 1.10.2 (EGNO): A left dual of an object X in a monoidal category C is an object *X equipped with evaluation and coevaluation morphisms satisfying the triangle identities.

@[reducible, inline]

abbrev Definition_1_10_11 (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] : Type (max u_1 u_2)

Definition 1.10.11 (EGNO): A monoidal category C is called rigid if every object has both a right dual and a left dual.

@[reducible, inline]

abbrev def_1_10_2 {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X : C) : Type (max u_1 u_2)

Short alias for Definition_1_10_2 (left dual).

@[reducible, inline]

abbrev def_1_10_11 (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] : Type (max u_1 u_2)

Short alias for Definition_1_10_11 (rigid monoidal category).