Documentation

Mathlib.CategoryTheory.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.binaryProductAdjunction (X : Type v₁) :
CategoryTheory.Limits.Types.binaryProductFunctor.obj X ⊣ CategoryTheory.coyoneda.obj (Opposite.op X)

The adjunction Limits.Types.binaryProductFunctor.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.instIsLeftAdjointObjFunctorTypeBinaryProductFunctor (X : Type v₁) :
    (CategoryTheory.Limits.Types.binaryProductFunctor.obj X).IsLeftAdjoint
    Equations
    • ⋯ = ⋯
    source
    instance CategoryTheory.instCartesianClosedType :
    CategoryTheory.CartesianClosed (Type v₁)
    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance CategoryTheory.instCartesianClosedFunctorType {C : Type v₁} [CategoryTheory.SmallCategory C] :
    CategoryTheory.CartesianClosed (CategoryTheory.Functor C (Type v₁))
    Equations
    • One or more equations did not get rendered due to their size.
    source
    def CategoryTheory.cartesianClosedFunctorToTypes {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
    CategoryTheory.CartesianClosed (CategoryTheory.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.instCartesianClosedFunctorType_1 {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
      CategoryTheory.CartesianClosed (CategoryTheory.Functor C (Type (max u₁ v₁)))
      Equations
      • CategoryTheory.instCartesianClosedFunctorType_1 = CategoryTheory.cartesianClosedFunctorToTypes
      source
      instance CategoryTheory.instCartesianClosedFunctorTypeOfEssentiallySmall {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.EssentiallySmall.{v₁, v₁, u₁} C] :
      CategoryTheory.CartesianClosed (CategoryTheory.Functor C (Type v₁))
      Equations
      • One or more equations did not get rendered due to their size.