Theorems · Definition · category theory

CategoryTheory.ihom

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → (A : C) → [CategoryTheory.Closed A] → CategoryTheory.Functor C C

This is the internal hom A ⟶[C] -.

Defined in

Mathlib.CategoryTheory.Monoidal.Closed.Basic

Cited by

179 results in Mathlib

Foundations

Depth 4 from the axioms, rests on 6 definitions · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.Closed