Documentation

Mathlib.CategoryTheory.Monoidal.Closed.Types

Cartesian closure of Type #

Show that Type u₁ is Cartesian closed, and C ⥤ Type u₁ is Cartesian closed for C a small category in Type u₁. Note this implies that the category of presheaves on a small category C is Cartesian closed.

source
def CategoryTheory.Types.tensorProductAdjunction (X : Type v₁) :
MonoidalCategory.tensorLeft X ⊣ coyoneda.obj (Opposite.op X)

The adjunction tensorLeft.obj X ⊣ coyoneda.obj (Opposite.op X) for any X : Type v₁.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    instance CategoryTheory.instIsLeftAdjointTensorLeft (X : Type v₁) :
    (MonoidalCategory.tensorLeft X).IsLeftAdjoint
    source
    instance CategoryTheory.instMonoidalClosedType :
    MonoidalClosed (Type v₁)
    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance CategoryTheory.instMonoidalClosedFunctorType {C : Type v₁} [SmallCategory C] :
    MonoidalClosed (Functor C (Type v₁))
    Equations
    • One or more equations did not get rendered due to their size.
    source
    def CategoryTheory.cartesianClosedFunctorToTypes {C : Type u₁} [Category.{v₁, u₁} C] :
    MonoidalClosed (Functor C (Type (max u₁ v₁ u₂)))

    This is not a good instance because of the universe levels. Below is the instance where the target category is Type (max u₁ v₁).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      instance CategoryTheory.instMonoidalClosedFunctorType_1 {C : Type u₁} [Category.{v₁, u₁} C] :
      MonoidalClosed (Functor C (Type (max u₁ v₁)))
      Equations
      source
      instance CategoryTheory.instMonoidalClosedFunctorTypeOfEssentiallySmall {C : Type u₁} [Category.{v₁, u₁} C] [EssentiallySmall.{v₁, v₁, u₁} C] :
      MonoidalClosed (Functor C (Type v₁))
      Equations
      • One or more equations did not get rendered due to their size.