Theorems · Definition · category theory

CategoryTheory.Pi.ihom

{I : Type w₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] →
        [(i : I) → CategoryTheory.MonoidalClosed (C i)] →
          ((i : I) → C i) → CategoryTheory.Functor ((i : I) → C i) ((i : I) → C i)

The internal hom functor X ⟶[∀ i, C i] -

Defined in

Mathlib.CategoryTheory.Pi.Monoidal

Cited by

7 results in Mathlib

Foundations

Depth 12 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.MonoidalClosed