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