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 { unop := 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.instHasFiniteProductsType :
    CategoryTheory.Limits.HasFiniteProducts (Type v₁)
    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.instHasFiniteProductsFunctorType {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
    CategoryTheory.Limits.HasFiniteProducts (CategoryTheory.Functor C (Type u₂))
    Equations
    • ⋯ = ⋯
    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.