Theorems · Theorem · category theory

CategoryTheory.Pi.closedCounit_app

∀ {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 Y : (i : I) → C i) (i : I), (CategoryTheory.Pi.closedCounit X).app Y i = (CategoryTheory.ihom.ev (X i)).app (Y i)

Defined in

Mathlib.CategoryTheory.Pi.Monoidal

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.MonoidalClosed