Theorems · Definition · category theory

CategoryTheory.Pi.closedCounit

{I : Type w₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] →
        [inst_2 : (i : I) → CategoryTheory.MonoidalClosed (C i)] →
          (X : (i : I) → C i) →
            (CategoryTheory.Pi.ihom X).comp (CategoryTheory.MonoidalCategory.tensorLeft X) ⟶
              CategoryTheory.Functor.id ((i : I) → C i)

The counit for the adjunction tensorLeft X ⊣ ihom X.

Defined in

Mathlib.CategoryTheory.Pi.Monoidal

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.MonoidalClosed