Theorems · Definition · category theory

CategoryTheory.MonoidalClosed.id

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (x : C) → [inst_2 : CategoryTheory.Closed x] → CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ x ⟹ x

The C-identity morphism 𝟙_ C ⟶ hom(x, x) used to equip C with the structure of a C-category

Defined in

Mathlib.CategoryTheory.Monoidal.Closed.Basic

Cited by

7 results in Mathlib

Foundations

Depth 26 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.Closed