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.
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
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.instCartesianClosedFunctorType
{C : Type v₁}
[SmallCategory C]
:
CartesianClosed (Functor C (Type v₁))
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.cartesianClosedFunctorToTypes
{C : Type u₁}
[Category.{v₁, u₁} C]
:
CartesianClosed (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₁}
[Category.{v₁, u₁} C]
:
CartesianClosed (Functor C (Type (max u₁ v₁)))
instance
CategoryTheory.instCartesianClosedFunctorTypeOfEssentiallySmall
{C : Type u₁}
[Category.{v₁, u₁} C]
[EssentiallySmall.{v₁, v₁, u₁} C]
:
CartesianClosed (Functor C (Type v₁))
Equations
- One or more equations did not get rendered due to their size.